theorem
ProbabilityTheory.mgf_const_mul
{Ω : Type u_1}
{m : MeasurableSpace Ω}
{X : Ω → ℝ}
{μ : MeasureTheory.Measure Ω}
{t : ℝ}
(α : ℝ)
:
theorem
ProbabilityTheory.integrable_of_mem_interior_integrableExpSet
{Ω : Type u_1}
{m : MeasurableSpace Ω}
{X : Ω → ℝ}
{μ : MeasureTheory.Measure Ω}
(h : 0 ∈ interior (integrableExpSet X μ))
:
If 0 belongs to the interior of the interval integrableExpSet X μ, then X is integrable.
theorem
ProbabilityTheory.Kernel.HasSubgaussianMGF.id_map_iff
{Ω : Type u_1}
{Ω' : Type u_2}
{mΩ : MeasurableSpace Ω}
{mΩ' : MeasurableSpace Ω'}
{ν : MeasureTheory.Measure Ω'}
{κ : Kernel Ω' Ω}
{X : Ω → ℝ}
{c : NNReal}
(hX : Measurable X)
:
theorem
ProbabilityTheory.Kernel.HasSubgaussianMGF.const_mul
{Ω : Type u_1}
{Ω' : Type u_2}
{mΩ : MeasurableSpace Ω}
{mΩ' : MeasurableSpace Ω'}
{ν : MeasureTheory.Measure Ω'}
{κ : Kernel Ω' Ω}
{X : Ω → ℝ}
{c : NNReal}
(h : HasSubgaussianMGF X c κ ν)
(r : ℝ)
:
theorem
ProbabilityTheory.HasSubgaussianMGF.id_map_iff
{Ω : Type u_1}
{mΩ : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
{X : Ω → ℝ}
{c : NNReal}
(hX : AEMeasurable X μ)
:
theorem
ProbabilityTheory.HasSubgaussianMGF.congr_identDistrib
{Ω : Type u_1}
{mΩ : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
{X : Ω → ℝ}
{c : NNReal}
{Ω' : Type u_2}
{mΩ' : MeasurableSpace Ω'}
{μ' : MeasureTheory.Measure Ω'}
{Y : Ω' → ℝ}
(hX : HasSubgaussianMGF X c μ)
(hXY : IdentDistrib X Y μ μ')
:
HasSubgaussianMGF Y c μ'
theorem
ProbabilityTheory.HasSubgaussianMGF.const_mul
{Ω : Type u_1}
{mΩ : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
{X : Ω → ℝ}
{c : NNReal}
(h : HasSubgaussianMGF X c μ)
(r : ℝ)
:
theorem
ProbabilityTheory.HasSubgaussianMGF.sub_of_indepFun
{Ω : Type u_1}
{mΩ : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
{X Y : Ω → ℝ}
{cX cY : NNReal}
(hX : HasSubgaussianMGF X cX μ)
(hY : HasSubgaussianMGF Y cY μ)
(hindep : IndepFun X Y μ)
:
HasSubgaussianMGF (fun (ω : Ω) => X ω - Y ω) (cX + cY) μ
theorem
ProbabilityTheory.HasSubgaussianMGF.measure_le_le
{Ω : Type u_1}
{mΩ : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
{X Y : Ω → ℝ}
{cX cY : NNReal}
(hX : HasSubgaussianMGF (fun (ω : Ω) => X ω - ∫ (x : Ω), X x ∂μ) cX μ)
(hY : HasSubgaussianMGF (fun (ω : Ω) => Y ω - ∫ (x : Ω), Y x ∂μ) cY μ)
(hindep : IndepFun X Y μ)
(h_le : ∫ (x : Ω), Y x ∂μ ≤ ∫ (x : Ω), X x ∂μ)
:
theorem
ProbabilityTheory.HasSubgaussianMGF.integrableExpSet_eq_univ
{Ω : Type u_1}
{mΩ : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
{X : Ω → ℝ}
{c : NNReal}
(hX : HasSubgaussianMGF X c μ)
:
theorem
ProbabilityTheory.HasSubgaussianMGF.integrable
{Ω : Type u_1}
{mΩ : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
{X : Ω → ℝ}
{c : NNReal}
(hX : HasSubgaussianMGF X c μ)
:
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 ∂μ)
:
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 ∂μ)
: