awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
x t p : ℝ
hp : 0 ≤ p
ht : 0 < t
hp_zero : ¬p = 0
h_x_le : ∀ (c : ℝ) (hc : 0 < c), x ≤ c⁻¹ * rexp (c * x)
h_neg_x_le : ∀ (c : ℝ) (hc : 0 < c), -x ≤ c⁻¹ * rexp (-c * x)
h_abs_le : ∀ (c : ℝ) (hc : 0 < c), |x| ≤ c⁻¹ * max (rexp (c * x)) (rexp (-c * x))
rw : (t / p)⁻¹ ^ p * max (rexp (t / p * x)) (rexp (-t / p * x)) ^ p = (p / t) ^ p * max (rexp (t * x)) (rexp (-t * x))
⊢ ((t / p)⁻¹ * max (rexp (t / p * x)) (rexp (-t / p * x))) ^ p = (p / t) ^ p * max (rexp (t * x)) (rexp (-t * x))

Tactic:
rw [mul_rpow (by positivity) (by positivity)]

Premises used: Real.mul_rpow
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
x t p : ℝ
hp : 0 ≤ p
ht : 0 < t
hp_zero : ¬p = 0
h_x_le : ∀ (c : ℝ) (hc : 0 < c), x ≤ c⁻¹ * rexp (c * x)
h_neg_x_le : ∀ (c : ℝ) (hc : 0 < c), -x ≤ c⁻¹ * rexp (-c * x)
h_abs_le : ∀ (c : ℝ) (hc : 0 < c), |x| ≤ c⁻¹ * max (rexp (c * x)) (rexp (-c * x))
e_a : (t / p)⁻¹ = p / t
e_a₁ : max (rexp (t / p * x)) (rexp (-t / p * x)) ^ p = max (rexp (t * x)) (rexp (-t * x))
⊢ (t / p)⁻¹ ^ p * max (rexp (t / p * x)) (rexp (-t / p * x)) ^ p = (p / t) ^ p * max (rexp (t * x)) (rexp (-t * x))

Tactic:
congr
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
x t p : ℝ
hp : 0 ≤ p
ht : 0 < t
hp_zero : ¬p = 0
h_x_le : ∀ (c : ℝ) (hc : 0 < c), x ≤ c⁻¹ * rexp (c * x)
h_neg_x_le : ∀ (c : ℝ) (hc : 0 < c), -x ≤ c⁻¹ * rexp (-c * x)
h_abs_le : ∀ (c : ℝ) (hc : 0 < c), |x| ≤ c⁻¹ * max (rexp (c * x)) (rexp (-c * x))
⊢ (t / p)⁻¹ = p / t

Tactic:
simp
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
x t p : ℝ
hp : 0 ≤ p
ht : 0 < t
hp_zero : ¬p = 0
h_x_le : ∀ (c : ℝ) (hc : 0 < c), x ≤ c⁻¹ * rexp (c * x)
h_neg_x_le : ∀ (c : ℝ) (hc : 0 < c), -x ≤ c⁻¹ * rexp (-c * x)
h_abs_le : ∀ (c : ℝ) (hc : 0 < c), |x| ≤ c⁻¹ * max (rexp (c * x)) (rexp (-c * x))
⊢ 0 ≤ rexp (t / p * x)

Tactic:
positivity
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
x t p : ℝ
hp : 0 ≤ p
ht : 0 < t
hp_zero : ¬p = 0
h_x_le : ∀ (c : ℝ) (hc : 0 < c), x ≤ c⁻¹ * rexp (c * x)
h_neg_x_le : ∀ (c : ℝ) (hc : 0 < c), -x ≤ c⁻¹ * rexp (-c * x)
h_abs_le : ∀ (c : ℝ) (hc : 0 < c), |x| ≤ c⁻¹ * max (rexp (c * x)) (rexp (-c * x))
⊢ 0 ≤ rexp (-t / p * x)

