InductionState #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
noncomputable def
Algsuperdiff.Frozen.Section3.inductionState
{d : ℕ}
(M : Section3.ABKModel d)
(m0 : ℤ)
(E : { E : ℝ // 1 ≤ E })
:
The diffusivity and quantitative estimates required through the induction scale.
Equations
- One or more equations did not get rendered due to their size.