GeometricResummation

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

Descendant resummation in the corrected 3/8 coarse gauge

This module proves the geometric resummation over triadic descendants that underlies the Lambda_{s,2} sensitivity estimate. The source mechanism is the display in ABK26: the weighted descendant sum of the per-cube lower coarse-grained ellipticity inverses is bounded by a multiple of the global lower coarse-grained ellipticity inverse, by a sum interchange plus a geometric series, producing a pole constant.

q = 2 series formulas

theorem Algsuperdiff.Section24.Sensitivity.Provider.Multiscale.summable_weighted_maxDescendantSigmaStarInv_two {d : ℕ} [NeZero d] (Q : HCPolySupport.TriadicCube d) (A : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) {s : ℝ} (hs : 0 < s) : Summable fun (n : ℕ) => HCPolySupport.Book.Ch02.geometricWeight s 2 n * HCPolySupport.Book.Ch02.maxDescendantSigmaStarInvMatrixNormAtScale Q (Q.scale - ↑n) A

Summability of the weighted sigma_*^{-1} descendant maxima at q = 2.

theorem Algsuperdiff.Section24.Sensitivity.Provider.Multiscale.summable_weighted_maxDescendantB_two {d : ℕ} [NeZero d] (Q : HCPolySupport.TriadicCube d) (A : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) {s : ℝ} (hs : 0 < s) : Summable fun (n : ℕ) => HCPolySupport.Book.Ch02.geometricWeight s 2 n * HCPolySupport.Book.Ch02.maxDescendantBMatrixNormAtScale Q (Q.scale - ↑n) A

Summability of the weighted b descendant maxima at q = 2.

theorem Algsuperdiff.Section24.Sensitivity.Provider.Multiscale.lambdaSq_two_inv_eq_tsum {d : ℕ} (Q : HCPolySupport.TriadicCube d) (A : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) {s : ℝ} (hs : 0 < s) : (HCPolySupport.Book.Ch02.lambdaSq Q s (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) A)⁻¹ = ∑' (n : ℕ), HCPolySupport.Book.Ch02.geometricWeight s 2 n * HCPolySupport.Book.Ch02.maxDescendantSigmaStarInvMatrixNormAtScale Q (Q.scale - ↑n) A

The literal q = 2 series formula for lambda_{s,2}^{-1}.

theorem Algsuperdiff.Section24.Sensitivity.Provider.Multiscale.LambdaSq_two_eq_tsum {d : ℕ} (Q : HCPolySupport.TriadicCube d) (A : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) {s : ℝ} (hs : 0 < s) : HCPolySupport.Book.Ch02.LambdaSq Q s (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) A = ∑' (n : ℕ), HCPolySupport.Book.Ch02.geometricWeight s 2 n * HCPolySupport.Book.Ch02.maxDescendantBMatrixNormAtScale Q (Q.scale - ↑n) A

The literal q = 2 series formula for Lambda_{s,2}.

The corrected geometric kernel

theorem Algsuperdiff.Section24.Sensitivity.Provider.Multiscale.rpow_three_two_mul_sub_lt_one {s : ℝ} (hs : s < 3 / 8) : Real.rpow 3 (2 * s - 3 / 4) < 1

The corrected kernel ratio 3^{2s-3/4} is < 1 exactly on s < 3/8.

theorem Algsuperdiff.Section24.Sensitivity.Provider.Multiscale.tsum_geometric_threeEighths_le_pole {s : ℝ} (hs0 : 0 < s) (hs : s < 3 / 8) : ∑' (j : ℕ), Real.rpow 3 (2 * s - 3 / 4) ^ j ≤ (3 / 8 - s)⁻¹

The corrected geometric series bound. This is the exact place where the admissible range tightens from the printed s < 1/2 to s < 3/8, and where the pole (3/8-s)^{-1} appears.

The triangular reindexing

The nonnegative-series reindexing below is not an assumed Fubini step: the map (n,j) ↦ (n+j, j) is an injection of ℕ × ℕ into itself, so the monotone comparison for injections applies directly.

