BlockConcentration

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

Concentration for independent sums with geometrically growing scales

ABK26's stream estimate e.k.ell.upscales applies the concentration proposition p.concentration to the family {j_k(0)}_{k ∈ (n, m]}, whose scales 3^{γk} are not uniform, and reads off the ℓ²-aggregated amplitude

(∑_{k ∈ (n, m]} 3^{2γk})^{1/2} ≤ C min{γ^{-1/2}, (m-n)^{1/2}} 3^{γm}.

The concentration proposition available in CoarseGraining, Homogenization.Book.Ch04.isBigO_gammaSigma_finset_sum_of_iIndepFun_of_isBigO_of_integral_eq_zero, is stated at a uniform scale K with amplitude C √N K. Used with K = 3^{γm} it produces C (m-n)^{1/2} 3^{γm}, which is the correct answer exactly when m - n ≤ γ^{-1} and is lossy beyond that.

This module supplies the missing regime by the standard blocking argument, using only proved tools: split (n, m] into consecutive blocks of width r = ⌈γ^{-1}⌉, apply the uniform concentration on each block at its own largest scale, and recombine with the generalized triangle inequality Homogenization.IndependentSums.isBigO_finset_sum_of_isBigO_gammaSigma. Since γ r ≥ 1, the block amplitudes C √r 3^{γ(m - jr)} decay at least geometrically with ratio 1/3, so their sum is at most (3/2) C √r 3^{γm}, and √r ≤ √2 γ^{-1/2}.

Nothing here refers to the ABK model: the statements are about an arbitrary independent centered family with Γ₂ tails at the scales 3^{γk}.

Main definitions

• Algsuperdiff.Section3.Provider.Stream.geometricBlockWidth
• Algsuperdiff.Section3.Provider.Stream.geometricBlockEnd
• Algsuperdiff.Section3.Provider.Stream.geometricConcentrationConst

Main results

• isBigO_gammaSigma_two_sum_Ioc_of_card: the uniform-scale branch, with amplitude C (m-n)^{1/2} 3^{γm}.
• isBigO_gammaSigma_two_sum_Ioc_of_inv_gamma: the blocked branch, with amplitude C γ^{-1/2} 3^{γm}.
• isBigO_gammaSigma_two_sum_Ioc_geometric: the combined estimate with the source's min{γ^{-1/2}, (m-n)^{1/2}} amplitude.

References

• ABK26, e.k.ell.upscales.
• ABK26, Proposition p.concentration.
• ABK26, Lemma l.Gamma.sigma.triangle.

Elementary preliminaries

theorem Algsuperdiff.Section3.Provider.Stream.sum_Ioc_consecutive_int {M : Type u_2} [AddCommMonoid M] (f : ℤ → M) {a b c : ℤ} (hab : a ≤ b) (hbc : b ≤ c) : ∑ i ∈ Finset.Ioc a b, f i + ∑ i ∈ Finset.Ioc b c, f i = ∑ i ∈ Finset.Ioc a c, f i

Consecutive half-open integer intervals split a sum. This is the integer analogue of Finset.sum_Ioc_consecutive, which Mathlib states only for ℕ.

theorem Algsuperdiff.Section3.Provider.Stream.sum_range_geom_third_le (J : ℕ) : ∑ j ∈ Finset.range J, (1 / 3) ^ j ≤ 3 / 2

The truncated geometric series with ratio 1/3.

