-- Mathlib/Probability/Moments/IntegrableExpMul.lean
lemma integrable_exp_mul_of_le_of_le {a b : ℝ}
    (ha : Integrable (fun ω ↦ exp (a * X ω)) μ) (hb : Integrable (fun ω ↦ exp (b * X ω)) μ)
    (hat : a ≤ t) (htb : t ≤ b) :
    Integrable (fun ω ↦ exp (t * X ω)) μ

Proof state:
case refine_2
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t a b : ℝ
ha : Integrable (fun ω => rexp (a * X ω)) μ
hb : Integrable (fun ω => rexp (b * X ω)) μ
hat : a ≤ t
htb : t ≤ b
ω : Ω
⊢ rexp (t * X ω) ≤ rexp (a * X ω) + rexp (b * X ω)

Tactic:
rcases le_total 0 (X ω) with h | h

Result:
case refine_2.inl
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t a b : ℝ
ha : Integrable (fun ω => rexp (a * X ω)) μ
hb : Integrable (fun ω => rexp (b * X ω)) μ
hat : a ≤ t
htb : t ≤ b
ω : Ω
h : 0 ≤ X ω
⊢ rexp (t * X ω) ≤ rexp (a * X ω) + rexp (b * X ω)

case refine_2.inr
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t a b : ℝ
ha : Integrable (fun ω => rexp (a * X ω)) μ
hb : Integrable (fun ω => rexp (b * X ω)) μ
hat : a ≤ t
htb : t ≤ b
ω : Ω
h : X ω ≤ 0
⊢ rexp (t * X ω) ≤ rexp (a * X ω) + rexp (b * X ω)

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t a b : ℝ
ha : Integrable (fun ω => rexp (a * X ω)) μ
hb : Integrable (fun ω => rexp (b * X ω)) μ
hat : a ≤ t
htb : t ≤ b
⊢ Integrable (fun ω => rexp (t * X ω)) μ

Tactic:
refine Integrable.mono (ha.add hb) ?_ (ae_of_all _ fun ω ↦ ?_)

Result:
case refine_1
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t a b : ℝ
ha : Integrable (fun ω => rexp (a * X ω)) μ
hb : Integrable (fun ω => rexp (b * X ω)) μ
hat : a ≤ t
htb : t ≤ b
⊢ AEStronglyMeasurable (fun ω => rexp (t * X ω)) μ

case refine_2
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t a b : ℝ
ha : Integrable (fun ω => rexp (a * X ω)) μ
hb : Integrable (fun ω => rexp (b * X ω)) μ
hat : a ≤ t
htb : t ≤ b
ω : Ω
⊢ ‖rexp (t * X ω)‖ ≤ ‖((fun ω => rexp (a * X ω)) + fun ω => rexp (b * X ω)) ω‖

Proof state:
case pos
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t a b : ℝ
ha : Integrable (fun ω => rexp (a * X ω)) μ
hb : Integrable (fun ω => rexp (b * X ω)) μ
hat : a ≤ t
htb : t ≤ b
hab : ¬0 = b
ha_zero : a = 0
⊢ b ≠ 0

Tactic:
exact Ne.symm hab

Result:
no goals

Proof state:
case pos
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t a b : ℝ
ha : Integrable (fun ω => rexp (a * X ω)) μ
hb : Integrable (fun ω => rexp (b * X ω)) μ
hat : a ≤ t
htb : t ≤ b
hab : ¬a = b
ha_zero : a = 0
⊢ AEMeasurable X μ

Tactic:
refine aemeasurable_of_aemeasurable_exp_mul ?_ hb.1.aemeasurable

Result:
case pos
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t a b : ℝ
ha : Integrable (fun ω => rexp (a * X ω)) μ
hb : Integrable (fun ω => rexp (b * X ω)) μ
hat : a ≤ t
htb : t ≤ b
hab : ¬a = b
ha_zero : a = 0
⊢ b ≠ 0

Proof state:
case refine_1
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t a b : ℝ
ha : Integrable (fun ω => rexp (a * X ω)) μ
hb : Integrable (fun ω => rexp (b * X ω)) μ
hat : a ≤ t
htb : t ≤ b
⊢ AEStronglyMeasurable (fun ω => rexp (t * X ω)) μ

Tactic:
by_cases hab : a = b

Result:
case pos
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t a b : ℝ
ha : Integrable (fun ω => rexp (a * X ω)) μ
hb : Integrable (fun ω => rexp (b * X ω)) μ
hat : a ≤ t
htb : t ≤ b
hab : a = b
⊢ AEStronglyMeasurable (fun ω => rexp (t * X ω)) μ

case neg
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t a b : ℝ
ha : Integrable (fun ω => rexp (a * X ω)) μ
hb : Integrable (fun ω => rexp (b * X ω)) μ
hat : a ≤ t
htb : t ≤ b
hab : ¬a = b
⊢ AEStronglyMeasurable (fun ω => rexp (t * X ω)) μ

Proof state:
case pos
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t a b : ℝ
ha : Integrable (fun ω => rexp (a * X ω)) μ
hb : Integrable (fun ω => rexp (b * X ω)) μ
hat : a ≤ t
htb : t ≤ b
hab : a = b
⊢ AEStronglyMeasurable (fun ω => rexp (t * X ω)) μ

Tactic:
have ha_eq_t : a = t := le_antisymm hat (hab ▸ htb)

