KickSplit

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

The clamp split of a two-term (Γ₂, Γ_{1/2}) display

This module supplies the decomposition that meets both demands at once. Given a nonnegative X with a two-term display X ≤ 𝒪_{Γ₂}(A₁) + 𝒪_{Γ_{1/2}}(A₂), the two legs are the clamp and the overshoot at the deterministic threshold

lam := 8 A₁ ρ ,      ρ := (A₁/A₂)^{1/3}  (equivalently ρ³A₂ = A₁) ,
min(X, lam) ≤ 𝒪_{Γ₂}(8A₁) ,      X − min(X, lam) ≤ 𝒪_{Γ_{1/2}}(8A₂) .

Both legs are measurable functions of X alone, so they inherit verbatim every independence property of X: this is what makes provable rather than assumed. A split built from the two Γ-witnesses of the display instead would lose it, because the witnesses are supplied by the Section 3 anchor as bare existentials with no locality.

Why the threshold is at (A₁/A₂)^{1/3}

ρ is the crossover of the two tails, and the exponent 1/3 is forced. The Γ₂ leg needs the Γ_{1/2} witness to be negligible on levels below lam, which costs √(A₁/A₂ · t) ≥ t² for t ≤ ρ, i.e. ρ³ ≥ ρ⁴/ρ; the Γ_{1/2} leg needs the Γ₂ witness to be negligible on levels above lam, which costs (lam/A₁)² ≥ √t for t up to ρ⁴. The two demands meet exactly at ρ ≍ (A₁/A₂)^{1/3}; the numerical factor 8 is what makes both hold with room to spare, and the proof below exhibits that room (15 t² ≥ log 2 and 15 √t ≥ log 2).

Main results

• isBigOWith_min_of_isTwoTermBigOWith — the Γ₂ leg.
• isBigOWith_sub_min_of_isTwoTermBigOWith — the Γ_{1/2} leg.

ρ is a free parameter constrained only by ρ³A₂ = A₁, so no root is ever formed: the caller supplies ρ (in KickTails.lean, as (A₁/A₂)^{1/3}).

Scope

Carrier-free: generic in the measure space.

References

• ABK26, l.minimal.scale.sep, Step 1.

rpow bookkeeping at the two Orlicz indices

theorem Algsuperdiff.Section4.Provider.MinimalScale.rpow_two_eq (t : ℝ) : t ^ 2 = t ^ 2

theorem Algsuperdiff.Section4.Provider.MinimalScale.rpow_half_eq (t : ℝ) : t ^ (1 / 2) = √t

theorem Algsuperdiff.Section4.Provider.MinimalScale.one_le_sqrt_of_one_le {t : ℝ} (ht : 1 ≤ t) : 1 ≤ √t

theorem Algsuperdiff.Section4.Provider.MinimalScale.sqrt_four_mul (t : ℝ) : √(4 * t) = 2 * √t

The Γ₂ leg: the clamp

theorem Algsuperdiff.Section4.Provider.MinimalScale.isBigOWith_min_of_isTwoTermBigOWith {Omega : Type u_1} [MeasurableSpace Omega] {mu : MeasureTheory.Measure Omega} [MeasureTheory.IsFiniteMeasure mu] {X : Omega → ℝ} {A1 A2 rho : ℝ} (hratio : rho ^ 3 * A2 = A1) (hX : Section3.Probability.IsTwoTermBigOWith mu (HCPolySupport.IndependentSums.gammaSigma 2) (HCPolySupport.IndependentSums.gammaSigma (1 / 2)) X A1 A2) : HCPolySupport.IndependentSums.IsBigOWith mu (HCPolySupport.IndependentSums.gammaSigma 2) (fun (omega : Omega) => min (X omega) (8 * A1 * rho)) (8 * A1)

The Γ₂ leg X^{(1)} = min(X, 8A₁ρ). Below the threshold the Γ_{1/2} witness is negligible against a Γ₂ tail, and above it the clamp makes the tail event empty.

The Γ_{1/2} leg: the overshoot

theorem Algsuperdiff.Section4.Provider.MinimalScale.isBigOWith_sub_min_of_isTwoTermBigOWith {Omega : Type u_1} [MeasurableSpace Omega] {mu : MeasureTheory.Measure Omega} [MeasureTheory.IsFiniteMeasure mu] {X : Omega → ℝ} {A1 A2 rho : ℝ} (hrho : 0 < rho) (hratio : rho ^ 3 * A2 = A1) (hX : Section3.Probability.IsTwoTermBigOWith mu (HCPolySupport.IndependentSums.gammaSigma 2) (HCPolySupport.IndependentSums.gammaSigma (1 / 2)) X A1 A2) : HCPolySupport.IndependentSums.IsBigOWith mu (HCPolySupport.IndependentSums.gammaSigma (1 / 2)) (fun (omega : Omega) => X omega - min (X omega) (8 * A1 * rho)) (8 * A2)

The Γ_{1/2} leg X^{(2)} = X − min(X, 8A₁ρ). Above the threshold the Γ₂ witness is negligible against a Γ_{1/2} tail: at levels below ρ⁴ the constant part 4ρ of the normalized level already dominates √t, and above ρ⁴ the growing part 4t/ρ³ does.