Documentation

LeanPool.Superdiffusion.Algsuperdiff.Section3.Provider.CoarseEllipticity.SuperposedFluxLowerAmplitude

SuperposedFluxLowerAmplitude #

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

A uniform depth-amplitude majorant for the sharp lower lane #

This file replaces the exact grid-net amplitude of the pointwise representative by a single dimension-only prefactor times (n+1)^4 3^(gamma n) exp(-c E⁻² gamma⁻¹). It is the quantitative input shared by the finite q < 2, finite 2 ≤ q, and endpoint branches.

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

Uniform grid-net constant once the tail exponent is at least 1/4.

Equations
Instances For
    source
    theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.superposedFluxGridNetConst_pos {d : ℕ} (hd : 2 ≤ d) :
    0 < superposedFluxGridNetConst d
    source
    noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.superposedFluxDepthAmpConst (d : ℕ) :
    ℝ

    Dimension-only prefactor of the depth-amplitude majorant.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.superposedFluxDepthAmpConst_pos {d : ℕ} (hd : 2 ≤ d) :
      0 < superposedFluxDepthAmpConst d
      source
      noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.superposedFluxDepthAmpProfile {d : ℕ} (M : ABKModel d) (E : ℝ) (n : ℕ) :
      ℝ

      Uniform depth-amplitude majorant used by all lower exponent branches.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.superposedFluxDepthAmpProfile_pos {d : ℕ} (hd : 2 ≤ d) (M : ABKModel d) (E : ℝ) (n : ℕ) :
        0 < superposedFluxDepthAmpProfile M E n
        source
        theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.superposedFluxSharpDepthAmp_le_profile {d : ℕ} (hd : 2 ≤ d) (M : ABKModel d) (m : ℤ) (E : { E : ℝ // 1 ≤ E }) {sigma : ℝ} (hsigma : 0 < sigma) (hsigmaHalf : sigma ≤ 1 / 2) (hmax : max (Real.exp (profileAuxiliaryConst d / sigma)) (Disorder.cstar M)⁻¹ ≤ ↑E) (hEgamma : ↑E ≤ M.gamma ^ (-(1 / 5))) (n : ℕ) :
        superposedFluxSharpDepthAmp M m (↑E) sigma n.pred ≤ superposedFluxDepthAmpProfile M (↑E) n

        The exact representative amplitude is bounded by the uniform depth profile. Every scalar gate is discharged from the frozen max/fifth-root hypotheses.