theorem Algsuperdiff.Section24.Sensitivity.Provider.Multiscale.tsum_shifted_product_le (F r : ℕ → ℝ) (hF0 : ∀ (n : ℕ), 0 ≤ F n) (hr0 : ∀ (j : ℕ), 0 ≤ r j) (hF : Summable F) (hr : Summable r) : ∑' (n : ℕ) (j : ℕ), F (n + j) * r j ≤ (∑' (n : ℕ), F n) * ∑' (j : ℕ), r j

Triangular reindexing bound for nonnegative series.

theorem Algsuperdiff.Section24.Sensitivity.Provider.Multiscale.summable_tsum_shifted_product (F r : ℕ → ℝ) (hF0 : ∀ (n : ℕ), 0 ≤ F n) (hr0 : ∀ (j : ℕ), 0 ≤ r j) (hF : Summable F) (hr : Summable r) : Summable fun (n : ℕ) => ∑' (j : ℕ), F (n + j) * r j

Summability of the outer triangular series.

The descendant expansion in the 3/8 gauge

theorem Algsuperdiff.Section24.Sensitivity.Provider.Multiscale.maxDescendantLowerEllipticityInv_threeEighths_le_nested_tsum {d : ℕ} [NeZero d] (Q : HCPolySupport.TriadicCube d) (A : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) (n : ℕ) : HCPolySupport.Book.Ch02.maxDescendantLowerEllipticityInvAtScale Q (Q.scale - ↑n) (3 / 8) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) A ≤ ∑' (j : ℕ), HCPolySupport.Book.Ch02.geometricWeight (3 / 8) 2 j * HCPolySupport.Book.Ch02.maxDescendantSigmaStarInvMatrixNormAtScale Q (Q.scale - ↑(n + j)) A

The inverse lower ellipticity of every depth-n descendant has the literal q = 2 expansion over its own descendants; transitivity of triadic descendants embeds those terms at global depth n + j. This is the structural (non-numerical) half of the double resummation.

The main resummation

theorem Algsuperdiff.Section24.Sensitivity.Provider.Multiscale.tsum_weighted_maxDescendantLowerEllipticityInv_threeEighths_le {d : ℕ} [NeZero d] (Q : HCPolySupport.TriadicCube d) (A : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) {s : ℝ} (hs0 : 0 < s) (hs : s < 3 / 8) : ∑' (n : ℕ), HCPolySupport.Book.Ch02.geometricWeight s 2 n * HCPolySupport.Book.Ch02.maxDescendantLowerEllipticityInvAtScale Q (Q.scale - ↑n) (3 / 8) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) A ≤ (3 / 8 - s)⁻¹ * (HCPolySupport.Book.Ch02.lambdaSq Q s (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) A)⁻¹

Descendant resummation in the corrected 3/8 gauge. The weighted descendant sum of the per-cube lower coarse-grained ellipticity inverses lambda_{3/8,2}^{-1}(z + cube_n; a) is bounded by the pole constant (3/8-s)^{-1} times the global lambda_{s,2}^{-1}(cube_0; a). This is the corrected form of the display in ABK26.

theorem Algsuperdiff.Section24.Sensitivity.Provider.Multiscale.summable_weighted_maxDescendantLowerEllipticityInv_threeEighths {d : ℕ} [NeZero d] (Q : HCPolySupport.TriadicCube d) (A : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) {s : ℝ} (hs0 : 0 < s) (hs : s < 3 / 8) : Summable fun (n : ℕ) => HCPolySupport.Book.Ch02.geometricWeight s 2 n * HCPolySupport.Book.Ch02.maxDescendantLowerEllipticityInvAtScale Q (Q.scale - ↑n) (3 / 8) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) A

Summability companion of tsum_weighted_maxDescendantLowerEllipticityInv_threeEighths_le.

The Lambda_{s,2} endpoint

