awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : 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 (v * X a + x * |X a|) ≤ (p / (|t| - x)) ^ p * rexp (v * X a + |t| * |X a|)

Tactic:
have h_le a : |X a| ^ p * exp (v * X a + x * |X a|)
      ≤ (p / (|t| - x)) ^ p * exp (v * X a + |t| * |X a|) := by
    simp_rw [exp_add, mul_comm (exp (v * X a)), ← mul_assoc]
    gcongr ?_ * _
    have : |t| = |t| - x + x := by simp
    nth_rw 2 [this]
    rw [add_mul, exp_add, ← mul_assoc]
    gcongr ?_ * _
    convert! rpow_abs_le_mul_exp_abs (X a) hp (t := |t| - x) _ using 4
    · nth_rw 2 [abs_of_nonneg]
      simp [hx.le]
    · nth_rw 2 [abs_of_nonneg]
      simp [hx.le]
    · rw [sub_ne_zero]
      exact hx.ne'
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : 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:
Integrable.mono (g := fun a ↦ (p / (|t| - x)) ^ p * exp (v * X a + |t| * |X a|))
    ?_ ?_ <| ae_of_all _ fun ω ↦ ?_

Premises used: MeasureTheory.Integrable.mono, MeasureTheory.ae_of_all
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : 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|)
refine_2 : Integrable (ε := ℝ) (fun (a : Ω) ↦ (p / (|t| - x)) ^ p * rexp (v * X a + |t| * |X a|)) μ
refine_2₁ : AEStronglyMeasurable (β := ℝ) (fun (a : Ω) ↦ ||X a| ^ p| * rexp (v * X a + x * |X a|)) μ
refine_2₂ :
  ∀ (ω : Ω),
    ‖||X ω| ^ p| * rexp (v * X ω + x * |X ω|)‖ ≤
      Norm.norm (E := ℝ) ((fun (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 ω ↦ ?_

Premises used: MeasureTheory.Integrable.mono, MeasureTheory.ae_of_all
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : 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|)) μ

Tactic:
Integrable.const_mul ?_ _

Premises used: MeasureTheory.Integrable.const_mul
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : 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|)
refine_2 : Integrable (ε := ℝ) (fun (a : Ω) ↦ rexp (v * X a + |t| * |X a|)) μ
⊢ Integrable (ε := ℝ) (fun (a : Ω) ↦ (p / (|t| - x)) ^ p * rexp (v * X a + |t| * |X a|)) μ

Tactic:
refine Integrable.const_mul ?_ _

Premises used: MeasureTheory.Integrable.const_mul
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : 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|)
refine_2 : Integrable (ε := ℝ) (fun (a : Ω) ↦ rexp (|t| * |X a| + v * X a)) μ
⊢ Integrable (ε := ℝ) (fun (a : Ω) ↦ rexp (v * X a + |t| * |X a|)) μ

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

Premises used: HMul.hMul, add_comm
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : 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)) μ

Tactic:
integrable_exp_abs_mul_abs_add h_int_pos h_int_neg

Premises used: ProbabilityTheory.integrable_exp_abs_mul_abs_add
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : 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)) μ

Tactic:
exact integrable_exp_abs_mul_abs_add h_int_pos h_int_neg

Premises used: ProbabilityTheory.integrable_exp_abs_mul_abs_add
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : 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|)
funProp : 0 ≤ p
⊢ AEStronglyMeasurable (β := ℝ) (fun (a : Ω) ↦ ||X a| ^ p| * rexp (v * X a + x * |X a|)) μ

Tactic:
fun_prop
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : 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|)
ω : Ω
refine_2 : |(||X ω| ^ p|)| * rexp (v * X ω + x * |X ω|) ≤ |(p / (|t| - x)) ^ p| * rexp (v * X ω + |t| * |X ω|)
⊢ ‖||X ω| ^ p| * rexp (v * X ω + x * |X ω|)‖ ≤
    Norm.norm (E := ℝ) ((fun (a : Ω) ↦ (p / (|t| - x)) ^ p * rexp (v * X a + |t| * |X a|)) ω)

Tactic:
simp only [norm_mul, norm_eq_abs, abs_exp]

Premises used: norm_mul, Real.norm_eq_abs, Real.abs_exp
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : 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|)
ω : Ω
refine_2 : |X ω| ^ p * rexp (v * X ω + x * |X ω|) ≤ |(p / (|t| - x)) ^ p| * rexp (v * X ω + |t| * |X ω|)
⊢ |(||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]

Premises used: Real.abs_rpow_of_nonneg, abs_abs, abs_nonneg
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : 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:
(h_le ω).trans_eq ?_

