StepOneGoodEvent

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

The Step-1 good-event bound and the kick collapse

ABK26, §4.2, Step 1 of l.minimal.scale.sep. Step 1 opens with a purely deterministic estimate off the good event:

∑_{i ≤ j−1} 3^{−½s(j−i)} max_{z ∈ 3^iℤ^d ∩ (□_j∖□_{j−1})} 𝓔_{s,2,2}(z+□_i;·)
    · 1_{𝒢(k;s,1)}
  ≤ C s^{−3/2} 3^{⅛s(k−j)} ,

then reads the printed two-leg display

… ≤ X_j^{(1)} + min{X_j^{(2)}, C s^{−3/2}3^{⅛s(k−j)}} ,

and collapses it into X_j = X_j^{(1)} + (Cs^{−9/2}X_j^{(2)})^{1/4}.

The exponent bookkeeping, honestly

There is in fact no Cauchy--Schwarz in the honest derivation, and the printed constant comes out exactly:

• 𝒢₂(k;s,1) reads s ∑_{j'≤k} ∑_{i≤j'−1} 3^{−¼s(k−i)} (max 𝓔)² ≤ 1; dropping all but ONE term gives, for every i ≤ j−1 ≤ k−1, the pointwise max 𝓔 ≤ s^{−1/2} 3^{⅛s(k−i)} — the 1/8 is the 1/4 halved by the square root of that single term, nothing else;
• summing against the §4.2 weight 3^{−½s(j−i)} and splitting 3^{⅛s(k−i)} = 3^{⅛s(k−j)}·3^{⅛s(j−i)} leaves the geometric series ∑_p 3^{−⅜s(p+1)} ≤ (1−3^{−⅜s})^{−1} ≤ 16/(3s) ≤ 6/s;
• hence the bound 6 s^{−3/2}3^{⅛s(k−j)} — the printed s^{−3/2} on the nose, at the explicit constant 6.

A Cauchy--Schwarz argument would give the sharper s^{−1}; it is not needed, and the crude termwise route is what reproduces the printed exponent, so the s^{−3/2} here is not a defect.

The collapse constant is explicit: 216 = 6³

With B := 6 s^{−3/2}3^{⅛s(k−j)} and W := 3^{−⅛s(k−j)} ≤ 1, the printed collapse needs W⁸B³ ≤ K for the coefficient K, and W⁸B³ = 216 s^{−9/2} W⁵ ≤ 216 s^{−9/2}. So K = 216 s^{−9/2} suffices, and any larger coefficient does too (kickCollapsed_le_mul_of_coeff_le).

Main results

• weighted_annularKick_le_kickCollapsed — the collapse step: the weighted inner sum at weight 3^{−½s(k−j)} is below 3^{−¼s(k−j)}·X_j.

References

• ABK26, l.minimal.scale.sep, Step 1; d.good.event.for.lambda, (𝒢₂).

1. weightThird algebra

theorem Algsuperdiff.Section4.Provider.MinimalScale.weightThird_add (a : ℝ) (m n : ℕ) : Proportion.weightThird a (m + n) = Proportion.weightThird a m * Proportion.weightThird a n

weightThird is multiplicative in the offset.

theorem Algsuperdiff.Section4.Provider.MinimalScale.weightThird_sq (a : ℝ) (n : ℕ) : Proportion.weightThird a n ^ 2 = Proportion.weightThird (2 * a) n

Squaring the weight doubles its rate.

theorem Algsuperdiff.Section4.Provider.MinimalScale.weightThird_pow_four (a : ℝ) (n : ℕ) : Proportion.weightThird a n ^ 4 = Proportion.weightThird (4 * a) n

Quadrupling the rate is the fourth power of the weight.

theorem Algsuperdiff.Section4.Provider.MinimalScale.weightThird_div_eq (a : ℝ) (n : ℕ) : Proportion.weightThird (4 * a) n * (Proportion.weightThird a n)⁻¹ = Proportion.weightThird (3 * a) n

The ratio of the Step-1 weight to the good-event growth factor is geometric at rate ⅜s: 3^{−½s·} · 3^{⅛s·} = 3^{−⅜s·}.

theorem Algsuperdiff.Section4.Provider.MinimalScale.weightThird_le_one {a : ℝ} (ha : 0 ≤ a) (n : ℕ) : Proportion.weightThird a n ≤ 1

theorem Algsuperdiff.Section4.Provider.MinimalScale.tsum_weightThird_succ_le {a : ℝ} (ha : 0 < a) : ∑' (p : ℕ), Proportion.weightThird a (p + 1) ≤ Probability.geomTailConst a

The geometric series of the shifted weights, at the closure constant.

theorem Algsuperdiff.Section4.Provider.MinimalScale.summable_weightThird_succ {a : ℝ} (ha : 0 < a) : Summable fun (p : ℕ) => Proportion.weightThird a (p + 1)

Summability of the shifted weights.

theorem Algsuperdiff.Section4.Provider.MinimalScale.three_rpow_eq_weightThird (a : ℝ) {x : ℤ} (hx : 0 ≤ x) : Real.rpow 3 (-(a * ↑x)) = Proportion.weightThird a x.toNat

The ℤ-offset rendering of the weight: at a nonnegative offset the anchor's 3^{−a·x} is weightThird a x.toNat.

2. The Finset maximum of the squares