theorem Algsuperdiff.Section3.Provider.Stream.isBigO_gammaSigma_zero_fun {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {A sigma : ℝ} (hA : 0 ≤ A) : HCPolySupport.IndependentSums.IsBigO μ (HCPolySupport.IndependentSums.gammaSigma sigma) (fun (x : Ω) => 0) A

The identically zero random variable satisfies every nonnegative weak-Orlicz bound.

theorem Algsuperdiff.Section3.Provider.Stream.gammaSigmaIndependentSumConst_two_pos : 0 < HCPolySupport.Book.Ch04.gammaSigmaIndependentSumConst 2

The σ = 2 instance of CoarseGraining's concentration constant is positive.

Blocks

noncomputable def Algsuperdiff.Section3.Provider.Stream.geometricBlockWidth (gamma : ℝ) : ℕ

The block width ⌈γ⁻¹⌉ used to split (n, m] into consecutive blocks on which the geometric amplitudes 3^{γk} are comparable. Since γ ⌈γ⁻¹⌉ ≥ 1, consecutive block amplitudes decay by at least a factor 3.

Equations

• Algsuperdiff.Section3.Provider.Stream.geometricBlockWidth gamma = ⌈gamma⁻¹⌉₊

noncomputable def Algsuperdiff.Section3.Provider.Stream.geometricBlockEnd (gamma : ℝ) (n m : ℤ) (j : ℕ) : ℤ

The right endpoint of the j-th block of (n, m], counted downwards from m. The truncation at n makes all sufficiently late blocks empty.

Equations

• Algsuperdiff.Section3.Provider.Stream.geometricBlockEnd gamma n m j = max n (m - ↑j * ↑(Algsuperdiff.Section3.Provider.Stream.geometricBlockWidth gamma))

theorem Algsuperdiff.Section3.Provider.Stream.geometricBlockEnd_eq (gamma : ℝ) (n m : ℤ) (j : ℕ) : geometricBlockEnd gamma n m j = max n (m - ↑j * ↑(geometricBlockWidth gamma))

theorem Algsuperdiff.Section3.Provider.Stream.geometricBlockWidth_pos {gamma : ℝ} (hgamma : 0 < gamma) : 0 < geometricBlockWidth gamma

theorem Algsuperdiff.Section3.Provider.Stream.one_le_gamma_mul_geometricBlockWidth {gamma : ℝ} (hgamma : 0 < gamma) : 1 ≤ gamma * ↑(geometricBlockWidth gamma)

theorem Algsuperdiff.Section3.Provider.Stream.geometricBlockWidth_le_two_mul_inv {gamma : ℝ} (hgamma : 0 < gamma) (hquarter : gamma ≤ 1 / 4) : ↑(geometricBlockWidth gamma) ≤ 2 * gamma⁻¹

theorem Algsuperdiff.Section3.Provider.Stream.geometricBlockEnd_antitone (gamma : ℝ) (n m : ℤ) : Antitone (geometricBlockEnd gamma n m)

theorem Algsuperdiff.Section3.Provider.Stream.geometricBlockEnd_zero {gamma : ℝ} {n m : ℤ} (hnm : n ≤ m) : geometricBlockEnd gamma n m 0 = m

theorem Algsuperdiff.Section3.Provider.Stream.geometricBlockEnd_toNat {gamma : ℝ} (hgamma : 0 < gamma) {n m : ℤ} (hnm : n ≤ m) : geometricBlockEnd gamma n m (m - n).toNat = n

The per-block estimate

theorem Algsuperdiff.Section3.Provider.Stream.isBigO_gammaSigma_two_geometricBlock {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ℤ → Ω → ℝ} {gamma : ℝ} {n m : ℤ} (j : ℕ) (hgamma : 0 < gamma) (h_indep : ProbabilityTheory.iIndepFun X μ) (h_meas : ∀ (k : ℤ), Measurable (X k)) (hX : ∀ (k : ℤ), HCPolySupport.IndependentSums.IsBigO μ (HCPolySupport.IndependentSums.gammaSigma 2) (X k) (3 ^ (gamma * ↑k))) (h_mean : ∀ (k : ℤ), ∫ (omega : Ω), X k omega ∂μ = 0) : HCPolySupport.IndependentSums.IsBigO μ (HCPolySupport.IndependentSums.gammaSigma 2) (fun (omega : Ω) => ∑ k ∈ Finset.Ioc (geometricBlockEnd gamma n m (j + 1)) (geometricBlockEnd gamma n m j), X k omega) (HCPolySupport.Book.Ch04.gammaSigmaIndependentSumConst 2 * √↑(geometricBlockWidth gamma) * 3 ^ (gamma * (↑m - ↑j * ↑(geometricBlockWidth gamma))))

Each block of (n, m] obeys the uniform-scale concentration estimate at its own largest amplitude 3^{γ(m - jr)}, with at most r summands.

Telescoping the blocks

theorem Algsuperdiff.Section3.Provider.Stream.sum_geometricBlocks {Ω : Type u_1} (gamma : ℝ) (n m : ℤ) (X : ℤ → Ω → ℝ) (omega : Ω) (J : ℕ) : ∑ j ∈ Finset.range J, ∑ k ∈ Finset.Ioc (geometricBlockEnd gamma n m (j + 1)) (geometricBlockEnd gamma n m j), X k omega = ∑ k ∈ Finset.Ioc (geometricBlockEnd gamma n m J) (geometricBlockEnd gamma n m 0), X k omega

The blocks of (n, m] exhaust the interval.

The two branches

theorem Algsuperdiff.Section3.Provider.Stream.isBigO_gammaSigma_two_sum_Ioc_of_card {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ℤ → Ω → ℝ} {gamma : ℝ} {n m : ℤ} (hgamma : 0 < gamma) (hnm : n < m) (h_indep : ProbabilityTheory.iIndepFun X μ) (h_meas : ∀ (k : ℤ), Measurable (X k)) (hX : ∀ (k : ℤ), HCPolySupport.IndependentSums.IsBigO μ (HCPolySupport.IndependentSums.gammaSigma 2) (X k) (3 ^ (gamma * ↑k))) (h_mean : ∀ (k : ℤ), ∫ (omega : Ω), X k omega ∂μ = 0) : HCPolySupport.IndependentSums.IsBigO μ (HCPolySupport.IndependentSums.gammaSigma 2) (fun (omega : Ω) => ∑ k ∈ Finset.Ioc n m, X k omega) (HCPolySupport.Book.Ch04.gammaSigmaIndependentSumConst 2 * √(↑m - ↑n) * 3 ^ (gamma * ↑m))

The uniform-scale branch of ABK26's e.k.ell.upscales: applying the concentration proposition at the single largest scale 3^{γm} gives the amplitude C (m-n)^{1/2} 3^{γm}.

theorem Algsuperdiff.Section3.Provider.Stream.isBigO_gammaSigma_two_sum_Ioc_of_inv_gamma {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ℤ → Ω → ℝ} {gamma : ℝ} {n m : ℤ} (hgamma : 0 < gamma) (hquarter : gamma ≤ 1 / 4) (hnm : n < m) (h_indep : ProbabilityTheory.iIndepFun X μ) (h_meas : ∀ (k : ℤ), Measurable (X k)) (hX : ∀ (k : ℤ), HCPolySupport.IndependentSums.IsBigO μ (HCPolySupport.IndependentSums.gammaSigma 2) (X k) (3 ^ (gamma * ↑k))) (h_mean : ∀ (k : ℤ), ∫ (omega : Ω), X k omega ∂μ = 0) : HCPolySupport.IndependentSums.IsBigO μ (HCPolySupport.IndependentSums.gammaSigma 2) (fun (omega : Ω) => ∑ k ∈ Finset.Ioc n m, X k omega) (3 * HCPolySupport.IndependentSums.gammaTriangleConst 2 * HCPolySupport.Book.Ch04.gammaSigmaIndependentSumConst 2 * √gamma⁻¹ * 3 ^ (gamma * ↑m))

The blocked branch of ABK26's e.k.ell.upscales: splitting (n, m] into blocks of width ⌈γ^{-1}⌉ and summing the block estimates with the generalized triangle inequality gives the amplitude C γ^{-1/2} 3^{γm}, with no dependence on m - n.

The combined estimate

noncomputable def Algsuperdiff.Section3.Provider.Stream.geometricConcentrationConst : ℝ

The explicit universal constant of ABK26's e.k.ell.upscales.

Equations

• Algsuperdiff.Section3.Provider.Stream.geometricConcentrationConst = HCPolySupport.Book.Ch04.gammaSigmaIndependentSumConst 2 * (1 + 3 * HCPolySupport.IndependentSums.gammaTriangleConst 2)

theorem Algsuperdiff.Section3.Provider.Stream.geometricConcentrationConst_eq : geometricConcentrationConst = HCPolySupport.Book.Ch04.gammaSigmaIndependentSumConst 2 * (1 + 3 * HCPolySupport.IndependentSums.gammaTriangleConst 2)

theorem Algsuperdiff.Section3.Provider.Stream.geometricConcentrationConst_pos : 0 < geometricConcentrationConst

theorem Algsuperdiff.Section3.Provider.Stream.isBigO_gammaSigma_two_sum_Ioc_geometric {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ℤ → Ω → ℝ} {gamma : ℝ} {n m : ℤ} (hgamma : 0 < gamma) (hquarter : gamma ≤ 1 / 4) (hnm : n < m) (h_indep : ProbabilityTheory.iIndepFun X μ) (h_meas : ∀ (k : ℤ), Measurable (X k)) (hX : ∀ (k : ℤ), HCPolySupport.IndependentSums.IsBigO μ (HCPolySupport.IndependentSums.gammaSigma 2) (X k) (3 ^ (gamma * ↑k))) (h_mean : ∀ (k : ℤ), ∫ (omega : Ω), X k omega ∂μ = 0) : HCPolySupport.IndependentSums.IsBigO μ (HCPolySupport.IndependentSums.gammaSigma 2) (fun (omega : Ω) => ∑ k ∈ Finset.Ioc n m, X k omega) (geometricConcentrationConst * min √gamma⁻¹ √(↑m - ↑n) * 3 ^ (gamma * ↑m))

ABK26's e.k.ell.upscales in abstract form: for an independent centered family with Γ₂ tails at the geometric scales 3^{γk},

∑_{k ∈ (n, m]} X_k = O_{Γ₂}(C min{γ^{-1/2}, (m-n)^{1/2}} 3^{γm}).

The source obtains this amplitude by evaluating the ℓ² aggregate (∑_{k ∈ (n,m]} 3^{2γk})^{1/2} through e.geo.part.sum; the proof here instead splits (n, m] into ⌈γ^{-1}⌉-wide blocks, so that only the uniform-scale concentration proposition and the generalized triangle inequality are used. The constant is explicit and universal.