-- 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.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 ω|)

Tactic:
simp_rw [abs_rpow_of_nonneg (abs_nonneg _), abs_abs]

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 ω|)

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) ≠ 0

Tactic:
simp [ht]

Result:
no goals

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
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|)
⊢ AEMeasurable (fun a => ||X a| ^ p|) μ

Tactic:
fun_prop

Result:
no goals

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
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|)
⊢ AEMeasurable (fun a => v * X a + x * |X a|) μ

Tactic:
fun_prop

Result:
no goals

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 : Ω
this : |t| = |t| - x + x
⊢ |X a| ^ p * rexp (x * |X a|) ≤ (p / (|t| - x)) ^ p * rexp ((|t| - x) * |X a|) * rexp (x * |X a|)

Tactic:
gcongr ?_ * _

Result:
case h.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 ≤ (p / (|t| - x)) ^ p * rexp ((|t| - 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
⊢ |t| ≠ 0

Tactic:
exact (h_nonneg.trans_lt hx).ne'

Result:
no goals

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

Tactic:
simp_rw [add_comm (v * X _)]

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

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 : Ω
this : |t| = |t| - x + x
⊢ |X a| ^ p * rexp (x * |X a|) ≤ (p / (|t| - x)) ^ p * rexp ((|t| - x + x) * |X a|)

Tactic:
rw [add_mul, exp_add, ← mul_assoc]

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) * |X a|) * rexp (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
hX : AEMeasurable X μ
a : Ω
⊢ |X a| ^ p * rexp (x * |X a|) * rexp (v * X a) ≤ (p / (|t| - x)) ^ p * rexp (|t| * |X a|) * rexp (v * X a)

Tactic:
gcongr ?_ * _

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 : Ω
⊢ |X a| ^ p * rexp (x * |X a|) ≤ (p / (|t| - x)) ^ p * rexp (|t| * |X a|)

Proof state:
case refine_2.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 μ
h_le : ∀ (a : Ω), |X a| ^ p * rexp (v * X a + x * |X a|) ≤ (p / (|t| - x)) ^ p * rexp (v * X a + |t| * |X a|)
⊢ AEStronglyMeasurable (fun a => ||X a| ^ p| * rexp (v * X a + x * |X a|)) μ

Tactic:
refine AEMeasurable.aestronglyMeasurable ?_

Result:
case refine_2.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 μ
h_le : ∀ (a : Ω), |X a| ^ p * rexp (v * X a + x * |X a|) ≤ (p / (|t| - x)) ^ p * rexp (v * X a + |t| * |X a|)
⊢ AEMeasurable (fun a => ||X a| ^ p| * rexp (v * X a + x * |X a|)) μ