Coarse-graining support: Support.Probability.IndependentSums.WeakOrlicz

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

Weak-Orlicz tail notation for the independent-sums probability mini-library.

This file follows the Chapter 4 note-facing convention directly:

• X ≤ O_Ψ(A) means P[X > A t] ≤ Ψ(t)⁻¹ for every t ≥ 1;
• X = O_Ψ(A) means the same bound for |X|;
• Γ_σ and Ψ_σ are the stretched-exponential and log-normal model classes.

The definitions are intentionally tail-based rather than Banach-space based: the notes use a weak-tail calculus, and this is the theorem surface needed for the later concentration arguments.

def HCPolySupport.IndependentSums.upperTailEvent {Ω : Type u_1} (X : Ω → ℝ) (a : ℝ) : Set Ω

The upper-tail event {X > a}.

Equations

• HCPolySupport.IndependentSums.upperTailEvent X a = {ω : Ω | a < X ω}

def HCPolySupport.IndependentSums.absTailEvent {Ω : Type u_1} (X : Ω → ℝ) (a : ℝ) : Set Ω

The absolute upper-tail event {|X| > a}.

Equations

• HCPolySupport.IndependentSums.absTailEvent X a = HCPolySupport.IndependentSums.upperTailEvent (fun (ω : Ω) => |X ω|) a

@[simp]

theorem HCPolySupport.IndependentSums.mem_upperTailEvent {Ω : Type u_1} {X : Ω → ℝ} {a : ℝ} {ω : Ω} : ω ∈ upperTailEvent X a ↔ a < X ω

@[simp]

theorem HCPolySupport.IndependentSums.mem_absTailEvent {Ω : Type u_1} {X : Ω → ℝ} {a : ℝ} {ω : Ω} : ω ∈ absTailEvent X a ↔ a < |X ω|

theorem HCPolySupport.IndependentSums.upperTailEvent_mono_right {Ω : Type u_1} {X : Ω → ℝ} {a b : ℝ} (hab : a ≤ b) : upperTailEvent X b ⊆ upperTailEvent X a

theorem HCPolySupport.IndependentSums.absTailEvent_mono_right {Ω : Type u_1} {X : Ω → ℝ} {a b : ℝ} (hab : a ≤ b) : absTailEvent X b ⊆ absTailEvent X a

