-- 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:
refine (h_le ω).trans_eq ?_

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

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 : Ω
⊢ |t| = |t| - x + x

Tactic:
simp

Result:
no goals

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

Tactic:
rw [← integrable_norm_iff]

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_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|)) μ

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

Tactic:
congr

Result:
case refine_2.refine_3.e_a
Ω : 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|)
ω : Ω
⊢ (p / (|t| - x)) ^ p = |(p / (|t| - x)) ^ p|

Proof state:
case h.e'_4.h.e'_6.h.e'_1.h.e'_5
Ω : 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
⊢ 0 ≤ |t| - x

Tactic:
simp [hx.le]

Result:
no goals

Proof state:
case h.e'_4.h.e'_5.h.e'_5.h.e'_6
Ω : 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
⊢ 0 ≤ |t| - x

Tactic:
simp [hx.le]

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

Tactic:
nth_rw 2 [this]

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) * |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 μ
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 => ||X a| ^ p| * rexp (v * X a + x * |X a|)) μ

Tactic:
refine Integrable.mono (g := fun a ↦ (p / (|t| - x)) ^ p * exp (v * X a + |t| * |X a|))
  ?_ ?_ <| ae_of_all _ fun ω ↦ ?_

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 => (p / (|t| - x)) ^ p * rexp (v * X a + |t| * |X a|)) μ

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

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