Scales

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

Section 3 scale vocabulary

The two distinguished induction landmarks from ABK26, equations e.mstarstar and e.mstar, and the adopted Section 3.2 Option-A loss.

noncomputable def Algsuperdiff.Section3.mStarStar {d : ℕ} (model : ABKModel d) : ℤ

The base-case starting scale m**, using the source-normalized Frobenius origin-mass constant cstarPlus.

Equations

• Algsuperdiff.Section3.mStarStar model = ⌊(2 * model.gamma)⁻¹ * Real.logb 3 (model.nu ^ 2 * model.gamma ^ 3 / (2 * Real.log 3 * Algsuperdiff.Section3.Disorder.cstarPlus model))⌋

noncomputable def Algsuperdiff.Section3.mStar {d : ℕ} (model : ABKModel d) : ℤ

The base-plateau scale m*, using the source-normalized Frobenius origin-mass constant cstarPlus.

Equations

• Algsuperdiff.Section3.mStar model = ⌊(2 * model.gamma)⁻¹ * Real.logb 3 (model.nu ^ 2 * model.gamma / (2 * Real.log 3 * Algsuperdiff.Section3.Disorder.cstarPlus model))⌋

noncomputable def Algsuperdiff.Section3.baseLoss (d : ℕ) (s : { s : ℝ // s ∈ Set.Ioo 0 1 }) : ℝ

The adopted Option-A all-scale loss in the Section 3.2 base case, on the literal source range 0 < s < 1.

Equations

• Algsuperdiff.Section3.baseLoss d s = 1 + 6 * ↑d * Real.log 3 / ↑s