LatticeCountingInterface.lean

1 import Mathlib.Analysis.BoxIntegral.UnitPartition
2 import Mathlib.Analysis.Convex.Topology
3 import Mathlib.MeasureTheory.Measure.Typeclasses.Finite
4 
5 /-! A finite, dimension-correct Lipschitz frontier atlas. The quantitative
6 counting theorem will prove its bound from this geometric data. -/
7 noncomputable section
8 open Set MeasureTheory
9 open scoped Topology NNReal
10 
11 namespace PaperX.LatticeCounting
12 
13 structure LipschitzBoundaryAtlas (ι : Type*) [Fintype ι] (D : Set (ι → ℝ)) where
14   charts : ℕ
15   lip : ℝ≥0
16   map : Fin charts → (Fin (Fintype.card ι - 1) → ℝ) → (ι → ℝ)
17   lipschitz : ∀ j, LipschitzOnWith lip (map j) (Icc 0 1)
18   covers : frontier D ⊆ ⋃ j, map j '' Icc 0 1
19 
20 variable {ι : Type*} [Fintype ι]
21 
22 abbrev gridCell (z : ι → ℤ) : Set (ι → ℝ) :=
23   (BoxIntegral.unitPartition.box 1 z : Set (ι → ℝ))
24 
25 abbrev closedGridCell (z : ι → ℤ) : Set (ι → ℝ) :=
26   BoxIntegral.Box.Icc (BoxIntegral.unitPartition.box 1 z)
27 
28 abbrev gridTag (z : ι → ℤ) : ι → ℝ := BoxIntegral.unitPartition.tag 1 z
29 
30 /-- Closed unit cells meeting the actual topological boundary. -/
31 def boundaryCells (D : Set (ι → ℝ)) : Set (ι → ℤ) :=
32   {z | (closedGridCell z ∩ frontier D).Nonempty}
33 
34 /-- A connected cell containing a point in a set and a point outside it meets the boundary. -/
35 theorem connected_meets_frontier {E : Type*} [TopologicalSpace E]
36     {C D : Set E} (hC : IsPreconnected C) {x y : E}
37     (hx : x ∈ C) (hy : y ∈ C) (hxD : x ∈ D) (hyD : y ∉ D) :
38     (C ∩ frontier D).Nonempty := by
39   by_contra h
40   have hdis : ∀ z ∈ C, z ∉ frontier D := by
41     intro z hz hzD
42     exact h ⟨z, hz, hzD⟩
43   have hcover : C ⊆ interior D ∪ interior Dᶜ := by
44     intro z hz
45     by_cases hzD : z ∈ D
46     · exact Or.inl (not_not.mp ((mem_frontier_iff_notMem_interior hzD).not.mp (hdis z hz)))
47     · exact Or.inr (not_not.mp ((mem_frontier_iff_notMem_interior (s := Dᶜ) hzD).not.mp
48         (by simpa using hdis z hz)))
49   rcases hC.subset_or_subset isOpen_interior isOpen_interior
50     (disjoint_compl_right.mono interior_subset interior_subset) hcover with hD | hDc
51   · exact hyD (interior_subset (hD hy))
52   · exact (interior_subset (hDc hx)) hxD
53 
54 end PaperX.LatticeCounting

Back to source controls