Documentation

LeanPool.Superdiffusion.Algsuperdiff.Section3.Provider.CoarseEllipticity.FiniteQProfile

FiniteQProfile #

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

The finite-q deterministic profile #

This file isolates the geometric-series arithmetic in the lower coarse-ellipticity estimate of ABK26. The per-depth deterministic profile is C * 3^(gamma n). At every positive finite exponent q, its weighted ell^(q/2) aggregate is computed exactly and bounded by

C * (2 * s / (2 * s - gamma))^(2 / q).

For 2 <= q, the outer exponent is at most one and the base is at least one, so this is at most the printed first-order pole 2 * C * s * (2 * s - gamma)⁻¹. For q < 2, the exponent 2 / q cannot be dropped; this is the correction adopted in S33-CGLOWER-POLE-a/b. The q >= 2 specialization is the deterministic leg vindicated.

Main declarations #

source
noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.finiteQGeometricProfile (C gamma : ℝ) (n : ℕ) :
ℝ

The extremal deterministic profile from the lower multiscale input: C * 3^(gamma n) at depth n.

Equations
Instances For
    source
    theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.finiteQGeometricProfile_nonneg {C : ℝ} (hC : 0 ≤ C) (gamma : ℝ) (n : ℕ) :
    0 ≤ finiteQGeometricProfile C gamma n
    source
    noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.finiteQProfileRatio (s gamma q : ℝ) :
    ℝ

    The common ratio left after the collar 3^(gamma n) cancels part of the weight 3^(-s q n).

    Equations
    Instances For
      source
      theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.summable_geometricWeight_mul_finiteQGeometricProfile_rpow {s q gamma C : ℝ} (hC : 0 ≤ C) (hgap : 0 < 2 * s - gamma) (hq : 0 < q) :
      Summable fun (n : ℕ) => HCPolySupport.Book.Ch02.geometricWeight s q n * finiteQGeometricProfile C gamma n ^ (q / 2)

      The weighted q/2 powers of the deterministic profile form a summable geometric series whenever q > 0 and 2s - gamma > 0.

      source
      theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.tsum_geometricWeight_mul_finiteQGeometricProfile_rpow_eq {s q gamma C : ℝ} (hC : 0 ≤ C) (hgap : 0 < 2 * s - gamma) (hq : 0 < q) :
      ∑' (n : ℕ), HCPolySupport.Book.Ch02.geometricWeight s q n * finiteQGeometricProfile C gamma n ^ (q / 2) = HCPolySupport.Book.Ch02.geometricDiscount s q * C ^ (q / 2) * (1 - finiteQProfileRatio s gamma q)⁻¹

      Exact geometric-profile aggregation before the outer 2/q root.

      source
      theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.finiteQGeometricProfile_aggregate_eq {s q gamma C : ℝ} (hC : 0 ≤ C) (hs : 0 < s) (hq : 0 < q) (hgap : 0 < 2 * s - gamma) :
      (∑' (n : ℕ), HCPolySupport.Book.Ch02.geometricWeight s q n * finiteQGeometricProfile C gamma n ^ (q / 2)) ^ (2 / q) = C * (HCPolySupport.Book.Ch02.geometricDiscount s q * (1 - finiteQProfileRatio s gamma q)⁻¹) ^ (2 / q)

      Exact geometric-profile aggregation after the outer 2/q root.

      source
      theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.finiteQGeometricProfile_aggregate_le {s q gamma C : ℝ} (hC : 0 ≤ C) (hgamma : 0 ≤ gamma) (hs : 0 < s) (hq : 0 < q) (hgap : 0 < 2 * s - gamma) :
      (∑' (n : ℕ), HCPolySupport.Book.Ch02.geometricWeight s q n * finiteQGeometricProfile C gamma n ^ (q / 2)) ^ (2 / q) ≤ C * (2 * s / (2 * s - gamma)) ^ (2 / q)

      The corrected deterministic finite-q profile bound. Its pole order is 2/q, and the statement is valid for every q > 0.

      source
      theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.finiteQGeometricProfile_aggregate_le_of_two_le {s q gamma C : ℝ} (hC : 0 ≤ C) (hgamma : 0 ≤ gamma) (hs : 0 < s) (hq : 2 ≤ q) (hgap : 0 < 2 * s - gamma) :
      (∑' (n : ℕ), HCPolySupport.Book.Ch02.geometricWeight s q n * finiteQGeometricProfile C gamma n ^ (q / 2)) ^ (2 / q) ≤ 2 * C * s * (2 * s - gamma)⁻¹

      On the ruled range 2 <= q, the corrected positive-q profile reduces to the printed first-order pole, with the dimension-independent multiplier 2.