Documentation

LeanPool.Superdiffusion.Algsuperdiff.Section3.Provider.CoarseEllipticity.UpperSaturatedProfile

UpperSaturatedProfile #

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

Saturated finite-q upper-profile arithmetic #

This module studies the concrete depth profile

A * (n + 1) * min 1 (gamma * (n + 1)) * 3^(gamma n).

The saturation supplies the missing small-depth factor when 1 <= q <= 2. Splitting according to whether 2 * s - gamma is below or above gamma reduces the profile to a linear or quadratic polynomial times a geometric factor. Half of the positive gap absorbs that polynomial, and the exact normalized Book.Ch02.geometricWeight is retained throughout.

This is an internal conditional arithmetic helper.

source
noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.upperSaturatedProfile (A gamma : ℝ) (n : ℕ) :
ℝ

The saturated linear-times-geometric depth profile.

Equations
Instances For
    source
    theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.upperSaturatedProfile_nonneg {A gamma : ℝ} (hA : 0 ≤ A) (hgamma : 0 ≤ gamma) (n : ℕ) :
    0 ≤ upperSaturatedProfile A gamma n
    source
    theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.natCast_succ_le_inv_mul_three_rpow {rho : ℝ} (hrho : 0 < rho) (hrho2 : rho ≤ 2) (n : ℕ) :
    ↑n + 1 ≤ 6 * rho⁻¹ * 3 ^ (rho / 2 * ↑n)

    Half of a positive gap absorbs one linear depth factor. The constant is deliberately coarse and universal.

    source
    theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.upperSaturatedProfile_aggregate_le_of_one_le_of_le_two {A gamma s q : ℝ} (hA : 0 ≤ A) (hgamma : 0 ≤ gamma) (hs : 0 < s) (hs1 : s ≤ 1) (hq1 : 1 ≤ q) (hq2 : q ≤ 2) (hgap : 0 < 2 * s - gamma) :
    (∑' (n : ℕ), HCPolySupport.Book.Ch02.geometricWeight s q n * upperSaturatedProfile A gamma n ^ (q / 2)) ^ (2 / q) ≤ 3072 * A * s * gamma * (2 * s - gamma)⁻¹ ^ 3

    The exact normalized finite-q aggregate of the saturated profile has the cubic gap pole uniformly on 1 <= q <= 2.