-- Mathlib/Probability/Moments/IntegrableExpMul.lean
/-- If `exp ((v + t) * X)` and `exp ((v - t) * X)` are integrable, then for all nonnegative `p : ℝ`,
`X ^ p * exp (v * X)` is integrable. -/
lemma integrable_rpow_mul_exp_of_integrable_exp_mul (ht : t ≠ 0)
    (ht_int_pos : Integrable (fun ω ↦ exp ((v + t) * X ω)) μ)
    (ht_int_neg : Integrable (fun ω ↦ exp ((v - t) * X ω)) μ) {p : ℝ} (hp : 0 ≤ p) :
    Integrable (fun ω ↦ X ω ^ p * exp (v * X ω)) μ

Proof state:
case refine_2
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v : ℝ
ht : t ≠ 0
ht_int_pos : Integrable (fun ω => rexp ((v + t) * X ω)) μ
ht_int_neg : Integrable (fun ω => rexp ((v - t) * X ω)) μ
p : ℝ
hp : 0 ≤ p
hX : AEMeasurable X μ
h : Integrable (fun ω => |X ω| ^ p * rexp (v * X ω)) μ
⊢ Integrable (fun a => |X a ^ p| * rexp (v * X a)) μ

Tactic:
refine h.mono' ?_ ?_

Result:
case refine_2.refine_1
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v : ℝ
ht : t ≠ 0
ht_int_pos : Integrable (fun ω => rexp ((v + t) * X ω)) μ
ht_int_neg : Integrable (fun ω => rexp ((v - t) * X ω)) μ
p : ℝ
hp : 0 ≤ p
hX : AEMeasurable X μ
h : Integrable (fun ω => |X ω| ^ p * rexp (v * X ω)) μ
⊢ AEStronglyMeasurable (fun a => |X a ^ p| * rexp (v * X a)) μ

case refine_2.refine_2
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v : ℝ
ht : t ≠ 0
ht_int_pos : Integrable (fun ω => rexp ((v + t) * X ω)) μ
ht_int_neg : Integrable (fun ω => rexp ((v - t) * X ω)) μ
p : ℝ
hp : 0 ≤ p
hX : AEMeasurable X μ
h : Integrable (fun ω => |X ω| ^ p * rexp (v * X ω)) μ
⊢ ∀ᵐ (a : Ω) ∂μ, ‖|X a ^ p| * rexp (v * X a)‖ ≤ |X a| ^ p * rexp (v * X a)

Proof state:
case refine_2.refine_2.h
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v : ℝ
ht : t ≠ 0
ht_int_pos : Integrable (fun ω => rexp ((v + t) * X ω)) μ
ht_int_neg : Integrable (fun ω => rexp ((v - t) * X ω)) μ
p : ℝ
hp : 0 ≤ p
hX : AEMeasurable X μ
h : Integrable (fun ω => |X ω| ^ p * rexp (v * X ω)) μ
ω : Ω
⊢ |X ω ^ p| ≤ |X ω| ^ p

Tactic:
exact abs_rpow_le_abs_rpow _ _

Result:
no goals

Proof state:
case refine_2
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v : ℝ
ht : t ≠ 0
ht_int_pos : Integrable (fun ω => rexp ((v + t) * X ω)) μ
ht_int_neg : Integrable (fun ω => rexp ((v - t) * X ω)) μ
p : ℝ
hp : 0 ≤ p
hX : AEMeasurable X μ
⊢ Integrable (fun a => ‖X a ^ p * rexp (v * X a)‖) μ

Tactic:
simp_rw [norm_eq_abs, abs_mul, abs_exp]

Result:
case refine_2
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v : ℝ
ht : t ≠ 0
ht_int_pos : Integrable (fun ω => rexp ((v + t) * X ω)) μ
ht_int_neg : Integrable (fun ω => rexp ((v - t) * X ω)) μ
p : ℝ
hp : 0 ≤ p
hX : AEMeasurable X μ
⊢ Integrable (fun a => |X a ^ p| * rexp (v * X a)) μ

Proof state:
case refine_2
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v : ℝ
ht : t ≠ 0
ht_int_pos : Integrable (fun ω => rexp ((v + t) * X ω)) μ
ht_int_neg : Integrable (fun ω => rexp ((v - t) * X ω)) μ
p : ℝ
hp : 0 ≤ p
hX : AEMeasurable X μ
⊢ Integrable (fun ω => X ω ^ p * rexp (v * X ω)) μ

Tactic:
rw [← integrable_norm_iff]

Result:
case refine_2
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v : ℝ
ht : t ≠ 0
ht_int_pos : Integrable (fun ω => rexp ((v + t) * X ω)) μ
ht_int_neg : Integrable (fun ω => rexp ((v - t) * X ω)) μ
p : ℝ
hp : 0 ≤ p
hX : AEMeasurable X μ
⊢ Integrable (fun a => ‖X a ^ p * rexp (v * X a)‖) μ

case refine_2
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v : ℝ
ht : t ≠ 0
ht_int_pos : Integrable (fun ω => rexp ((v + t) * X ω)) μ
ht_int_neg : Integrable (fun ω => rexp ((v - t) * X ω)) μ
p : ℝ
hp : 0 ≤ p
hX : AEMeasurable X μ
⊢ AEStronglyMeasurable (fun ω => X ω ^ p * rexp (v * X ω)) μ

