IndisputableMonolith.Gravity.Analysis.QuadratureLimit
IndisputableMonolith/Gravity/Analysis/QuadratureLimit.lean · 266 lines · 5 declarations
show as:
view math explainer →
1import Mathlib
2
3/-!
4# Quadrature limit toolkit: hinge sums converge to continuum integrals
5
6QG full-theory campaign, Phase 2a (reusable analysis toolkit).
7
8## Status: THEOREM (all results below are proved, axiom-clean; no sorry,
9## no admit, no `: True` shells).
10
11## What this module provides
12
13Mathlib (as vendored here) has no elementary "uniform-mesh Riemann sums of a
14continuous function converge to the interval integral" statement: the
15`BoxIntegral` library works at the level of tagged-partition filters, and
16`TrapezoidalRule` gives error bounds for C^2 integrands only. The core lemma
17`riemannSum_tendsto_integral` below is therefore proved from scratch via
18Heine-Cantor uniform continuity (`IsCompact.uniformContinuousOn_of_continuous`)
19and the adjacent-interval splitting
20`intervalIntegral.sum_integral_adjacent_intervals`.
21
22## Lemmas and their campaign consumers
23
24* `riemannSum_tendsto_integral`: for `f` continuous on `[a, b]`, the
25 left-endpoint uniform-mesh Riemann sums
26 `Σ_{k<N} f(a + k(b-a)/N) · (b-a)/N` tend to `∫ x in a..b, f x`.
27 Consumed by Phase 5 (continuum bracket limit) as the generic
28 discrete-action-to-integral bridge.
29* `latticeSum_tendsto_integral`: the campaign-facing hinge-sum shape,
30 `(1/N) Σ_{k<N} f(k/N) → ∫ x in 0..1, f x`.
31 Consumed by Phase 4 (curved operator convergence) and Phase 5.
32* `weightedLatticeSum_tendsto`: same with a continuous weight,
33 `(1/N) Σ_{k<N} f(k/N) w(k/N) → ∫ f·w`. Consumed by Phase 5 for
34 measure-weighted hinge sums.
35* `sq_error_sum_tendsto_zero`: a uniform per-term `C/N²` bound forces the
36 N-term absolute error sum to vanish. Consumed by Phase 4 remainder
37 estimates (curved perturbation of the flat spectrum).
38* `error_sum_tendsto_zero`: signed version of the previous lemma.
39
40These generalize the scoped quadrature reductions in
41`IndisputableMonolith/Gravity/D2ScalarDirichletQuadratureLimit.lean` (which
42packages the limit as a hypothesis structure) by actually proving the limit
43for continuous integrands, and they generalize the flat eigenvalue
44convergence pattern of
45`IndisputableMonolith/Gravity/SevenGaps/DiscreteLichnerowicz.lean`.
46-/
47
48namespace IndisputableMonolith
49namespace Gravity
50namespace Analysis
51
52open Filter Topology MeasureTheory
53
54/-- THEOREM (core quadrature limit). For `f : ℝ → ℝ` continuous on `[a, b]`
55with `a ≤ b`, the left-endpoint uniform-mesh Riemann sums
56`Σ_{k<N} f(a + k(b-a)/N) · ((b-a)/N)` converge to `∫ x in a..b, f x` as
57`N → ∞`.
58
59Proof: Heine-Cantor gives uniform continuity of `f` on the compact interval;
60splitting the integral over the `N` mesh cells
61(`intervalIntegral.sum_integral_adjacent_intervals`) reduces the error to a
62sum of `N` cell errors, each bounded by `ε · (b-a)/N` once the mesh
63`(b-a)/N` is below the uniform-continuity scale `δ`. -/
64theorem riemannSum_tendsto_integral (f : ℝ → ℝ) (a b : ℝ) (hab : a ≤ b)
65 (hf : ContinuousOn f (Set.Icc a b)) :
66 Filter.Tendsto
67 (fun N : ℕ => ∑ k ∈ Finset.range N,
68 f (a + (k : ℝ) * (b - a) / (N : ℝ)) * ((b - a) / (N : ℝ)))
69 Filter.atTop (nhds (∫ x in a..b, f x)) := by
70 rcases eq_or_lt_of_le hab with heq | hlt
71 · subst heq
72 simp only [sub_self, mul_zero, zero_div, add_zero,
73 Finset.sum_const_zero, intervalIntegral.integral_same]
74 exact tendsto_const_nhds
75 · have hba : 0 < b - a := sub_pos.2 hlt
76 rw [Metric.tendsto_atTop]
77 intro ε hε
78 set ε' : ℝ := ε / (2 * (b - a)) with hε'def
79 have hε' : 0 < ε' := div_pos hε (by linarith)
80 obtain ⟨δ, hδpos, hδ⟩ :=
81 Metric.uniformContinuousOn_iff_le.1
82 (isCompact_Icc.uniformContinuousOn_of_continuous hf) ε' hε'
83 obtain ⟨M, hM⟩ := exists_nat_ge ((b - a) / δ)
84 refine ⟨max M 1, fun N hN => ?_⟩
85 have hN1 : 1 ≤ N := le_trans (le_max_right M 1) hN
86 have hNM : M ≤ N := le_trans (le_max_left M 1) hN
87 have hNpos : (0 : ℝ) < (N : ℝ) := by exact_mod_cast Nat.lt_of_lt_of_le Nat.zero_lt_one hN1
88 have hN0 : (N : ℝ) ≠ 0 := ne_of_gt hNpos
89 have hmesh : (b - a) / (N : ℝ) ≤ δ := by
90 rw [div_le_iff₀ hNpos]
91 have h1 : (b - a) / δ ≤ (N : ℝ) := le_trans hM (by exact_mod_cast hNM)
92 have h2 : δ * ((b - a) / δ) ≤ δ * (N : ℝ) :=
93 mul_le_mul_of_nonneg_left h1 hδpos.le
94 have h3 : δ * ((b - a) / δ) = b - a := by field_simp
95 linarith
96 set p : ℕ → ℝ := fun k => a + (k : ℝ) * (b - a) / (N : ℝ) with hp
97 have hp0 : p 0 = a := by simp [hp]
98 have hpN : p N = b := by
99 simp only [hp]
100 field_simp
101 ring
102 have hstep : ∀ k : ℕ, p (k + 1) - p k = (b - a) / (N : ℝ) := by
103 intro k
104 simp only [hp]
105 push_cast
106 ring
107 have hmeshpos : 0 ≤ (b - a) / (N : ℝ) := div_nonneg hba.le hNpos.le
108 have hple : ∀ k : ℕ, p k ≤ p (k + 1) := by
109 intro k
110 have := hstep k
111 linarith
112 have hmem : ∀ k : ℕ, k ≤ N → p k ∈ Set.Icc a b := by
113 intro k hk
114 have hkN : (k : ℝ) ≤ (N : ℝ) := by exact_mod_cast hk
115 have hq : 0 ≤ (b - a) / (N : ℝ) := hmeshpos
116 have h2 := mul_le_mul_of_nonneg_left hkN hq
117 have hNb : (b - a) / (N : ℝ) * (N : ℝ) = b - a := by field_simp
118 have hknn : 0 ≤ (k : ℝ) * (b - a) / (N : ℝ) :=
119 div_nonneg (mul_nonneg (Nat.cast_nonneg k) hba.le) hNpos.le
120 have hcomm : (k : ℝ) * (b - a) / (N : ℝ) = (b - a) / (N : ℝ) * (k : ℝ) := by
121 ring
122 constructor
123 · simp only [hp]
124 linarith
125 · simp only [hp]
126 linarith [h2, hNb, hcomm]
127 have hint : ∀ k, k < N → IntervalIntegrable f volume (p k) (p (k + 1)) := by
128 intro k hk
129 apply ContinuousOn.intervalIntegrable
130 apply hf.mono
131 rw [Set.uIcc_of_le (hple k)]
132 exact Set.Icc_subset_Icc (hmem k hk.le).1 (hmem (k + 1) hk).2
133 have hsplit : (∑ k ∈ Finset.range N, ∫ x in p k..p (k + 1), f x)
134 = ∫ x in a..b, f x := by
135 rw [intervalIntegral.sum_integral_adjacent_intervals hint, hp0, hpN]
136 have hkey : (∑ k ∈ Finset.range N, f (p k) * ((b - a) / (N : ℝ)))
137 - (∫ x in a..b, f x)
138 = ∑ k ∈ Finset.range N, ∫ x in p k..p (k + 1), (f (p k) - f x) := by
139 rw [← hsplit, ← Finset.sum_sub_distrib]
140 refine Finset.sum_congr rfl fun k hk => ?_
141 have hk' : k < N := Finset.mem_range.1 hk
142 have hsub : (∫ x in p k..p (k + 1), (f (p k) - f x))
143 = (∫ _x in p k..p (k + 1), f (p k)) - ∫ x in p k..p (k + 1), f x :=
144 intervalIntegral.integral_sub intervalIntegrable_const (hint k hk')
145 rw [hsub, intervalIntegral.integral_const, hstep k, smul_eq_mul]
146 ring
147 have hbound : ∀ k ∈ Finset.range N,
148 |∫ x in p k..p (k + 1), (f (p k) - f x)| ≤ ε' * ((b - a) / (N : ℝ)) := by
149 intro k hk
150 have hk' : k < N := Finset.mem_range.1 hk
151 have hCbound : ∀ x ∈ Set.uIoc (p k) (p (k + 1)), ‖f (p k) - f x‖ ≤ ε' := by
152 intro x hx
153 rw [Set.uIoc_of_le (hple k)] at hx
154 have hxmem : x ∈ Set.Icc a b :=
155 ⟨le_trans (hmem k hk'.le).1 hx.1.le, le_trans hx.2 (hmem (k + 1) hk').2⟩
156 have hdist : dist (p k) x ≤ δ := by
157 rw [Real.dist_eq, abs_of_nonpos (by linarith [hx.1.le] : p k - x ≤ 0)]
158 have hupper : x ≤ p k + (b - a) / (N : ℝ) := by
159 have := hstep k
160 linarith [hx.2]
161 linarith [hmesh]
162 have h := hδ (p k) (hmem k hk'.le) x hxmem hdist
163 rw [Real.dist_eq] at h
164 rwa [Real.norm_eq_abs]
165 calc |∫ x in p k..p (k + 1), (f (p k) - f x)|
166 ≤ ε' * |p (k + 1) - p k| := by
167 rw [← Real.norm_eq_abs]
168 exact intervalIntegral.norm_integral_le_of_norm_le_const hCbound
169 _ = ε' * ((b - a) / (N : ℝ)) := by
170 rw [hstep k, abs_of_nonneg hmeshpos]
171 have hsum_bound : |(∑ k ∈ Finset.range N, f (p k) * ((b - a) / (N : ℝ)))
172 - ∫ x in a..b, f x| ≤ ε' * (b - a) := by
173 rw [hkey]
174 calc |∑ k ∈ Finset.range N, ∫ x in p k..p (k + 1), (f (p k) - f x)|
175 ≤ ∑ k ∈ Finset.range N, |∫ x in p k..p (k + 1), (f (p k) - f x)| :=
176 Finset.abs_sum_le_sum_abs _ _
177 _ ≤ ∑ _k ∈ Finset.range N, ε' * ((b - a) / (N : ℝ)) :=
178 Finset.sum_le_sum hbound
179 _ = (N : ℝ) * (ε' * ((b - a) / (N : ℝ))) := by
180 rw [Finset.sum_const, Finset.card_range, nsmul_eq_mul]
181 _ = ε' * (b - a) := by
182 field_simp
183 have hfinal : ε' * (b - a) < ε := by
184 have hhalf : ε' * (b - a) = ε / 2 := by
185 rw [hε'def]
186 field_simp
187 linarith [hhalf]
188 rw [Real.dist_eq]
189 exact lt_of_le_of_lt hsum_bound hfinal
190
191/-- THEOREM (campaign-facing hinge-sum form). For `f` continuous on `[0, 1]`,
192the lattice averages `(1/N) Σ_{k<N} f(k/N)` converge to `∫ x in 0..1, f x`.
193This is the exact shape of discrete-gravity hinge sums (one summand per
194lattice hinge, spacing `1/N`); Phases 4 and 5 consume it directly. -/
195theorem latticeSum_tendsto_integral (f : ℝ → ℝ)
196 (hf : ContinuousOn f (Set.Icc 0 1)) :
197 Filter.Tendsto
198 (fun N : ℕ => (1 / (N : ℝ)) * ∑ k ∈ Finset.range N, f ((k : ℝ) / (N : ℝ)))
199 Filter.atTop (nhds (∫ x in (0:ℝ)..1, f x)) := by
200 have h := riemannSum_tendsto_integral f 0 1 zero_le_one hf
201 refine h.congr fun N => ?_
202 rw [Finset.mul_sum]
203 refine Finset.sum_congr rfl fun k _ => ?_
204 have harg : (0 : ℝ) + (k : ℝ) * (1 - 0) / (N : ℝ) = (k : ℝ) / (N : ℝ) := by ring
205 have hw : ((1 : ℝ) - 0) / (N : ℝ) = 1 / (N : ℝ) := by norm_num
206 rw [harg, hw, mul_comm]
207
208/-- THEOREM (weighted hinge-sum form). For `f` and a weight `w` both
209continuous on `[0, 1]`, `(1/N) Σ_{k<N} f(k/N) w(k/N) → ∫ x in 0..1, f x · w x`.
210A direct corollary of `latticeSum_tendsto_integral` applied to `f·w`; stated
211separately because Phase 5 consumes exactly this weighted shape
212(measure-weighted hinge sums). -/
213theorem weightedLatticeSum_tendsto (f w : ℝ → ℝ)
214 (hf : ContinuousOn f (Set.Icc 0 1)) (hw : ContinuousOn w (Set.Icc 0 1)) :
215 Filter.Tendsto
216 (fun N : ℕ => (1 / (N : ℝ)) *
217 ∑ k ∈ Finset.range N, f ((k : ℝ) / (N : ℝ)) * w ((k : ℝ) / (N : ℝ)))
218 Filter.atTop (nhds (∫ x in (0:ℝ)..1, f x * w x)) :=
219 latticeSum_tendsto_integral (fun x => f x * w x) (hf.mul hw)
220
221/-- THEOREM (remainder collapse). If the per-term errors `g N k` are
222uniformly bounded by `C/N²` for `k < N`, then the `N`-term absolute error
223sum `Σ_{k<N} |g N k|` tends to `0`: the total error is at most `C/N`.
224Load-bearing for Phase 4 remainder terms (curved perturbations of the flat
225spectrum enter as `O(1/N²)` per mode). -/
226theorem sq_error_sum_tendsto_zero (g : ℕ → ℕ → ℝ) (C : ℝ)
227 (hg : ∀ N : ℕ, ∀ k, k < N → |g N k| ≤ C / (N : ℝ) ^ 2) :
228 Filter.Tendsto (fun N : ℕ => ∑ k ∈ Finset.range N, |g N k|)
229 Filter.atTop (nhds 0) := by
230 have hub : ∀ N : ℕ, (∑ k ∈ Finset.range N, |g N k|) ≤ C / (N : ℝ) := by
231 intro N
232 calc (∑ k ∈ Finset.range N, |g N k|)
233 ≤ ∑ _k ∈ Finset.range N, C / (N : ℝ) ^ 2 :=
234 Finset.sum_le_sum fun k hk => hg N k (Finset.mem_range.1 hk)
235 _ = (N : ℝ) * (C / (N : ℝ) ^ 2) := by
236 rw [Finset.sum_const, Finset.card_range, nsmul_eq_mul]
237 _ = C / (N : ℝ) := by
238 rcases Nat.eq_zero_or_pos N with h0 | hpos
239 · subst h0; simp
240 · have hN0 : (N : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr hpos.ne'
241 field_simp
242 exact squeeze_zero (fun N => Finset.sum_nonneg fun k _ => abs_nonneg _) hub
243 (tendsto_const_div_atTop_nhds_zero_nat C)
244
245/-- THEOREM (signed remainder collapse). Same hypothesis as
246`sq_error_sum_tendsto_zero`; the signed error sum `Σ_{k<N} g N k` also tends
247to `0`. Phase 4 consumes this form when remainders carry signs. -/
248theorem error_sum_tendsto_zero (g : ℕ → ℕ → ℝ) (C : ℝ)
249 (hg : ∀ N : ℕ, ∀ k, k < N → |g N k| ≤ C / (N : ℝ) ^ 2) :
250 Filter.Tendsto (fun N : ℕ => ∑ k ∈ Finset.range N, g N k)
251 Filter.atTop (nhds 0) := by
252 have h1 := sq_error_sum_tendsto_zero g C hg
253 have h2 : Filter.Tendsto (fun N : ℕ => |∑ k ∈ Finset.range N, g N k|)
254 Filter.atTop (nhds 0) :=
255 squeeze_zero (fun N => abs_nonneg _)
256 (fun N => Finset.abs_sum_le_sum_abs _ _) h1
257 have hneg : Filter.Tendsto (fun N : ℕ => -|∑ k ∈ Finset.range N, g N k|)
258 Filter.atTop (nhds 0) := by
259 simpa using h2.neg
260 exact tendsto_of_tendsto_of_tendsto_of_le_of_le hneg h2
261 (fun N => neg_abs_le _) (fun N => le_abs_self _)
262
263end Analysis
264end Gravity
265end IndisputableMonolith
266