integrable_exp_abs_mul_abs — Mathlib

English

If exp(t X) and exp(-t X) are μ-integrable, then exp(|t| |X|) is μ-integrable.

Русский

Если интегрируемы exp(t X) и exp(-t X), то интегрируема exp(|t| |X|).

LaTeX

$$$\\text{Integrable}(\\exp(|t|\\,|X|))$$$

Lean4

/-- If `ω ↦ exp (t * X ω)` is integrable at `t` and `-t`, then `ω ↦ exp (|t| * |X ω|)` is
integrable. -/
theorem integrable_exp_abs_mul_abs (ht_int_pos : Integrable (fun ω ↦ exp (t * X ω)) μ)
    (ht_int_neg : Integrable (fun ω ↦ exp (-t * X ω)) μ) : Integrable (fun ω ↦ exp (|t| * |X ω|)) μ :=
  by
  rcases le_total 0 t with ht_nonneg | ht_nonpos
  · simp_rw [abs_of_nonneg ht_nonneg]
    exact integrable_exp_mul_abs ht_int_pos ht_int_neg
  · simp_rw [abs_of_nonpos ht_nonpos]
    exact integrable_exp_mul_abs ht_int_neg (by simpa using ht_int_pos)

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