Resum

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

The annular resummation of the Section 4.1 chain

Local helpers for ABK26, Section 4.1, proof of Proposition p.mathcalE.annular.decomp: the step the manuscript compresses into one sentence, summing the five-term "ugly" estimate over the annular double sum sum_{j <= m} sum_{n <= j-1} and composing the result with the Step-1 estimate.

Everything here is a proved conditional helper over abstract reals and abstract real sequences. The caller-supplied inequalities (the ugly estimate, the Step-1 estimate, the four summability facts, the essential-sup prefactor) are conditional A obligations, not source premises; no source node is claimed, realized or closed by this module.

Contents

• annFam / annDouble -- the guarded annular family over Z x Z and the guarded iterated double sum sum_{j <= m} sum_{n <= j-1}, with the bridge tsum_annFam. Termwise comparisons live in the product reading; the iterated reading is what the Section 4.1 displays speak.
• weight_collapse_one / weight_collapse_two -- the two scale-weight collapses 3^(-2sq) 3^(sq) = 3^(-sq) and 3^(-2sq) 3^((s+gamma)q) = 3^(-(s-gamma)q).
• half_le_one_sub_threeRpow_neg -- the elementary convexity input 1 - 3^(-x) >= x/2 on (0,1], behind every c^(-1) geometric constant.
• annWeightFam_tsum_le -- the annulus-multiplicity weight sum sum_{j <= m} sum_{n <= j-1} 3^(-c(m-n)) <= 4 c^(-2): for each scale n there are m - n annuli, so this double geometric sum is a polynomial-times-geometric quantity, and its c^(-2) blow-up is the origin of the s^(-2) prefactor of the fifth pre.zero term.
• annularResum_core / annularResum -- the resummation, over abstract weights and then at the manuscript's weights.
• IsAnnularDecompPre -- a local abbreviation for the Step-1 shape.
• preZero_of_pre_and_ugly -- the composition delivering the five-term pre.zero shape.

The annulus multiplicity

Plugging the ugly estimate into the annular double sum costs a factor m - n -- the number of annuli j in [n+1, m] -- on every term whose content does not depend on the annulus index j. The manuscript carries this multiplicity explicitly in the two Step-3 displays (: the factors m-n+1 and (m-n+1)^2) and its fifth pre.zero term is stated with the compatible prefactor, but its second (sigma-bar continuity) term is printed as a single sum, without the multiplicity. Nothing downstream breaks: the Step-3 consumer takes the sigma-bar sum with a free constant Csig, and the multiplicity costs one extra power of (s - 2 gamma)^(-1).

The guarded annular family and double sum

def Algsuperdiff.Section4.Provider.Annular.annFam (m : ℤ) (h : ℤ → ℤ → ℝ) : ℤ × ℤ → ℝ

The guarded annular family over Z x Z: supported on {(j,n) : j <= m, n <= j-1}, the index region of every Section 4.1 annular double sum.

Equations

• Algsuperdiff.Section4.Provider.Annular.annFam m h p = if p.1 ≤ m ∧ p.2 ≤ p.1 - 1 then h p.1 p.2 else 0

@[simp]

theorem Algsuperdiff.Section4.Provider.Annular.annFam_apply (m : ℤ) (h : ℤ → ℤ → ℝ) (j n : ℤ) : annFam m h (j, n) = if j ≤ m ∧ n ≤ j - 1 then h j n else 0

noncomputable def Algsuperdiff.Section4.Provider.Annular.annDouble (m : ℤ) (h : ℤ → ℤ → ℝ) : ℝ

The guarded annular double sum sum_{j <= m} sum_{n <= j-1} h j n.

Equations

• Algsuperdiff.Section4.Provider.Annular.annDouble m h = ∑' (j : ℤ), if j ≤ m then ∑' (n : ℤ), if n ≤ j - 1 then h j n else 0 else 0

theorem Algsuperdiff.Section4.Provider.Annular.annDouble_def (m : ℤ) (h : ℤ → ℤ → ℝ) : annDouble m h = ∑' (j : ℤ), if j ≤ m then ∑' (n : ℤ), if n ≤ j - 1 then h j n else 0 else 0

