integrable_exp_mul_abs — Mathlib

English

If exp(a X) and exp(b X) are μ-integrable and a ≤ t ≤ b, then exp(t X) is μ-integrable.

Русский

Если exp(a X) и exp(b X) интегрируемы по μ и a ≤ t ≤ b, то exp(t X) интегрируема по μ.

LaTeX

$$$\\text{Integrable}(\\exp(t X)) \\leq ?$$$

Lean4

/-- If `ω ↦ exp (t * X ω)` is integrable at `t` and `-t`, then `ω ↦ exp (t * |X ω|)` is
integrable. -/
theorem integrable_exp_mul_abs (ht_int_pos : Integrable (fun ω ↦ exp (t * X ω)) μ)
    (ht_int_neg : Integrable (fun ω ↦ exp (-t * X ω)) μ) : Integrable (fun ω ↦ exp (t * |X ω|)) μ :=
  by
  have h := integrable_exp_mul_abs_add (t := t) (μ := μ) (X := X) (v := 0) ?_ ?_
  · simpa using h
  · simpa using ht_int_pos
  · simpa using ht_int_neg

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