-- Mathlib/Probability/Moments/IntegrableExpMul.lean
/-- If `exp ((v + t) * X)` and `exp ((v - t) * X)` are integrable
then for nonnegative `p : ℝ` and any `x ∈ [0, |t|)`,
`|X| ^ p * exp (v * X + x * |X|)` is integrable. -/
lemma integrable_rpow_abs_mul_exp_add_of_integrable_exp_mul {x : ℝ}
    (h_int_pos : Integrable (fun ω ↦ exp ((v + t) * X ω)) μ)
    (h_int_neg : Integrable (fun ω ↦ exp ((v - t) * X ω)) μ) (h_nonneg : 0 ≤ x) (hx : x < |t|)
    {p : ℝ} (hp : 0 ≤ p) :
    Integrable (fun a ↦ |X a| ^ p * exp (v * X a + x * |X a|)) μ

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

Tactic:
exact AEMeasurable.aestronglyMeasurable <| by fun_prop

Result:
no goals

Proof state:
case refine_1
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v x : ℝ
h_int_pos : Integrable (fun ω => rexp ((v + t) * X ω)) μ
h_int_neg : Integrable (fun ω => rexp ((v - t) * X ω)) μ
h_nonneg : 0 ≤ x
hx : x < |t|
p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
⊢ v + t ≠ v - t

Tactic:
rw [← sub_ne_zero]

Result:
case refine_1
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v x : ℝ
h_int_pos : Integrable (fun ω => rexp ((v + t) * X ω)) μ
h_int_neg : Integrable (fun ω => rexp ((v - t) * X ω)) μ
h_nonneg : 0 ≤ x
hx : x < |t|
p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
⊢ v + t - (v - t) ≠ 0

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

Tactic:
have : |t| = |t| - x + x := by simp

Result:
case h
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v x : ℝ
h_int_pos : Integrable (fun ω => rexp ((v + t) * X ω)) μ
h_int_neg : Integrable (fun ω => rexp ((v - t) * X ω)) μ
h_nonneg : 0 ≤ x
hx : x < |t|
p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
hX : AEMeasurable X μ
a : Ω
this : |t| = |t| - x + x
⊢ |X a| ^ p * rexp (x * |X a|) ≤ (p / (|t| - x)) ^ p * rexp (|t| * |X a|)

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

case refine_1
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v x : ℝ
h_int_pos : Integrable (fun ω => rexp ((v + t) * X ω)) μ
h_int_neg : Integrable (fun ω => rexp ((v - t) * X ω)) μ
h_nonneg : 0 ≤ x
hx : x < |t|
p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
⊢ v + t ≠ v - t

Tactic:
swap

Result:
case refine_1
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v x : ℝ
h_int_pos : Integrable (fun ω => rexp ((v + t) * X ω)) μ
h_int_neg : Integrable (fun ω => rexp ((v - t) * X ω)) μ
h_nonneg : 0 ≤ x
hx : x < |t|
p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
⊢ v + t ≠ v - t

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

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

case refine_2
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v x : ℝ
h_int_pos : Integrable (fun ω => rexp ((v + t) * X ω)) μ
h_int_neg : Integrable (fun ω => rexp ((v - t) * X ω)) μ
h_nonneg : 0 ≤ x
hx : x < |t|
p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
hX : AEMeasurable X μ
⊢ AEStronglyMeasurable (fun a => |X a| ^ p * rexp (v * X a + x * |X a|)) μ

Tactic:
swap

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

case refine_2
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v x : ℝ
h_int_pos : Integrable (fun ω => rexp ((v + t) * X ω)) μ
h_int_neg : Integrable (fun ω => rexp ((v - t) * X ω)) μ
h_nonneg : 0 ≤ x
hx : x < |t|
p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
hX : AEMeasurable X μ
⊢ Integrable (fun a => ‖|X a| ^ p * rexp (v * X a + x * |X a|)‖) μ

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v x : ℝ
h_int_pos : Integrable (fun ω => rexp ((v + t) * X ω)) μ
h_int_neg : Integrable (fun ω => rexp ((v - t) * X ω)) μ
h_nonneg : 0 ≤ x
hx : x < |t|
p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
⊢ Integrable (fun a => |X a| ^ p * rexp (v * X a + x * |X a|)) μ

Tactic:
have hX : AEMeasurable X μ := aemeasurable_of_integrable_exp_mul ?_ h_int_pos h_int_neg

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

case refine_1
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v x : ℝ
h_int_pos : Integrable (fun ω => rexp ((v + t) * X ω)) μ
h_int_neg : Integrable (fun ω => rexp ((v - t) * X ω)) μ
h_nonneg : 0 ≤ x
hx : x < |t|
p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
⊢ v + t ≠ v - t

Proof state:
case refine_2.refine_3
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v x : ℝ
h_int_pos : Integrable (fun ω => rexp ((v + t) * X ω)) μ
h_int_neg : Integrable (fun ω => rexp ((v - t) * X ω)) μ
h_nonneg : 0 ≤ x
hx : x < |t|
p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
hX : AEMeasurable X μ
h_le : ∀ (a : Ω), |X a| ^ p * rexp (v * X a + x * |X a|) ≤ (p / (|t| - x)) ^ p * rexp (v * X a + |t| * |X a|)
ω : Ω
⊢ ‖||X ω| ^ p| * rexp (v * X ω + x * |X ω|)‖ ≤ ‖(fun a => (p / (|t| - x)) ^ p * rexp (v * X a + |t| * |X a|)) ω‖

Tactic:
simp only [sq_abs, norm_mul, norm_pow, norm_eq_abs, abs_exp, norm_div, norm_ofNat]

Result:
case refine_2.refine_3
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v x : ℝ
h_int_pos : Integrable (fun ω => rexp ((v + t) * X ω)) μ
h_int_neg : Integrable (fun ω => rexp ((v - t) * X ω)) μ
h_nonneg : 0 ≤ x
hx : x < |t|
p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
hX : AEMeasurable X μ
h_le : ∀ (a : Ω), |X a| ^ p * rexp (v * X a + x * |X a|) ≤ (p / (|t| - x)) ^ p * rexp (v * X a + |t| * |X a|)
ω : Ω
⊢ |(||X ω| ^ p|)| * rexp (v * X ω + x * |X ω|) ≤ |(p / (|t| - x)) ^ p| * rexp (v * X ω + |t| * |X ω|)