ResidueLatticeFibers.lean

1 import PaperX.LatticeCountingFull
2 
3 /-! Actual additive residue fibers of a full sublattice. -/
4 set_option autoImplicit false
5 noncomputable section
6 namespace PaperX.ResidueLattice
7 open Set Module MeasureTheory
8 open scoped Pointwise
9 
10 variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
11   (L₀ L : Submodule ℤ E)
12 
13 /-- The genuine additive quotient of the ambient lattice by the sublattice. -/
14 abbrev Residues := L ⧸ L₀.comap L.subtype
15 
16 /-- The number of points in an actual additive residue fiber in a dilated region. -/
17 def fiberCount (D : Set E) (c : Residues L₀ L) (t : ℝ) : ℕ :=
18   Nat.card {x : L // (Submodule.Quotient.mk x : Residues L₀ L) = c ∧ (x : E) ∈ t • D}
19 
20 omit [InnerProductSpace ℝ E] in
21 /-- Equality of residue classes is exactly the ambient sublattice congruence. -/
22 theorem residue_eq_iff (x a : L) :
23     (Submodule.Quotient.mk x : Residues L₀ L) = Submodule.Quotient.mk a ↔
24       (x : E) - (a : E) ∈ L₀ := by
25   exact Submodule.Quotient.eq (L₀.comap L.subtype)
26 
27 /-- Every residue fiber is an actual affine coset, with an explicit point bijection. -/
28 def fiberCosetEquiv (h : L₀ ≤ L) (D : Set E) (a : L) (t : ℝ) :
29     {x : L // (Submodule.Quotient.mk x : Residues L₀ L) = Submodule.Quotient.mk a ∧
30       (x : E) ∈ t • D} ≃
31       (((fun x : E => (a : E) + x) '' (L₀ : Set E)) ∩ (t • D) : Set E) where
32   toFun x := ⟨x.1.1, by
33     refine ⟨⟨(x.1 : E) - (a : E), (residue_eq_iff L₀ L _ _).mp x.2.1, ?_⟩, x.2.2⟩
34     simp⟩
35   invFun x := ⟨⟨x.1, by
36     obtain ⟨l, hl, he⟩ := x.2.1
37     change (a : E) + l = x.1 at he
38     rw [← he]
39     exact L.add_mem a.2 (h hl)⟩, by
40     refine ⟨(residue_eq_iff L₀ L _ _).mpr ?_, x.2.2⟩
41     obtain ⟨l, hl, he⟩ := x.2.1
42     change (a : E) + l = x.1 at he
43     rw [← he]
44     simpa using hl⟩
45   left_inv x := by rfl
46   right_inv x := by rfl
47 
48 /-- The exact cardinality identity identifies the residue count with a coset count. -/
49 theorem fiberCount_eq_cosetCount (h : L₀ ≤ L) (D : Set E) (a : L) (t : ℝ) :
50     fiberCount L₀ L D (Submodule.Quotient.mk a) t =
51       Nat.card (((fun x : E => (a : E) + x) '' (L₀ : Set E)) ∩ (t • D) : Set E) :=
52   Nat.card_congr (fiberCosetEquiv L₀ L h D a t)
53 
54 omit [InnerProductSpace ℝ E] in
55 /-- The quotient cardinal is the actual relative lattice index. -/
56 theorem card_residues :
57     Nat.card (Residues L₀ L) = L₀.toAddSubgroup.relIndex L.toAddSubgroup := rfl
58 
59 variable [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
60   [DiscreteTopology L₀] [IsZLattice ℝ L₀]
61   [DiscreteTopology L] [IsZLattice ℝ L]
62 
63 /-- The finite residue cardinal is the covolume ratio. -/
64 theorem card_residues_eq_covolume_ratio (h : L₀ ≤ L) :
65     (Nat.card (Residues L₀ L) : ℝ) = ZLattice.covolume L₀ / ZLattice.covolume L := by
66   rw [card_residues, ZLattice.covolume_div_covolume_eq_relIndex' L₀ L h]
67 
68 /-- Finiteness of the residue quotient follows from the two full lattice hypotheses. -/
69 theorem finite_residues (h : L₀ ≤ L) : Finite (Residues L₀ L) := by
70   have hn : Nat.card (Residues L₀ L) ≠ 0 := by
71     intro hz
72     have hc := card_residues_eq_covolume_ratio L₀ L h
73     rw [hz, Nat.cast_zero] at hc
74     exact (div_ne_zero (ZLattice.covolume_ne_zero L₀) (ZLattice.covolume_ne_zero L)) hc.symm
75   exact Nat.finite_of_card_ne_zero hn
76 
77 /-- Every residue has the same main-term density, normalized by the actual index. -/
78 theorem residue_density (h : L₀ ≤ L) (D : Set E) :
79     volume.real D / ZLattice.covolume L₀ =
80       (volume.real D / ZLattice.covolume L) / Nat.card (Residues L₀ L) := by
81   rw [card_residues_eq_covolume_ratio L₀ L h]
82   field_simp [ZLattice.covolume_ne_zero L, ZLattice.covolume_ne_zero L₀]
83 
84 /-- One constant works for every actual residue class and every dilation at least one. -/
85 theorem exists_fiber_discrepancy_bound (h : L₀ ≤ L)
86     {ι : Type*} [Fintype ι] (b : Basis ι ℤ L₀) {D : Set E}
87     (hDm : MeasurableSet D) (hDb : Bornology.IsBounded D)
88     (A : LatticeCounting.LipschitzBoundaryAtlas ι
89       (LatticeCountingTransport.coordinates L₀ b '' D)) :
90     ∃ C : ℝ, 0 ≤ C ∧ ∀ (c : Residues L₀ L) (t : ℝ), 1 ≤ t →
91       |(fiberCount L₀ L D c t : ℝ) -
92         t ^ Fintype.card ι * ((volume.real D / ZLattice.covolume L) /
93           Nat.card (Residues L₀ L))| ≤ C * (t ^ (Fintype.card ι - 1) + 1) := by
94   obtain ⟨C, hC, hbound⟩ :=
95     LatticeCountingTransport.exists_coset_discrepancy_bound L₀ b hDm hDb A
96   refine ⟨C, hC, fun c t ht => ?_⟩
97   obtain ⟨a, rfl⟩ := Submodule.Quotient.mk_surjective (L₀.comap L.subtype) c
98   rw [fiberCount_eq_cosetCount L₀ L h D a t, ← residue_density L₀ L h D]
99   exact hbound a t ht
100 
101 end PaperX.ResidueLattice

Back to source controls