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))))