Documentation

LeanPool.Superdiffusion.Algsuperdiff.StochasticProcess.Common.Regularity.Ported.DyadicRadii

DyadicRadii #

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

Radius arithmetic for the small-contrast iteration #

source
noncomputable def Algsuperdiff.StochasticProcess.Common.Regularity.Ported.smallContrastDyadicRadius (R : ℝ) (n : ℕ) :
ℝ

The dyadic radius R 2^{-n}.

Equations
Instances For
    source
    theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.smallContrastDyadicRadius_zero (R : ℝ) :
    smallContrastDyadicRadius R 0 = R
    source
    theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.smallContrastDyadicRadius_pos {R : ℝ} (hR : 0 < R) (n : ℕ) :
    0 < smallContrastDyadicRadius R n
    source
    theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.smallContrastDyadicRadius_succ (R : ℝ) (n : ℕ) :
    smallContrastDyadicRadius R (n + 1) = smallContrastDyadicRadius R n / 2
    source
    theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.smallContrastDyadicRadius_le {R : ℝ} (hR : 0 ≤ R) (n : ℕ) :
    smallContrastDyadicRadius R n ≤ R
    source
    theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.smallContrastDyadicRadius_succ_rpow {R alpha : ℝ} (hR : 0 ≤ R) (n : ℕ) :
    smallContrastDyadicRadius R (n + 1) ^ (1 - alpha) = (1 / 2) ^ (1 - alpha) * smallContrastDyadicRadius R n ^ (1 - alpha)

    Scale-weight factorization at one dyadic step.

    source
    theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.smallContrast_source_scale_cancel {d : ℕ} {alpha r : ℝ} (hd : 1 ≤ d) (halpha : alpha < 1) (hr : 0 < r) :
    r ^ (1 - alpha) * r ^ (-↑d / schauderSourceExponent d alpha) = 1

    Cancellation of the source scaling r^{1-alpha} r^{-d/p}.

    source
    theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.half_source_coefficient_le_dimension_only {d : ℕ} {alpha : ℝ} (halpha : alpha < 1) :
    2 * (1 / 2) ^ (-↑d / 2) * (1 / 2) ^ (1 - alpha) ≤ 2 * (1 / 2) ^ (-↑d / 2)

    On the exponent range [1/2,1), the half-scale source coefficient is bounded by a dimension-only quantity.