theorem Algsuperdiff.Section24.Sensitivity.Provider.Multiscale.maxDescendantB_le_of_descendant_bound_coeff {d : ℕ} (Q : HCPolySupport.TriadicCube d) (A₀ A₁ : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) {K c : ℝ} (hK : 0 ≤ K) (hc : 0 ≤ c) (hdesc : ∀ (n : ℕ), ∀ R ∈ HCPolySupport.descendantsAtScale Q (Q.scale - ↑n), HCPolySupport.Book.Ch02.coarseBMatrixNorm R A₁ ≤ c * HCPolySupport.Book.Ch02.coarseBMatrixNorm R A₀ + K * (HCPolySupport.Book.Ch02.lambdaSq R (3 / 8) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) A₀)⁻¹) (n : ℕ) : HCPolySupport.Book.Ch02.maxDescendantBMatrixNormAtScale Q (Q.scale - ↑n) A₁ ≤ c * HCPolySupport.Book.Ch02.maxDescendantBMatrixNormAtScale Q (Q.scale - ↑n) A₀ + K * HCPolySupport.Book.Ch02.maxDescendantLowerEllipticityInvAtScale Q (Q.scale - ↑n) (3 / 8) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) A₀

Passage from a per-descendant one-cube estimate to the finite descendant maximum, with a general same-index coefficient c.

theorem Algsuperdiff.Section24.Sensitivity.Provider.Multiscale.LambdaSq_two_le_of_descendant_bound_coeff {d : ℕ} [NeZero d] (Q : HCPolySupport.TriadicCube d) (A₀ A₁ : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) {K c s : ℝ} (hK : 0 ≤ K) (hc : 0 ≤ c) (hs0 : 0 < s) (hs : s < 3 / 8) (hdesc : ∀ (n : ℕ), ∀ R ∈ HCPolySupport.descendantsAtScale Q (Q.scale - ↑n), HCPolySupport.Book.Ch02.coarseBMatrixNorm R A₁ ≤ c * HCPolySupport.Book.Ch02.coarseBMatrixNorm R A₀ + K * (HCPolySupport.Book.Ch02.lambdaSq R (3 / 8) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) A₀)⁻¹) : HCPolySupport.Book.Ch02.LambdaSq Q s (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) A₁ ≤ c * HCPolySupport.Book.Ch02.LambdaSq Q s (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) A₀ + K * (3 / 8 - s)⁻¹ * (HCPolySupport.Book.Ch02.lambdaSq Q s (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) A₀)⁻¹

The Lambda_{s,2} endpoint with a general same-index coefficient c. Its sole analytic input hdesc is the per-descendant one-cube estimate; the finite maxima, the nested descendant expansion, the triangular reindexing, and both q = 2 observable rewrites happen inside this proof.

theorem Algsuperdiff.Section24.Sensitivity.Provider.Multiscale.LambdaSq_two_le_of_descendant_bound {d : ℕ} [NeZero d] (Q : HCPolySupport.TriadicCube d) (A₀ A₁ : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) {K s : ℝ} (hK : 0 ≤ K) (hs0 : 0 < s) (hs : s < 3 / 8) (hdesc : ∀ (n : ℕ), ∀ R ∈ HCPolySupport.descendantsAtScale Q (Q.scale - ↑n), HCPolySupport.Book.Ch02.coarseBMatrixNorm R A₁ ≤ 4 * HCPolySupport.Book.Ch02.coarseBMatrixNorm R A₀ + K * (HCPolySupport.Book.Ch02.lambdaSq R (3 / 8) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) A₀)⁻¹) : HCPolySupport.Book.Ch02.LambdaSq Q s (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) A₁ ≤ 4 * HCPolySupport.Book.Ch02.LambdaSq Q s (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) A₀ + K * (3 / 8 - s)⁻¹ * (HCPolySupport.Book.Ch02.lambdaSq Q s (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) A₀)⁻¹

The Lambda_{s,2} endpoint of the corrected coarse-gauge argument. Its sole analytic input hdesc is the per-descendant one-cube estimate; the finite maxima, the nested descendant expansion, the triangular reindexing, and both q = 2 observable rewrites happen inside this proof. The 4 and the (3/8-s)^{-1} pole are exactly the constants appearing in the frozen bigLambda_sensitivity.