Proof state:
case refine_2.refine_1
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v : ℝ
ht : t ≠ 0
ht_int_pos : Integrable (fun ω => rexp ((v + t) * X ω)) μ
ht_int_neg : Integrable (fun ω => rexp ((v - t) * X ω)) μ
p : ℝ
hp : 0 ≤ p
hX : AEMeasurable X μ
h : Integrable (fun ω => |X ω| ^ p * rexp (v * X ω)) μ
⊢ AEStronglyMeasurable (fun a => |X a ^ p| * rexp (v * X a)) μ

Tactic:
exact ((hX.pow_const _).abs.mul
  (measurable_exp.comp_aemeasurable (hX.const_mul _))).aestronglyMeasurable

Result:
no goals

Proof state:
case refine_2
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v : ℝ
ht : t ≠ 0
ht_int_pos : Integrable (fun ω => rexp ((v + t) * X ω)) μ
ht_int_neg : Integrable (fun ω => rexp ((v - t) * X ω)) μ
p : ℝ
hp : 0 ≤ p
hX : AEMeasurable X μ
⊢ Integrable (fun ω => X ω ^ p * rexp (v * X ω)) μ

case refine_1
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v : ℝ
ht : t ≠ 0
ht_int_pos : Integrable (fun ω => rexp ((v + t) * X ω)) μ
ht_int_neg : Integrable (fun ω => rexp ((v - t) * X ω)) μ
p : ℝ
hp : 0 ≤ p
⊢ v + t ≠ v - t

Tactic:
swap

Result:
case refine_1
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v : ℝ
ht : t ≠ 0
ht_int_pos : Integrable (fun ω => rexp ((v + t) * X ω)) μ
ht_int_neg : Integrable (fun ω => rexp ((v - t) * X ω)) μ
p : ℝ
hp : 0 ≤ p
⊢ v + t ≠ v - t

case refine_2
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v : ℝ
ht : t ≠ 0
ht_int_pos : Integrable (fun ω => rexp ((v + t) * X ω)) μ
ht_int_neg : Integrable (fun ω => rexp ((v - t) * X ω)) μ
p : ℝ
hp : 0 ≤ p
hX : AEMeasurable X μ
⊢ Integrable (fun ω => X ω ^ p * rexp (v * X ω)) μ

Proof state:
case refine_2
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v : ℝ
ht : t ≠ 0
ht_int_pos : Integrable (fun ω => rexp ((v + t) * X ω)) μ
ht_int_neg : Integrable (fun ω => rexp ((v - t) * X ω)) μ
p : ℝ
hp : 0 ≤ p
hX : AEMeasurable X μ
⊢ AEStronglyMeasurable (fun ω => X ω ^ p * rexp (v * X ω)) μ

Tactic:
exact ((hX.pow_const _).mul
  (measurable_exp.comp_aemeasurable (hX.const_mul _))).aestronglyMeasurable

Result:
no goals

Proof state:
case refine_2.refine_2
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v : ℝ
ht : t ≠ 0
ht_int_pos : Integrable (fun ω => rexp ((v + t) * X ω)) μ
ht_int_neg : Integrable (fun ω => rexp ((v - t) * X ω)) μ
p : ℝ
hp : 0 ≤ p
hX : AEMeasurable X μ
h : Integrable (fun ω => |X ω| ^ p * rexp (v * X ω)) μ
ω : Ω
⊢ |X ω ^ p| * rexp (v * X ω) ≤ |X ω| ^ p * rexp (v * X ω)

Tactic:
gcongr

Result:
case refine_2.refine_2.h
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v : ℝ
ht : t ≠ 0
ht_int_pos : Integrable (fun ω => rexp ((v + t) * X ω)) μ
ht_int_neg : Integrable (fun ω => rexp ((v - t) * X ω)) μ
p : ℝ
hp : 0 ≤ p
hX : AEMeasurable X μ
h : Integrable (fun ω => |X ω| ^ p * rexp (v * X ω)) μ
ω : Ω
⊢ |X ω ^ p| ≤ |X ω| ^ p

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

Tactic:
have hX : AEMeasurable X μ := aemeasurable_of_integrable_exp_mul ?_ ht_int_pos ht_int_neg

Result:
case refine_2
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v : ℝ
ht : t ≠ 0
ht_int_pos : Integrable (fun ω => rexp ((v + t) * X ω)) μ
ht_int_neg : Integrable (fun ω => rexp ((v - t) * X ω)) μ
p : ℝ
hp : 0 ≤ p
hX : AEMeasurable X μ
⊢ Integrable (fun ω => X ω ^ p * rexp (v * X ω)) μ

case refine_1
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v : ℝ
ht : t ≠ 0
ht_int_pos : Integrable (fun ω => rexp ((v + t) * X ω)) μ
ht_int_neg : Integrable (fun ω => rexp ((v - t) * X ω)) μ
p : ℝ
hp : 0 ≤ p
⊢ v + t ≠ v - t