theorem Algsuperdiff.Section4.Provider.MinimalScale.fmax_sq_le {iota : Type u_1} (S : Finset iota) (f : iota → ℝ) (hf : ∀ i ∈ S, 0 ≤ f i) : Proportion.fmax S f ^ 2 ≤ Proportion.fmax S fun (i : iota) => f i ^ 2

The square of a 0-floored maximum is below the maximum of the squares.

theorem Algsuperdiff.Section4.Provider.MinimalScale.kickAnnMax_sq_le_errorAnnMax {d : ℕ} (M : Section3.ABKModel d) (s : { s : ℝ // 0 < s }) (j i : ℤ) (omega : Section3.Cutoff.CutoffSample d) : kickAnnMax M s j i omega ^ 2 ≤ Proportion.errorAnnMax M s j i omega

The unsquared lattice maximum, squared, is below the §4.1 squared maximum. Both are 0-floored maxima of the same nonnegative atom over the same Finset.

3. The good-event bound

theorem Algsuperdiff.Section4.Provider.MinimalScale.kickAnnMax_le_of_mem_eventG2 {d : ℕ} (M : Section3.ABKModel d) (s : { s : ℝ // 0 < s }) {k j i : ℤ} (hjk : j ≤ k) (hij : i ≤ j - 1) {omega : Section3.Cutoff.CutoffSample d} (hmem : omega ∈ Support.eventG2 M k s 1) : kickAnnMax M s j i omega ≤ (√↑s)⁻¹ * (Proportion.weightThird (↑s / 8) (k - i).toNat)⁻¹

The Step-1 good-event bound, per inner scale. On 𝒢₂(k;s,1) every atom of the inner-scale sum obeys max 𝓔 ≤ s^{−1/2}3^{⅛s(k−i)}: a single term of the event's own double sum, square-rooted.

theorem Algsuperdiff.Section4.Provider.MinimalScale.annularKickE_le_of_mem_eventG2 {d : ℕ} (M : Section3.ABKModel d) (s : { s : ℝ // 0 < s }) {k j : ℤ} (hjk : j ≤ k) (hs1 : ↑s ≤ 1) {omega : Section3.Cutoff.CutoffSample d} (hmem : omega ∈ Support.eventG2 M k s 1) : annularKickE M s j omega ≤ ENNReal.ofReal (6 * (√↑s ^ 3)⁻¹ * (Proportion.weightThird (↑s / 8) (k - j).toNat)⁻¹)

The Step-1 good-event bound, in ℝ≥0∞. On 𝒢₂(k;s,1) the inner-scale sum is bounded by 6 s^{−3/2}3^{⅛s(k−j)} — the printed C s^{−3/2}3^{⅛s(k−j)} at the explicit constant C = 6. In particular the sum is on the good event; that finiteness is the source of every summability statement in the Step-1 assembly.

theorem Algsuperdiff.Section4.Provider.MinimalScale.annularKick_le_of_mem_eventG2 {d : ℕ} (M : Section3.ABKModel d) (s : { s : ℝ // 0 < s }) {k j : ℤ} (hjk : j ≤ k) (hs1 : ↑s ≤ 1) {omega : Section3.Cutoff.CutoffSample d} (hmem : omega ∈ Support.eventG2 M k s 1) : annularKick M s j omega ≤ 6 * (√↑s ^ 3)⁻¹ * (Proportion.weightThird (↑s / 8) (k - j).toNat)⁻¹

The real reading of the good-event bound.

4. The printed two-leg display and the collapse

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

y ≤ (x)^{1/4} from y⁴ ≤ x, in nested-root form.

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

The collapsed variable is monotone in its coefficient, up to the fourth root of the ratio. This is the one bookkeeping step that lets the collapse be read at the explicit coefficient 216 s^{−9/2} of the good-event bound while the Γ₂ tail and the first moment are supplied by exists_kickCollapse at its own coefficient.

theorem Algsuperdiff.Section4.Provider.MinimalScale.weighted_annularKick_le_kickCollapsed {d : ℕ} (M : Section3.ABKModel d) (s : { s : ℝ // 0 < s }) {k j : ℤ} {lam K : ℝ} (hlam : 0 ≤ lam) (hjk : j ≤ k) (hs1 : ↑s ≤ 1) (hK : 216 * (√↑s ^ 9)⁻¹ ≤ K) {omega : Section3.Cutoff.CutoffSample d} (hmem : omega ∈ Support.eventG2 M k s 1) : Proportion.weightThird (↑s / 2) (k - j).toNat * annularKick M s j omega ≤ Proportion.weightThird (↑s / 4) (k - j).toNat * kickCollapsed M s lam K j omega

The collapse step. On the good event, the Step-1 inner sum at the §4.2 weight 3^{−½s(k−j)} is below the collapsed variable at the quarter weight 3^{−¼s(k−j)}:

3^{−½s(k−j)} · annularKick_j  ≤  3^{−¼s(k−j)} · X_j ,
   X_j = X_j^{(1)} + (K X_j^{(2)})^{1/4} ,   K ≥ 216 s^{−9/2} .

The exponent bookkeeping is the printed one: −½ + ⅜·¾ = −13/32 ≤ −¼, here in the equivalent form W⁸B³ ≤ K with W = 3^{−⅛s(k−j)} ≤ 1 and B the good-event bound. The threshold 216 = 6³ is the cube of the good-event constant.