EventReading

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

Reading the good events 𝒢₁ and 𝒢₂ back into real estimates

Support.eventG1 and Support.eventG2 (ABK26, d.good.event.for.lambda) are stated in [0,∞], with no convergence side condition. Every consumer inside the proof of p.mathcalE.annular.decomp needs the real readings: a finite sum, a bound on it, and -- the point of working in [0,∞] in the first place -- the summability that keeps Lean's junk value 0 out of the real tsums.

This module supplies exactly those readings, each with the event membership as its only substantive hypothesis.

Part A -- the [0,∞]-to-real transport

summable_of_ofReal_tsum_ne_top and tsum_le_of_ofReal_tsum_le: a nonnegative real family whose ENNReal.ofReal sum is finite is summable, and its sum obeys the same bound. ennreal_tsum_annFam_eq identifies the ℤ × ℤ sum of the guarded annular family Resum.annFam with the iterated subtype sum in which the events are written, which is what turns a 𝒢₂ membership into the hsumE binder of ClauseOne.clauseOne_bound.

Part B -- the 𝒢₁ readings

• the first component gives Summable for the k ≥ m shell tail, the bound Σ ≤ T, and hence gradTailSq M m ω ≤ T² -- the G₁ᵃ bracket that A2b's frontier item (d) recorded as missing;
• the second component gives the summability and the bound ≤ T² for the single shell sum at the event's own weight 3^{−(s/4)v}, at the A5b-pinned family DisplaySlots.shellBlockLatticeReal. The two consequences the assembly needs are the hAsum binder (at the display weight 3^{−(s/2)v}, which is smaller) and the partial-sum budget Σ_{v<q+2} A(m−v)² ≤ 3^{s/4} T² 3^{(s/4)q} feeding AssemblyFeed.summable_annFam_grad and AssemblyFeed.summable_annFam_l2.

Part A -- the [0,infinity]-to-real transport

