ResidueLatticeWeights.lean

1 import PaperX.ResidueLatticeIdeal
2 import PaperX.ResidueLatticePointSums
3 import Mathlib.Analysis.Complex.Basic
4 
5 /-! Complex weighted counts of actual finite additive residue fibers. -/
6 set_option autoImplicit false
7 set_option maxHeartbeats 50000
8 set_option backward.isDefEq.respectTransparency.types false
9 noncomputable section
10 namespace PaperX.ResidueLattice
11 open Set Module MeasureTheory
12 open scoped Pointwise BigOperators
13 
14 /-- Summing a common real error bound against arbitrary complex weights. -/
15 theorem norm_weighted_error_le {Q : Type*} [Fintype Q] (w : Q → ℂ) (a : Q → ℝ)
16     (main B : ℝ) (h : ∀ c, |a c - main| ≤ B) :
17     ‖(∑ c, w c * (a c : ℂ)) - (main : ℂ) * ∑ c, w c‖ ≤
18       (∑ c, ‖w c‖) * B := by
19   have he : (∑ c, w c * (a c : ℂ)) - (main : ℂ) * ∑ c, w c =
20       ∑ c, w c * ((a c - main : ℝ) : ℂ) := by
21     simp only [Complex.ofReal_sub, mul_sub, Finset.sum_sub_distrib,
22       Finset.mul_sum]
23     congr 1
24     exact Finset.sum_congr rfl (fun c _ => mul_comm _ _)
25   rw [he, Finset.sum_mul]
26   exact (norm_sum_le _ _).trans (Finset.sum_le_sum (fun c _ => by
27     rw [norm_mul, Complex.norm_real, Real.norm_eq_abs]
28     exact mul_le_mul_of_nonneg_left (h c) (norm_nonneg _)))
29 
30 /-- The same weighted estimate for natural counting functions, with casts normalized once. -/
31 theorem norm_weighted_nat_error_le {Q : Type*} [Fintype Q] (w : Q → ℂ) (a : Q → ℕ)
32     (main B : ℝ) (h : ∀ c, |(a c : ℝ) - main| ≤ B) :
33     ‖(∑ c, w c * (a c : ℂ)) - (main : ℂ) * ∑ c, w c‖ ≤
34       (∑ c, ‖w c‖) * B := by
35   simpa only [Complex.ofReal_natCast] using norm_weighted_error_le w (fun c => (a c : ℝ)) main B h
36 
37 /-- A common weighted discrepancy estimate over a specified finite index type. -/
38 def WeightedEstimate {Q : Type*} [Fintype Q] (a : Q → ℝ → ℕ)
39     (main boundary : ℝ → ℝ) : Prop :=
40   ∃ C : ℝ, 0 ≤ C ∧ ∀ (w : Q → ℂ) (t : ℝ), 1 ≤ t →
41     ‖(∑ c : Q, w c * (a c t : ℂ)) - (main t : ℂ) * ∑ c : Q, w c‖ ≤
42       (∑ c : Q, ‖w c‖) * C * boundary t
43 
44 /-- The zero-mean version of a weighted discrepancy estimate. -/
45 def ZeroMeanEstimate {Q : Type*} [Fintype Q] (a : Q → ℝ → ℕ)
46     (boundary : ℝ → ℝ) : Prop :=
47   ∃ C : ℝ, 0 ≤ C ∧ ∀ (w : Q → ℂ), (∑ c : Q, w c) = 0 →
48     ∀ t : ℝ, 1 ≤ t → ‖∑ c : Q, w c * (a c t : ℂ)‖ ≤
49       (∑ c : Q, ‖w c‖) * C * boundary t
50 
51 /-- An abstract finite-family estimate transports uniform counting errors to every complex weight. -/
52 theorem weightedEstimate_of_uniform_bound {Q : Type*} [Fintype Q]
53     (a : Q → ℝ → ℕ) (main boundary : ℝ → ℝ)
54     (h : ∃ C : ℝ, 0 ≤ C ∧ ∀ c t, 1 ≤ t → |(a c t : ℝ) - main t| ≤ C * boundary t) :
55     WeightedEstimate a main boundary := by
56   obtain ⟨C, hC, hb⟩ := h
57   refine ⟨C, hC, fun w t ht => ?_⟩
58   exact (norm_weighted_nat_error_le w (fun c => a c t) (main t) (C * boundary t)
59     (fun c => hb c t ht)).trans_eq (mul_assoc _ _ _).symm
60 
61 /-- Zero mean cancels the common main coefficient. -/
62 theorem WeightedEstimate.zeroMean {Q : Type*} [Fintype Q] {a : Q → ℝ → ℕ}
63     {main boundary : ℝ → ℝ} (h : WeightedEstimate a main boundary) :
64     ZeroMeanEstimate a boundary := by
65   obtain ⟨C, hC, hb⟩ := h
66   refine ⟨C, hC, fun w hw t ht => ?_⟩
67   simpa only [hw, mul_zero, sub_zero] using hb w t ht
68 
69 variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
70   [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
71   (L₀ L : Submodule ℤ E) [DiscreteTopology L₀] [IsZLattice ℝ L₀]
72   [DiscreteTopology L] [IsZLattice ℝ L]
73   [Fintype (Residues L₀ L)]
74 
75 /-- One constant controls every weight on the actual residue quotient by its finite L1 norm. -/
76 theorem exists_weightedFiber_bound (h : L₀ ≤ L)
77     {ι : Type*} [Fintype ι] (b : Basis ι ℤ L₀) {D : Set E}
78     (hDm : MeasurableSet D) (hDb : Bornology.IsBounded D)
79     (A : LatticeCounting.LipschitzBoundaryAtlas ι
80       (LatticeCountingTransport.coordinates L₀ b '' D)) :
81     WeightedEstimate (fiberCount L₀ L D)
82       (fun t => t ^ Fintype.card ι * ((volume.real D / ZLattice.covolume L) /
83         Nat.card (Residues L₀ L)))
84       (fun t => t ^ (Fintype.card ι - 1) + 1) :=
85   weightedEstimate_of_uniform_bound _ _ _
86     (exists_fiber_discrepancy_bound (E := E) L₀ L h (ι := ι) b (D := D) hDm hDb A)
87 
88 /-- A zero-mean actual residue weight cancels the entire main term. -/
89 theorem exists_zeroMean_weightedFiber_bound (h : L₀ ≤ L)
90     {ι : Type*} [Fintype ι] (b : Basis ι ℤ L₀) {D : Set E}
91     (hDm : MeasurableSet D) (hDb : Bornology.IsBounded D)
92     (A : LatticeCounting.LipschitzBoundaryAtlas ι
93       (LatticeCountingTransport.coordinates L₀ b '' D)) :
94     ZeroMeanEstimate (fiberCount L₀ L D) (fun t => t ^ (Fintype.card ι - 1) + 1) :=
95   (exists_weightedFiber_bound (E := E) L₀ L h (ι := ι) b (D := D) hDm hDb A).zeroMean
96 
97 end PaperX.ResidueLattice

Back to source controls