Tactic:
positivity
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
x t p : ℝ
hp : 0 ≤ p
ht : 0 < t
hp_zero : ¬p = 0
h_x_le : ∀ (c : ℝ) (hc : 0 < c), x ≤ c⁻¹ * rexp (c * x)
h_neg_x_le : ∀ (c : ℝ) (hc : 0 < c), -x ≤ c⁻¹ * rexp (-c * x)
h_abs_le : ∀ (c : ℝ) (hc : 0 < c), |x| ≤ c⁻¹ * max (rexp (c * x)) (rexp (-c * x))
e_a : max (rexp (t / p * x * p)) (rexp (-t / p * x * p)) = max (rexp (t * x)) (rexp (-t * x))
⊢ max (rexp (t / p * x)) (rexp (-t / p * x)) ^ p = max (rexp (t * x)) (rexp (-t * x))

Tactic:
rw [rpow_max (by positivity) (by positivity) hp, ← exp_mul, ← exp_mul]

Premises used: Real.exp_mul, Real.rpow_max
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
x t p : ℝ
hp : 0 ≤ p
ht : 0 < t
hp_zero : ¬p = 0
h_x_le : ∀ (c : ℝ) (hc : 0 < c), x ≤ c⁻¹ * rexp (c * x)
h_neg_x_le : ∀ (c : ℝ) (hc : 0 < c), -x ≤ c⁻¹ * rexp (-c * x)
h_abs_le : ∀ (c : ℝ) (hc : 0 < c), |x| ≤ c⁻¹ * max (rexp (c * x)) (rexp (-c * x))
e_a : max (rexp (t * p * p⁻¹ * x)) (rexp (-(t * p * p⁻¹ * x))) = max (rexp (t * x)) (rexp (-(t * x)))
⊢ max (rexp (t / p * x * p)) (rexp (-t / p * x * p)) = max (rexp (t * x)) (rexp (-t * x))

Tactic:
ring_nf
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
x t p : ℝ
hp : 0 ≤ p
ht : 0 < t
hp_zero : ¬p = 0
h_x_le : ∀ (c : ℝ) (hc : 0 < c), x ≤ c⁻¹ * rexp (c * x)
h_neg_x_le : ∀ (c : ℝ) (hc : 0 < c), -x ≤ c⁻¹ * rexp (-c * x)
h_abs_le : ∀ (c : ℝ) (hc : 0 < c), |x| ≤ c⁻¹ * max (rexp (c * x)) (rexp (-c * x))
e_a e_a₁ : t * p * p⁻¹ = t
⊢ max (rexp (t * p * p⁻¹ * x)) (rexp (-(t * p * p⁻¹ * x))) = max (rexp (t * x)) (rexp (-(t * x)))

Tactic:
congr
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
x t p : ℝ
hp : 0 ≤ p
ht : 0 < t
hp_zero : ¬p = 0
h_x_le : ∀ (c : ℝ) (hc : 0 < c), x ≤ c⁻¹ * rexp (c * x)
h_neg_x_le : ∀ (c : ℝ) (hc : 0 < c), -x ≤ c⁻¹ * rexp (-c * x)
h_abs_le : ∀ (c : ℝ) (hc : 0 < c), |x| ≤ c⁻¹ * max (rexp (c * x)) (rexp (-c * x))
e_a : t * (p * p⁻¹) = t
e_a₁ : t * 1 = t
e_a₂ e_a₃ : t = t
⊢ t * p * p⁻¹ = t

Tactic:
rw [mul_assoc, mul_inv_cancel₀ hp_zero, mul_one]

Premises used: mul_inv_cancel₀, mul_assoc, mul_one
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
x t p : ℝ
hp : 0 ≤ p
ht : 0 < t
hp_zero : ¬p = 0
h_x_le : ∀ (c : ℝ) (hc : 0 < c), x ≤ c⁻¹ * rexp (c * x)
h_neg_x_le : ∀ (c : ℝ) (hc : 0 < c), -x ≤ c⁻¹ * rexp (-c * x)
h_abs_le : ∀ (c : ℝ) (hc : 0 < c), |x| ≤ c⁻¹ * max (rexp (c * x)) (rexp (-c * x))
calc : |x| ^ p ≤ ((t / p)⁻¹ * max (rexp (t / p * x)) (rexp (-t / p * x))) ^ p
calc₁ : ((t / p)⁻¹ * max (rexp (t / p * x)) (rexp (-t / p * x))) ^ p = (p / t) ^ p * max (rexp (t * x)) (rexp (-t * x))
⊢ |x| ^ p ≤ (p / t) ^ p * max (rexp (t * x)) (rexp (-t * x))

