Coarse-graining support: Support.Probability.IndependentSums.GammaSigmaConcentration.LargeRegime #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
theorem
HCPolySupport.IndependentSums.upperTailProbability_finiteSum_le_exp_neg_of_iIndepFun_of_isBigO
{Ω : Type u_1}
{ι : Type u_2}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure μ]
{X : ι → Ω → ℝ}
{s : Finset ι}
{σ t : ℝ}
(h_indep : ProbabilityTheory.iIndepFun X μ)
(h_meas : ∀ (i : ι), Measurable (X i))
(hs : s.Nonempty)
(hσ₀ : 0 < σ)
(hσ₁ : σ < 1)
(hX : ∀ i ∈ s, IsBigO μ (gammaSigma σ) (X i) 1)
(h_mean : ∀ i ∈ s, ∫ (ω : Ω), X i ω ∂μ = 0)
(ht : 1 ≤ t)
(hlarge : ↑s.card ^ (σ / (2 * (2 - σ))) ≤ t)
:
Large-regime one-sided heavy-tail concentration for centered independent
unit-scale O_{Γ_σ} summands.
theorem
HCPolySupport.IndependentSums.isBigOWith_gammaSigma_finset_sum_unit_of_iIndepFun_of_isBigO_of_integral_eq_zero_of_lt_one
{Ω : Type u_1}
{ι : Type u_2}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure μ]
{X : ι → Ω → ℝ}
{s : Finset ι}
{σ : ℝ}
(h_indep : ProbabilityTheory.iIndepFun X μ)
(h_meas : ∀ (i : ι), Measurable (X i))
(hs : s.Nonempty)
(hσ₀ : 0 < σ)
(hσ₁ : σ < 1)
(hX : ∀ i ∈ s, IsBigO μ (gammaSigma σ) (X i) 1)
(h_mean : ∀ i ∈ s, ∫ (ω : Ω), X i ω ∂μ = 0)
:
IsBigOWith μ (gammaSigma σ) (fun (ω : Ω) => ∑ i ∈ s, X i ω) (gammaSigmaHeavyTailConst σ * √↑s.card)
One-sided heavy-tail concentration for centered independent unit-scale
O_{Γ_σ} summands on the range 0 < σ < 1.
theorem
HCPolySupport.IndependentSums.isBigOWith_gammaSigma_finset_sum_of_iIndepFun_of_isBigO_of_integral_eq_zero_of_lt_one
{Ω : Type u_1}
{ι : Type u_2}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure μ]
{X : ι → Ω → ℝ}
{s : Finset ι}
{σ K : ℝ}
(h_indep : ProbabilityTheory.iIndepFun X μ)
(h_meas : ∀ (i : ι), Measurable (X i))
(hs : s.Nonempty)
(hσ₀ : 0 < σ)
(hσ₁ : σ < 1)
(hK : 0 < K)
(hX : ∀ i ∈ s, IsBigO μ (gammaSigma σ) (X i) K)
(h_mean : ∀ i ∈ s, ∫ (ω : Ω), X i ω ∂μ = 0)
:
IsBigOWith μ (gammaSigma σ) (fun (ω : Ω) => ∑ i ∈ s, X i ω) (gammaSigmaHeavyTailConst σ * √↑s.card * K)
One-sided heavy-tail concentration for centered independent O_{Γ_σ}
summands on the range 0 < σ < 1.
theorem
HCPolySupport.IndependentSums.isBigO_gammaSigma_sum_iIndep_bigO_meanZero_ltOne
{Ω : Type u_1}
{ι : Type u_2}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure μ]
{X : ι → Ω → ℝ}
{s : Finset ι}
{σ K : ℝ}
(h_indep : ProbabilityTheory.iIndepFun X μ)
(h_meas : ∀ (i : ι), Measurable (X i))
(hs : s.Nonempty)
(hσ₀ : 0 < σ)
(hσ₁ : σ < 1)
(hK : 0 < K)
(hX : ∀ i ∈ s, IsBigO μ (gammaSigma σ) (X i) K)
(h_mean : ∀ i ∈ s, ∫ (ω : Ω), X i ω ∂μ = 0)
:
IsBigO μ (gammaSigma σ) (fun (ω : Ω) => ∑ i ∈ s, X i ω) (gammaSigmaHeavyTailEndpointConst σ * √↑s.card * K)
Symmetric heavy-tail concentration for centered independent O_{Γ_σ}
summands on the range 0 < σ < 1.
theorem
HCPolySupport.IndependentSums.isBigO_gammaSigma_average_iIndep_bigO_meanZero_ltOne
{Ω : Type u_1}
{ι : Type u_2}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure μ]
{X : ι → Ω → ℝ}
{s : Finset ι}
{σ K : ℝ}
(h_indep : ProbabilityTheory.iIndepFun X μ)
(h_meas : ∀ (i : ι), Measurable (X i))
(hs : s.Nonempty)
(hσ₀ : 0 < σ)
(hσ₁ : σ < 1)
(hK : 0 < K)
(hX : ∀ i ∈ s, IsBigO μ (gammaSigma σ) (X i) K)
(h_mean : ∀ i ∈ s, ∫ (ω : Ω), X i ω ∂μ = 0)
:
Averaging preserves the heavy-tail Γ_σ concentration scale in the range
0 < σ < 1.