-- Mathlib/Probability/Moments/IntegrableExpMul.lean
/-- If `ω ↦ exp (t * X ω)` is integrable at `t` and `-t`, then `ω ↦ exp (|t| * |X ω|)` is
integrable. -/
lemma 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 ω|)) μ

Proof state:
case inr
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht_int_pos : Integrable (fun ω => rexp (t * X ω)) μ
ht_int_neg : Integrable (fun ω => rexp (-t * X ω)) μ
ht_nonpos : t ≤ 0
⊢ Integrable (fun ω => rexp (|t| * |X ω|)) μ

Tactic:
simp_rw [abs_of_nonpos ht_nonpos]

Result:
case inr
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht_int_pos : Integrable (fun ω => rexp (t * X ω)) μ
ht_int_neg : Integrable (fun ω => rexp (-t * X ω)) μ
ht_nonpos : t ≤ 0
⊢ Integrable (fun ω => rexp (-t * |X ω|)) μ

Proof state:
case inl
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht_int_pos : Integrable (fun ω => rexp (t * X ω)) μ
ht_int_neg : Integrable (fun ω => rexp (-t * X ω)) μ
ht_nonneg : 0 ≤ t
⊢ Integrable (fun ω => rexp (t * |X ω|)) μ

Tactic:
exact integrable_exp_mul_abs ht_int_pos ht_int_neg

Result:
no goals

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht_int_pos : Integrable (fun ω => rexp (t * X ω)) μ
ht_int_neg : Integrable (fun ω => rexp (-t * X ω)) μ
⊢ Integrable (fun ω => rexp (|t| * |X ω|)) μ

Tactic:
rcases le_total 0 t with ht_nonneg | ht_nonpos

Result:
case inl
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht_int_pos : Integrable (fun ω => rexp (t * X ω)) μ
ht_int_neg : Integrable (fun ω => rexp (-t * X ω)) μ
ht_nonneg : 0 ≤ t
⊢ Integrable (fun ω => rexp (|t| * |X ω|)) μ

case inr
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht_int_pos : Integrable (fun ω => rexp (t * X ω)) μ
ht_int_neg : Integrable (fun ω => rexp (-t * X ω)) μ
ht_nonpos : t ≤ 0
⊢ Integrable (fun ω => rexp (|t| * |X ω|)) μ

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht_int_pos : Integrable (fun ω => rexp (t * X ω)) μ
ht_int_neg : Integrable (fun ω => rexp (-t * X ω)) μ
ht_nonpos : t ≤ 0
⊢ Integrable (fun ω => rexp (- -t * X ω)) μ

Tactic:
simpa using ht_int_pos

Result:
no goals

Proof state:
case inl
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht_int_pos : Integrable (fun ω => rexp (t * X ω)) μ
ht_int_neg : Integrable (fun ω => rexp (-t * X ω)) μ
ht_nonneg : 0 ≤ t
⊢ Integrable (fun ω => rexp (|t| * |X ω|)) μ

Tactic:
simp_rw [abs_of_nonneg ht_nonneg]

Result:
case inl
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht_int_pos : Integrable (fun ω => rexp (t * X ω)) μ
ht_int_neg : Integrable (fun ω => rexp (-t * X ω)) μ
ht_nonneg : 0 ≤ t
⊢ Integrable (fun ω => rexp (t * |X ω|)) μ

Proof state:
case inr
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht_int_pos : Integrable (fun ω => rexp (t * X ω)) μ
ht_int_neg : Integrable (fun ω => rexp (-t * X ω)) μ
ht_nonpos : t ≤ 0
⊢ Integrable (fun ω => rexp (-t * |X ω|)) μ

Tactic:
exact integrable_exp_mul_abs ht_int_neg (by simpa using ht_int_pos)

Result:
no goals