Documentation

LeanPool.Superdiffusion.Algsuperdiff.Section3.Provider.CoarseEllipticity.SuperposedFluxLowerLtTwoSeries

SuperposedFluxLowerLtTwoSeries #

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

Scale-series estimates below exponent two #

For 1 ≤ q < 2, the amplitude remains inside the q/2 power. This file retains the collar exponent exactly and bounds only the dimension-only and polynomial factors. The resulting statements are conditional Provider helpers and assert no source-node status.

source
noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.superposedFluxDepthAmpMaxConst (d : ℕ) :
ℝ

Uniform replacement of the dimension-only amplitude under powers in [1/2,1].

Equations
Instances For
    source
    theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.superposedFluxDepthAmpMaxConst_pos (d : ℕ) :
    0 < superposedFluxDepthAmpMaxConst d
    source
    noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.superposedFluxLtTwoSeriesConst (d : ℕ) :
    ℝ

    Fixed prefactor in the subquadratic amplitude series.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.superposedFluxLtTwoSeriesConst_pos (d : ℕ) :
      0 < superposedFluxLtTwoSeriesConst d
      source
      noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.superposedFluxLtTwoBudgetConst (d : ℕ) :
      ℝ

      Fixed prefactor in the subquadratic final Orlicz budget.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.superposedFluxLtTwoBudgetConst_pos (d : ℕ) :
        0 < superposedFluxLtTwoBudgetConst d
        source
        theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.summable_geometricWeight_mul_depthAmp_rpow_lt_two {d : ℕ} (hd : 2 ≤ d) (M : ABKModel d) (E : ℝ) {s q : ℝ} (hs : 0 < s) (hqOne : 1 ≤ q) (hqTwo : q < 2) (hgap : 0 < 2 * s - M.gamma) :
        Summable fun (n : ℕ) => HCPolySupport.Book.Ch02.geometricWeight s q n * superposedFluxDepthAmpProfile M E n ^ (q / 2)
        source
        theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.tsum_geometricWeight_mul_depthAmp_rpow_lt_two_le {d : ℕ} (hd : 2 ≤ d) (M : ABKModel d) (E : ℝ) {s q rare : ℝ} (hs : 0 < s) (hsOne : s ≤ 1) (hqOne : 1 ≤ q) (hqTwo : q < 2) (hrare : 0 < rare) (hrareOne : rare ≤ 1) (hwindow : M.gamma / 2 + rare ≤ s) :
        ∑' (n : ℕ), HCPolySupport.Book.Ch02.geometricWeight s q n * superposedFluxDepthAmpProfile M E n ^ (q / 2) ≤ superposedFluxLtTwoSeriesConst d * Real.exp (-(superposedFluxBfaRate d / 2 * (E⁻¹ ^ 2 * M.gamma⁻¹))) * rare⁻¹ ^ 5