Tactic:
calc |x| ^ p
  _ ≤ ((t / p)⁻¹ * max (exp (t / p * x)) (exp (-t / p * x))) ^ p := by
    gcongr
    convert! h_abs_le (t / p) (div_pos ht (hp.lt_of_ne' hp_zero)) using 5
    rw [neg_div]
  _ = (p / t) ^ p * max (exp (t * x)) (exp (-t * x)) := by
    rw [mul_rpow (by positivity) (by positivity)]
    congr
    · simp
    · rw [rpow_max (by positivity) (by positivity) hp, ← exp_mul, ← exp_mul]
      ring_nf
      congr <;> rw [mul_assoc, mul_inv_cancel₀ hp_zero, mul_one]

Premises used: HMul.hMul, HDiv.hDiv, Real.exp, Inv.inv, Max.max, Neg.neg
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
x t p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
inl : ∀ (ht_neg : t < 0), |x| ^ p ≤ (p / |t|) ^ p * max (rexp (t * x)) (rexp (-t * x))
inr : ∀ (ht_pos : 0 < t), |x| ^ p ≤ (p / |t|) ^ p * max (rexp (t * x)) (rexp (-t * x))
⊢ |x| ^ p ≤ (p / |t|) ^ p * max (rexp (t * x)) (rexp (-t * x))

Tactic:
rcases lt_or_gt_of_ne ht with ht_neg | ht_pos

Premises used: lt_or_gt_of_ne
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
x t p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
ht_neg : t < 0
inl : |x| ^ p ≤ (p / -t) ^ p * max (rexp (-t * x)) (rexp (t * x))
⊢ |x| ^ p ≤ (p / |t|) ^ p * max (rexp (t * x)) (rexp (-t * x))

Tactic:
rw [abs_of_nonpos ht_neg.le, sup_comm]

Premises used: LT.lt.le, abs_of_nonpos, sup_comm
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
x t p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
ht_neg : t < 0
⊢ 0 < -t

Tactic:
simp [ht_neg]
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
x t p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
ht_neg : t < 0
h : t = - -t
⊢ |x| ^ p ≤ (p / -t) ^ p * max (rexp (-t * x)) (rexp (t * x))

Tactic:
convert! rpow_abs_le_mul_max_exp_of_pos x hp (t := -t) (by simp [ht_neg])

Premises used: ProbabilityTheory.rpow_abs_le_mul_max_exp_of_pos
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
x t p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
ht_neg : t < 0
⊢ t = - -t

Tactic:
simp
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
x t p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
ht_pos : 0 < t
inr : |x| ^ p ≤ (p / t) ^ p * max (rexp (t * x)) (rexp (-t * x))
⊢ |x| ^ p ≤ (p / |t|) ^ p * max (rexp (t * x)) (rexp (-t * x))

Tactic:
rw [abs_of_nonneg ht_pos.le]

Premises used: LT.lt.le, abs_of_nonneg
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
x t p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
ht_pos : 0 < t
⊢ |x| ^ p ≤ (p / t) ^ p * max (rexp (t * x)) (rexp (-t * x))

Tactic:
rpow_abs_le_mul_max_exp_of_pos x hp ht_pos

Premises used: ProbabilityTheory.rpow_abs_le_mul_max_exp_of_pos
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
x t p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
ht_pos : 0 < t
⊢ |x| ^ p ≤ (p / t) ^ p * max (rexp (t * x)) (rexp (-t * x))

Tactic:
exact rpow_abs_le_mul_max_exp_of_pos x hp ht_pos

Premises used: ProbabilityTheory.rpow_abs_le_mul_max_exp_of_pos
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
x t p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
⊢ |x| ^ p ≤ (p / |t|) ^ p * rexp (|t| * |x|)

Tactic:
(rpow_abs_le_mul_max_exp_of_pos x hp (t := |t|) ?_).trans_eq ?_

Premises used: LE.le.trans_eq, ProbabilityTheory.rpow_abs_le_mul_max_exp_of_pos
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
x t p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
refine_1 : 0 < |t|
refine_2 : (p / |t|) ^ p * max (rexp (|t| * x)) (rexp (-|t| * x)) = (p / |t|) ^ p * rexp (|t| * |x|)
⊢ |x| ^ p ≤ (p / |t|) ^ p * rexp (|t| * |x|)

Tactic:
refine (rpow_abs_le_mul_max_exp_of_pos x hp (t := |t|) ?_).trans_eq ?_

Premises used: LE.le.trans_eq, ProbabilityTheory.rpow_abs_le_mul_max_exp_of_pos
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
x t p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
⊢ 0 < |t|

Tactic:
simp [ht]
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
x t p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
refine_2 : max (rexp (|t| * x)) (rexp (-|t| * x)) = rexp (|t| * |x|)
⊢ (p / |t|) ^ p * max (rexp (|t| * x)) (rexp (-|t| * x)) = (p / |t|) ^ p * rexp (|t| * |x|)

Tactic:
congr
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
x t p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
refine_2 : ∀ (hx : 0 ≤ x), max (rexp (|t| * x)) (rexp (-|t| * x)) = rexp (|t| * |x|)
refine_2₁ : ∀ (hx : x ≤ 0), max (rexp (|t| * x)) (rexp (-|t| * x)) = rexp (|t| * |x|)
⊢ max (rexp (|t| * x)) (rexp (-|t| * x)) = rexp (|t| * |x|)

Tactic:
rcases le_total 0 x with hx | hx

Premises used: le_total, OfNat.ofNat
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
x t p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
hx : 0 ≤ x
refine_2 : max (rexp (|t| * x)) (rexp (-|t| * x)) = rexp (|t| * x)
⊢ max (rexp (|t| * x)) (rexp (-|t| * x)) = rexp (|t| * |x|)

Tactic:
rw [abs_of_nonneg hx]

Premises used: abs_of_nonneg
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
x t p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
hx : 0 ≤ x
refine_2 : 0 ≤ |t| * x
⊢ max (rexp (|t| * x)) (rexp (-|t| * x)) = rexp (|t| * x)

Tactic:
simp only [neg_mul, sup_eq_left, exp_le_exp, neg_le_self_iff]

Premises used: neg_le_self_iff, sup_eq_left, Real.exp_le_exp, neg_mul
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
x t p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
hx : 0 ≤ x
⊢ 0 ≤ |t| * x

Tactic:
positivity
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
x t p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
hx : x ≤ 0
refine_2 : max (rexp (|t| * x)) (rexp (-|t| * x)) = rexp (|t| * -x)
⊢ max (rexp (|t| * x)) (rexp (-|t| * x)) = rexp (|t| * |x|)

Tactic:
rw [abs_of_nonpos hx]

Premises used: abs_of_nonpos
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
x t p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
hx : x ≤ 0
refine_2 : |t| * x ≤ 0
⊢ max (rexp (|t| * x)) (rexp (-|t| * x)) = rexp (|t| * -x)

Tactic:
simp only [neg_mul, mul_neg, sup_eq_right, exp_le_exp, le_neg_self_iff]

Premises used: le_neg_self_iff, Real.exp_le_exp, sup_eq_right, neg_mul, mul_neg
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
x t p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
hx : x ≤ 0
⊢ |t| * x ≤ 0

Tactic:
mul_nonpos_of_nonneg_of_nonpos (abs_nonneg _) hx

Premises used: mul_nonpos_of_nonneg_of_nonpos, abs_nonneg
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
x t p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
hx : x ≤ 0
⊢ |t| * x ≤ 0

Tactic:
exact mul_nonpos_of_nonneg_of_nonpos (abs_nonneg _) hx

Premises used: mul_nonpos_of_nonneg_of_nonpos
-- 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
this : |t| ≠ 0
⊢ t ≠ 0

Tactic:
simpa
-- 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
suffices : |t| ≠ 0
⊢ t ≠ 0

Tactic:
suffices |t| ≠ 0 by simpa
-- 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
⊢ |t| ≠ 0

Tactic:
(h_nonneg.trans_lt hx).ne'

Premises used: LT.lt.ne', LE.le.trans_lt
-- 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
⊢ |t| ≠ 0

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

Premises used: LT.lt.ne', LE.le.trans_lt
-- 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
⊢ t ≠ 0

Tactic:
have ht : t ≠ 0 := by
    suffices |t| ≠ 0 by simpa
    exact (h_nonneg.trans_lt 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
refine_2 : ∀ (hX : AEMeasurable X μ), Integrable (ε := ℝ) (fun (a : Ω) ↦ |X a| ^ p * rexp (v * X a + x * |X a|)) μ
refine_1 : v + t ≠ v - t
⊢ 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
-- 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
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 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]
-- 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 μ
refine_2 : Integrable (ε := ℝ) (fun (a : Ω) ↦ ‖|X a| ^ p * rexp (v * X a + x * |X a|)‖) μ
refine_2₁ : AEStronglyMeasurable (β := ℝ) (fun (a : Ω) ↦ |X a| ^ p * rexp (v * X a + x * |X a|)) μ
⊢ Integrable (ε := ℝ) (fun (a : Ω) ↦ |X a| ^ p * rexp (v * X a + x * |X a|)) μ

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 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 μ
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 μ
refine_2 : Integrable (ε := ℝ) (fun (a : Ω) ↦ ||X a| ^ p| * rexp (v * X a + x * |X a|)) μ
⊢ Integrable (ε := ℝ) (fun (a : Ω) ↦ ‖|X a| ^ p * rexp (v * X a + x * |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 μ
a : Ω
simp_rw : |X a| ^ p * rexp (x * |X a|) * rexp (v * X a) ≤ (p / (|t| - x)) ^ p * rexp (|t| * |X a|) * rexp (v * X a)
⊢ |X a| ^ p * rexp (v * X a + x * |X a|) ≤ (p / (|t| - x)) ^ p * rexp (v * X a + |t| * |X a|)

Tactic:
simp_rw [exp_add, mul_comm (exp (v * X a)), ← mul_assoc]

Premises used: HMul.hMul, mul_assoc, Real.exp, mul_comm, Real.exp_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 μ
a : Ω
hbc : |X a| ^ p * rexp (x * |X a|) ≤ (p / (|t| - x)) ^ p * rexp (|t| * |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 ?_ * _
-- 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 : Ω
⊢ |t| = |t| - x + x

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

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

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

Premises used: add_mul, mul_assoc, Real.exp_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 μ
a : Ω
this : |t| = |t| - x + x
hbc : |X a| ^ p ≤ (p / (|t| - x)) ^ p * rexp ((|t| - x) * |X a|)
⊢ |X a| ^ p * rexp (x * |X a|) ≤ (p / (|t| - x)) ^ p * rexp ((|t| - x) * |X a|) * rexp (x * |X a|)

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

Tactic:
rpow_abs_le_mul_exp_abs (X a) hp (t := |t| - x) _

Premises used: ProbabilityTheory.rpow_abs_le_mul_exp_abs
-- 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 : Ω
this : |t| = |t| - x + x
h h₁ : |t| - x = ||t| - x|
hbc : |t| - x ≠ 0
⊢ |X a| ^ p ≤ (p / (|t| - x)) ^ p * rexp ((|t| - x) * |X a|)

Tactic:
convert! rpow_abs_le_mul_exp_abs (X a) hp (t := |t| - x) _ using 4

Premises used: ProbabilityTheory.rpow_abs_le_mul_exp_abs
-- 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 : Ω
this : |t| = |t| - x + x
h : 0 ≤ |t| - x
⊢ |t| - x = ||t| - x|

Tactic:
nth_rw 2 [abs_of_nonneg]

Premises used: abs_of_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 μ
a : Ω
this : |t| = |t| - x + x
⊢ 0 ≤ |t| - x

Tactic:
simp [hx.le]

Premises used: 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|
p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
hX : AEMeasurable X μ
a : Ω
this : |t| = |t| - x + x
hbc : |t| ≠ x
⊢ |t| - x ≠ 0

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 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
⊢ |t| ≠ x

Tactic:
hx.ne'

Premises used: LT.lt.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 μ
a : Ω
this : |t| = |t| - x + x
⊢ |t| ≠ x

Tactic:
exact hx.ne'

Premises used: LT.lt.ne'