Documentation

LeanPool.Superdiffusion.Algsuperdiff.Section3.Disorder.Cstar

Cstar #

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

source
theorem Algsuperdiff.Section3.Disorder.existsUnique_cstar_raw (d : ℕ) (P : MeasureTheory.ProbabilityMeasure (ℤ → Frozen.Assumptions.ShellField d)) (hd : 2 ≤ d) (hJ1 : Frozen.Assumptions.ShellLawJ1 d P) (hJ2 : Frozen.Assumptions.ShellLawJ2 d P) (hJ4 : Frozen.Assumptions.ShellLawJ4 d P hd hJ1 hJ2) :
∃! value : ℝ, 0 < value ∧ ∀ (e : { e : HCPolySupport.Vec d // HCPolySupport.Book.Ch02.vecNorm e = 1 }), ‖Frozen.Assumptions.ShellField.zeroShellPotentialCorrector P ⋯ ↑e ⋯‖ ^ 2 = value * Real.log 3
source
noncomputable def Algsuperdiff.Section3.Disorder.cstar {d : ℕ} (M : ABKModel d) :
ℝ

The positive J4 non-degeneracy constant selected from the standing ABK model.

Equations
Instances For
    source
    theorem Algsuperdiff.Section3.Disorder.cstar_characterization {d : ℕ} (M : ABKModel d) :
    0 < cstar M ∧ (∀ (e : { e : HCPolySupport.Vec d // HCPolySupport.Book.Ch02.vecNorm e = 1 }), ‖Frozen.Assumptions.ShellField.zeroShellPotentialCorrector M.P ⋯ ↑e ⋯‖ ^ 2 = cstar M * Real.log 3) ∧ ∀ (other : ℝ), 0 < other → (∀ (e : { e : HCPolySupport.Vec d // HCPolySupport.Book.Ch02.vecNorm e = 1 }), ‖Frozen.Assumptions.ShellField.zeroShellPotentialCorrector M.P ⋯ ↑e ⋯‖ ^ 2 = other * Real.log 3) → other = cstar M

    The canonical cstar is positive, has the literal J4 energy identity on every unit direction, and is the unique value with those two properties.

    source
    theorem Algsuperdiff.Section3.Disorder.integrable_originFrobeniusMass {d : ℕ} (M : ABKModel d) :
    MeasureTheory.Integrable (fun (F : ℤ → Frozen.Assumptions.ShellField d) => HCPolySupport.Book.Ch02.matrixFrobeniusNormSq ((↑(F 0)).1 0)) ↑M.P

    J2's Gaussian tail makes the literal zero-shell Frobenius mass integrable.

    source
    noncomputable def Algsuperdiff.Section3.Disorder.originFrobeniusMass {d : ℕ} (M : ABKModel d) :
    ℝ

    The literal squared Frobenius mass of the zero shell at the origin. The preceding theorem admits this expectation from the standing J2 tail bound.

    Equations
    Instances For
      source
      noncomputable def Algsuperdiff.Section3.Disorder.cstarPlus {d : ℕ} (M : ABKModel d) :
      ℝ

      The normalized Frobenius origin-mass constant.

      Equations
      Instances For
        source
        theorem Algsuperdiff.Section3.Disorder.cstarPlus_characterization {d : ℕ} (M : ABKModel d) :
        originFrobeniusMass M = cstarPlus M * Real.log 3

        The Frobenius constant is normalized so that its defining origin mass is cstarPlus * log 3.

        source
        theorem Algsuperdiff.Section3.Disorder.cstarPlus_nonneg {d : ℕ} (M : ABKModel d) :
        0 ≤ cstarPlus M

        The Frobenius constant is nonnegative because its defining mass is an expectation of a squared Frobenius norm.

        source
        theorem Algsuperdiff.Section3.Disorder.dim_mul_cstar_le_cstarPlus {d : ℕ} (M : ABKModel d) :
        ↑d * cstar M ≤ cstarPlus M

        J4's directional energy is controlled, after summing an orthonormal basis, by the J2-admissible Frobenius origin mass.

        source
        theorem Algsuperdiff.Section3.Disorder.cstarPlus_pos {d : ℕ} (M : ABKModel d) :
        0 < cstarPlus M

        The normalized Frobenius origin-mass constant is strictly positive.