LatticeCountingTransport.lean

1 import PaperX.LatticeCountingInterface
2 import Mathlib.Algebra.Module.ZLattice.Covolume
3 
4 /-! Exact transport of lattice counts and volume to integer coordinates. -/
5 set_option autoImplicit false
6 noncomputable section
7 namespace PaperX.LatticeCountingTransport
8 open Set MeasureTheory Module
9 open scoped Pointwise Topology
10 
11 variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
12   [FiniteDimensional ℝ E]
13   (L : Submodule ℤ E) [DiscreteTopology L] [IsZLattice ℝ L]
14   {ι : Type*} [Fintype ι] (b : Basis ι ℤ L)
15 
16 /-- Real coordinates associated with an actual integral lattice basis. -/
17 def coordinates : E ≃L[ℝ] (ι → ℝ) := (b.ofZLatticeBasis ℝ L).equivFunL
18 
19 /-- On lattice elements the real coordinates are exactly the integral coefficients. -/
20 theorem coordinates_lattice (x : L) :
21     coordinates L b (x : E) = fun i => (b.equivFun x i : ℝ) := by
22   ext i
23   exact b.ofZLatticeBasis_repr_apply ℝ L x i
24 
25 /-- The coordinate equivalence preserves the actual finite point-counting objects. -/
26 def latticePointsEquiv (S : Set E) :
27     (S ∩ (L : Set E) : Set E) ≃
28       {z : ι → ℤ // (fun i => (z i : ℝ)) ∈ coordinates L b '' S} where
29   toFun x := ⟨b.equivFun ⟨x.1, x.2.2⟩,
30     ⟨x.1, x.2.1, coordinates_lattice L b ⟨x.1, x.2.2⟩⟩⟩
31   invFun z := ⟨(b.equivFun.symm z.1 : L), by
32     constructor
33     · obtain ⟨y, hy, he⟩ := z.2
34       have hc : coordinates L b (b.equivFun.symm z.1 : L) = coordinates L b y := by
35         rw [coordinates_lattice]
36         simpa only [b.equivFun.apply_symm_apply] using he.symm
37       exact (coordinates L b).injective hc ▸ hy
38     · exact (b.equivFun.symm z.1).2⟩
39   left_inv x := by
40     apply Subtype.ext
41     simp only [b.equivFun.symm_apply_apply]
42   right_inv z := by
43     apply Subtype.ext
44     exact b.equivFun.apply_symm_apply z.1
45 
46 /-- Integral lattice counts become ordinary integer-grid counts. -/
47 theorem lattice_count_eq_grid_count (S : Set E) :
48     Nat.card (S ∩ (L : Set E) : Set E) =
49       {z : ι → ℤ | (fun i => (z i : ℝ)) ∈ coordinates L b '' S}.ncard := by
50   exact Nat.card_congr (latticePointsEquiv L b S)
51 
52 variable [MeasurableSpace E] [BorelSpace E]
53 
54 /-- The coordinate image has exactly the original volume divided by the covolume. -/
55 theorem volumeReal_coordinates_image {S : Set E} (hS : MeasurableSet S) :
56     volume.real (coordinates L b '' S) = volume.real S / ZLattice.covolume L := by
57   change (volume ((b.ofZLatticeBasis ℝ L).equivFun '' S)).toReal = _
58   rw [ZLattice.volume_image_eq_volume_div_covolume' L b hS.nullMeasurableSet,
59     ENNReal.toReal_div, ENNReal.toReal_ofReal (ZLattice.covolume_pos L volume).le]
60   rfl
61 
62 omit [MeasurableSpace E] [BorelSpace E] in
63 /-- Translation and real dilation commute with the lattice coordinate map. -/
64 theorem coordinates_affine_image (D : Set E) (a : E) (t : ℝ) :
65     coordinates L b '' ((fun x => a + t • x) '' D) =
66       (fun y => coordinates L b a + t • y) '' (coordinates L b '' D) := by
67   rw [← Set.image_comp, ← Set.image_comp]
68   congr 1
69   ext x
70   simp
71 
72 end PaperX.LatticeCountingTransport

Back to source controls