KickingLemma

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

l.minimal.scale.sep: the kicking lemma e.good.scale.kicking

ABK26, §4.2. This module assembles the three Steps of l.minimal.scale.sep into the lemma itself: for every window [n, m] with n < m,

avsum_{k=n}^m sup_{L ≥ k} 𝓔_{s,∞,2}(□_k; a_L − (k_L − k_k)_{□_k}, σ_k) 1_{𝒢(k;s,1)}
  ≤ C c⋆^{−1}s^{−7/2}√γ + 𝒪_{Γ₂}( C c⋆^{−1}s^{−9/2}√γ (m−n)^{−1/2} ) .

The four inputs are already proved and are consumed by name:

• exists_dDecomposition_absorbed — the √-split of the annular anchor's clause (i) with the deterministic remainder already absorbed into the envelope;
• exists_stepOne_d1_bound — the D₁ half of e.kick.Dees.Dees;
• exists_D2k_kicked — e.D2k.kicked at a free prefactor;
• exists_D3k_kicked with stepThree_det_closed / stepThree_fluc_closed — e.D3k.kicked and its two closed s-powers.

The two coordination bridges

Steps 2 and 3 are stated against their own inner objects gradInnerE / hessInnerE, the D-decomposition against dTwo / dThree. The bridges are:

• dTwo_eq_ofReal_mul_gradInnerE — an identity (rfl): the two spellings of the ∇𝐣 group agree termwise, prefactor included.
• dThree_le_ofReal_mul_hessInnerE — the 𝐣-Hessian group needs the iSup → fmax step (inner_le_scoreG1b, re-derived here because the Proportion original is private) and the weight-spelling identity 3^{−¼s(k−n)} = stepThreeWt (s/4) (k−n). The ℓ² → ℓ¹ halving is NOT owed here: dThree is already the ℓ¹ object at the quarter exponent.

The prefactor c⋆^{−1/2}s^{−1}γ^{1/2} of the two 𝐣 groups is compared with the lemma's envelope by sqrt_cstar_inv_le (the standing c⋆ ≤ 3/2, never c⋆ ≤ 1) — the √(C X²) = √C X bookkeeping.

The exponent

The fluctuation slot is s^{−9/2}, not the printed s^{−7/2}: Step 3's below-window channel forces it (stepThree_fluc_closed) and the printed amplitude is sharp. The deterministic slot is the printed s^{−7/2}.

Finiteness

The three groups are read in ℝ through toReal, so the assembly needs them finite: D₁ is finite at every sample (dOne_ne_top), and D₂, D₃ are finite almost surely at every scale of the window — from the proved first-moment arguments ae_gradSeries_finite and ae_hessHeadSeries_finite, never assumed.

References

• ABK26, l.minimal.scale.sep.

1. Numerical facts

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

The three-term Γ₂ triangle constant is at most 2.

theorem Algsuperdiff.Section4.Provider.MinimalScale.stepThreeDetConst_pos (d : ℕ) : 0 < stepThreeDetConst d

The Step-3 deterministic constant is positive.

theorem Algsuperdiff.Section4.Provider.MinimalScale.stepThreeFlucConst_pos (d : ℕ) : 0 < stepThreeFlucConst d

The Step-3 fluctuation constant is positive.

2. The prefactor arithmetic of the two 𝐣 groups

theorem Algsuperdiff.Section4.Provider.MinimalScale.sqrt_cstar_inv_le {d : ℕ} (M : Section3.ABKModel d) : (√(Section3.Disorder.cstar M))⁻¹ ≤ 2 * (Section3.Disorder.cstar M)⁻¹

The √c⋆ bookkeeping. The 𝐣 groups carry c⋆^{−1/2}, the lemma's envelope carries c⋆^{−1}; the standing c⋆ ≤ 3/2 (never c⋆ ≤ 1) converts one into the other at the absolute cost 2.

