-- Mathlib/Probability/Moments/IntegrableExpMul.lean
/-- If `ω ↦ exp (u * X ω)` is integrable at `u` and `-u`, then it is integrable on `[-u, u]`. -/
lemma integrable_exp_mul_of_abs_le
    (hu_int_pos : Integrable (fun ω ↦ exp (u * X ω)) μ)
    (hu_int_neg : Integrable (fun ω ↦ exp (- u * X ω)) μ)
    (htu : |t| ≤ |u|) :
    Integrable (fun ω ↦ exp (t * X ω)) μ

Proof state:
case refine_3
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t u : ℝ
hu_int_pos : Integrable (fun ω => rexp (u * X ω)) μ
hu_int_neg : Integrable (fun ω => rexp (-u * X ω)) μ
htu : |t| ≤ |u|
⊢ -|u| ≤ t

Tactic:
rw [neg_le]

Result:
case refine_3
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t u : ℝ
hu_int_pos : Integrable (fun ω => rexp (u * X ω)) μ
hu_int_neg : Integrable (fun ω => rexp (-u * X ω)) μ
htu : |t| ≤ |u|
⊢ -t ≤ |u|

Proof state:
case refine_2.inl
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t u : ℝ
hu_int_pos : Integrable (fun ω => rexp (u * X ω)) μ
hu_int_neg : Integrable (fun ω => rexp (-u * X ω)) μ
htu : |t| ≤ |u|
hu : 0 ≤ u
⊢ Integrable (fun ω => rexp (|u| * X ω)) μ

Tactic:
rwa [abs_of_nonneg hu]

Result:
no goals

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t u : ℝ
hu_int_pos : Integrable (fun ω => rexp (u * X ω)) μ
hu_int_neg : Integrable (fun ω => rexp (-u * X ω)) μ
htu : |t| ≤ |u|
⊢ Integrable (fun ω => rexp (t * X ω)) μ

Tactic:
refine integrable_exp_mul_of_le_of_le (a := -|u|) (b := |u|) ?_ ?_ ?_ ?_

Result:
case refine_1
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t u : ℝ
hu_int_pos : Integrable (fun ω => rexp (u * X ω)) μ
hu_int_neg : Integrable (fun ω => rexp (-u * X ω)) μ
htu : |t| ≤ |u|
⊢ Integrable (fun ω => rexp (-|u| * X ω)) μ

case refine_2
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t u : ℝ
hu_int_pos : Integrable (fun ω => rexp (u * X ω)) μ
hu_int_neg : Integrable (fun ω => rexp (-u * X ω)) μ
htu : |t| ≤ |u|
⊢ Integrable (fun ω => rexp (|u| * X ω)) μ

case refine_3
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t u : ℝ
hu_int_pos : Integrable (fun ω => rexp (u * X ω)) μ
hu_int_neg : Integrable (fun ω => rexp (-u * X ω)) μ
htu : |t| ≤ |u|
⊢ -|u| ≤ t

case refine_4
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t u : ℝ
hu_int_pos : Integrable (fun ω => rexp (u * X ω)) μ
hu_int_neg : Integrable (fun ω => rexp (-u * X ω)) μ
htu : |t| ≤ |u|
⊢ t ≤ |u|

Proof state:
case refine_4
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t u : ℝ
hu_int_pos : Integrable (fun ω => rexp (u * X ω)) μ
hu_int_neg : Integrable (fun ω => rexp (-u * X ω)) μ
htu : |t| ≤ |u|
⊢ t ≤ |u|

Tactic:
exact (le_abs_self t).trans htu

Result:
no goals

Proof state:
case refine_1
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t u : ℝ
hu_int_pos : Integrable (fun ω => rexp (u * X ω)) μ
hu_int_neg : Integrable (fun ω => rexp (-u * X ω)) μ
htu : |t| ≤ |u|
⊢ Integrable (fun ω => rexp (-|u| * X ω)) μ

Tactic:
rcases le_total 0 u with hu | hu

Result:
case refine_1.inl
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t u : ℝ
hu_int_pos : Integrable (fun ω => rexp (u * X ω)) μ
hu_int_neg : Integrable (fun ω => rexp (-u * X ω)) μ
htu : |t| ≤ |u|
hu : 0 ≤ u
⊢ Integrable (fun ω => rexp (-|u| * X ω)) μ

case refine_1.inr
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t u : ℝ
hu_int_pos : Integrable (fun ω => rexp (u * X ω)) μ
hu_int_neg : Integrable (fun ω => rexp (-u * X ω)) μ
htu : |t| ≤ |u|
hu : u ≤ 0
⊢ Integrable (fun ω => rexp (-|u| * X ω)) μ

Proof state:
case refine_3
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t u : ℝ
hu_int_pos : Integrable (fun ω => rexp (u * X ω)) μ
hu_int_neg : Integrable (fun ω => rexp (-u * X ω)) μ
htu : |t| ≤ |u|
⊢ -t ≤ |u|

Tactic:
exact (neg_le_abs t).trans htu

Result:
no goals

Proof state:
case refine_1.inl
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t u : ℝ
hu_int_pos : Integrable (fun ω => rexp (u * X ω)) μ
hu_int_neg : Integrable (fun ω => rexp (-u * X ω)) μ
htu : |t| ≤ |u|
hu : 0 ≤ u
⊢ Integrable (fun ω => rexp (-|u| * X ω)) μ

Tactic:
rwa [abs_of_nonneg hu]

Result:
no goals

Proof state:
case refine_1.inr
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t u : ℝ
hu_int_pos : Integrable (fun ω => rexp (u * X ω)) μ
hu_int_neg : Integrable (fun ω => rexp (-u * X ω)) μ
htu : |t| ≤ |u|
hu : u ≤ 0
⊢ Integrable (fun ω => rexp (-|u| * X ω)) μ

Tactic:
simpa [abs_of_nonpos hu]

Result:
no goals

Proof state:
case refine_2.inr
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t u : ℝ
hu_int_pos : Integrable (fun ω => rexp (u * X ω)) μ
hu_int_neg : Integrable (fun ω => rexp (-u * X ω)) μ
htu : |t| ≤ |u|
hu : u ≤ 0
⊢ Integrable (fun ω => rexp (|u| * X ω)) μ

Tactic:
rwa [abs_of_nonpos hu]

Result:
no goals

Proof state:
case refine_2
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t u : ℝ
hu_int_pos : Integrable (fun ω => rexp (u * X ω)) μ
hu_int_neg : Integrable (fun ω => rexp (-u * X ω)) μ
htu : |t| ≤ |u|
⊢ Integrable (fun ω => rexp (|u| * X ω)) μ

Tactic:
rcases le_total 0 u with hu | hu

Result:
case refine_2.inl
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t u : ℝ
hu_int_pos : Integrable (fun ω => rexp (u * X ω)) μ
hu_int_neg : Integrable (fun ω => rexp (-u * X ω)) μ
htu : |t| ≤ |u|
hu : 0 ≤ u
⊢ Integrable (fun ω => rexp (|u| * X ω)) μ

case refine_2.inr
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t u : ℝ
hu_int_pos : Integrable (fun ω => rexp (u * X ω)) μ
hu_int_neg : Integrable (fun ω => rexp (-u * X ω)) μ
htu : |t| ≤ |u|
hu : u ≤ 0
⊢ Integrable (fun ω => rexp (|u| * X ω)) μ