MinimalScaleShift

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

t.regularity Step 1/Step 2: the parameter names, the + k + 3 shift, and the

tail arithmetic

Contents

• stepOneS, stepOneSEighth, stepOneDelta — the Step-1 parameter names of e.parameter.choices.regularity: s := 1/4, the minimal-scale argument s/8, and δ := C₁⁻¹(1-α).
• minimalScaleX — e.def.X.m.alpha: X_m(α) := Z_m + k + 3, written for an arbitrary ℕ∞-valued Z so that the shift is a lemma about Z, never about a particular producer.
• measurable_minimalScaleX, le_minimalScaleX, tail_minimalScaleX_subset — the three facts the shift contributes: measurability is inherited (ℕ∞ is discrete), Z ≤ X pointwise (so every a.s. clause gated by Z transports to the strictly smaller gate X), and the tail event of X at level N is contained in the tail event of Z at level N - (k+3).
• exp_tail_dom, rate_dom, gate_of_sq_le — the three abstract-real inequalities behind the conversion of the p.minimal.scale.separation.sec4 tail into the shape printed in the anchor's minimal-scale clause. Every transcendental atom is opaque: Real.exp is touched only through Real.exp_le_exp, and no nonlinear-arithmetic closer is used anywhere.

References

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

The Step-1 parameters

noncomputable def Algsuperdiff.Section4.Provider.Regularity.stepOneS : ℝ

The Step-1 scale parameter s := 1/4 of e.parameter.choices.regularity.

Equations

• Algsuperdiff.Section4.Provider.Regularity.stepOneS = 1 / 4

noncomputable def Algsuperdiff.Section4.Provider.Regularity.stepOneSEighth : ℝ

The minimal-scale argument s/8 of e.def.X.m.alpha, i.e. the first argument of Z_m(s/8, δ).

Equations

• Algsuperdiff.Section4.Provider.Regularity.stepOneSEighth = Algsuperdiff.Section4.Provider.Regularity.stepOneS / 8

noncomputable def Algsuperdiff.Section4.Provider.Regularity.stepOneDelta (C1 alpha : ℝ) : ℝ

The Step-1 tolerance δ := C₁⁻¹(1-α) of e.parameter.choices.regularity. C₁ is the abstract Step-1 constant.

Equations

• Algsuperdiff.Section4.Provider.Regularity.stepOneDelta C1 alpha = C1⁻¹ * (1 - alpha)

theorem Algsuperdiff.Section4.Provider.Regularity.stepOneSEighth_eq : stepOneSEighth = 1 / 32

s/8 = 1/32.

theorem Algsuperdiff.Section4.Provider.Regularity.stepOneSEighth_pos : 0 < stepOneSEighth

0 < s/8.

theorem Algsuperdiff.Section4.Provider.Regularity.stepOneSEighth_mem : stepOneSEighth ∈ Set.Ioc 0 (1 / 4)

s/8 ∈ (0, 1/4]: the s-window of p.minimal.scale.separation.sec4.

theorem Algsuperdiff.Section4.Provider.Regularity.stepOneSEighth_pow_le_one : stepOneSEighth ^ 9 ≤ 1

(s/8)^9 ≤ 1.

theorem Algsuperdiff.Section4.Provider.Regularity.stepOneSEighth_pow_pos : 0 < stepOneSEighth ^ 9

0 < (s/8)^9.

theorem Algsuperdiff.Section4.Provider.Regularity.stepOneDelta_mem {C1 alpha : ℝ} (hC1 : 2 ≤ C1) (halpha0 : 0 < alpha) (halpha1 : alpha < 1) : stepOneDelta C1 alpha ∈ Set.Ioc 0 (1 / 2)

δ ∈ (0, 1/2]: the δ-window of p.minimal.scale.separation.sec4, at the pin C₁ ≥ 2.

The + k + 3 shift

def Algsuperdiff.Section4.Provider.Regularity.minimalScaleX {Omega : Type u_1} (Z : Omega → ℕ∞) (k : ℕ) : Omega → ℕ∞

e.def.X.m.alpha: the Step-2 minimal scale X_m(α) := Z_m(s/8, δ) + k + 3, as a function of an arbitrary ℕ∞-valued minimal scale Z and the abstract Step-1 constant k.

Equations

• Algsuperdiff.Section4.Provider.Regularity.minimalScaleX Z k omega = Z omega + ↑k + 3

