ShiftedConcentration

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

Re-basing the Appendix-D concentration engine at an arbitrary scale m₀

ABK26, Appendix D (p.concentration.for.scales) and §4.1. The proved Proposition ScalesConcentration.p_concentration_for_scales_Cstar is stated for the window {0,…,m}; the manuscript's own reduction is "translate the array". This module carries out that translation, once and generically, so that no lane has to redo it.

Contents

• shiftArray m₀ X — the re-based array X'_{k,j} = X_{k+m₀, j+m₀}. Both indices move: the row index because the window moves, the column index because the Appendix-D weight wt s k j = 3^{-s|k-j|} is difference-only, so only the diagonal translation preserves the row sums. (Translating the row index alone — the phrasing in the proved module docstring — does not preserve Y_k; see Yk_shiftArray.)
• Yk_shiftArray — Y_k(X') = Y_{k+m₀}(X), by re-indexing the two-sided tsum with Equiv.addRight m₀.
• columnsIndep_shiftArray — ColumnsIndep transfers: the residue class b of the shifted array is the residue class b + m₀ of the original, read through the measurable relabelling g ↦ (k ↦ g (k + m₀)) of ℤ → ℝ.
• ratioTail_of_concentration_shift — the reusable endpoint: the proved IndicatorDensity.ratioTail_of_concentration at the window {m₀,…,m₀+n}. Its hypothesis list is identical to the base-0 one except that the deterministic reduction is asked at every scale m : ℤ instead of only at m ≥ 0 — which is what all three §4.1 lanes in fact prove (their 0 ≤ m binders are unused).
• scalePropFrom and scalePropFrom_eq_scaleProp — the window re-index: the Finset.range (Mw+1)-indexed average of Set.indicators at the scales m₀ + k, in which the frozen proportion display is written, is the proved Finset.Icc-indexed scaleProp of the shifted family.

References

• ABK26, p.concentration.for.scales, (the m₀ reduction); p.independence.between.scales.
• Also.

1. The re-based array and its row sums

def Algsuperdiff.Section4.Provider.Proportion.shiftArray {Ω : Type u_1} (m0 : ℤ) (X : ℤ → ℤ → Ω → ℝ) : ℤ → ℤ → Ω → ℝ

The Appendix-D array re-based at m₀, X'_{k,j} = X_{k+m₀, j+m₀}.

Equations

• Algsuperdiff.Section4.Provider.Proportion.shiftArray m0 X k j omega = X (k + m0) (j + m0) omega

@[simp]

theorem Algsuperdiff.Section4.Provider.Proportion.shiftArray_apply {Ω : Type u_1} (m0 : ℤ) (X : ℤ → ℤ → Ω → ℝ) (k j : ℤ) (omega : Ω) : shiftArray m0 X k j omega = X (k + m0) (j + m0) omega

theorem Algsuperdiff.Section4.Provider.Proportion.idist_add_right (k j m0 : ℤ) : Probability.ScalesConcentration.idist (k + m0) (j + m0) = Probability.ScalesConcentration.idist k j

The Appendix-D index distance is translation invariant.

theorem Algsuperdiff.Section4.Provider.Proportion.wt_add_right (s : ℝ) (k j m0 : ℤ) : Probability.ScalesConcentration.wt s (k + m0) (j + m0) = Probability.ScalesConcentration.wt s k j

The Appendix-D weight 3^{-s|k-j|} is difference-only, hence translation invariant. This is the fact that forces the diagonal shift.

theorem Algsuperdiff.Section4.Provider.Proportion.Yk_shiftArray {Ω : Type u_1} (X : ℤ → ℤ → Ω → ℝ) (s : ℝ) (m0 k : ℤ) (omega : Ω) : Probability.ScalesConcentration.Yk (shiftArray m0 X) s k omega = Probability.ScalesConcentration.Yk X s (k + m0) omega

The re-based row sum is the original row sum at the shifted scale. The tsum over ℤ is re-indexed by Equiv.addRight m₀, and the weight is translation invariant.

2. The window re-index

The frozen §4.1 proportion display averages Set.indicators of the events at the scales m₀ + k over k ∈ Finset.range (Mw+1). The proved scaleProp averages if-indicators over m ∈ Finset.Icc (0:ℤ) (Mw:ℤ). The two are the same number.

theorem Algsuperdiff.Section4.Provider.Proportion.sum_Icc_zero_eq_sum_range {A : Type u_2} [AddCommMonoid A] (f : ℤ → A) (n : ℕ) : ∑ m ∈ Finset.Icc 0 ↑n, f m = ∑ k ∈ Finset.range (n + 1), f ↑k

The integer window {0,…,n} re-indexed by Finset.range (n+1).

noncomputable def Algsuperdiff.Section4.Provider.Proportion.scalePropFrom {Ω : Type u_1} (Ev : ℤ → Set Ω) (m0 : ℤ) (Mw : ℕ) (omega : Ω) : ℝ

The proportion of scales in the window {m₀,…,m₀+Mw}, in the frozen display's own form: the Finset.range (Mw+1)-indexed average of the Set.indicators of Ev (m₀ + k).

Equations

• Algsuperdiff.Section4.Provider.Proportion.scalePropFrom Ev m0 Mw omega = 1 / (↑Mw + 1) * ∑ k ∈ Finset.range (Mw + 1), (Ev (m0 + ↑k)).indicator (fun (x : Ω) => 1) omega

theorem Algsuperdiff.Section4.Provider.Proportion.scalePropFrom_eq_scaleProp {Ω : Type u_1} (Ev : ℤ → Set Ω) (m0 : ℤ) (Mw : ℕ) (omega : Ω) : scalePropFrom Ev m0 Mw omega = Probability.IndicatorDensity.scaleProp (fun (k : ℤ) => Ev (m0 + k)) Mw omega

The window re-index. The frozen display's Finset.range-indexed indicator average at base m₀ is the proved Finset.Icc-indexed scaleProp of the shifted family.

3. Transport of the independence hypothesis

theorem Algsuperdiff.Section4.Provider.Proportion.columnsIndep_shiftArray {Ω : Type u_1} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} {X : ℤ → ℤ → Ω → ℝ} {r : ℕ} (m0 : ℤ) (h : Probability.ScalesConcentration.ColumnsIndep P X r) : Probability.ScalesConcentration.ColumnsIndep P (shiftArray m0 X) r