theorem Algsuperdiff.Section4.Provider.Annular.annFam_nonneg {m : ℤ} {h : ℤ → ℤ → ℝ} (hh : ∀ (j n : ℤ), 0 ≤ h j n) (p : ℤ × ℤ) : 0 ≤ annFam m h p

theorem Algsuperdiff.Section4.Provider.Annular.annDouble_nonneg {m : ℤ} {h : ℤ → ℤ → ℝ} (hh : ∀ (j n : ℤ), 0 ≤ h j n) : 0 ≤ annDouble m h

theorem Algsuperdiff.Section4.Provider.Annular.tsum_annFam {m : ℤ} {h : ℤ → ℤ → ℝ} (hs : Summable (annFam m h)) : ∑' (p : ℤ × ℤ), annFam m h p = annDouble m h

The product-to-iterated bridge. For a summable guarded annular family the Z x Z sum is the iterated double sum.

The two scale-weight collapses

theorem Algsuperdiff.Section4.Provider.Annular.weight_collapse_one (s q : ℝ) : 3 ^ (-(2 * s * q)) * 3 ^ (s * q) = 3 ^ (-(s * q))

3^(-2sq) * 3^(sq) = 3^(-sq) -- the weight collapse of the first four pre.zero terms: the ugly estimate's growth factor eats one of the two s-powers of the Step-1 weight.

theorem Algsuperdiff.Section4.Provider.Annular.weight_collapse_two (s gamma q : ℝ) : 3 ^ (-(2 * s * q)) * 3 ^ ((s + gamma) * q) = 3 ^ (-((s - gamma) * q))

3^(-2sq) * 3^((s+gamma)q) = 3^(-(s-gamma)q) -- the weight collapse of the fifth pre.zero term.

The elementary convexity input

theorem Algsuperdiff.Section4.Provider.Annular.half_le_one_sub_threeRpow_neg {x : ℝ} (hx0 : 0 < x) (hx1 : x ≤ 1) : x / 2 ≤ 1 - 3 ^ (-x)

1 - 3^(-x) >= x/2 for x in (0,1]. From exp y >= 1 + y one gets 3^(-x) <= (1 + x log 3)^(-1), and x log 3 / (1 + x log 3) >= x / 2 reduces to log 3 >= 1. This is the linear lower bound behind every c^(-1) and c^(-2) geometric constant of the Section 4.1 sums.

The annulus-multiplicity weight sum

noncomputable def Algsuperdiff.Section4.Provider.Annular.annWeightFam (c : ℝ) (m : ℤ) : ℤ × ℤ → ℝ

The fifth pre.zero term's weight family: the guarded annular family of the pure weight 3^(-c(m-n)). Summing it over the annular region counts, for each scale n, the m - n annuli j in [n+1, m].

Equations

• Algsuperdiff.Section4.Provider.Annular.annWeightFam c m = Algsuperdiff.Section4.Provider.Annular.annFam m fun (x n : ℤ) => 3 ^ (-(c * ↑(m - n)))

theorem Algsuperdiff.Section4.Provider.Annular.annWeightFam_def (c : ℝ) (m : ℤ) : annWeightFam c m = annFam m fun (x n : ℤ) => 3 ^ (-(c * ↑(m - n)))

def Algsuperdiff.Section4.Provider.Annular.annIdx (m : ℤ) : ℕ × ℕ → ℤ × ℤ

The transport of the guarded annular region to N x N.

Equations

• Algsuperdiff.Section4.Provider.Annular.annIdx m ab = (m - ↑ab.1, m - ↑ab.1 - 1 - ↑ab.2)

theorem Algsuperdiff.Section4.Provider.Annular.annWeightFam_summable {c : ℝ} (hc : 0 < c) (m : ℤ) : Summable (annWeightFam c m)

The annulus-multiplicity weight sum is summable.

theorem Algsuperdiff.Section4.Provider.Annular.annWeightFam_tsum_le {c : ℝ} (hc0 : 0 < c) (hc1 : c ≤ 1) (m : ℤ) : ∑' (p : ℤ × ℤ), annWeightFam c m p ≤ 4 / c ^ 2

