Coarse-graining support: Support.Probability.IndependentSums.GammaSigmaExpRegime.FiniteSums

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

theorem HCPolySupport.IndependentSums.mgf_finset_sum_le_exp_of_iIndepFun {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {ι : Type u_2} {X : ι → Ω → ℝ} {v : ι → ℝ} {s : Finset ι} {l : ℝ} (h_indep : ProbabilityTheory.iIndepFun X μ) (h_meas : ∀ (i : ι), Measurable (X i)) (hmgf : ∀ i ∈ s, ProbabilityTheory.mgf (X i) μ l ≤ Real.exp (v i)) : ProbabilityTheory.mgf (fun (ω : Ω) => ∑ i ∈ s, X i ω) μ l ≤ Real.exp (∑ i ∈ s, v i)

Finite independent sums inherit exponential mgf bounds when each summand has one.

theorem HCPolySupport.IndependentSums.mgf_finset_sum_le_exp_card_mul_of_iIndepFun_of_isBigO_gammaSigma_of_one_lt {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {ι : Type u_2} {X : ι → Ω → ℝ} {s : Finset ι} {σ K l : ℝ} (h_indep : ProbabilityTheory.iIndepFun X μ) (h_meas : ∀ (i : ι), Measurable (X i)) (hσ : 1 < σ) (hK : 0 < K) (hl : 0 ≤ l) (hX : ∀ i ∈ s, IsBigO μ (gammaSigma σ) (X i) K) : ProbabilityTheory.mgf (fun (ω : Ω) => ∑ i ∈ s, X i ω) μ l ≤ Real.exp (↑s.card * (Real.log 2 + gammaSigmaLargeMgfConst σ * (K * l) ^ gammaExpConjExponent σ))

Finite independent sums inherit the large-λ exponential mgf bound in the note-facing O_{Γ_σ} language when σ > 1.

theorem HCPolySupport.IndependentSums.upperTail_sum_le_exp_of_independent_bigO {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {ι : Type u_2} {X : ι → Ω → ℝ} {s : Finset ι} {σ K l a : ℝ} (h_indep : ProbabilityTheory.iIndepFun X μ) (h_meas : ∀ (i : ι), Measurable (X i)) (hσ : 1 < σ) (hK : 0 < K) (hl : 0 ≤ l) (hX : ∀ i ∈ s, IsBigO μ (gammaSigma σ) (X i) K) : μ.real (upperTailEvent (fun (ω : Ω) => ∑ i ∈ s, X i ω) a) ≤ Real.exp (-l * a + ↑s.card * (Real.log 2 + gammaSigmaLargeMgfConst σ * (K * l) ^ gammaExpConjExponent σ))

Large-λ Chernoff bound for finite sums of independent O_{Γ_σ} variables when σ > 1.

theorem HCPolySupport.IndependentSums.mgf_finset_sum_le_exp_of_iIndepFun_of_gammaMomentGrowth_small_of_integral_eq_zero {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {ι : Type u_2} {X : ι → Ω → ℝ} {M : ι → ℝ} {s : Finset ι} {σ l : ℝ} (h_indep : ProbabilityTheory.iIndepFun X μ) (h_meas : ∀ (i : ι), Measurable (X i)) (hσ : 1 ≤ σ) (hl : 0 ≤ l) (hM : ∀ i ∈ s, 0 ≤ M i) (hl_small : ∀ i ∈ s, l ≤ (2 * Real.exp 1 * M i)⁻¹) (hXmean : ∀ i ∈ s, ∫ (ω : Ω), X i ω ∂μ = 0) (hXmom : ∀ i ∈ s, HasGammaMomentGrowthWith μ σ (X i) (M i)) : ProbabilityTheory.mgf (fun (ω : Ω) => ∑ i ∈ s, X i ω) μ l ≤ Real.exp (∑ i ∈ s, 2 * (Real.exp 1 * M i * l) ^ 2)

Small-λ exponential mgf bound for finite independent sums of centered Γ_σ variables.

theorem HCPolySupport.IndependentSums.upperTailProbability_finiteSum_le_exp_of_iIndepFun {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {ι : Type u_2} {X : ι → Ω → ℝ} {M : ι → ℝ} {s : Finset ι} {σ l a : ℝ} (h_indep : ProbabilityTheory.iIndepFun X μ) (h_meas : ∀ (i : ι), Measurable (X i)) (hσ : 1 ≤ σ) (hl : 0 ≤ l) (hM : ∀ i ∈ s, 0 ≤ M i) (hl_small : ∀ i ∈ s, l ≤ (2 * Real.exp 1 * M i)⁻¹) (hXmean : ∀ i ∈ s, ∫ (ω : Ω), X i ω ∂μ = 0) (hXmom : ∀ i ∈ s, HasGammaMomentGrowthWith μ σ (X i) (M i)) : μ.real (upperTailEvent (fun (ω : Ω) => ∑ i ∈ s, X i ω) a) ≤ Real.exp (-l * a + ∑ i ∈ s, 2 * (Real.exp 1 * M i * l) ^ 2)

Chernoff upper-tail estimate for finite independent sums of centered Γ_σ variables in the small-λ regime.

theorem HCPolySupport.IndependentSums.mgf_finset_sum_le_exp_card_mul_of_iIndepFun_of_gammaMomentGrowth_small_of_integral_eq_zero {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {ι : Type u_2} {X : ι → Ω → ℝ} {s : Finset ι} {σ M l : ℝ} (h_indep : ProbabilityTheory.iIndepFun X μ) (h_meas : ∀ (i : ι), Measurable (X i)) (hσ : 1 ≤ σ) (hM : 0 ≤ M) (hl : 0 ≤ l) (hl_small : l ≤ (2 * Real.exp 1 * M)⁻¹) (hXmean : ∀ i ∈ s, ∫ (ω : Ω), X i ω ∂μ = 0) (hXmom : ∀ i ∈ s, HasGammaMomentGrowthWith μ σ (X i) M) : ProbabilityTheory.mgf (fun (ω : Ω) => ∑ i ∈ s, X i ω) μ l ≤ Real.exp (2 * ↑s.card * (Real.exp 1 * M * l) ^ 2)

Uniform-witness version of the finite-sum small-λ exponential mgf estimate.

theorem HCPolySupport.IndependentSums.upperTailProbability_finiteSum_le_exp_card_mul_of_iIndepFun {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {ι : Type u_2} {X : ι → Ω → ℝ} {s : Finset ι} {σ M l a : ℝ} (h_indep : ProbabilityTheory.iIndepFun X μ) (h_meas : ∀ (i : ι), Measurable (X i)) (hσ : 1 ≤ σ) (hM : 0 ≤ M) (hl : 0 ≤ l) (hl_small : l ≤ (2 * Real.exp 1 * M)⁻¹) (hXmean : ∀ i ∈ s, ∫ (ω : Ω), X i ω ∂μ = 0) (hXmom : ∀ i ∈ s, HasGammaMomentGrowthWith μ σ (X i) M) : μ.real (upperTailEvent (fun (ω : Ω) => ∑ i ∈ s, X i ω) a) ≤ Real.exp (-l * a + 2 * ↑s.card * (Real.exp 1 * M * l) ^ 2)

Uniform-witness version of the finite-sum small-λ Chernoff estimate.

noncomputable def HCPolySupport.IndependentSums.gammaSigmaExpRegimeConst (σ : ℝ) : ℝ

Explicit witness for the direct exponential-regime concentration theorem in the range 1 < σ ≤ 2.

Equations

• HCPolySupport.IndependentSums.gammaSigmaExpRegimeConst σ = max (8 * Real.exp 1 * HCPolySupport.IndependentSums.gammaMomentConst σ) (2 + HCPolySupport.IndependentSums.gammaSigmaLargeMgfConst σ)

theorem HCPolySupport.IndependentSums.gammaExpLargeLambdaConst_pos {σ : ℝ} (hσ : 1 < σ) : 0 < gammaExpLargeLambdaConst σ

theorem HCPolySupport.IndependentSums.gammaSigmaLargeMgfConst_pos {σ : ℝ} (hσ : 1 < σ) : 0 < gammaSigmaLargeMgfConst σ

theorem HCPolySupport.IndependentSums.isBigOWith_gammaSigma_finset_sum_of_iIndepFun_of_isBigO_of_integral_eq_zero_of_one_lt {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {ι : Type u_2} {X : ι → Ω → ℝ} {s : Finset ι} {σ K : ℝ} (h_indep : ProbabilityTheory.iIndepFun X μ) (h_meas : ∀ (i : ι), Measurable (X i)) (hs : s.Nonempty) (hσ : 1 < σ) (hσ₂ : σ ≤ 2) (hK : 0 < K) (hX : ∀ i ∈ s, IsBigO μ (gammaSigma σ) (X i) K) (hXmean : ∀ i ∈ s, ∫ (ω : Ω), X i ω ∂μ = 0) : IsBigOWith μ (gammaSigma σ) (fun (ω : Ω) => ∑ i ∈ s, X i ω) (gammaSigmaExpRegimeConst σ * √↑s.card * K)

One-sided direct concentration in the exponential regime 1 < σ ≤ 2.

theorem HCPolySupport.IndependentSums.isBigO_gammaSigma_finset_sum_of_iIndepFun_of_isBigO_of_integral_eq_zero_of_one_lt {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {ι : Type u_2} {X : ι → Ω → ℝ} {s : Finset ι} {σ K : ℝ} (h_indep : ProbabilityTheory.iIndepFun X μ) (h_meas : ∀ (i : ι), Measurable (X i)) (hs : s.Nonempty) (hσ : 1 < σ) (hσ₂ : σ ≤ 2) (hK : 0 < K) (hX : ∀ i ∈ s, IsBigO μ (gammaSigma σ) (X i) K) (hXmean : ∀ i ∈ s, ∫ (ω : Ω), X i ω ∂μ = 0) : IsBigO μ (gammaSigma σ) (fun (ω : Ω) => ∑ i ∈ s, X i ω) (2 * gammaSigmaExpRegimeConst σ * √↑s.card * K)

Symmetric direct concentration in the exponential regime 1 < σ ≤ 2.

theorem HCPolySupport.IndependentSums.isBigO_gammaSigma_finsetAverage_of_iIndepFun_of_isBigO_of_integral_eq_zero_of_one_lt {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {ι : Type u_2} {X : ι → Ω → ℝ} {s : Finset ι} {σ K : ℝ} (h_indep : ProbabilityTheory.iIndepFun X μ) (h_meas : ∀ (i : ι), Measurable (X i)) (hs : s.Nonempty) (hσ : 1 < σ) (hσ₂ : σ ≤ 2) (hK : 0 < K) (hX : ∀ i ∈ s, IsBigO μ (gammaSigma σ) (X i) K) (hXmean : ∀ i ∈ s, ∫ (ω : Ω), X i ω ∂μ = 0) : IsBigO μ (gammaSigma σ) (fun (ω : Ω) => (↑s.card)⁻¹ * ∑ i ∈ s, X i ω) (2 * gammaSigmaExpRegimeConst σ * (√↑s.card / ↑s.card) * K)

Averaging preserves the direct exponential-regime concentration scale in the range 1 < σ ≤ 2.

noncomputable def HCPolySupport.IndependentSums.gammaOneExpRegimeConst : ℝ

Explicit Γ₁ witness extracted from the small-λ exponential-regime argument.

Equations

• HCPolySupport.IndependentSums.gammaOneExpRegimeConst = 4 * Real.exp 1 * HCPolySupport.IndependentSums.gammaMomentConst 1

theorem HCPolySupport.IndependentSums.gammaOneExpRegimeConst_pos : 0 < gammaOneExpRegimeConst

theorem HCPolySupport.IndependentSums.isBigOWith_gammaOne_finset_sum_of_iIndepFun_of_isBigO_of_integral_eq_zero {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {ι : Type u_2} {X : ι → Ω → ℝ} {s : Finset ι} {K : ℝ} (h_indep : ProbabilityTheory.iIndepFun X μ) (h_meas : ∀ (i : ι), Measurable (X i)) (hs : s.Nonempty) (hK : 0 < K) (hX : ∀ i ∈ s, IsBigO μ (gammaSigma 1) (X i) K) (hXmean : ∀ i ∈ s, ∫ (ω : Ω), X i ω ∂μ = 0) : IsBigOWith μ (gammaSigma 1) (fun (ω : Ω) => ∑ i ∈ s, X i ω) (gammaOneExpRegimeConst * √↑s.card * K)

Centered independent O_{Γ₁} summands satisfy the one-sided Γ₁ concentration estimate with the expected sqrt(card) scaling.

theorem HCPolySupport.IndependentSums.isBigO_gammaOne_finset_sum_of_iIndepFun_of_isBigO_of_integral_eq_zero {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {ι : Type u_2} {X : ι → Ω → ℝ} {s : Finset ι} {K : ℝ} (h_indep : ProbabilityTheory.iIndepFun X μ) (h_meas : ∀ (i : ι), Measurable (X i)) (hs : s.Nonempty) (hK : 0 < K) (hX : ∀ i ∈ s, IsBigO μ (gammaSigma 1) (X i) K) (hXmean : ∀ i ∈ s, ∫ (ω : Ω), X i ω ∂μ = 0) : IsBigO μ (gammaSigma 1) (fun (ω : Ω) => ∑ i ∈ s, X i ω) (2 * gammaOneExpRegimeConst * √↑s.card * K)

Centered independent O_{Γ₁} summands satisfy the symmetric Γ₁ concentration estimate with the expected sqrt(card) scaling.

theorem HCPolySupport.IndependentSums.isBigO_gammaOne_finsetAverage_of_iIndepFun_of_isBigO_of_integral_eq_zero {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {ι : Type u_2} {X : ι → Ω → ℝ} {s : Finset ι} {K : ℝ} (h_indep : ProbabilityTheory.iIndepFun X μ) (h_meas : ∀ (i : ι), Measurable (X i)) (hs : s.Nonempty) (hK : 0 < K) (hX : ∀ i ∈ s, IsBigO μ (gammaSigma 1) (X i) K) (hXmean : ∀ i ∈ s, ∫ (ω : Ω), X i ω ∂μ = 0) : IsBigO μ (gammaSigma 1) (fun (ω : Ω) => (↑s.card)⁻¹ * ∑ i ∈ s, X i ω) (2 * gammaOneExpRegimeConst * (√↑s.card / ↑s.card) * K)

Averaging preserves the Γ₁ concentration scale of centered independent O_{Γ₁} summands.

noncomputable def HCPolySupport.IndependentSums.gammaSigmaExpRegimeEndpointConst (σ : ℝ) : ℝ

Unified endpoint constant for the Chapter 4 direct exponential-regime concentration theorem on the range σ ∈ [1, 2].

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.IndependentSums.isBigO_gammaSigma_sum_iIndep_bigO_meanZero_expRegime {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {ι : Type u_2} {X : ι → Ω → ℝ} {s : Finset ι} {σ K : ℝ} (h_indep : ProbabilityTheory.iIndepFun X μ) (h_meas : ∀ (i : ι), Measurable (X i)) (hs : s.Nonempty) (hσ₁ : 1 ≤ σ) (hσ₂ : σ ≤ 2) (hK : 0 < K) (hX : ∀ i ∈ s, IsBigO μ (gammaSigma σ) (X i) K) (hXmean : ∀ i ∈ s, ∫ (ω : Ω), X i ω ∂μ = 0) : IsBigO μ (gammaSigma σ) (fun (ω : Ω) => ∑ i ∈ s, X i ω) (gammaSigmaExpRegimeEndpointConst σ * √↑s.card * K)

Note-facing direct concentration theorem in the exponential regime σ ∈ [1, 2].

theorem HCPolySupport.IndependentSums.isBigO_gammaSigma_average_iIndep_bigO_meanZero_expRegime {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {ι : Type u_2} {X : ι → Ω → ℝ} {s : Finset ι} {σ K : ℝ} (h_indep : ProbabilityTheory.iIndepFun X μ) (h_meas : ∀ (i : ι), Measurable (X i)) (hs : s.Nonempty) (hσ₁ : 1 ≤ σ) (hσ₂ : σ ≤ 2) (hK : 0 < K) (hX : ∀ i ∈ s, IsBigO μ (gammaSigma σ) (X i) K) (hXmean : ∀ i ∈ s, ∫ (ω : Ω), X i ω ∂μ = 0) : IsBigO μ (gammaSigma σ) (fun (ω : Ω) => (↑s.card)⁻¹ * ∑ i ∈ s, X i ω) (gammaSigmaExpRegimeEndpointConst σ * (√↑s.card / ↑s.card) * K)

Averaged version of the direct exponential-regime concentration theorem on the range σ ∈ [1, 2].