KickCollapse

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

The Step-1 collapse and e.Xj.expectation.upinthere

ABK26, §4.2, Step 1 of l.minimal.scale.sep. After the two-leg split, collapses the pair into a single variable

X_j := X_j^{(1)} + (C s^{−9/2} X_j^{(2)})^{1/4} ,

asserts X_j ≤ 𝒪_{Γ₂}(C c⋆^{−1}s^{−5/2}√γ) "by e.powerofGammasigma, s ≥ 8γ and γ ≤ C^{−1}c⋆⁵" (the endpoint below uses the lemma's own stronger regime γ ≤ C^{−10}c⋆^{10} instead), and reads off

E[X_j] ≤ C c⋆^{−1} s^{−5/2} √γ                              (e.Xj.expectation.upinthere).

Both are proved here. The min{a,b} ≤ a^{1/4}b^{3/4} step is what motivates the shape and is not needed as an input: what the collapse consumes is the fourth root of the Γ_{1/2} leg, and the two facts that make it work are

• the collapse absorption KickArith.exp_neg_eighth_le_sqrt, which is where s ≥ 8γ and the regime enter: it says that the fourth root of the exponentially small amplitude is already below C c⋆^{−1}√γ, so the Γ_{1/2} leg contributes nothing to the printed exponent.

The s^{−9/8} produced by the fourth root of s^{−9/2} is below the printed s^{−5/2} because s ≤ 1; this is the only place the collapse's own s-power is used, and it is slack.

E[X_j], and why it is a corollary and not a new estimate

A Γ₂ tail at scale A gives E[X] ≤ gammaMomentConst 2 · A (Algsuperdiff.Probability.integral_le_of_isBigO_gammaSigma), so the printed first-moment constant is the tail constant times a dimensional factor. The endpoint below therefore proves the tail at an intermediate constant and states BOTH conclusions at the single larger constant C, which is exactly the manuscript's convention.

Main definitions and results

• kickCollapsed — the collapsed variable X_j, with K the printed coefficient C s^{−9/2} supplied by the caller.
• measurable_kickCollapsed, kickCollapsed_nonneg, rDependent_kickCollapsed — the engine's hmeas slot, positivity, and the r-dependence, the last of these free because X_j is a measurable function of annularKick_j.
• exists_kickCollapse — the endpoint: the Γ₂ tail AND e.Xj.expectation.upinthere, uniformly in j.

References

• ABK26, l.minimal.scale.sep, (the lemma's hypotheses), Step 1; e.powerofGammasigma (ff).

1. Two elementary devices

theorem Algsuperdiff.Section4.Provider.MinimalScale.sqrt_sqrt_le_of_le_pow_four {x y : ℝ} (hy : 0 ≤ y) (h : x ≤ y ^ 4) : √√x ≤ y

√√x ≤ y from x ≤ y⁴: the comparison that turns a fourth-power estimate into an estimate on the nested square root, with no rpow in sight.

theorem Algsuperdiff.Section4.Provider.MinimalScale.isBigOWith_sqrt_sqrt {Omega : Type u_1} [MeasurableSpace Omega] {mu : MeasureTheory.Measure Omega} [MeasureTheory.IsFiniteMeasure mu] {X : Omega → ℝ} {A : ℝ} (hA : 0 ≤ A) (hX0 : ∀ (omega : Omega), 0 ≤ X omega) (hX : HCPolySupport.IndependentSums.IsBigOWith mu (HCPolySupport.IndependentSums.gammaSigma (1 / 2)) X A) : HCPolySupport.IndependentSums.IsBigOWith mu (HCPolySupport.IndependentSums.gammaSigma 2) (fun (omega : Omega) => √√(X omega)) √√A

e.powerofGammasigma at the fourth root. A Γ_{1/2} tail at scale A for a nonnegative variable gives a Γ₂ tail at scale √√A for √√X: the proved power rule isBigOWith_gammaSigma_rpow applied twice at p = 1/2, since (1/2)/(1/2) = 1 and 1/(1/2) = 2.

2. The collapsed variable

noncomputable def Algsuperdiff.Section4.Provider.MinimalScale.kickCollapsed {d : ℕ} (M : Section3.ABKModel d) (s : { s : ℝ // 0 < s }) (lam K : ℝ) (j : ℤ) (omega : Section3.Cutoff.CutoffSample d) : ℝ

The collapsed Step-1 variable X_j = X_j^{(1)} + (K·X_j^{(2)})^{1/4}, with the printed coefficient K = C s^{−9/2} supplied by the caller and the fourth root written as a nested square root.

Equations

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

theorem Algsuperdiff.Section4.Provider.MinimalScale.kickCollapsed_nonneg {d : ℕ} (M : Section3.ABKModel d) (s : { s : ℝ // 0 < s }) {lam : ℝ} (hlam : 0 ≤ lam) (K : ℝ) (j : ℤ) (omega : Section3.Cutoff.CutoffSample d) : 0 ≤ kickCollapsed M s lam K j omega

theorem Algsuperdiff.Section4.Provider.MinimalScale.measurable_kickCollapsed {d : ℕ} (M : Section3.ABKModel d) (s : { s : ℝ // 0 < s }) (lam K : ℝ) (j : ℤ) : Measurable (kickCollapsed M s lam K j)

theorem Algsuperdiff.Section4.Provider.MinimalScale.rDependent_kickCollapsed {d : ℕ} (M : Section3.ABKModel d) (s : { s : ℝ // 0 < s }) (lam K : ℝ) {r : ℕ} (h : Probability.RDependent (↑(Section3.Cutoff.cutoffSampleLaw M)) (fun (j : ℤ) => annularKick M s j) r) : Probability.RDependent (↑(Section3.Cutoff.cutoffSampleLaw M)) (fun (j : ℤ) => kickCollapsed M s lam K j) r

The collapsed family is r-dependent whenever the inner-scale sum is: X_j is a measurable function of annularKick_j alone.

3. The two numerical facts of the assembly

theorem Algsuperdiff.Section4.Provider.MinimalScale.triangleConstTwo_le : (1 + Real.log 2) ^ 2⁻¹ ≤ 2

(1 + log 2)^{1/2} ≤ 2: the two-term Γ₂ triangle constant is at most 2, which is all the assembly needs from it.

4. The endpoint

theorem Algsuperdiff.Section4.Provider.MinimalScale.exists_kickCollapse (d : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ (M : Section3.ABKModel d), M.gamma ≤ C⁻¹ ^ 10 * Section3.Disorder.cstar M ^ 10 → ∀ (s : { s : ℝ // 0 < s }), 8 * M.gamma ≤ ↑s → ↑s ≤ 1 / 2 → ∃ (lam : ℝ), 0 ≤ lam ∧ (∀ (j : ℤ) (omega : Section3.Cutoff.CutoffSample d), kickLegLow M s lam j omega + kickLegHigh M s lam j omega = annularKick M s j omega) ∧ (∀ (j : ℤ), HCPolySupport.IndependentSums.IsBigOWith (↑(Section3.Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma 2) (kickCollapsed M s lam (C * (√↑s ^ 9)⁻¹) j) (C * (Section3.Disorder.cstar M)⁻¹ * (√↑s ^ 5)⁻¹ * √M.gamma)) ∧ ∀ (j : ℤ), ∫ (omega : Section3.Cutoff.CutoffSample d), kickCollapsed M s lam (C * (√↑s ^ 9)⁻¹) j omega ∂↑(Section3.Cutoff.cutoffSampleLaw M) ≤ C * (Section3.Disorder.cstar M)⁻¹ * (√↑s ^ 5)⁻¹ * √M.gamma

TH AND e.Xj.expectation.upinthere, UN.

There is a dimensional constant C such that for every model in the regime γ ≤ C^{−10}c⋆^{10} and every window parameter s ∈ [8γ, 1/2] there is a threshold lam for which, uniformly in the annulus index j, the two legs add up to the Step-1 inner sum and the collapsed variable

X_j = X_j^{(1)} + (C s^{−9/2} X_j^{(2)})^{1/4}

obeys X_j ≤ 𝒪_{Γ₂}(C c⋆^{−1}s^{−5/2}√γ) and E[X_j] ≤ C c⋆^{−1}s^{−5/2}√γ.

s^{−5/2} is ((√s)⁵)⁻¹ and s^{−9/2} is ((√s)⁹)⁻¹, so no rpow appears.

Hypotheses. Exactly the premises of l.minimal.scale.sep as printed: γ ≤ C^{−10}c⋆^{10} and s ∈ [8γ, 1/2]. The positivity of s is the typing datum of the observable's index and is implied by the window.