MinimalScaleX

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

t.regularity Step 2: the minimal scale X_m(α), its tail, and its

good-scales clause

The target

ABK26 t.regularity Step 2:

X_m(α) := Z_m(s/8, δ) + k + 3                                (e.def.X.m.alpha)
X_m(α)  = 𝒪_{Γ₁}( C c⋆^{-2} (1-α)^{-2} γ )        (e.X.m.stochastic.integrability)

at the Step-1 parameters s := 1/4, δ := C₁⁻¹(1-α) of e.parameter.choices.regularity.

What is delivered, and how it relates to the anchor's clause

step_two_minimalScaleX produces, for each m, a Z such that the four Step-2 items hold for X := minimalScaleX Z k (= Z + k + 3):

• (a) the definition: X is literally minimalScaleX Z k, i.e. fun omega => Z omega + (k : ℕ∞) + 3, with Z the minimal scale delivered by minimal_scale_separation at (s/8, δ) = (stepOneSEighth, stepOneDelta C₁ α). The identification of Z is machine-visible: the first two conjuncts of the conclusion are the producer's own Measurable Z and its a.s. good-scales clause at the tighter gate Z ω ≤ m - n, both delivered verbatim;
• (b) Measurable X;
• (c) the tail, in the anchor's own shape: for every N : ℕ, law {ω | N ≤ X ω} ≤.ofReal (C * exp (-((1-α)^2 * (N - C)) / (C * γ))). This conjunct is character-for-character the second conjunct of the minimal-scale block of the frozen anomalous_regularity (Algsuperdiff/Frozen/Section4/AnomalousRegularity.lean) with the anchor's bound X replaced by minimalScaleX Z k and the anchor's produced C by the one produced here;
• (d) the a.e. good-scales clause of minimal_scale_separation, transported from the gate Z ω ≤ m - n to the gate X ω ≤ m - n (GoodScaleWindows). The window family U_j and the bad set B_z of Step 3 are not formed here.

Deviation from the printed text

Since s is the Step-1 numeral 1/4, s⁷ → s⁹ is a pure constant move: it is absorbed into the produced C and the printed hypothesis α ≤ 1 - C γ^{1/2} is preserved verbatim.

References

• ABK26, t.regularity Steps 1--2.

The good-scales window clause

GoodScaleWindows is the conclusion body of the frozen block of Algsuperdiff.Frozen.Section4.minimal_scale_separation (MinimalScaleSeparation.lean) spliced verbatim: the two Cesàro displays of e.scale.sep.clauses, the flux-corrected error observable on the good event and the complement-indicator density, each ≤.ofReal δ, at the lattice centre family 3^{n-1}ℤ^d ∩ □_m. Only the binder names for (n, m, omega) are supplied; the body is unchanged.

def Algsuperdiff.Section4.Provider.Regularity.GoodScaleWindows {d : ℕ} (M : Section3.ABKModel d) (s delta : ℝ) (hs : 0 < s) (n m : ℤ) (omega : Section3.Cutoff.CutoffSample d) : Prop

The two Cesàro good-scale displays of p.minimal.scale.separation.sec4 at the window [n, m], spliced verbatim from the frozen block.

Equations

• One or more equations did not get rendered due to their size.

The produced constants

noncomputable def Algsuperdiff.Section4.Provider.Regularity.stepTwoGamma0 (Cm cs : ℝ) : ℝ

The produced γ-threshold: the first branch of the min in the γ-gate of p.minimal.scale.separation.sec4, together with the 8γ ≤ s/8 gate.

Equations

• Algsuperdiff.Section4.Provider.Regularity.stepTwoGamma0 Cm cs = min (Cm⁻¹ ^ 10 * cs ^ 10) (1 / 256)

noncomputable def Algsuperdiff.Section4.Provider.Regularity.stepTwoConst (Cm cs C1 : ℝ) (k : ℕ) : ℝ

The produced constant C = C(d, c⋆): large enough (i) to dominate the producer's prefactor, (ii) to exceed k + 4 (the shift), (iii) to make the producer's rate dominate the anchor's, and (iv) to make the theorem's own hypothesis α ≤ 1 - C γ^{1/2} imply the producer's γ-gate.

Equations

• One or more equations did not get rendered due to their size.

The Step-2 endpoint

theorem Algsuperdiff.Section4.Provider.Regularity.step_two_minimalScaleX (d : ℕ) (cstar : ℝ) (hcstar : 0 < cstar) (k : ℕ) (hk : 10 ≤ k) (C1 : ℝ) (hC1 : 2 ≤ C1) : ∃ (gamma0 : ℝ) (C : ℝ), 0 < gamma0 ∧ 0 < C ∧ ∀ (M : Section3.ABKModel d), Section3.Disorder.cstar M = cstar → M.gamma ≤ gamma0 → ∀ (alpha : ℝ), 0 < alpha → alpha ≤ 1 - C * √M.gamma → ∀ (m : ℤ), ∃ (Z : Section3.Cutoff.CutoffSample d → ℕ∞), Measurable Z ∧ (∀ᵐ (omega : Section3.Cutoff.CutoffSample d) ∂↑(Section3.Cutoff.cutoffSampleLaw M), ∀ n ≤ m, Z omega ≤ ↑(m - n).toNat → GoodScaleWindows M stepOneSEighth (stepOneDelta C1 alpha) stepOneSEighth_pos n m omega) ∧ Measurable (minimalScaleX Z k) ∧ (∀ (N : ℕ), ↑(Section3.Cutoff.cutoffSampleLaw M) {omega : Section3.Cutoff.CutoffSample d | ↑N ≤ minimalScaleX Z k omega} ≤ ENNReal.ofReal (C * Real.exp (-((1 - alpha) ^ 2 * (↑N - C)) / (C * M.gamma)))) ∧ ∀ᵐ (omega : Section3.Cutoff.CutoffSample d) ∂↑(Section3.Cutoff.cutoffSampleLaw M), ∀ n ≤ m, minimalScaleX Z k omega ≤ ↑(m - n).toNat → GoodScaleWindows M stepOneSEighth (stepOneDelta C1 alpha) stepOneSEighth_pos n m omega

t.regularity Step 2: the minimal scale X_m(α).

For every m there is a minimal scale Z of p.minimal.scale.separation.sec4 at the Step-1 parameters (s/8, δ) = (stepOneSEighth, stepOneDelta C₁ α) -- measurable, and carrying the producer's a.s. good-scales clause -- such that X := minimalScaleX Z k = Z + k + 3 (e.def.X.m.alpha) is measurable, has the shifted exponential tail in the shape printed in the minimal-scale clause of anomalous_regularity, and carries the same a.e. good-scales clause at its own (larger) gate X ω ≤ m - n, which is the form Steps 3--4 read.