integrable_exp_mul_of_le — Mathlib

English

If X is a.e.-measurable and X lies in Icc(a,b) μ-a.e., then exp(t X) is integrable for finite μ and arbitrary t.

Русский

Если X а.е. измерим и лежит в Icc(a,b) μ-a.e., то exp(t X) интегрируема.

LaTeX

$$$\text{AEMeasurable}(X, \mu) \wedge X(\omega) \in [a,b] \text{ a.e. } \Rightarrow \mathrm{Integrable}(\lambda \omega. e^{t X(\omega)}, \mu).$$$

Lean4

theorem integrable_exp_mul_of_le [IsFiniteMeasure μ] {X : Ω → ℝ} (t b : ℝ) (ht : 0 ≤ t) (hX : AEMeasurable X μ)
    (hb : ∀ᵐ ω ∂μ, X ω ≤ b) : Integrable (fun ω ↦ exp (t * X ω)) μ :=
  by
  refine .of_mem_Icc 0 (rexp (t * b)) (measurable_exp.comp_aemeasurable (hX.const_mul t)) ?_
  filter_upwards [hb] with ω hb
  exact ⟨by positivity, by gcongr⟩

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