Lemmas about sub-Gaussian random variables

theorem ProbabilityTheory.HasCondSubgaussianMGF.ae_trim_condExp_exp_sub_le_one {Ω : Type u_1} {m mΩ : MeasurableSpace Ω} {hm : m ≤ mΩ} [StandardBorelSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : Ω → ℝ} {c : NNReal} (h : HasCondSubgaussianMGF m hm X c μ) (t : ℝ) : ∀ᵐ (ω' : Ω) ∂μ.trim hm, μ[fun (ω : Ω) => Real.exp (t * X ω - ↑c * t ^ 2 / 2) | m] ω' ≤ 1

theorem ProbabilityTheory.HasCondSubgaussianMGF.ae_condExp_exp_sub_le_one {Ω : Type u_1} {m mΩ : MeasurableSpace Ω} {hm : m ≤ mΩ} [StandardBorelSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : Ω → ℝ} {c : NNReal} (h : HasCondSubgaussianMGF m hm X c μ) (t : ℝ) : ∀ᵐ (ω' : Ω) ∂μ, μ[fun (ω : Ω) => Real.exp (t * X ω - ↑c * t ^ 2 / 2) | m] ω' ≤ 1

theorem ProbabilityTheory.HasCondSubgaussianMGF.memLp_exp_mul_sub {Ω : Type u_1} {m mΩ : MeasurableSpace Ω} {hm : m ≤ mΩ} [StandardBorelSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : Ω → ℝ} {c : NNReal} (h : HasCondSubgaussianMGF m hm X c μ) (t : ℝ) (p : NNReal) : MeasureTheory.MemLp (fun (ω : Ω) => Real.exp (t * X ω - ↑c * t ^ 2 / 2)) (↑p) μ

theorem ProbabilityTheory.HasCondSubgaussianMGF.integrable_exp_mul_sub {Ω : Type u_1} {m mΩ : MeasurableSpace Ω} {hm : m ≤ mΩ} [StandardBorelSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : Ω → ℝ} {c : NNReal} (h : HasCondSubgaussianMGF m hm X c μ) (t : ℝ) : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * X ω - ↑c * t ^ 2 / 2)) μ

theorem ProbabilityTheory.HasSubgaussianMGF.measure_le_le {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {c : NNReal} (h : HasSubgaussianMGF X c μ) {ε : ℝ} (hε : 0 ≤ ε) : μ.real {ω : Ω | X ω ≤ -ε} ≤ Real.exp (-ε ^ 2 / (2 * ↑c))

Chernoff bound on the left tail of a sub-Gaussian random variable.

theorem ProbabilityTheory.HasSubgaussianMGF.measure_sum_le_le_of_iIndepFun {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ι : Type u_2} {X : ι → Ω → ℝ} (h_indep : iIndepFun X μ) {c : ι → NNReal} {s : Finset ι} (h_subG : ∀ i ∈ s, HasSubgaussianMGF (X i) (c i) μ) {ε : ℝ} (hε : 0 ≤ ε) : μ.real {ω : Ω | ∑ i ∈ s, X i ω ≤ -ε} ≤ Real.exp (-ε ^ 2 / (2 * ↑(∑ i ∈ s, c i)))

Hoeffding inequality for sub-Gaussian random variables.

theorem ProbabilityTheory.HasSubgaussianMGF.measure_sum_range_le_le_of_iIndepFun {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → ℝ} (h_indep : iIndepFun X μ) {c : NNReal} {n : ℕ} (h_subG : ∀ i < n, HasSubgaussianMGF (X i) c μ) {ε : ℝ} (hε : 0 ≤ ε) : μ.real {ω : Ω | ∑ i ∈ Finset.range n, X i ω ≤ -ε} ≤ Real.exp (-ε ^ 2 / (2 * ↑n * ↑c))

Hoeffding inequality for sub-Gaussian random variables.

theorem ProbabilityTheory.HasSubgaussianMGF.measure_sum_le_sum_le {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ι : Type u_2} {ι' : Type u_3} {X : ι → Ω → ℝ} {cX : ι → NNReal} {s : Finset ι} {Y : ι' → Ω → ℝ} {cY : ι' → NNReal} {t : Finset ι'} [MeasureTheory.IsFiniteMeasure μ] (hX_indep : iIndepFun X μ) (hY_indep : iIndepFun Y μ) (hX_subG : ∀ i ∈ s, HasSubgaussianMGF (fun (ω : Ω) => X i ω - ∫ (x : Ω), X i x ∂μ) (cX i) μ) (hY_subG : ∀ j ∈ t, HasSubgaussianMGF (fun (ω : Ω) => Y j ω - ∫ (x : Ω), Y j x ∂μ) (cY j) μ) (h_indep_sum : IndepFun (fun (ω : Ω) => ∑ i ∈ s, X i ω) (fun (ω : Ω) => ∑ j ∈ t, Y j ω) μ) (h_le : ∑ j ∈ t, ∫ (x : Ω), Y j x ∂μ ≤ ∑ i ∈ s, ∫ (x : Ω), X i x ∂μ) : μ.real {ω : Ω | ∑ i ∈ s, X i ω ≤ ∑ j ∈ t, Y j ω} ≤ Real.exp (-(∑ j ∈ t, ∫ (x : Ω), Y j x ∂μ - ∑ i ∈ s, ∫ (x : Ω), X i x ∂μ) ^ 2 / (2 * (↑(∑ i ∈ s, cX i) + ↑(∑ j ∈ t, cY j))))

theorem ProbabilityTheory.HasSubgaussianMGF.measure_sum_le_sum_le' {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ι : Type u_2} {ι' : Type u_3} {X : ι → Ω → ℝ} {cX : ι → NNReal} {s : Finset ι} {Y : ι' → Ω → ℝ} {cY : ι' → NNReal} {t : Finset ι'} [MeasureTheory.IsFiniteMeasure μ] (hX_indep : iIndepFun X μ) (hY_indep : iIndepFun Y μ) (hX_subG : ∀ i ∈ s, HasSubgaussianMGF (fun (ω : Ω) => X i ω - ∫ (x : Ω), X i x ∂μ) (cX i) μ) (hY_subG : ∀ j ∈ t, HasSubgaussianMGF (fun (ω : Ω) => Y j ω - ∫ (x : Ω), Y j x ∂μ) (cY j) μ) (h_indep_sum : IndepFun (fun (ω : Ω) (x : ι) => X x ω) (fun (ω : Ω) (x : ι') => Y x ω) μ) (h_le : ∑ j ∈ t, ∫ (x : Ω), Y j x ∂μ ≤ ∑ i ∈ s, ∫ (x : Ω), X i x ∂μ) : μ.real {ω : Ω | ∑ i ∈ s, X i ω ≤ ∑ j ∈ t, Y j ω} ≤ Real.exp (-(∑ j ∈ t, ∫ (x : Ω), Y j x ∂μ - ∑ i ∈ s, ∫ (x : Ω), X i x ∂μ) ^ 2 / (2 * (↑(∑ i ∈ s, cX i) + ↑(∑ j ∈ t, cY j))))