LatticeCountingDiscrepancy.lean

1 import PaperX.LatticeCountingInterface
2 import Mathlib.Analysis.Convex.PathConnected
3 
4 noncomputable section
5 open Set MeasureTheory
6 open scoped Topology NNReal symmDiff
7 
8 namespace PaperX.LatticeCounting
9 variable {ι : Type*} [Fintype ι]
10 
11 /-- Unit cells selected by their lattice tags. -/
12 def cellUnion (s : Finset (ι → ℤ)) : Set (ι → ℝ) := ⋃ z ∈ s, gridCell z
13 
14 theorem measurableSet_cellUnion (s : Finset (ι → ℤ)) : MeasurableSet (cellUnion s) := by
15   apply Finset.measurableSet_biUnion
16   intro z hz
17   exact (BoxIntegral.unitPartition.box 1 z).measurableSet_coe
18 
19 theorem isBounded_cellUnion (s : Finset (ι → ℤ)) : Bornology.IsBounded (cellUnion s) := by
20   classical
21   induction s using Finset.induction_on with
22   | empty => simp [cellUnion]
23   | insert z s hz ih =>
24     simpa [cellUnion] using (BoxIntegral.unitPartition.box 1 z).isBounded.union ih
25 
26 theorem volumeReal_gridCell (z : ι → ℤ) : volume.real (gridCell z) = 1 := by
27   simp [Measure.real, gridCell, BoxIntegral.unitPartition.volume_box]
28 
29 theorem volumeReal_cellUnion (s : Finset (ι → ℤ)) : volume.real (cellUnion s) = s.card := by
30   have hd : (↑s : Set (ι → ℤ)).PairwiseDisjoint gridCell := by
31     intro z hz w hw hzw
32     exact BoxIntegral.unitPartition.disjoint.mp hzw
33   have hm : ∀ z ∈ s, MeasurableSet (gridCell z) := by
34     intro z hz
35     exact (BoxIntegral.unitPartition.box 1 z).measurableSet_coe
36   have hf : ∀ z ∈ s, volume (gridCell z) ≠ ⊤ := by
37     intro z hz
38     simp [gridCell, BoxIntegral.unitPartition.volume_box]
39   rw [cellUnion, measureReal_biUnion_finset hd hm hf]
40   simp [volumeReal_gridCell]
41 
42 omit [Fintype ι] in
43 theorem tag_mem_closedGridCell (z : ι → ℤ) : gridTag z ∈ closedGridCell z :=
44   BoxIntegral.Box.coe_subset_Icc (BoxIntegral.unitPartition.tag_mem 1 z)
45 
46 omit [Fintype ι] in
47 theorem preconnected_closedGridCell (z : ι → ℤ) : IsPreconnected (closedGridCell z) := by
48   exact (convex_Icc _ _).isPreconnected
49 
50 omit [Fintype ι] in
51 theorem cellUnion_symmDiff_subset_boundary_union {D : Set (ι → ℝ)}
52     (s b : Finset (ι → ℤ)) (hs : ∀ z, z ∈ s ↔ gridTag z ∈ D)
53     (hb : ∀ z, z ∈ boundaryCells D → z ∈ b) :
54     cellUnion s ∆ D ⊆ cellUnion b := by
55   intro x hx
56   rcases hx with ⟨hxU, hxD⟩ | ⟨hxD, hxU⟩
57   · obtain ⟨z, hzs, hxz⟩ := mem_iUnion₂.mp hxU
58     have hzb : z ∈ b := hb z (connected_meets_frontier (preconnected_closedGridCell z)
59       (tag_mem_closedGridCell z) (BoxIntegral.Box.coe_subset_Icc hxz) ((hs z).mp hzs) hxD)
60     exact mem_iUnion₂.mpr ⟨z, hzb, hxz⟩
61   · let z := BoxIntegral.unitPartition.index 1 x
62     have hxz : x ∈ gridCell z := BoxIntegral.unitPartition.mem_box_iff_index.mpr rfl
63     have hznot : gridTag z ∉ D := by
64       intro hzD
65       exact hxU (mem_iUnion₂.mpr ⟨z, (hs z).mpr hzD, hxz⟩)
66     have hzb : z ∈ b := hb z (connected_meets_frontier (preconnected_closedGridCell z)
67       (BoxIntegral.Box.coe_subset_Icc hxz) (tag_mem_closedGridCell z) hxD hznot)
68     exact mem_iUnion₂.mpr ⟨z, hzb, hxz⟩
69 
70 /-- The discrepancy is bounded by the number of unit cells meeting the boundary.
71 The bound follows from an actual partition and exact unit-cell volumes. -/
72 theorem discrepancy_le_boundary_cells {D : Set (ι → ℝ)} (hD : MeasurableSet D)
73     (hDb : Bornology.IsBounded D) (s b : Finset (ι → ℤ))
74     (hs : ∀ z, z ∈ s ↔ gridTag z ∈ D)
75     (hb : ∀ z, z ∈ boundaryCells D → z ∈ b) :
76     |(s.card : ℝ) - volume.real D| ≤ b.card := by
77   rw [← volumeReal_cellUnion s, ← volumeReal_cellUnion b]
78   refine (abs_measureReal_sub_le_measureReal_symmDiff'
79     (measurableSet_cellUnion s).nullMeasurableSet hD.nullMeasurableSet
80     (isBounded_cellUnion s).measure_lt_top.ne hDb.measure_lt_top.ne).trans ?_
81   exact measureReal_mono (cellUnion_symmDiff_subset_boundary_union s b hs hb)
82     (isBounded_cellUnion b).measure_lt_top.ne
83 
84 end PaperX.LatticeCounting

Back to source controls