LatticeCountingFull.lean

1 import PaperX.LatticeCountingGrid
2 import PaperX.LatticeCountingTransport
3 
4 /-! Quantitative counting for every fixed full lattice, uniform in translation
5 and real dilation. The boundary atlas is genuine geometric data. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperX.LatticeCountingTransport
9 open Set MeasureTheory Module
10 open scoped Pointwise Topology
11 
12 variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
13   [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
14   (L : Submodule ℤ E) [DiscreteTopology L] [IsZLattice ℝ L]
15   {ι : Type*} [Fintype ι] (b : Basis ι ℤ L)
16 
17 /-- Exact lattice-coordinate transport yields the full translated discrepancy estimate. -/
18 theorem exists_lattice_discrepancy_bound {D : Set E}
19     (hDm : MeasurableSet D) (hDb : Bornology.IsBounded D)
20     (A : LatticeCounting.LipschitzBoundaryAtlas ι (coordinates L b '' D)) :
21     ∃ C : ℝ, 0 ≤ C ∧ ∀ (a : E) (t : ℝ), 1 ≤ t →
22       |(Nat.card (((fun x => a + t • x) '' D) ∩ (L : Set E) : Set E) : ℝ) -
23         t ^ Fintype.card ι * (volume.real D / ZLattice.covolume L)| ≤
24           C * (t ^ (Fintype.card ι - 1) + 1) := by
25   have hm : MeasurableSet (coordinates L b '' D) :=
26     (coordinates L b).toHomeomorph.toMeasurableEquiv.measurableSet_image.mpr hDm
27   have hb : Bornology.IsBounded (coordinates L b '' D) :=
28     (coordinates L b).toContinuousLinearMap.lipschitzWith.isBounded_image hDb
29   obtain ⟨C, hC, hbound⟩ := LatticeCounting.exists_grid_discrepancy_bound hm hb A
30   refine ⟨C, hC, fun a t ht => ?_⟩
31   have h := hbound (coordinates L b a) t ht
32   rw [← coordinates_affine_image L b D a t,
33     ← lattice_count_eq_grid_count L b,
34     volumeReal_coordinates_image L b hDm] at h
35   exact h
36 
37 omit [MeasurableSpace E] [BorelSpace E] [DiscreteTopology L] [IsZLattice ℝ L] in
38 /-- Moving a lattice coset to the origin translates the counting region in the opposite direction. -/
39 def cosetPointsEquiv (D : Set E) (a : E) (t : ℝ) :
40     (((fun x : E => a + x) '' (L : Set E)) ∩ (t • D) : Set E) ≃
41       (((fun x => -a + t • x) '' D) ∩ (L : Set E) : Set E) where
42   toFun x := ⟨x.1 - a, by
43     obtain ⟨l, hl, hxl⟩ := x.2.1
44     obtain ⟨d, hd, hxd⟩ := x.2.2
45     change a + l = x.1 at hxl
46     change t • d = x.1 at hxd
47     constructor
48     · refine ⟨d, hd, ?_⟩
49       change -a + t • d = x.1 - a
50       rw [hxd]
51       simp only [sub_eq_add_neg, add_comm]
52     · have he : x.1 - a = l := by rw [← hxl]; simp
53       rw [he]
54       exact hl⟩
55   invFun x := ⟨a + x.1, by
56     refine ⟨⟨x.1, x.2.2, rfl⟩, ?_⟩
57     obtain ⟨d, hd, hxd⟩ := x.2.1
58     change -a + t • d = x.1 at hxd
59     refine ⟨d, hd, ?_⟩
60     change t • d = a + x.1
61     rw [← hxd]
62     simp⟩
63   left_inv x := by apply Subtype.ext; simp
64   right_inv x := by apply Subtype.ext; simp
65 
66 /-- The requested lattice-coset form, uniformly for every translate and t at least one. -/
67 theorem exists_coset_discrepancy_bound {D : Set E}
68     (hDm : MeasurableSet D) (hDb : Bornology.IsBounded D)
69     (A : LatticeCounting.LipschitzBoundaryAtlas ι (coordinates L b '' D)) :
70     ∃ C : ℝ, 0 ≤ C ∧ ∀ (a : E) (t : ℝ), 1 ≤ t →
71       |(Nat.card (((fun x : E => a + x) '' (L : Set E)) ∩ (t • D) : Set E) : ℝ) -
72         t ^ Fintype.card ι * (volume.real D / ZLattice.covolume L)| ≤
73           C * (t ^ (Fintype.card ι - 1) + 1) := by
74   obtain ⟨C, hC, hbound⟩ := exists_lattice_discrepancy_bound L b hDm hDb A
75   refine ⟨C, hC, fun a t ht => ?_⟩
76   rw [Nat.card_congr (cosetPointsEquiv L D a t)]
77   exact hbound (-a) t ht
78 
79 end PaperX.LatticeCountingTransport

Back to source controls