integrable_exp_abs_mul_abs_add — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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