-- 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_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 refine_2
Ω : 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 ω)) μ
h_int_add : Integrable (fun a => rexp ((v + t) * X a) + rexp ((v - t) * X a)) μ
ω : Ω
⊢ ‖rexp (t * |X ω| + v * X ω)‖ ≤ ‖rexp ((v + t) * X ω) + rexp ((v - t) * X ω)‖

Tactic:
simp only [norm_eq_abs, abs_exp]

Result:
case refine_2
Ω : 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 ω)) μ
h_int_add : Integrable (fun a => rexp ((v + t) * X a) + rexp ((v - t) * X a)) μ
ω : Ω
⊢ rexp (t * |X ω| + v * X ω) ≤ |rexp ((v + t) * X ω) + rexp ((v - t) * X ω)|

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 ω)) μ
h_int_add : Integrable (fun a => rexp ((v + t) * X a) + rexp ((v - t) * X a)) μ
ω : Ω
⊢ 0 ≤ rexp ((v + t) * X ω) + rexp ((v - t) * X ω)

Tactic:
positivity

Result:
no goals

Proof state:
case neg.refine_2
Ω : 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 ω)) μ
h_int_add : Integrable (fun a => rexp ((v + t) * X a) + rexp ((v - t) * X a)) μ
ht : ¬t = 0
hX : AEMeasurable X μ
⊢ AEMeasurable (fun ω => rexp (t * |X ω| + v * X ω)) μ

Tactic:
exact measurable_exp.comp_aemeasurable ((hX.abs.const_mul _).add (hX.const_mul _))

Result:
no goals

Proof state:
case neg.refine_1
Ω : 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 ω)) μ
h_int_add : Integrable (fun a => rexp ((v + t) * X a) + rexp ((v - t) * X a)) μ
ht : ¬t = 0
⊢ v + t ≠ v - t

Tactic:
rw [← sub_ne_zero]

Result:
case neg.refine_1
Ω : 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 ω)) μ
h_int_add : Integrable (fun a => rexp ((v + t) * X a) + rexp ((v - t) * X a)) μ
ht : ¬t = 0
⊢ v + t - (v - t) ≠ 0

Proof state:
case pos
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v : ℝ
ht_int_neg : Integrable (fun ω => rexp ((v - t) * X ω)) μ
h_int_add : Integrable (fun a => rexp ((v + t) * X a) + rexp ((v - t) * X a)) μ
ht : t = 0
ht_int_pos : Integrable (fun ω => rexp (v * X ω)) μ
⊢ AEStronglyMeasurable (fun ω => rexp (v * X ω)) μ

Tactic:
exact ht_int_pos.1

Result:
no goals

Proof state:
case refine_2
Ω : 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 ω)) μ
h_int_add : Integrable (fun a => rexp ((v + t) * X a) + rexp ((v - t) * X a)) μ
ω : Ω
⊢ rexp (t * |X ω| + v * X ω) ≤ rexp ((v + t) * X ω) + rexp ((v - t) * X ω)

Tactic:
rcases le_total 0 (X ω) with h_nonneg | h_nonpos

Result:
case refine_2.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 ω)) μ
h_int_add : Integrable (fun a => rexp ((v + t) * X a) + rexp ((v - t) * X a)) μ
ω : Ω
h_nonneg : 0 ≤ X ω
⊢ rexp (t * |X ω| + v * X ω) ≤ rexp ((v + t) * X ω) + rexp ((v - t) * X ω)

case refine_2.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 ω)) μ
h_int_add : Integrable (fun a => rexp ((v + t) * X a) + rexp ((v - t) * X a)) μ
ω : Ω
h_nonpos : X ω ≤ 0
⊢ rexp (t * |X ω| + v * X ω) ≤ rexp ((v + t) * X ω) + rexp ((v - t) * X ω)

Proof state:
case neg.refine_1
Ω : 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 ω)) μ
h_int_add : Integrable (fun a => rexp ((v + t) * X a) + rexp ((v - t) * X a)) μ
ht : ¬t = 0
⊢ v + t - (v - t) ≠ 0

Tactic:
simp [ht]

Result:
no goals

Proof state:
case refine_2.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 ω)) μ
h_int_add : Integrable (fun a => rexp ((v + t) * X a) + rexp ((v - t) * X a)) μ
ω : Ω
h_nonneg : 0 ≤ X ω
⊢ rexp (t * |X ω| + v * X ω) ≤ rexp ((v + t) * X ω) + rexp ((v - t) * X ω)

Tactic:
rw [abs_of_nonneg h_nonneg, ← add_mul, add_comm, le_add_iff_nonneg_right]

Result:
case refine_2.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 ω)) μ
h_int_add : Integrable (fun a => rexp ((v + t) * X a) + rexp ((v - t) * X a)) μ
ω : Ω
h_nonneg : 0 ≤ X ω
⊢ 0 ≤ rexp ((v - t) * X ω)

Proof state:
case neg.refine_2
Ω : 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 ω)) μ
h_int_add : Integrable (fun a => rexp ((v + t) * X a) + rexp ((v - t) * X a)) μ
ht : ¬t = 0
hX : AEMeasurable X μ
⊢ AEStronglyMeasurable (fun ω => rexp (t * |X ω| + v * X ω)) μ

Tactic:
refine AEMeasurable.aestronglyMeasurable ?_

Result:
case neg.refine_2
Ω : 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 ω)) μ
h_int_add : Integrable (fun a => rexp ((v + t) * X a) + rexp ((v - t) * X a)) μ
ht : ¬t = 0
hX : AEMeasurable X μ
⊢ AEMeasurable (fun ω => rexp (t * |X ω| + v * X ω)) μ

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 ω)) μ
h_int_add : Integrable (fun a => rexp ((v + t) * X a) + rexp ((v - t) * X a)) μ
⊢ Integrable (fun ω => rexp (t * |X ω| + v * X ω)) μ

Tactic:
refine Integrable.mono h_int_add ?_ (ae_of_all _ fun ω ↦ ?_)

Result:
case refine_1
Ω : 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 ω)) μ
h_int_add : Integrable (fun a => rexp ((v + t) * X a) + rexp ((v - t) * X a)) μ
⊢ AEStronglyMeasurable (fun ω => rexp (t * |X ω| + v * X ω)) μ

case refine_2
Ω : 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 ω)) μ
h_int_add : Integrable (fun a => rexp ((v + t) * X a) + rexp ((v - t) * X a)) μ
ω : Ω
⊢ ‖rexp (t * |X ω| + v * X ω)‖ ≤ ‖rexp ((v + t) * X ω) + rexp ((v - t) * X ω)‖