The annulus-multiplicity weight sum. For c in (0,1],

sum_{j <= m} sum_{n <= j-1} 3^(-c(m-n)) = 3^(-c) (1 - 3^(-c))^(-2) <= 4 c^(-2) .

The double sum counts the m - n annuli at each scale; the bound uses the linear lower bound 1 - 3^(-c) >= c/2.

A five-way termwise comparison of infinite sums

theorem Algsuperdiff.Section4.Provider.Annular.tsum_le_five {iota : Type u_1} {f g₁ g₂ g₃ g₄ g₅ : iota → ℝ} (hf0 : ∀ (i : iota), 0 ≤ f i) (hle : ∀ (i : iota), f i ≤ g₁ i + g₂ i + g₃ i + g₄ i + g₅ i) (h₁ : Summable g₁) (h₂ : Summable g₂) (h₃ : Summable g₃) (h₄ : Summable g₄) (h₅ : Summable g₅) : ∑' (i : iota), f i ≤ ∑' (i : iota), g₁ i + ∑' (i : iota), g₂ i + ∑' (i : iota), g₃ i + ∑' (i : iota), g₄ i + ∑' (i : iota), g₅ i

Five-way termwise domination of infinite sums. A nonnegative family dominated termwise by the sum of five summable families has its sum dominated by the sum of their five sums.

theorem Algsuperdiff.Section4.Provider.Annular.summable_of_le_five {iota : Type u_1} {f g₁ g₂ g₃ g₄ g₅ : iota → ℝ} (hf0 : ∀ (i : iota), 0 ≤ f i) (hle : ∀ (i : iota), f i ≤ g₁ i + g₂ i + g₃ i + g₄ i + g₅ i) (h₁ : Summable g₁) (h₂ : Summable g₂) (h₃ : Summable g₃) (h₄ : Summable g₄) (h₅ : Summable g₅) : Summable f

Summability of a family dominated termwise by five summable families.

The resummation