def HCPolySupport.IndependentSums.IsBigOWith {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (Ψ : ℝ → ℝ) (X : Ω → ℝ) (A : ℝ) : Prop

The weak-Orlicz upper-tail relation X ≤ O_Ψ(A) from the notes.

Equations

• HCPolySupport.IndependentSums.IsBigOWith μ Ψ X A = ∀ ⦃t : ℝ⦄, 1 ≤ t → μ.real (HCPolySupport.IndependentSums.upperTailEvent X (A * t)) ≤ (Ψ t)⁻¹

def HCPolySupport.IndependentSums.IsBigO {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (Ψ : ℝ → ℝ) (X : Ω → ℝ) (A : ℝ) : Prop

The symmetric weak-Orlicz relation X = O_Ψ(A), defined through |X|.

Equations

• HCPolySupport.IndependentSums.IsBigO μ Ψ X A = HCPolySupport.IndependentSums.IsBigOWith μ Ψ (fun (ω : Ω) => |X ω|) A

def HCPolySupport.IndependentSums.AdmissiblePsi (Ψ : ℝ → ℝ) : Prop

The baseline regularity package for a weak-Orlicz tail function: monotonicity on [0, ∞) and the lower bound Ψ ≥ 1 there.

Equations

• HCPolySupport.IndependentSums.AdmissiblePsi Ψ = (MonotoneOn Ψ (Set.Ici 0) ∧ ∀ ⦃t : ℝ⦄, 0 ≤ t → 1 ≤ Ψ t)

theorem HCPolySupport.IndependentSums.IsBigOWith.of_le {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {Ψ : ℝ → ℝ} {X Y : Ω → ℝ} {A : ℝ} (hX : IsBigOWith μ Ψ X A) (hYX : ∀ (ω : Ω), Y ω ≤ X ω) : IsBigOWith μ Ψ Y A

theorem HCPolySupport.IndependentSums.IsBigO.of_abs_le {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {Ψ : ℝ → ℝ} {X Y : Ω → ℝ} {A : ℝ} (hX : IsBigO μ Ψ X A) (hYX : ∀ (ω : Ω), |Y ω| ≤ |X ω|) : IsBigO μ Ψ Y A

theorem HCPolySupport.IndependentSums.IsBigOWith.mono_scale {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {Ψ : ℝ → ℝ} {X : Ω → ℝ} {A B : ℝ} (hX : IsBigOWith μ Ψ X A) (hAB : A ≤ B) : IsBigOWith μ Ψ X B

theorem HCPolySupport.IndependentSums.IsBigO.mono_scale {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {Ψ : ℝ → ℝ} {X : Ω → ℝ} {A B : ℝ} (hX : IsBigO μ Ψ X A) (hAB : A ≤ B) : IsBigO μ Ψ X B

theorem HCPolySupport.IndependentSums.IsBigOWith.const_mul {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {Ψ : ℝ → ℝ} {X : Ω → ℝ} {A c : ℝ} (hc : 0 ≤ c) (hX : IsBigOWith μ Ψ X A) : IsBigOWith μ Ψ (fun (ω : Ω) => c * X ω) (c * A)

theorem HCPolySupport.IndependentSums.IsBigO.const_mul {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {Ψ : ℝ → ℝ} {X : Ω → ℝ} {A c : ℝ} (hc : 0 ≤ c) (hX : IsBigO μ Ψ X A) : IsBigO μ Ψ (fun (ω : Ω) => c * X ω) (c * A)

theorem HCPolySupport.IndependentSums.IsBigO.neg {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {Ψ : ℝ → ℝ} {X : Ω → ℝ} {A : ℝ} (hX : IsBigO μ Ψ X A) : IsBigO μ Ψ (fun (ω : Ω) => -X ω) A

noncomputable def HCPolySupport.IndependentSums.gammaSigma (σ : ℝ) : ℝ → ℝ

The stretched-exponential model tail function Γ_σ(t) = exp(t^σ).

Equations

• HCPolySupport.IndependentSums.gammaSigma σ t = Real.exp (t ^ σ)

noncomputable def HCPolySupport.IndependentSums.psiSigma (σ : ℝ) : ℝ → ℝ

The log-normal model tail function Ψ_σ(t) = exp((σ⁻¹)^2 log(1 + σ t)^2).

Equations

• HCPolySupport.IndependentSums.psiSigma σ t = Real.exp ((σ ^ 2)⁻¹ * Real.log (1 + σ * t) ^ 2)

@[simp]

theorem HCPolySupport.IndependentSums.gammaSigma_apply (σ t : ℝ) : gammaSigma σ t = Real.exp (t ^ σ)

@[simp]

theorem HCPolySupport.IndependentSums.psiSigma_apply (σ t : ℝ) : psiSigma σ t = Real.exp ((σ ^ 2)⁻¹ * Real.log (1 + σ * t) ^ 2)

theorem HCPolySupport.IndependentSums.gammaSigma_inv (σ t : ℝ) : (gammaSigma σ t)⁻¹ = Real.exp (-t ^ σ)

theorem HCPolySupport.IndependentSums.psiSigma_inv (σ t : ℝ) : (psiSigma σ t)⁻¹ = Real.exp (-((σ ^ 2)⁻¹ * Real.log (1 + σ * t) ^ 2))

theorem HCPolySupport.IndependentSums.one_le_gammaSigma {σ t : ℝ} (ht : 0 ≤ t) : 1 ≤ gammaSigma σ t

theorem HCPolySupport.IndependentSums.one_le_psiSigma {σ t : ℝ} : 1 ≤ psiSigma σ t

theorem HCPolySupport.IndependentSums.gammaSigma_monotoneOn {σ : ℝ} (hσ : 0 ≤ σ) : MonotoneOn (gammaSigma σ) (Set.Ici 0)

theorem HCPolySupport.IndependentSums.admissiblePsi_gammaSigma {σ : ℝ} (hσ : 0 ≤ σ) : AdmissiblePsi (gammaSigma σ)

theorem HCPolySupport.IndependentSums.psiSigma_monotoneOn {σ : ℝ} (hσ : 0 ≤ σ) : MonotoneOn (psiSigma σ) (Set.Ici 0)

theorem HCPolySupport.IndependentSums.admissiblePsi_psiSigma {σ : ℝ} (hσ : 0 ≤ σ) : AdmissiblePsi (psiSigma σ)

theorem HCPolySupport.IndependentSums.isBigOWith_gammaSigma_iff {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {A σ : ℝ} : IsBigOWith μ (gammaSigma σ) X A ↔ ∀ ⦃t : ℝ⦄, 1 ≤ t → μ.real (upperTailEvent X (A * t)) ≤ Real.exp (-t ^ σ)

theorem HCPolySupport.IndependentSums.isBigO_gammaSigma_iff {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {A σ : ℝ} : IsBigO μ (gammaSigma σ) X A ↔ ∀ ⦃t : ℝ⦄, 1 ≤ t → μ.real (absTailEvent X (A * t)) ≤ Real.exp (-t ^ σ)

theorem HCPolySupport.IndependentSums.isBigOWith_psiSigma_iff {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {A σ : ℝ} : IsBigOWith μ (psiSigma σ) X A ↔ ∀ ⦃t : ℝ⦄, 1 ≤ t → μ.real (upperTailEvent X (A * t)) ≤ Real.exp (-((σ ^ 2)⁻¹ * Real.log (1 + σ * t) ^ 2))

theorem HCPolySupport.IndependentSums.isBigO_psiSigma_iff {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {A σ : ℝ} : IsBigO μ (psiSigma σ) X A ↔ ∀ ⦃t : ℝ⦄, 1 ≤ t → μ.real (absTailEvent X (A * t)) ≤ Real.exp (-((σ ^ 2)⁻¹ * Real.log (1 + σ * t) ^ 2))