Model

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

The standing ABK model

This file packages precisely the paper data used throughout Section 3.

Main definitions

• Algsuperdiff.Section3.ABKModel: molecular diffusivity, the canonical shell sequence law, and the exact prefix and (J1)--(J4) assumptions of ABK26.

References

• ABK26.

structure Algsuperdiff.Section3.ABKModel (d : ℕ) : Type

The complete standing probabilistic model of ABK26.

The dimension is an external parameter. Its lower bound and the complete admissible range for gamma belong exactly to prefix; this aggregate adds only molecular diffusivity positivity and the four separately frozen shell-law assumptions. The shell carrier enforces qualitative C² regularity, which strengthens the paper's local C^{1,1} assumption.

• nu : ℝ

  The molecular diffusivity from ABK26.

• nu_pos : 0 < self.nu

  Molecular diffusivity is strictly positive.

• gamma : ℝ

  The scale parameter from ABK26.

• P : MeasureTheory.ProbabilityMeasure (ℤ → Frozen.Assumptions.ShellField d)

  The canonical probability law of the bi-infinite shell sequence.

• shellPrefix : Frozen.Assumptions.ShellLawPrefix d self.gamma self.P

  The exact dimension, scale, independence, and marginal-scaling prefix.

• J1 : Frozen.Assumptions.ShellLawJ1 d self.P

  The exact mean-zero, stationarity, and finite-range assumption (J1).

• J2 : Frozen.Assumptions.ShellLawJ2 d self.P

  The Gaussian-tail assumption (J2), with C² regularity in the shell carrier.

• J3 : Frozen.Assumptions.ShellLawJ3 d self.P

  The exact joint hyperoctahedral and negation invariance assumption (J3).

• J4 : Frozen.Assumptions.ShellLawJ4 d self.P ⋯ ⋯ ⋯

  The exact stationary potential-projection nondegeneracy assumption (J4).