Premises used: LE.le.trans_eq
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : 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|)
ω : Ω
refine_2 : (p / (|t| - x)) ^ p * rexp (v * X ω + |t| * |X ω|) = |(p / (|t| - x)) ^ p| * rexp (v * X ω + |t| * |X ω|)
⊢ |X ω| ^ p * rexp (v * X ω + x * |X ω|) ≤ |(p / (|t| - x)) ^ p| * rexp (v * X ω + |t| * |X ω|)

Tactic:
refine (h_le ω).trans_eq ?_

Premises used: LE.le.trans_eq
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : 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|)
ω : Ω
refine_2 : (p / (|t| - x)) ^ p = |(p / (|t| - x)) ^ p|
⊢ (p / (|t| - x)) ^ p * rexp (v * X ω + |t| * |X ω|) = |(p / (|t| - x)) ^ p| * rexp (v * X ω + |t| * |X ω|)

Tactic:
congr
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : 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|)
ω : Ω
refine_2 : |(p / (|t| - x)) ^ p| = (p / (|t| - x)) ^ p
⊢ (p / (|t| - x)) ^ p = |(p / (|t| - x)) ^ p|

Tactic:
symm
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : 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|)
ω : Ω
refine_2 : 0 ≤ (p / (|t| - x)) ^ p
⊢ |(p / (|t| - x)) ^ p| = (p / (|t| - x)) ^ p

Tactic:
simp only [abs_eq_self]

Premises used: abs_eq_self
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : 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|)
ω : Ω
refine_2 refine_2₁ refine_2₂ refine_2₃ : 0 ≤ |t| - x → 0 ≤ (p / (|t| - x)) ^ p
⊢ 0 ≤ (p / (|t| - x)) ^ p

Tactic:
positivity [sub_nonneg_of_le hx.le]

Premises used: sub_nonneg_of_le, LT.lt.le
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : 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|
n : ℕ
⊢ Integrable (ε := ℝ) (fun (a : Ω) ↦ HPow.hPow (β := ℝ) |X a| (↑n : ℝ) * rexp (v * X a + x * |X a|)) μ

Tactic:
integrable_rpow_abs_mul_exp_add_of_integrable_exp_mul h_int_pos h_int_neg h_nonneg hx
      n.cast_nonneg

Premises used: Nat.cast_nonneg, ProbabilityTheory.integrable_rpow_abs_mul_exp_add_of_integrable_exp_mul
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : 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|
n : ℕ
h : ∀ (x : Ω), |X x| ^ n = HPow.hPow (β := ℝ) |X x| (↑n : ℝ)
⊢ Integrable (ε := ℝ) (fun (a : Ω) ↦ |X a| ^ n * rexp (v * X a + x * |X a|)) μ

Tactic:
convert!
    integrable_rpow_abs_mul_exp_add_of_integrable_exp_mul h_int_pos h_int_neg h_nonneg hx
      n.cast_nonneg

Premises used: Nat.cast_nonneg, ProbabilityTheory.integrable_rpow_abs_mul_exp_add_of_integrable_exp_mul
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : 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|
n : ℕ
x_1 : Ω
⊢ |X x_1| ^ n = HPow.hPow (β := ℝ) |X x_1| (↑n : ℝ)

Tactic:
simp
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : 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 (a : Ω) ↦ |X a| ^ p * rexp (v * X a + 0 * |X a|)) μ

Tactic:
integrable_rpow_abs_mul_exp_add_of_integrable_exp_mul ht_int_pos ht_int_neg le_rfl _ hp

Premises used: le_rfl, ProbabilityTheory.integrable_rpow_abs_mul_exp_add_of_integrable_exp_mul
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : 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
h : ∀ (x : Ω), v * X x = v * X x + 0 * |X x|
integrable_rpow_abs_mul_exp_add_of_integrable_exp_mul : 0 < |t|
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ |X ω| ^ p * rexp (v * X ω)) μ

Tactic:
convert!
    integrable_rpow_abs_mul_exp_add_of_integrable_exp_mul ht_int_pos ht_int_neg le_rfl _ hp using 4

Premises used: le_rfl, ProbabilityTheory.integrable_rpow_abs_mul_exp_add_of_integrable_exp_mul
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : 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
x : Ω
⊢ v * X x = v * X x + 0 * |X x|

Tactic:
simp
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : 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
⊢ 0 < |t|

Tactic:
simp [ht]
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : 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 ω)) μ
n : ℕ
⊢ LE.le (α := ℝ) 0 (↑n : ℝ)

Tactic:
positivity
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : 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 ω)) μ
n : ℕ
h : ∀ (ω : Ω), |X ω| ^ n = HPow.hPow (β := ℝ) |X ω| (↑n : ℝ)
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ |X ω| ^ n * rexp (v * X ω)) μ