theorem Algsuperdiff.Section4.Provider.MinimalScale.pref_le_two_mul_envSeven {d : ℕ} (M : Section3.ABKModel d) (s : { s : ℝ // 0 < s }) (hs1 : ↑s ≤ 1) : (√(Section3.Disorder.cstar M))⁻¹ * (↑s)⁻¹ * √M.gamma ≤ 2 * ((Section3.Disorder.cstar M)⁻¹ * (√↑s ^ 7)⁻¹ * √M.gamma)

The D₂ deterministic prefactor against the lemma's envelope.

theorem Algsuperdiff.Section4.Provider.MinimalScale.pref_mul_inv_five_le {d : ℕ} (M : Section3.ABKModel d) (s : { s : ℝ // 0 < s }) (hs1 : ↑s ≤ 1) : (√(Section3.Disorder.cstar M))⁻¹ * (↑s)⁻¹ * √M.gamma * (√↑s ^ 5)⁻¹ ≤ 2 * ((Section3.Disorder.cstar M)⁻¹ * (√↑s ^ 7)⁻¹ * √M.gamma)

The D₃ deterministic prefactor against the lemma's envelope.

theorem Algsuperdiff.Section4.Provider.MinimalScale.pref_mul_inv_seven_le {d : ℕ} (M : Section3.ABKModel d) (s : { s : ℝ // 0 < s }) (hs1 : ↑s ≤ 1) : (√(Section3.Disorder.cstar M))⁻¹ * (↑s)⁻¹ * √M.gamma * (√↑s ^ 7)⁻¹ ≤ 2 * ((Section3.Disorder.cstar M)⁻¹ * (√↑s ^ 9)⁻¹ * √M.gamma)

The D₃ fluctuation prefactor against the-corrected envelope.

theorem Algsuperdiff.Section4.Provider.MinimalScale.envSeven_le_envNine {d : ℕ} (M : Section3.ABKModel d) (s : { s : ℝ // 0 < s }) (hs1 : ↑s ≤ 1) : (Section3.Disorder.cstar M)⁻¹ * (√↑s ^ 7)⁻¹ * √M.gamma ≤ (Section3.Disorder.cstar M)⁻¹ * (√↑s ^ 9)⁻¹ * √M.gamma

The printed envelope is below the-corrected one.

theorem Algsuperdiff.Section4.Provider.MinimalScale.envNine_nonneg {d : ℕ} (M : Section3.ABKModel d) (s : { s : ℝ // 0 < s }) : 0 ≤ (Section3.Disorder.cstar M)⁻¹ * (√↑s ^ 9)⁻¹ * √M.gamma

Positivity of the-corrected envelope.

theorem Algsuperdiff.Section4.Provider.MinimalScale.envSeven_nonneg {d : ℕ} (M : Section3.ABKModel d) (s : { s : ℝ // 0 < s }) : 0 ≤ (Section3.Disorder.cstar M)⁻¹ * (√↑s ^ 7)⁻¹ * √M.gamma

Positivity of the printed envelope.

3. The two coordination bridges

theorem Algsuperdiff.Section4.Provider.MinimalScale.dTwo_eq_ofReal_mul_gradInnerE {d : ℕ} (M : Section3.ABKModel d) (s : { s : ℝ // 0 < s }) (k : ℤ) (omega : Section3.Cutoff.CutoffSample d) : dTwo M s k omega = ENNReal.ofReal ((√(Section3.Disorder.cstar M))⁻¹ * (↑s)⁻¹ * √M.gamma) * gradInnerE M k omega

The D₂ bridge: an identity. D₂(k) is the D-s23 inner sum times the printed prefactor, on the nose.

theorem Algsuperdiff.Section4.Provider.MinimalScale.inner_le_scoreG1b {d : ℕ} (M : Section3.ABKModel d) {i k : ℤ} (hik : i ≤ k) (omega : Section3.Cutoff.CutoffSample d) : ENNReal.ofReal (Real.rpow 3 ((2 - M.gamma) * ↑i)) * ⨆ (v : ↑(Support.latticeCubeSet d i k)), ENNReal.ofReal (Support.shellW2InfNormAt (Support.triadicLatticePoint i ↑v) i (↑omega i)) ≤ ENNReal.ofReal (Proportion.scoreG1b M k i omega)

The iSup → fmax step (re-derived: Proportion's inner_le_score is private). The anchor's inner block at one scale is below the 𝒢₁b score field.

theorem Algsuperdiff.Section4.Provider.MinimalScale.three_rpow_quarter_eq_stepThreeWt (a : ℝ) (t : ℤ) : Real.rpow 3 (-(1 / 4) * a * ↑t) = stepThreeWt (a / 4) t

The weight-spelling identity of the D₃ bridge.

theorem Algsuperdiff.Section4.Provider.MinimalScale.dThree_le_ofReal_mul_hessInnerE {d : ℕ} (M : Section3.ABKModel d) (s : { s : ℝ // 0 < s }) (k : ℤ) (omega : Section3.Cutoff.CutoffSample d) : dThree M s k omega ≤ ENNReal.ofReal ((√(Section3.Disorder.cstar M))⁻¹ * (↑s)⁻¹ * √M.gamma) * hessInnerE M (↑s / 4) k omega

The D₃ bridge. D₃(k) is below the printed prefactor times D-s23's ℓ¹ inner object at α = s/4. The two steps are the weight spelling and the iSup → fmax domination; no ℓ² → ℓ¹ halving is needed (D-s1's dThree is already the ℓ¹ object).

4. Finiteness of the three groups

theorem Algsuperdiff.Section4.Provider.MinimalScale.dTwo_ne_top {d : ℕ} (M : Section3.ABKModel d) (s : { s : ℝ // 0 < s }) (k : ℤ) {omega : Section3.Cutoff.CutoffSample d} (hfin : Proportion.wsumE (fun (p : ℕ) => Proportion.atomG1a M (k + ↑p)) (gradWeight M) omega ≠ ⊤) : dTwo M s k omega ≠ ⊤

D₂(k) is finite wherever the Step-2 majorant series converges — almost surely, at every scale (ae_gradSeries_finite).

theorem Algsuperdiff.Section4.Provider.MinimalScale.hessInnerE_ne_top {d : ℕ} (M : Section3.ABKModel d) {alpha : ℝ} (halpha : 0 < alpha) {n m : ℤ} {omega : Section3.Cutoff.CutoffSample d} (hfin : Proportion.wsumE (fun (r : ℕ) => hessHead M alpha n m r) (fun (r : ℕ) => stepThreeWeight alpha (r + 1)) omega ≠ ⊤) {k : ℤ} (hk : k ∈ Finset.Icc n m) : hessInnerE M alpha k omega ≠ ⊤

The Step-3 inner object is finite at every scale of the window wherever the below-window channel converges — almost surely (ae_hessHeadSeries_finite).

theorem Algsuperdiff.Section4.Provider.MinimalScale.dThree_ne_top {d : ℕ} (M : Section3.ABKModel d) (s : { s : ℝ // 0 < s }) {n m : ℤ} {omega : Section3.Cutoff.CutoffSample d} (hfin : Proportion.wsumE (fun (r : ℕ) => hessHead M (↑s / 4) n m r) (fun (r : ℕ) => stepThreeWeight (↑s / 4) (r + 1)) omega ≠ ⊤) {k : ℤ} (hk : k ∈ Finset.Icc n m) : dThree M s k omega ≠ ⊤

D₃(k) is finite at every scale of the window wherever the Step-3 below-window channel converges — almost surely (ae_hessHeadSeries_finite).

The two real readings

theorem Algsuperdiff.Section4.Provider.MinimalScale.jPref_nonneg {d : ℕ} (M : Section3.ABKModel d) (s : { s : ℝ // 0 < s }) : 0 ≤ (√(Section3.Disorder.cstar M))⁻¹ * (↑s)⁻¹ * √M.gamma

The D₂ prefactor is nonnegative.

theorem Algsuperdiff.Section4.Provider.MinimalScale.dTwo_toReal_eq {d : ℕ} (M : Section3.ABKModel d) (s : { s : ℝ // 0 < s }) (k : ℤ) (omega : Section3.Cutoff.CutoffSample d) : (dTwo M s k omega).toReal = (√(Section3.Disorder.cstar M))⁻¹ * (↑s)⁻¹ * √M.gamma * gradInner M k omega

The real reading of D₂(k): the printed prefactor times D-s23's inner sum.

theorem Algsuperdiff.Section4.Provider.MinimalScale.dThree_toReal_le {d : ℕ} (M : Section3.ABKModel d) (s : { s : ℝ // 0 < s }) {n m : ℤ} {omega : Section3.Cutoff.CutoffSample d} (hfin : Proportion.wsumE (fun (r : ℕ) => hessHead M (↑s / 4) n m r) (fun (r : ℕ) => stepThreeWeight (↑s / 4) (r + 1)) omega ≠ ⊤) {k : ℤ} (hk : k ∈ Finset.Icc n m) : (dThree M s k omega).toReal ≤ (√(Section3.Disorder.cstar M))⁻¹ * (↑s)⁻¹ * √M.gamma * hessInner M (↑s / 4) k omega

The real reading of D₃(k), at the scales of a window where the Step-3 below-window channel converges.

5. The ℝ≥0∞ window average, converted to the real Cesàro averages

theorem Algsuperdiff.Section4.Provider.MinimalScale.window_avg_le_ofReal_cesaro {d : ℕ} (M : Section3.ABKModel d) (Ccg : ℝ) (s : { s : ℝ // 0 < s }) {n m : ℤ} (hnm : n ≤ m) {CD E : ℝ} (hCD : 0 ≤ CD) (hE : 0 ≤ E) {omega : Section3.Cutoff.CutoffSample d} (hdec : ∀ k ∈ Finset.Icc n m, (Support.goodEventBase M Ccg k s 1).indicator (fun (omega' : Section3.Cutoff.CutoffSample d) => Support.fluxCorrectedErrorObservableSup M k s omega') omega ≤ ENNReal.ofReal CD * (dOne M Ccg s k omega + dTwo M s k omega + dThree M s k omega + ENNReal.ofReal E)) (h1 : ∀ k ∈ Finset.Icc n m, dOne M Ccg s k omega ≠ ⊤) (h2 : ∀ k ∈ Finset.Icc n m, dTwo M s k omega ≠ ⊤) (h3 : ∀ k ∈ Finset.Icc n m, dThree M s k omega ≠ ⊤) : (↑(m - n).toNat + 1)⁻¹ * ∑ k ∈ Finset.Icc n m, (Support.goodEventBase M Ccg k s 1).indicator (fun (omega' : Section3.Cutoff.CutoffSample d) => Support.fluxCorrectedErrorObservableSup M k s omega') omega ≤ ENNReal.ofReal (CD * (Probability.cesaroAvg (fun (k : ℤ) => (dOne M Ccg s k omega).toReal) n m + Probability.cesaroAvg (fun (k : ℤ) => (dTwo M s k omega).toReal) n m + Probability.cesaroAvg (fun (k : ℤ) => (dThree M s k omega).toReal) n m + E))

The conversion step. Given the D-decomposition at every scale of the window and the finiteness of the three groups there, the frozen ℝ≥0∞ window average of the gated observable is below the ofReal of the real Cesàro sum. The window normaliser (((m−n).toNat : ℝ≥0∞) + 1)⁻¹ is exactly ofReal of cesaroAvg's own 1/(m−n+1).