LatticeCountingGrid.lean

1 import PaperX.LatticeCountingDiscrepancy
2 import PaperX.IntegerCellFiniteCharts
3 import Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
4 
5 noncomputable section
6 open Set MeasureTheory
7 open scoped Topology NNReal symmDiff Pointwise
8 
9 namespace PaperX.LatticeCounting
10 variable {ι : Type*} [Fintype ι]
11 
12 omit [Fintype ι] in
13 theorem closedGridCell_eq (z : ι → ℤ) :
14     closedGridCell z = IntegerCellBounds.closedCell z := by
15   simp [closedGridCell, BoxIntegral.Box.Icc_def, IntegerCellBounds.closedCell,
16     BoxIntegral.unitPartition.box]
17 
18 omit [Fintype ι] in
19 theorem boundaryCells_eq (D : Set (ι → ℝ)) :
20     boundaryCells D = IntegerCellBounds.touching (frontier D) := by
21   simp [boundaryCells, IntegerCellBounds.touching, closedGridCell_eq]
22 
23 omit [Fintype ι] in
24 theorem gridTag_eq (z : ι → ℤ) : gridTag z = fun i => (z i : ℝ) + 1 := by
25   funext i
26   simp [gridTag, BoxIntegral.unitPartition.tag_apply]
27 
28 omit [Fintype ι] in
29 /-- Counting upper-right cell tags agrees exactly with counting integer vectors. -/
30 theorem ncard_upper_tags_eq (D : Set (ι → ℝ)) :
31     {z : ι → ℤ | gridTag z ∈ D}.ncard =
32       {z : ι → ℤ | (fun i => (z i : ℝ)) ∈ D}.ncard := by
33   apply Set.ncard_congr (fun z _ => z + 1)
34   · intro z hz
35     simpa [gridTag_eq, Int.cast_add] using hz
36   · intro z w hz hw h
37     exact add_right_cancel h
38   · intro z hz
39     refine ⟨z - 1, ?_, sub_add_cancel z 1⟩
40     simpa [gridTag_eq, Int.cast_sub] using hz
41 
42 /-- The actual standard integer-lattice discrepancy is bounded by boundary cells. -/
43 theorem integer_discrepancy_le_touching {D : Set (ι → ℝ)}
44     (hDm : MeasurableSet D) (hDb : Bornology.IsBounded D)
45     (hB : (IntegerCellBounds.touching (frontier D)).Finite) :
46     |({z : ι → ℤ | (fun i => (z i : ℝ)) ∈ D}.ncard : ℝ) - volume.real D| ≤
47       (IntegerCellBounds.touching (frontier D)).ncard := by
48   have hS : {z : ι → ℤ | gridTag z ∈ D}.Finite := by
49     simpa [gridTag_eq] using
50       IntegerCellBounds.finite_upper_tags_of_isBounded hDb
51   have h := discrepancy_le_boundary_cells hDm hDb hS.toFinset hB.toFinset
52     (by intro z; simp) (by intro z hz; simpa [boundaryCells_eq] using hz)
53   rw [← Set.ncard_eq_toFinset_card _ hS, ← Set.ncard_eq_toFinset_card _ hB,
54     ncard_upper_tags_eq] at h
55   exact h
56 
57 omit [Fintype ι] in
58 /-- Translation and nonzero dilation carry the entire topological boundary. -/
59 theorem frontier_affine_image (D : Set (ι → ℝ)) (a : ι → ℝ) (t : ℝ) (ht : t ≠ 0) :
60     frontier ((fun x => a + t • x) '' D) =
61       (fun x => a + t • x) '' frontier D := by
62   let e := (Homeomorph.smulOfNeZero t ht : (ι → ℝ) ≃ₜ (ι → ℝ)).trans
63     (Homeomorph.addLeft a)
64   exact (e.image_frontier D).symm
65 
66 theorem measurableSet_affine_image {D : Set (ι → ℝ)} (hD : MeasurableSet D)
67     (a : ι → ℝ) (t : ℝ) (ht : t ≠ 0) :
68     MeasurableSet ((fun x => a + t • x) '' D) := by
69   let e := (Homeomorph.smulOfNeZero t ht : (ι → ℝ) ≃ₜ (ι → ℝ)).trans
70     (Homeomorph.addLeft a)
71   exact e.toMeasurableEquiv.measurableSet_image.mpr hD
72 
73 theorem isBounded_affine_image {D : Set (ι → ℝ)} (hD : Bornology.IsBounded D)
74     (a : ι → ℝ) (t : ℝ) : Bornology.IsBounded ((fun x => a + t • x) '' D) := by
75   have hf : LipschitzWith ‖t‖₊ (fun x : ι → ℝ => a + t • x) := by
76     exact LipschitzWith.of_dist_le_mul fun x y => by
77       simpa only [dist_eq_norm, add_sub_add_left_eq_sub, ← smul_sub, norm_smul, coe_nnnorm] using
78         (le_refl (‖t‖ * ‖x - y‖))
79   exact hf.isBounded_image hD
80 
81 theorem volumeReal_affine_image (D : Set (ι → ℝ)) (a : ι → ℝ) (t : ℝ) (ht : 0 ≤ t) :
82     volume.real ((fun x => a + t • x) '' D) =
83       t ^ Fintype.card ι * volume.real D := by
84   have heq : (fun x => a + t • x) '' D = (fun y => a + y) '' (t • D) := by
85     rw [← image_smul, image_image]
86   rw [heq, Measure.real, image_add_left, measure_preimage_add,
87     volume.addHaar_smul_of_nonneg ht]
88   simp [ENNReal.toReal_mul, ENNReal.toReal_ofReal (pow_nonneg ht _),
89     Measure.real]
90 
91 /-- Every bounded measurable region with a finite Lipschitz frontier atlas has
92 uniform translated standard-lattice discrepancy of surface order. -/
93 theorem exists_grid_discrepancy_bound {D : Set (ι → ℝ)}
94     (hDm : MeasurableSet D) (hDb : Bornology.IsBounded D)
95     (A : LipschitzBoundaryAtlas ι D) :
96     ∃ C : ℝ, 0 ≤ C ∧ ∀ (a : ι → ℝ) (t : ℝ), 1 ≤ t →
97       |({z : ι → ℤ | (fun i => (z i : ℝ)) ∈ (fun x => a + t • x) '' D}.ncard : ℝ) -
98         t ^ Fintype.card ι * volume.real D| ≤ C * (t ^ (Fintype.card ι - 1) + 1) := by
99   let C : ℝ := (A.charts : ℝ) * 3 ^ (Fintype.card ι - 1) *
100     (2 * Nat.ceil ((A.lip : ℝ) + 1) + 3) ^ Fintype.card ι
101   have hC : 0 ≤ C := by dsimp [C]; positivity
102   refine ⟨C, hC, ?_⟩
103   intro a t ht
104   have ht0 : 0 ≤ t := by linarith
105   have htne : t ≠ 0 := by linarith
106   have hcov : frontier ((fun x => a + t • x) '' D) ⊆
107       ⋃ j, (fun x => a + t • A.map j x) '' Icc 0 1 := by
108     rw [frontier_affine_image D a t htne]
109     rintro y ⟨x, hx, rfl⟩
110     obtain ⟨j, hj⟩ := mem_iUnion.mp (A.covers hx)
111     obtain ⟨z, hz, rfl⟩ := hj
112     exact mem_iUnion.mpr ⟨j, mem_image_of_mem _ hz⟩
113   obtain ⟨hfin, hcount⟩ := IntegerCellBounds.touching_finite_charts_polynomial_bound
114     (frontier ((fun x => a + t • x) '' D)) A.map A.lip A.lipschitz a t ht hcov
115   have hdisc := integer_discrepancy_le_touching (measurableSet_affine_image hDm a t htne)
116     (isBounded_affine_image hDb a t) hfin
117   rw [volumeReal_affine_image D a t ht0] at hdisc
118   refine hdisc.trans ((show _ ≤ C * t ^ (Fintype.card ι - 1) by
119     simpa [C] using hcount).trans ?_)
120   exact mul_le_mul_of_nonneg_left (le_add_of_nonneg_right zero_le_one) hC
121 
122 end PaperX.LatticeCounting

Back to source controls