theorem Algsuperdiff.Section4.Provider.Annular.annularResum_core {cstar gamma C₂ gradM Wsum : ℝ} {m : ℤ} {w2 W Wg v vg : ℤ → ℝ} {Jann E2 L2f gradNf : ℤ → ℤ → ℝ} {sig : ℤ → ℝ} (hw20 : ∀ (n : ℤ), 0 ≤ w2 n) (hb0 : 0 ≤ C₂ * cstar⁻¹ * gamma) (hgradM : 0 ≤ gradM) (hcol1 : ∀ (n : ℤ), w2 n * W n = v n) (hcol2 : ∀ (n : ℤ), w2 n * Wg n = vg n) (hJann0 : ∀ (j n : ℤ), 0 ≤ Jann j n) (hugly : ∀ (j n : ℤ), j ≤ m → n ≤ j - 1 → Jann j n ≤ C₂ * W n * E2 j n + C₂ * W n * sig n + C₂ * cstar⁻¹ * gamma * W n * L2f j n + C₂ * cstar⁻¹ * gamma * W n * gradNf j n + C₂ * cstar⁻¹ * gamma * Wg n * gradM) (hsumE : Summable (annFam m fun (j n : ℤ) => v n * E2 j n)) (hsumS : Summable (annFam m fun (x n : ℤ) => v n * sig n)) (hsumL : Summable (annFam m fun (j n : ℤ) => v n * L2f j n)) (hsumG : Summable (annFam m fun (j n : ℤ) => v n * gradNf j n)) (hsumW : Summable (annFam m fun (x n : ℤ) => vg n)) (hWsum : ∑' (p : ℤ × ℤ), annFam m (fun (x n : ℤ) => vg n) p ≤ Wsum) : (annDouble m fun (j n : ℤ) => w2 n * Jann j n) ≤ ((((C₂ * annDouble m fun (j n : ℤ) => v n * E2 j n) + C₂ * annDouble m fun (x n : ℤ) => v n * sig n) + C₂ * cstar⁻¹ * gamma * annDouble m fun (j n : ℤ) => v n * L2f j n) + C₂ * cstar⁻¹ * gamma * annDouble m fun (j n : ℤ) => v n * gradNf j n) + C₂ * cstar⁻¹ * gamma * Wsum * gradM

The resummation, abstract-weight core.

Summing the five-term ugly estimate over the guarded annular double sum produces the five pre.zero terms: the first four keep their (j,n)-dependent contents at the collapsed weight v = w2 * W, and the fifth, whose content gradM is (j,n)-independent, is resummed against the weight sum of vg = w2 * Wg over the whole annular region.

Stated over abstract weights so that no Real.rpow term is entered by a numeric tactic; annularResum instantiates them at the manuscript's weights.

theorem Algsuperdiff.Section4.Provider.Annular.annularResum {s gamma cstar C₂ gradM : ℝ} {m : ℤ} {Jann E2 L2f gradNf : ℤ → ℤ → ℝ} {sig : ℤ → ℝ} (hs0 : 0 < s) (hs1 : s ≤ 1) (hgamma0 : 0 ≤ gamma) (hsg : 8 * gamma ≤ s) (hcstar : 0 < cstar) (hC₂ : 0 ≤ C₂) (hgradM : 0 ≤ gradM) (hJann0 : ∀ (j n : ℤ), 0 ≤ Jann j n) (hugly : ∀ (j n : ℤ), j ≤ m → n ≤ j - 1 → Jann j n ≤ C₂ * 3 ^ (s * ↑(m - n)) * E2 j n + C₂ * 3 ^ (s * ↑(m - n)) * sig n + C₂ * cstar⁻¹ * gamma * 3 ^ (s * ↑(m - n)) * L2f j n + C₂ * cstar⁻¹ * gamma * 3 ^ (s * ↑(m - n)) * gradNf j n + C₂ * cstar⁻¹ * gamma * 3 ^ ((s + gamma) * ↑(m - n)) * gradM) (hsumE : Summable (annFam m fun (j n : ℤ) => 3 ^ (-(s * ↑(m - n))) * E2 j n)) (hsumS : Summable (annFam m fun (x n : ℤ) => 3 ^ (-(s * ↑(m - n))) * sig n)) (hsumL : Summable (annFam m fun (j n : ℤ) => 3 ^ (-(s * ↑(m - n))) * L2f j n)) (hsumG : Summable (annFam m fun (j n : ℤ) => 3 ^ (-(s * ↑(m - n))) * gradNf j n)) : (annDouble m fun (j n : ℤ) => 3 ^ (-(2 * s * ↑(m - n))) * Jann j n) ≤ ((((C₂ * annDouble m fun (j n : ℤ) => 3 ^ (-(s * ↑(m - n))) * E2 j n) + C₂ * annDouble m fun (x n : ℤ) => 3 ^ (-(s * ↑(m - n))) * sig n) + C₂ * cstar⁻¹ * gamma * annDouble m fun (j n : ℤ) => 3 ^ (-(s * ↑(m - n))) * L2f j n) + C₂ * cstar⁻¹ * gamma * annDouble m fun (j n : ℤ) => 3 ^ (-(s * ↑(m - n))) * gradNf j n) + C₂ * cstar⁻¹ * gamma * (6 * (s ^ 2)⁻¹) * gradM

The resummation at the manuscript's weights.

The instantiation of annularResum_core at w2 n = 3^(-2s(m-n)), W n = 3^(s(m-n)), Wg n = 3^((s+gamma)(m-n)), with the fifth term's weight sum bounded by 6 s^(-2) (the multiplicity sum at c = s - gamma >= 7s/8, using the standing hypothesis s >= 8 gamma).

The sigma-bar continuity term is produced as a double sum: it inherits the annulus multiplicity that the printed pre.zero display omits (see the module docstring).

The Step-1 shape and the pre.zero composition

def Algsuperdiff.Section4.Provider.Annular.IsAnnularDecompPre (s : ℝ) (m : ℤ) (Jgrid : ℤ → ℝ) (Jann : ℤ → ℤ → ℝ) (C : ℝ) : Prop

A local abbreviation for the Step-1 shape: the full-grid weighted sum is controlled by the annular double sum,

sum_{n <= m} 3^(-2s(m-n)) Jgrid n
  <= C sum_{j <= m} sum_{n <= j-1} 3^(-2s(m-n)) Jann j n .

This is a naming convenience inside this provider module. It is not a source-facing declaration and closes no node.

Equations

• One or more equations did not get rendered due to their size.

theorem Algsuperdiff.Section4.Provider.Annular.preZero_of_pre_and_ugly {s gamma cstar Cess C₁ C₂ C gradM Ecal2 : ℝ} {m : ℤ} {Jgrid : ℤ → ℝ} {Jann E2 L2f gradNf : ℤ → ℤ → ℝ} {sig : ℤ → ℝ} (hs0 : 0 < s) (hs1 : s ≤ 1) (hgamma0 : 0 ≤ gamma) (hsg : 8 * gamma ≤ s) (hcstar : 0 < cstar) (hCess : 0 ≤ Cess) (hC₁ : 0 ≤ C₁) (hC₂ : 0 ≤ C₂) (hgradM : 0 ≤ gradM) (hJann0 : ∀ (j n : ℤ), 0 ≤ Jann j n) (hE0 : ∀ (j n : ℤ), 0 ≤ E2 j n) (hsig0 : ∀ (n : ℤ), 0 ≤ sig n) (hL20 : ∀ (j n : ℤ), 0 ≤ L2f j n) (hgrad0 : ∀ (j n : ℤ), 0 ≤ gradNf j n) (hess : Ecal2 ≤ Cess * s * ∑' (n : ℤ), if n ≤ m then 3 ^ (-(2 * s * ↑(m - n))) * Jgrid n else 0) (hpreA : IsAnnularDecompPre s m Jgrid Jann C₁) (hugly : ∀ (j n : ℤ), j ≤ m → n ≤ j - 1 → Jann j n ≤ C₂ * 3 ^ (s * ↑(m - n)) * E2 j n + C₂ * 3 ^ (s * ↑(m - n)) * sig n + C₂ * cstar⁻¹ * gamma * 3 ^ (s * ↑(m - n)) * L2f j n + C₂ * cstar⁻¹ * gamma * 3 ^ (s * ↑(m - n)) * gradNf j n + C₂ * cstar⁻¹ * gamma * 3 ^ ((s + gamma) * ↑(m - n)) * gradM) (hsumE : Summable (annFam m fun (j n : ℤ) => 3 ^ (-(s * ↑(m - n))) * E2 j n)) (hsumS : Summable (annFam m fun (x n : ℤ) => 3 ^ (-(s * ↑(m - n))) * sig n)) (hsumL : Summable (annFam m fun (j n : ℤ) => 3 ^ (-(s * ↑(m - n))) * L2f j n)) (hsumG : Summable (annFam m fun (j n : ℤ) => 3 ^ (-(s * ↑(m - n))) * gradNf j n)) (hCge : 6 * Cess * C₁ * C₂ ≤ C) : Ecal2 ≤ ((((C * s * annDouble m fun (j n : ℤ) => 3 ^ (-(s * ↑(m - n))) * E2 j n) + C * s * annDouble m fun (x n : ℤ) => 3 ^ (-(s * ↑(m - n))) * sig n) + C * cstar⁻¹ * gamma * s * annDouble m fun (j n : ℤ) => 3 ^ (-(s * ↑(m - n))) * L2f j n) + C * cstar⁻¹ * gamma * s * annDouble m fun (j n : ℤ) => 3 ^ (-(s * ↑(m - n))) * gradNf j n) + C * cstar⁻¹ * (s ^ 2)⁻¹ * gamma * gradM

The five-term pre.zero shape, from Step 1 and the ugly estimate.

Composition of three caller-supplied layers:

• hess -- the essential-sup prefactor bound: Ecal2 is bounded by Cess * s times the full-grid weighted sum;
• hpreA -- the Step-1 shape;
• hugly with the four summability facts -- the ugly estimate, resummed by annularResum.

The output is the shape the Step-3 regrouping consumes. Every hypothesis is a conditional A obligation on the caller.