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

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

Tactic:
simp_rw [abs_of_nonneg ht_nonneg]

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

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

Tactic:
exact integrable_exp_mul_abs_add ht_int_neg (by simpa using ht_int_pos)

Result:
no goals

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

Tactic:
simp_rw [abs_of_nonpos ht_nonpos]

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

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

Tactic:
exact integrable_exp_mul_abs_add ht_int_pos ht_int_neg

Result:
no goals

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

Tactic:
simpa using ht_int_pos

Result:
no goals

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

Tactic:
rcases le_total 0 t with ht_nonneg | ht_nonpos

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

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