ResidueLatticePointSums.lean

1 import PaperX.ResidueLatticeFibers
2 import Mathlib.Analysis.Complex.Basic
3 import Mathlib.Algebra.BigOperators.Finprod
4 import Mathlib.Analysis.Normed.Module.Ball.Pointwise
5 
6 /-! Exact identification of residue-weighted counts with sums over actual lattice points. -/
7 set_option autoImplicit false
8 noncomputable section
9 namespace PaperX.ResidueLattice
10 open Set Module MeasureTheory
11 open scoped Pointwise BigOperators
12 
13 variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
14   (L₀ L : Submodule ℤ E)
15 
16 /-- The exact residue-weighted count, using actual points in every fiber. -/
17 def weightedFiberCount [Fintype (Residues L₀ L)] (D : Set E) (w : Residues L₀ L → ℂ) (t : ℝ) : ℂ :=
18   ∑ c, w c * (fiberCount L₀ L D c t : ℂ)
19 
20 /-- The actual points of a lattice lying in the dilated region. -/
21 abbrev LatticePoints (D : Set E) (t : ℝ) := {x : L // (x : E) ∈ t • D}
22 
23 /-- The quotient fiber of the bounded-point map is exactly the original residue fiber. -/
24 def pointFiberEquiv (D : Set E) (t : ℝ) (c : Residues L₀ L) :
25     {x : LatticePoints L D t // (Submodule.Quotient.mk x.1 : Residues L₀ L) = c} ≃
26     {x : L // (Submodule.Quotient.mk x : Residues L₀ L) = c ∧ (x : E) ∈ t • D} where
27   toFun x := ⟨x.1.1, x.2, x.1.2⟩
28   invFun x := ⟨⟨x.1, x.2.2⟩, x.2.1⟩
29   left_inv _x := rfl
30   right_inv _x := rfl
31 
32 /-- An actual finite sum of residue weights over the points, independent of a chosen enumeration. -/
33 def latticePointSum (D : Set E) (w : Residues L₀ L → ℂ) (t : ℝ) : ℂ :=
34   ∑ᶠ x : LatticePoints L D t, w (Submodule.Quotient.mk x.1)
35 
36 variable [FiniteDimensional ℝ E] [DiscreteTopology L]
37 
38 /-- A bounded region contains only finitely many points of the discrete lattice. -/
39 theorem finite_latticePoints {D : Set E} (hDb : Bornology.IsBounded D) (t : ℝ) :
40     Finite (LatticePoints L D t) := by
41   have hs : (t • D ∩ (L : Set E)).Finite :=
42     Metric.finite_isBounded_inter_isClosed DiscreteTopology.isDiscrete
43       (hDb.smul₀ t) (AddSubgroup.isClosed_of_discrete (H := L.toAddSubgroup))
44   let : Finite (t • D ∩ (L : Set E) : Set E) := hs.to_subtype
45   exact Finite.of_injective
46     (fun x : LatticePoints L D t => (⟨x.1.1, x.2, x.1.2⟩ : (t • D ∩ (L : Set E) : Set E)))
47     (by
48       intro x y h
49       apply Subtype.ext
50       apply Subtype.ext
51       exact congrArg (fun z : (t • D ∩ (L : Set E) : Set E) => z.1) h)
52 
53 variable [Fintype (Residues L₀ L)]
54 
55 /-- The finite residue decomposition is exactly the sum over the actual lattice points. -/
56 theorem weightedFiberCount_eq_pointSum {D : Set E} (hDb : Bornology.IsBounded D)
57     (w : Residues L₀ L → ℂ) (t : ℝ) :
58     weightedFiberCount L₀ L D w t = latticePointSum L₀ L D w t := by
59   classical
60   let : Finite (LatticePoints L D t) := finite_latticePoints L hDb t
61   let : Fintype (LatticePoints L D t) := Fintype.ofFinite (LatticePoints L D t)
62   unfold weightedFiberCount latticePointSum
63   rw [finsum_eq_sum_of_fintype, ← Fintype.sum_fiberwise
64     (fun x : LatticePoints L D t => (Submodule.Quotient.mk x.1 : Residues L₀ L))]
65   apply Finset.sum_congr rfl
66   intro c _
67   have he := Nat.card_congr (pointFiberEquiv L₀ L D t c)
68   change Nat.card _ = fiberCount L₀ L D c t at he
69   rw [← he, Nat.card_eq_fintype_card]
70   conv_rhs =>
71     arg 2
72     ext x
73     rw [x.2]
74   simp only [Finset.sum_const, Finset.card_univ, nsmul_eq_mul]
75   exact mul_comm _ _
76 
77 end PaperX.ResidueLattice

Back to source controls