Tactic:
convert!
    integrable_rpow_abs_mul_exp_of_integrable_exp_mul ht ht_int_pos ht_int_neg
      (by positivity : 0 ≤ (n : ℝ)) with
    ω

Premises used: ProbabilityTheory.integrable_rpow_abs_mul_exp_of_integrable_exp_mul
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : 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 ω)) μ
n : ℕ
ω : Ω
⊢ |X ω| ^ n = HPow.hPow (β := ℝ) |X ω| (↑n : ℝ)

Tactic:
simp
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : 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
refine_2 : ∀ (hX : AEMeasurable X μ), Integrable (ε := ℝ) (fun (ω : Ω) ↦ X ω ^ p * rexp (v * X ω)) μ
refine_1 : v + t ≠ v - t
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ X ω ^ p * rexp (v * X ω)) μ

Tactic:
have hX : AEMeasurable X μ := aemeasurable_of_integrable_exp_mul ?_ ht_int_pos ht_int_neg
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : 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
refine_1 : v + t - (v - t) ≠ 0
⊢ v + t ≠ v - t

Tactic:
rw [← sub_ne_zero]

Premises used: sub_ne_zero
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : 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) ≠ 0

Tactic:
simp [ht]
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : 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 μ
refine_2 : Integrable (ε := ℝ) (fun (a : Ω) ↦ ‖X a ^ p * rexp (v * X a)‖) μ
refine_2₁ : AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ X ω ^ p * rexp (v * X ω)) μ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ X ω ^ p * rexp (v * X ω)) μ

Tactic:
rw [← integrable_norm_iff]

Premises used: MeasureTheory.integrable_norm_iff
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : 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 μ
refine_2 : Integrable (ε := ℝ) (fun (a : Ω) ↦ |X a ^ p| * rexp (v * X a)) μ
⊢ Integrable (ε := ℝ) (fun (a : Ω) ↦ ‖X a ^ p * rexp (v * X a)‖) μ

Tactic:
simp_rw [norm_eq_abs, abs_mul, abs_exp]

Premises used: abs_mul, Real.norm_eq_abs, Real.abs_exp
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : 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:
have h := integrable_rpow_abs_mul_exp_of_integrable_exp_mul ht ht_int_pos ht_int_neg hp
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : 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:
h.mono' ?_ ?_

Premises used: MeasureTheory.Integrable.mono'
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : 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 ω)) μ
refine_2 : AEStronglyMeasurable (β := ℝ) (fun (a : Ω) ↦ |X a ^ p| * rexp (v * X a)) μ
refine_2₁ : ∀ᵐ (a : Ω) ∂μ, ‖|X a ^ p| * rexp (v * X a)‖ ≤ |X a| ^ p * rexp (v * X a)
⊢ Integrable (ε := ℝ) (fun (a : Ω) ↦ |X a ^ p| * rexp (v * X a)) μ

Tactic:
refine h.mono' ?_ ?_

Premises used: MeasureTheory.Integrable.mono'
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : 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 ω)) μ
funProp : 0 ≤ p
⊢ AEStronglyMeasurable (β := ℝ) (fun (a : Ω) ↦ |X a ^ p| * rexp (v * X a)) μ

Tactic:
fun_prop
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : 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)

Tactic:
ae_of_all _ fun ω ↦ ?_

Premises used: MeasureTheory.ae_of_all
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : 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 ω)) μ
refine_2 : ∀ (ω : Ω), ‖|X ω ^ p| * rexp (v * X ω)‖ ≤ |X ω| ^ p * rexp (v * X ω)
⊢ ∀ᵐ (a : Ω) ∂μ, ‖|X a ^ p| * rexp (v * X a)‖ ≤ |X a| ^ p * rexp (v * X a)

Tactic:
refine ae_of_all _ fun ω ↦ ?_

Premises used: MeasureTheory.ae_of_all
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : 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 ω)) μ
ω : Ω
refine_2 : |X ω ^ p| * rexp (v * X ω) ≤ |X ω| ^ p * rexp (v * X ω)
⊢ ‖|X ω ^ p| * rexp (v * X ω)‖ ≤ |X ω| ^ p * rexp (v * X ω)

Tactic:
simp only [norm_mul, norm_eq_abs, abs_abs, abs_exp]

Premises used: norm_mul, abs_abs, Real.norm_eq_abs, Real.abs_exp
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : 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 ω)) μ
ω : Ω
refine_2 : |X ω ^ p| ≤ |X ω| ^ p
⊢ |X ω ^ p| * rexp (v * X ω) ≤ |X ω| ^ p * rexp (v * X ω)

Tactic:
gcongr