ColumnsIndep is stable under the diagonal shift. The residue-b class of the shifted array is the residue-(b+m₀) class of the original, composed with the relabelling g ↦ (k ↦ g (k+m₀)) of ℤ → ℝ, which is measurable; mutual independence is preserved by iIndepFun.comp.

4. The re-based ratio-tail endpoint

theorem Algsuperdiff.Section4.Provider.Proportion.ratioTail_of_concentration_shift {Ω : Type u_1} [MeasurableSpace Ω] (P : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure P] (X : ℤ → ℤ → Ω → ℝ) {p s' theta c1 Q : ℝ} {r : ℕ} (Ev : ℤ → Set Ω) (m0 : ℤ) (hp : 1 ≤ p) (hs' : 0 < s') (hs'1 : s' ≤ 1) (hsp : 1 ≤ s' * p) (hr1 : 1 ≤ r) (hXmeas : ∀ (k j : ℤ), Measurable (X k j)) (hXnn : ∀ (k j : ℤ) (omega : Ω), 0 ≤ X k j omega) (hmomL : ∀ (k j : ℤ), ∫⁻ (omega : Ω), ENNReal.ofReal (X k j omega ^ p) ∂P ≤ 1) (hindep : Probability.ScalesConcentration.ColumnsIndep P X r) (hQ : 1 ≤ Q) (htheta0 : 0 < theta) (hthetar : theta * (↑r + 1) < 1) (hc1 : 0 ≤ c1) (hrate : Real.log (Q * ↑r) + c1 * ↑r ≤ s' * p * theta / (16 * ↑r)) (hreduce : ∀ (m : ℤ), ∀ omega ∈ (Ev m)ᶜ, 9 * s'⁻¹ * Probability.ScalesConcentration.Cstar ^ (1 / p) * theta ^ (-1 / p) < Probability.ScalesConcentration.Yk X s' m omega) (n : ℕ) : P {omega : Ω | theta < Probability.IndicatorDensity.scaleProp (fun (k : ℤ) => (Ev (m0 + k))ᶜ) n omega} ≤ ENNReal.ofReal (Real.exp (-c1 * ↑n) / Q)

The §4.1 ratio-tail endpoint at an arbitrary base scale m₀.

Given, for one array X and one event family Ev, the four Appendix-D hypotheses, the parameter conditions of the proved IndicatorDensity.ratioTail_of_concentration, and the deterministic reduction hreduce at every scale m : ℤ, the density of scales in the window {m₀,…,m₀+n} at which Ev fails obeys

ℙ[ θ < density of bad scales over {m₀,…,m₀+n} ] ≤ exp(−c₁n)/Q

for every n : ℕ, including the short windows n < r that p.concentration.for.scales does not itself reach (covered inside the proved ratioTail_of_concentration).

The proof is the diagonal translation of the array: Y_k(X') = Y_{k+m₀}(X), ColumnsIndep transports, and the three remaining Appendix-D hypotheses are per-entry, hence transport entrywise.