theorem Algsuperdiff.Section4.Provider.Regularity.minimalScaleX_eq_add_cast {Omega : Type u_1} (Z : Omega → ℕ∞) (k : ℕ) (omega : Omega) : minimalScaleX Z k omega = Z omega + ↑(k + 3)

X_m(α) = Z_m + (k+3) with the offset collected into a single natural cast.

theorem Algsuperdiff.Section4.Provider.Regularity.le_minimalScaleX {Omega : Type u_1} (Z : Omega → ℕ∞) (k : ℕ) (omega : Omega) : Z omega ≤ minimalScaleX Z k omega

Z_m ≤ X_m(α) pointwise. This is what transports a good-scales clause gated by Z_m ≤ m - n to the same clause gated by X_m(α) ≤ m - n.

theorem Algsuperdiff.Section4.Provider.Regularity.measurable_minimalScaleX {Omega : Type u_1} [MeasurableSpace Omega] {Z : Omega → ℕ∞} (hZ : Measurable Z) (k : ℕ) : Measurable (minimalScaleX Z k)

Measurability of X_m(α) is inherited from Z_m: ℕ∞ is a discrete measurable space, so post-composition with · + k + 3 is measurable.

theorem Algsuperdiff.Section4.Provider.Regularity.tail_minimalScaleX_subset {Omega : Type u_1} (Z : Omega → ℕ∞) (k N : ℕ) : {omega : Omega | ↑N ≤ minimalScaleX Z k omega} ⊆ {omega : Omega | ↑(N - (k + 3)) ≤ Z omega}

The + k + 3 index shift on tail events: {N ≤ X_m(α)} ⊆ {N - (k+3) ≤ Z_m}.

The abstract-real tail arithmetic

All three lemmas are stated for opaque reals. Real.exp is used only through Real.exp_le_exp; the rest is monotonicity of multiplication and division.

theorem Algsuperdiff.Section4.Provider.Regularity.exp_tail_dom {Cm Co A B : ℝ} (hCm : 0 < Cm) (hCmCo : Cm ≤ Co) (hBA : B ≤ A) : Cm * Real.exp (-A) ≤ Co * Real.exp (-B)

Prefactor-and-rate domination for exponential tails: a larger prefactor and a smaller rate weaken the bound.

theorem Algsuperdiff.Section4.Provider.Regularity.rate_dom {a g s cs C1 Cm Co t v : ℝ} (hg : 0 < g) (hCm : 0 < Cm) (hCo : 0 < Co) (ht : 0 ≤ t) (hvt : v ≤ t) (hkey : Cm ≤ s ^ 9 * cs ^ 2 * C1⁻¹ ^ 2 * Co) : a ^ 2 * v / (Co * g) ≤ t * s ^ 9 * cs ^ 2 * (C1⁻¹ * a) ^ 2 / (Cm * g)

With a := 1 - α, v := N - C, t := N - k - 4, Cm the p.minimal.scale.separation.sec4 constant and Co the produced one, the anchor's rate a²·v/(Co·g) is dominated by the producer's rate t·s⁹·cs²·(C₁⁻¹a)²/(Cm·g) as soon as Cm ≤ s⁹ cs² C₁⁻² Co.

theorem Algsuperdiff.Section4.Provider.Regularity.gate_of_sq_le {a g s cs C1 Cm Co : ℝ} (hg : 0 < g) (hs : 0 ≤ s) (hsq : Co ^ 2 * g ≤ a ^ 2) (hkey : 1 ≤ Cm⁻¹ ^ 10 * (C1⁻¹ ^ 2 * cs ^ 2 * s ^ 9) * Co ^ 2) : g ≤ Cm⁻¹ ^ 10 * ((C1⁻¹ * a) ^ 2 * cs ^ 2 * s ^ 9)

The γ-gate of p.minimal.scale.separation.sec4 at the Step-1 parameters. From the theorem's own hypothesis α ≤ 1 - C γ^{1/2} in the squared form Co² g ≤ a² (with a:= 1 - α), together with a size condition on Co, the second branch of the producer's min is met at δ = C₁⁻¹(1-α).

theorem Algsuperdiff.Section4.Provider.Regularity.one_le_shifted_exp {a g x Co : ℝ} (hCo : 1 ≤ Co) (hg : 0 < g) (hx : x ≤ Co) : 1 ≤ Co * Real.exp (-(a ^ 2 * (x - Co)) / (Co * g))

The small-N branch of the shifted tail: when N ≤ C, the printed right-hand side is at least 1, so the trivial probability bound already gives the estimate.