tilted_mul_apply_eq_ofReal_integral_cgf'

English

If X is measurable and almost surely lies in [a,b], then HasSubgaussianMGF X with parameter ((|b-a|_+) / 2)^2 holds provided [IsProbabilityMeasure μ].

Русский

Если X измерима и почти surely лежит в [a,b], то HasSubgaussianMGF X с параметром ((|b-a|_+)/2)^2 при условии IsProbabilityMeasure μ.

LaTeX

$$$[IsProbabilityMeasure μ] \Rightarrow X \text{ meas } μ \, \land \, X(ω) \in [a,b]\; a.e. \Rightarrow \mathrm{HasSubgaussianMGF}(X, (|b-a|_+ /2)^2, μ)$$$

Lean4

theorem tilted_mul_apply_eq_ofReal_integral_cgf' {s : Set Ω} (hs : MeasurableSet s)
    (ht : Integrable (fun ω ↦ exp (t * X ω)) μ) :
    μ.tilted (t * X ·) s = ENNReal.ofReal (∫ a in s, exp (t * X a - cgf X μ t) ∂μ) :=
  by
  rcases eq_zero_or_neZero μ with rfl | hμ
  · simp
  · simp_rw [tilted_mul_apply_eq_ofReal_integral_mgf' hs, exp_sub]
    rwa [exp_cgf]

Похожие утверждения