IndicatorArray

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

The column-only Appendix-D array and its two probabilistic hypotheses

ABK26, Appendix D (p.concentration.for.scales) and §4.1 (the three ratio lemmas). Proposition p.concentration.for.scales consumes a two-index array together with two probabilistic hypotheses,

• hmomL : ∀ k j, ∫⁻ ω.ofReal ((X k j ω) ^ p) ∂P ≤ 1 (e.Xk.p.moment.twosided),
• hindep : ColumnsIndep r (e.independent.columns.twosided).

This module supplies the carrier-neutral machinery that produces both from a sequence of per-scale atoms with a Γ_σ upper tail.

The array is column-only

In each of the three ratio lemmas the array fed to p.concentration.for.scales is a single sequence of per-scale atoms, constant along the row index: for 𝒢₀ it is X_{k,n} = 𝒴_n, and the row sum is Y_k = ∑_n 3^{-¼γ|k-n|} 𝒴_n. The two Appendix-D hypotheses then read: unit p-th moments of the atoms, and r-dependence of the atom sequence. colArray is that embedding.

The moment route

A Γ_σ upper tail with scale K gives E[Y^p]^{1/p} ≤ gammaMomentConst σ · p^{1/σ} · K (CoarseGraining lintegral_rpow_le_of_isBigOWith_gammaSigma); normalizing the atom by any D above that constant delivers the unit moment ∫⁻ (Y/D)^p ≤ 1. This is the paper's "by taking p := exp(K⁻¹c⋆²γ⁻¹) with K(d) large enough we obtain E[𝒴ⁿ_p] ≤ 1".

Scope

Provider material: carrier-neutral local helpers over an abstract probability space. The Γ_σ tails, the nonnegativity/measurability of the atoms, and the residue-class independence enter as conditional A hypotheses; no ABK carrier, model, or standing assumption is used. No sorry, no custom axioms, no set_option maxHeartbeats.

The column-only Appendix-D array

def Algsuperdiff.Section4.Probability.IndicatorDensity.colArray {Ω : Type u_1} (Y : ℤ → Ω → ℝ) : ℤ → ℤ → Ω → ℝ

The Appendix-D array of a sequence of per-scale atoms, X_{k,j} = Y_j. This is the array shape of all three ratio lemmas: the row index only selects the geometric weight, the randomness lives in the columns.

Equations

• Algsuperdiff.Section4.Probability.IndicatorDensity.colArray Y x✝ j ω = Y j ω

@[simp]

theorem Algsuperdiff.Section4.Probability.IndicatorDensity.colArray_apply {Ω : Type u_1} (Y : ℤ → Ω → ℝ) (k j : ℤ) (ω : Ω) : colArray Y k j ω = Y j ω

theorem Algsuperdiff.Section4.Probability.IndicatorDensity.Yk_colArray {Ω : Type u_1} (Y : ℤ → Ω → ℝ) (s : ℝ) (k : ℤ) (ω : Ω) : ScalesConcentration.Yk (colArray Y) s k ω = ∑' (j : ℤ), ScalesConcentration.wt s k j * Y j ω

theorem Algsuperdiff.Section4.Probability.IndicatorDensity.Yk_colArray_const_mul {Ω : Type u_1} (Y : ℤ → Ω → ℝ) (c s : ℝ) (k : ℤ) (ω : Ω) : ScalesConcentration.Yk (colArray fun (j : ℤ) (ω : Ω) => c * Y j ω) s k ω = c * ScalesConcentration.Yk (colArray Y) s k ω

The weighted row sum is homogeneous in the atoms.

hmomL — unit p-th moments from a Γ_σ tail

The Appendix-D moment hypothesis in its honest ∫⁻ reading (see the module docstring of ScalesConcentration/Statement.lean).