Result:
case pos
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t a b : ℝ
ha : Integrable (fun ω => rexp (a * X ω)) μ
hb : Integrable (fun ω => rexp (b * X ω)) μ
hat : a ≤ t
htb : t ≤ b
hab : a = b
ha_eq_t : a = t
⊢ AEStronglyMeasurable (fun ω => rexp (t * X ω)) μ

Proof state:
case pos
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t a b : ℝ
ha : Integrable (fun ω => rexp (a * X ω)) μ
hb : Integrable (fun ω => rexp (b * X ω)) μ
hat : a ≤ t
htb : t ≤ b
hab : ¬a = b
ha_zero : a = 0
⊢ b ≠ 0

Tactic:
rw [ha_zero] at hab

Result:
case pos
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t a b : ℝ
ha : Integrable (fun ω => rexp (a * X ω)) μ
hb : Integrable (fun ω => rexp (b * X ω)) μ
hat : a ≤ t
htb : t ≤ b
hab : ¬0 = b
ha_zero : a = 0
⊢ b ≠ 0

Proof state:
case neg
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t a b : ℝ
ha : Integrable (fun ω => rexp (a * X ω)) μ
hb : Integrable (fun ω => rexp (b * X ω)) μ
hat : a ≤ t
htb : t ≤ b
hab : ¬a = b
⊢ AEStronglyMeasurable (fun ω => rexp (t * X ω)) μ

Tactic:
refine AEMeasurable.aestronglyMeasurable ?_

Result:
case neg
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t a b : ℝ
ha : Integrable (fun ω => rexp (a * X ω)) μ
hb : Integrable (fun ω => rexp (b * X ω)) μ
hat : a ≤ t
htb : t ≤ b
hab : ¬a = b
⊢ AEMeasurable (fun ω => rexp (t * X ω)) μ

Proof state:
case neg
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t a b : ℝ
ha : Integrable (fun ω => rexp (a * X ω)) μ
hb : Integrable (fun ω => rexp (b * X ω)) μ
hat : a ≤ t
htb : t ≤ b
hab : ¬a = b
⊢ AEMeasurable (fun ω => rexp (t * X ω)) μ

Tactic:
refine measurable_exp.comp_aemeasurable (AEMeasurable.const_mul ?_ _)

Result:
case neg
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t a b : ℝ
ha : Integrable (fun ω => rexp (a * X ω)) μ
hb : Integrable (fun ω => rexp (b * X ω)) μ
hat : a ≤ t
htb : t ≤ b
hab : ¬a = b
⊢ AEMeasurable X μ

Proof state:
case pos
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t a b : ℝ
ha : Integrable (fun ω => rexp (a * X ω)) μ
hb : Integrable (fun ω => rexp (b * X ω)) μ
hat : a ≤ t
htb : t ≤ b
hab : a = b
ha_eq_t : a = t
⊢ AEStronglyMeasurable (fun ω => rexp (t * X ω)) μ

Tactic:
rw [← ha_eq_t]

Result:
case pos
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t a b : ℝ
ha : Integrable (fun ω => rexp (a * X ω)) μ
hb : Integrable (fun ω => rexp (b * X ω)) μ
hat : a ≤ t
htb : t ≤ b
hab : a = b
ha_eq_t : a = t
⊢ AEStronglyMeasurable (fun ω => rexp (a * X ω)) μ

Proof state:
case refine_2.inl
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t a b : ℝ
ha : Integrable (fun ω => rexp (a * X ω)) μ
hb : Integrable (fun ω => rexp (b * X ω)) μ
hat : a ≤ t
htb : t ≤ b
ω : Ω
h : 0 ≤ X ω
⊢ rexp (t * X ω) ≤ rexp (a * X ω) + rexp (b * X ω)

Tactic:
calc exp (t * X ω)
_ ≤ exp (b * X ω) := exp_le_exp.mpr (mul_le_mul_of_nonneg_right htb h)
_ ≤ exp (a * X ω) + exp (b * X ω) := le_add_of_nonneg_left (exp_nonneg _)

Result:
no goals

Proof state:
case refine_2
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t a b : ℝ
ha : Integrable (fun ω => rexp (a * X ω)) μ
hb : Integrable (fun ω => rexp (b * X ω)) μ
hat : a ≤ t
htb : t ≤ b
ω : Ω
⊢ ‖rexp (t * X ω)‖ ≤ ‖((fun ω => rexp (a * X ω)) + fun ω => rexp (b * X ω)) ω‖

Tactic:
simp only [norm_eq_abs, abs_exp, Pi.add_apply]

Result:
case refine_2
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t a b : ℝ
ha : Integrable (fun ω => rexp (a * X ω)) μ
hb : Integrable (fun ω => rexp (b * X ω)) μ
hat : a ≤ t
htb : t ≤ b
ω : Ω
⊢ rexp (t * X ω) ≤ |rexp (a * X ω) + rexp (b * X ω)|

Proof state:
case pos
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t a b : ℝ
ha : Integrable (fun ω => rexp (a * X ω)) μ
hb : Integrable (fun ω => rexp (b * X ω)) μ
hat : a ≤ t
htb : t ≤ b
hab : a = b
ha_eq_t : a = t
⊢ AEStronglyMeasurable (fun ω => rexp (a * X ω)) μ

Tactic:
exact ha.1

Result:
no goals