Landmarks

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

Landmark characterizations for the Section 3 induction scales

ABK26 introduces two distinguished small scales. The scale m** is the largest integer m with nu ^ 2 ≥ 2 (log 3) c gamma⁻³ 3 ^ (2 gamma m) and the scale m* is the largest integer m with nu ^ 2 ≥ 2 (log 3) c gamma⁻¹ 3 ^ (2 gamma m).

This file proves exactly those characterizations for the repository's Algsuperdiff.Section3.mStarStar and Algsuperdiff.Section3.mStar, together with the floor estimate that they imply and the ordering mStarStar ≤ mStar.

The Lean definitions use the normalized Frobenius origin-mass constant Algsuperdiff.Section3.Disorder.cstarPlus where the paper prints cstar. That substitution is already part of the frozen definitions and is not revisited here.

Main results

• le_mStar_iff: the source "largest integer" property.
• le_mStarStar_iff_rpow_le, le_mStar_iff_rpow_le: the same property in quotient form, which is the convenient shape for downstream estimates.
• mStarStar_le_mStar: the two landmarks are ordered.
• rpow_mStarStar_le: the upper half of the floor sandwich, the landmark mStarStar itself meeting its threshold.

References

• ABK26, equations e.mstarstar and e.mstar.

theorem Algsuperdiff.Section3.Provider.Scales.le_mStarStar_iff_rpow_le {d : ℕ} (M : ABKModel d) (m : ℤ) : m ≤ mStarStar M ↔ 3 ^ (2 * M.gamma * ↑m) ≤ M.nu ^ 2 * M.gamma ^ 3 / (2 * Real.log 3 * Disorder.cstarPlus M)

Quotient form of the defining property of mStarStar.

theorem Algsuperdiff.Section3.Provider.Scales.le_mStar_iff_rpow_le {d : ℕ} (M : ABKModel d) (m : ℤ) : m ≤ mStar M ↔ 3 ^ (2 * M.gamma * ↑m) ≤ M.nu ^ 2 * M.gamma / (2 * Real.log 3 * Disorder.cstarPlus M)

Quotient form of the defining property of mStar.

theorem Algsuperdiff.Section3.Provider.Scales.le_mStar_iff {d : ℕ} (M : ABKModel d) (m : ℤ) : m ≤ mStar M ↔ 2 * Real.log 3 * Disorder.cstarPlus M * M.gamma⁻¹ * 3 ^ (2 * M.gamma * ↑m) ≤ M.nu ^ 2

mStar M is the largest integer m with 2 (log 3) c⁺ gamma⁻¹ 3 ^ (2 gamma m) ≤ nu ^ 2, which is ABK26's defining description of m*.

theorem Algsuperdiff.Section3.Provider.Scales.mStarStar_le_mStar {d : ℕ} (M : ABKModel d) : mStarStar M ≤ mStar M

The base-case landmark never exceeds the base-plateau landmark, because gamma ≤ 1 / 4 forces gamma ^ 3 ≤ gamma.

theorem Algsuperdiff.Section3.Provider.Scales.rpow_mStarStar_le {d : ℕ} (M : ABKModel d) : 3 ^ (2 * M.gamma * ↑(mStarStar M)) ≤ M.nu ^ 2 * M.gamma ^ 3 / (2 * Real.log 3 * Disorder.cstarPlus M)

The upper half of the floor sandwich at mStarStar.