theorem Algsuperdiff.Section4.Provider.Annular.summable_of_ofReal_tsum_ne_top {iota : Type u_1} {f : iota → ℝ} (hf0 : ∀ (i : iota), 0 ≤ f i) (hfin : ∑' (i : iota), ENNReal.ofReal (f i) ≠ ⊤) : Summable f

A nonnegative real family whose ENNReal.ofReal sum is finite is summable.

theorem Algsuperdiff.Section4.Provider.Annular.tsum_le_of_ofReal_tsum_le {iota : Type u_1} {f : iota → ℝ} {T : ℝ} (hf0 : ∀ (i : iota), 0 ≤ f i) (hT : 0 ≤ T) (hle : ∑' (i : iota), ENNReal.ofReal (f i) ≤ ENNReal.ofReal T) : ∑' (i : iota), f i ≤ T

The real reading of an [0,infinity]-valued bound on a nonnegative real family: the sum obeys the same bound (and is not the junk value).

theorem Algsuperdiff.Section4.Provider.Annular.ennreal_tsum_annFam_eq (m : ℤ) (h : ℤ → ℤ → ℝ) : ∑' (p : ℤ × ℤ), ENNReal.ofReal (annFam m h p) = ∑' (j : { j : ℤ // j ≤ m }) (n : { n : ℤ // n ≤ ↑j - 1 }), ENNReal.ofReal (h ↑j ↑n)

The guarded annular family as the iterated subtype sum. The ℤ × ℤ sum of ENNReal.ofReal ∘ Resum.annFam is the iterated Σ_{j ≤ m} Σ_{n ≤ j−1} in which 𝒢₂ is written.

theorem Algsuperdiff.Section4.Provider.Annular.summable_annFam_of_ennreal_ne_top {m : ℤ} {h : ℤ → ℤ → ℝ} (hh0 : ∀ (j n : ℤ), 0 ≤ h j n) (hfin : ∑' (j : { j : ℤ // j ≤ m }) (n : { n : ℤ // n ≤ ↑j - 1 }), ENNReal.ofReal (h ↑j ↑n) ≠ ⊤) : Summable (annFam m h)

The [0,infinity] finiteness criterion for the guarded annular family.

Part B -- the two 𝒢₁ readings

noncomputable def Algsuperdiff.Section4.Provider.Annular.gradTailFam {d : ℕ} (M : Section3.ABKModel d) (m : ℤ) (omega : Section3.Cutoff.CutoffSample d) (k : { k : ℤ // m ≤ k }) : ℝ

The k >= m shell-tail family of the G_1^a content.

Equations

• Algsuperdiff.Section4.Provider.Annular.gradTailFam M m omega k = 3 ^ ((2 - M.gamma) * ↑m) * Algsuperdiff.Section4.Support.shellW1InfGradNorm m (↑omega ↑k)

theorem Algsuperdiff.Section4.Provider.Annular.summable_gradTail_of_eventG1 {d : ℕ} (M : Section3.ABKModel d) (m : ℤ) {s T : ℝ} {omega : Section3.Cutoff.CutoffSample d} (homega : omega ∈ Support.eventG1 M m s T) : Summable fun (k : { k : ℤ // m ≤ k }) => 3 ^ ((2 - M.gamma) * ↑m) * Support.shellW1InfGradNorm m (↑omega ↑k)

The 𝒢₁ᵃ reading, summability half. On 𝒢₁ the k ≥ m shell tail is a genuine convergent series, so the real tsum inside gradTailSq is not the junk value.

theorem Algsuperdiff.Section4.Provider.Annular.tsum_gradTail_le_of_eventG1 {d : ℕ} (M : Section3.ABKModel d) (m : ℤ) {s T : ℝ} (hT : 0 ≤ T) {omega : Section3.Cutoff.CutoffSample d} (homega : omega ∈ Support.eventG1 M m s T) : ∑' (k : { k : ℤ // m ≤ k }), 3 ^ ((2 - M.gamma) * ↑m) * Support.shellW1InfGradNorm m (↑omega ↑k) ≤ T

The 𝒢₁ᵃ reading, value half.

The 𝒢₁ᵇ reading at the pinned shell family

theorem Algsuperdiff.Section4.Provider.Annular.summable_shellQuarter_of_eventG1 {d : ℕ} (M : Section3.ABKModel d) (m : ℤ) {s T : ℝ} {omega : Section3.Cutoff.CutoffSample d} (homega : omega ∈ Support.eventG1 M m s T) : Summable fun (v : ℕ) => 3 ^ (-(s / 4) * ↑v) * shellBlockLatticeReal M m omega (m - ↑v) ^ 2

The 𝒢₁ᵇ reading, summability half, at the A5b-pinned shell family.

theorem Algsuperdiff.Section4.Provider.Annular.tsum_shellQuarter_le_of_eventG1 {d : ℕ} (M : Section3.ABKModel d) (m : ℤ) {s T : ℝ} (hT : 0 ≤ T) {omega : Section3.Cutoff.CutoffSample d} (homega : omega ∈ Support.eventG1 M m s T) : ∑' (v : ℕ), 3 ^ (-(s / 4) * ↑v) * shellBlockLatticeReal M m omega (m - ↑v) ^ 2 ≤ T ^ 2

The 𝒢₁ᵇ reading, value half.

theorem Algsuperdiff.Section4.Provider.Annular.summable_shellBlockLatticeReal_of_eventG1 {d : ℕ} (M : Section3.ABKModel d) (m : ℤ) {s T : ℝ} (hs0 : 0 ≤ s) {omega : Section3.Cutoff.CutoffSample d} (homega : omega ∈ Support.eventG1 M m s T) : Summable fun (v : ℕ) => 3 ^ (-(s / 2) * ↑v) * shellBlockLatticeReal M m omega (m - ↑v) ^ 2

The hAsum binder of ClauseOne.clauseOne_bound, at the A5b-pinned family: the display weight 3^{−(s/2)v} is below the event weight 3^{−(s/4)v}.

theorem Algsuperdiff.Section4.Provider.Annular.shellPartialSum_le_of_eventG1 {d : ℕ} (M : Section3.ABKModel d) (m : ℤ) {s T : ℝ} (hs0 : 0 ≤ s) (hT : 0 ≤ T) {omega : Section3.Cutoff.CutoffSample d} (homega : omega ∈ Support.eventG1 M m s T) (n : ℤ) (hnm : n ≤ m) : ∑ v ∈ Finset.range ((m - n).toNat + 2), shellBlockLatticeReal M m omega (m - ↑v) ^ 2 ≤ 3 ^ (s / 4) * T ^ 2 * 3 ^ (s / 4 * ↑(m - n))

The partial-sum budget feeding AssemblyFeed.summable_annFam_grad and AssemblyFeed.summable_annFam_l2: the head block of the shell family is at most 3^{s/4} T² times the honest weight 3^{(s/4)(m−n)}.

Part D -- the two budget-family summabilities at the pinned carriers

theorem Algsuperdiff.Section4.Provider.Annular.summable_annFam_annularGradBlock_of_eventG1 {d : ℕ} (M : Section3.ABKModel d) (m : ℤ) {s T : ℝ} (hs0 : 0 < s) (hs1 : s ≤ 1) (hT : 0 ≤ T) {omega : Section3.Cutoff.CutoffSample d} (homega : omega ∈ Support.eventG1 M m s T) : Summable (annFam m fun (j n : ℤ) => 3 ^ (-(s * ↑(m - n))) * annularGradBlock M m omega j n)

The hsumG binder at the A2b head-block gradient family. Composition of EventBudgets.annularGradBlock_le (the hcsGn slot at Kgn = 81) with the 𝒢₁ partial-sum budget.

theorem Algsuperdiff.Section4.Provider.Annular.summable_annFam_annularL2Block_of_eventG1 {d : ℕ} (M : Section3.ABKModel d) (m : ℤ) {s T : ℝ} (hs0 : 0 < s) (hs1 : s ≤ 1) (hsg : 8 * M.gamma ≤ s) (hT : 0 ≤ T) {omega : Section3.Cutoff.CutoffSample d} (homega : omega ∈ Support.eventG1 M m s T) : Summable (annFam m fun (j n : ℤ) => 3 ^ (-(s * ↑(m - n))) * annularL2Block M m omega j n)

The hsumL binder at the A2b head-block value family. Composition of EventBudgets.annularL2Block_le (the hcsL2 slot at Kl2 = 1) with the same budget; the extra 3^{2γ(m−n)} is absorbed by 8γ ≤ s.