theorem Algsuperdiff.Section4.Probability.IndicatorDensity.isBigOWith_const_mul {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {Ψ : ℝ → ℝ} {X : Ω → ℝ} {A c : ℝ} (hc : 0 < c) (h : HCPolySupport.IndependentSums.IsBigOWith μ Ψ X A) : HCPolySupport.IndependentSums.IsBigOWith μ Ψ (fun (ω : Ω) => c * X ω) (c * A)

Scaling of the weak-Orlicz upper-tail relation. X = O_Ψ(A) implies cX = O_Ψ(cA) for c > 0: the tail events coincide.

theorem Algsuperdiff.Section4.Probability.IndicatorDensity.lintegral_rpow_le_one_of_isBigOWith {Ω : Type u_1} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {Y : Ω → ℝ} {σ p K : ℝ} (hσ : 0 < σ) (hK : 0 < K) (hp : 1 ≤ p) (hYnn : ∀ (ω : Ω), 0 ≤ Y ω) (hYm : AEMeasurable Y P) (hY : HCPolySupport.IndependentSums.IsBigOWith P (HCPolySupport.IndependentSums.gammaSigma σ) Y K) (hsmall : HCPolySupport.IndependentSums.gammaMomentConst σ * p ^ σ⁻¹ * K ≤ 1) : ∫⁻ (ω : Ω), ENNReal.ofReal (Y ω ^ p) ∂P ≤ 1

Unit p-th moment from a Γ_σ tail (the hmomL engine). A nonnegative random variable with a stretched-exponential upper tail at scale K satisfies the Appendix-D moment hypothesis ∫⁻ Y^p ≤ 1 as soon as the moment-growth constant gammaMomentConst σ · p^{1/σ} · K is at most 1.

This is the Lean rendering of the paper's "by taking p := exp(K⁻¹c⋆²γ⁻¹) with K(d) large enough, we obtain E[𝒴ⁿ_p] ≤ 1".

theorem Algsuperdiff.Section4.Probability.IndicatorDensity.lintegral_rpow_le_one_of_array {Ω : Type u_1} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {Y : ℤ → ℤ → Ω → ℝ} {σ p K D : ℝ} (hσ : 0 < σ) (hK : 0 < K) (hp : 1 ≤ p) (hD : 0 < D) (hYnn : ∀ (m j : ℤ) (ω : Ω), 0 ≤ Y m j ω) (hYm : ∀ (m j : ℤ), AEMeasurable (Y m j) P) (hY : ∀ (m j : ℤ), HCPolySupport.IndependentSums.IsBigOWith P (HCPolySupport.IndependentSums.gammaSigma σ) (Y m j) K) (hnorm : HCPolySupport.IndependentSums.gammaMomentConst σ * p ^ σ⁻¹ * K ≤ D) (m j : ℤ) : ∫⁻ (ω : Ω), ENNReal.ofReal ((D⁻¹ * Y m j ω) ^ p) ∂P ≤ 1

hmomL for an arbitrary (two-index) Appendix-D array. Normalizing entries with a common Γ_σ tail scale K by any D ≥ gammaMomentConst σ · p^{1/σ}·K yields the Appendix-D unit-moment hypothesis for X_{m,k} = D⁻¹ Y_{m,k}. Stated at the two-index shape because not every §4.1 lane has a column-only array; the column-only case is the instance below.

theorem Algsuperdiff.Section4.Probability.IndicatorDensity.colArray_lintegral_rpow_le_one {Ω : Type u_1} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {Y : ℤ → Ω → ℝ} {σ p K D : ℝ} (hσ : 0 < σ) (hK : 0 < K) (hp : 1 ≤ p) (hD : 0 < D) (hYnn : ∀ (j : ℤ) (ω : Ω), 0 ≤ Y j ω) (hYm : ∀ (j : ℤ), AEMeasurable (Y j) P) (hY : ∀ (j : ℤ), HCPolySupport.IndependentSums.IsBigOWith P (HCPolySupport.IndependentSums.gammaSigma σ) (Y j) K) (hnorm : HCPolySupport.IndependentSums.gammaMomentConst σ * p ^ σ⁻¹ * K ≤ D) (k j : ℤ) : ∫⁻ (ω : Ω), ENNReal.ofReal (colArray (fun (n : ℤ) (ω : Ω) => D⁻¹ * Y n ω) k j ω ^ p) ∂P ≤ 1

hmomL for the column array. The column-only instance of lintegral_rpow_le_one_of_array.

hindep — ColumnsIndep for a column-only array

theorem Algsuperdiff.Section4.Probability.IndicatorDensity.columnsIndep_colArray {Ω : Type u_1} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} (Y : ℤ → Ω → ℝ) (r : ℕ) (h : ∀ (b : ℤ), ProbabilityTheory.iIndepFun (fun (j : ℤ) => Y (j * ↑r + b)) P) : ScalesConcentration.ColumnsIndep P (colArray Y) r

ColumnsIndep for a column-only array reduces to independence of the atoms within each residue class. A column of colArray Y is the constant-in-k (ℤ → ℝ)-valued random variable ω ↦ (fun _ => Y_j ω), a measurable image of the atom Y_j; iIndepFun.comp transports mutual independence.