awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (hypothesis)
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)
⊢ |x| ^ p ≤ (p / t) ^ p * max (rexp (t * x)) (rexp (-t * x))
have h_neg_x_le : ∀ (c : ℝ) (hc : 0 < c), -x ≤ c⁻¹ * rexp (-c * x)
Tactic: have h_neg_x_le c (hc : 0 < c) : -x ≤ c⁻¹ * exp (-c * x) := by simpa using le_inv_mul_exp (-x) hc
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
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)
c : ℝ
hc : 0 < c
⊢ |x| ≤ c⁻¹ * max (rexp (c * x)) (rexp (-c * x))
have refine_1 : -(c⁻¹ * max (rexp (c * x)) (rexp (-c * x))) ≤ x
Tactic: refine abs_le.mpr ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
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)
c : ℝ
hc : 0 < c
refine_1 : -(c⁻¹ * max (rexp (c * x)) (rexp (-c * x))) ≤ x
⊢ |x| ≤ c⁻¹ * max (rexp (c * x)) (rexp (-c * x))
have refine_2 : x ≤ c⁻¹ * max (rexp (c * x)) (rexp (-c * x))
Tactic: refine abs_le.mpr ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
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)
c : ℝ
hc : 0 < c
⊢ -(c⁻¹ * max (rexp (c * x)) (rexp (-c * x))) ≤ x
have refine_1 : -x ≤ c⁻¹ * max (rexp (c * x)) (rexp (-c * x))
Tactic: rw [neg_le]
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
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)
c : ℝ
hc : 0 < c
⊢ -x ≤ c⁻¹ * max (rexp (c * x)) (rexp (-c * x))
have refine_1 : c⁻¹ * rexp (-c * x) ≤ c⁻¹ * max (rexp (c * x)) (rexp (-c * x))
Tactic: refine (h_neg_x_le c hc).trans ?_
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
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)
c : ℝ
hc : 0 < c
⊢ c⁻¹ * rexp (-c * x) ≤ c⁻¹ * max (rexp (c * x)) (rexp (-c * x))
have refine_1 : rexp (-c * x) ≤ max (rexp (c * x)) (rexp (-c * x))
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
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)
c : ℝ
hc : 0 < c
⊢ x ≤ c⁻¹ * max (rexp (c * x)) (rexp (-c * x))
have refine_2 : c⁻¹ * rexp (c * x) ≤ c⁻¹ * max (rexp (c * x)) (rexp (-c * x))
Tactic: refine (h_x_le c hc).trans ?_
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
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)
c : ℝ
hc : 0 < c
⊢ c⁻¹ * rexp (c * x) ≤ c⁻¹ * max (rexp (c * x)) (rexp (-c * x))
have refine_2 : rexp (c * x) ≤ max (rexp (c * x)) (rexp (-c * x))
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (hypothesis)
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)
⊢ |x| ^ p ≤ (p / t) ^ p * max (rexp (t * x)) (rexp (-t * x))
have h_abs_le : ∀ (c : ℝ) (hc : 0 < c), |x| ≤ c⁻¹ * max (rexp (c * x)) (rexp (-c * x))
Tactic: have h_abs_le c (hc : 0 < c) : |x| ≤ c⁻¹ * max (exp (c * x)) (exp (-c * x)) := by
    refine abs_le.mpr ⟨?_, ?_⟩
    · rw [neg_le]
      refine (h_neg_x_le c hc).trans ?_
      gcongr
      exact le_max_right _ _
    · refine (h_x_le c hc).trans ?_
      gcongr
      exact le_max_left _ _
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
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))
⊢ |x| ^ p ≤ ((t / p)⁻¹ * max (rexp (t / p * x)) (rexp (-t / p * x))) ^ p
have h₁ : |x| ≤ (t / p)⁻¹ * max (rexp (t / p * x)) (rexp (-t / p * x))
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
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))
⊢ |x| ≤ (t / p)⁻¹ * max (rexp (t / p * x)) (rexp (-t / p * x))
have h : -t / p = -(t / p)
Tactic: convert! h_abs_le (t / p) (div_pos ht (hp.lt_of_ne' hp_zero)) using 5
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
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 = -(t / p)
have h : -(t / p) = -(t / p)
Tactic: rw [neg_div]
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
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)⁻¹ * max (rexp (t / p * x)) (rexp (-t / p * x))) ^ p = (p / t) ^ p * max (rexp (t * x)) (rexp (-t * x))
have rw : (t / p)⁻¹ ^ 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)]
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
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 * max (rexp (t / p * x)) (rexp (-t / p * x)) ^ p = (p / t) ^ p * max (rexp (t * x)) (rexp (-t * x))
have e_a : (t / p)⁻¹ = p / t
Tactic: congr
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
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
⊢ (t / p)⁻¹ ^ p * max (rexp (t / p * x)) (rexp (-t / p * x)) ^ p = (p / t) ^ p * max (rexp (t * x)) (rexp (-t * x))
have e_a₁ : max (rexp (t / p * x)) (rexp (-t / p * x)) ^ p = max (rexp (t * x)) (rexp (-t * x))
Tactic: congr
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
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))
⊢ max (rexp (t / p * x)) (rexp (-t / p * x)) ^ p = max (rexp (t * x)) (rexp (-t * x))
have e_a : max (rexp (t / p * x * p)) (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]
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
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))
⊢ max (rexp (t / p * x * p)) (rexp (-t / p * x * p)) = max (rexp (t * x)) (rexp (-t * x))
have e_a : max (rexp (t * p * p⁻¹ * x)) (rexp (-(t * p * p⁻¹ * x))) = max (rexp (t * x)) (rexp (-(t * x)))
Tactic: ring_nf
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
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))
⊢ max (rexp (t * p * p⁻¹ * x)) (rexp (-(t * p * p⁻¹ * x))) = max (rexp (t * x)) (rexp (-(t * x)))
have e_a : t * p * p⁻¹ = t
Tactic: congr
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
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
have e_a : t * (p * p⁻¹) = t
Tactic: rw [mul_assoc, mul_inv_cancel₀ hp_zero, mul_one]
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
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
⊢ t * p * p⁻¹ = t
have e_a₁ : t * 1 = t
Tactic: rw [mul_assoc, mul_inv_cancel₀ hp_zero, mul_one]
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
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
⊢ t * p * p⁻¹ = t
have e_a₂ : t = t
Tactic: rw [mul_assoc, mul_inv_cancel₀ hp_zero, mul_one]
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
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))
⊢ |x| ^ p ≤ (p / t) ^ p * max (rexp (t * x)) (rexp (-t * x))
have calc : |x| ^ p ≤ ((t / p)⁻¹ * max (rexp (t / p * x)) (rexp (-t / p * x))) ^ p
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]
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
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
⊢ |x| ^ p ≤ (p / t) ^ p * max (rexp (t * x)) (rexp (-t * x))
have calc₁ : ((t / p)⁻¹ * max (rexp (t / p * x)) (rexp (-t / p * 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]
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
x t p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
⊢ |x| ^ p ≤ (p / |t|) ^ p * max (rexp (t * x)) (rexp (-t * x))
have inl : ∀ (ht_neg : t < 0), |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
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
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))
⊢ |x| ^ p ≤ (p / |t|) ^ p * max (rexp (t * x)) (rexp (-t * x))
have inr : ∀ (ht_pos : 0 < t), |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
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
x t p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
ht_neg : t < 0
⊢ |x| ^ p ≤ (p / |t|) ^ p * max (rexp (t * x)) (rexp (-t * x))
have inl : |x| ^ p ≤ (p / -t) ^ p * max (rexp (-t * x)) (rexp (t * x))
Tactic: rw [abs_of_nonpos ht_neg.le, sup_comm]
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
x t p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
ht_neg : t < 0
⊢ |x| ^ p ≤ (p / -t) ^ p * max (rexp (-t * x)) (rexp (t * x))
have h : t = - -t
Tactic: convert! rpow_abs_le_mul_max_exp_of_pos x hp (t := -t) (by simp [ht_neg])
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
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))
have inr : |x| ^ p ≤ (p / t) ^ p * max (rexp (t * x)) (rexp (-t * x))
Tactic: rw [abs_of_nonneg ht_pos.le]
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
x t p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
⊢ |x| ^ p ≤ (p / |t|) ^ p * rexp (|t| * |x|)
have refine_1 : 0 < |t|
Tactic: refine (rpow_abs_le_mul_max_exp_of_pos x hp (t := |t|) ?_).trans_eq ?_
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
x t p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
refine_1 : 0 < |t|
⊢ |x| ^ p ≤ (p / |t|) ^ p * rexp (|t| * |x|)
have refine_2 : (p / |t|) ^ p * max (rexp (|t| * x)) (rexp (-|t| * x)) = (p / |t|) ^ p * rexp (|t| * |x|)
Tactic: refine (rpow_abs_le_mul_max_exp_of_pos x hp (t := |t|) ?_).trans_eq ?_
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
x t p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
⊢ (p / |t|) ^ p * max (rexp (|t| * x)) (rexp (-|t| * x)) = (p / |t|) ^ p * rexp (|t| * |x|)
have refine_2 : max (rexp (|t| * x)) (rexp (-|t| * x)) = rexp (|t| * |x|)
Tactic: congr
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
x t p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
⊢ max (rexp (|t| * x)) (rexp (-|t| * x)) = rexp (|t| * |x|)
have refine_2 : ∀ (hx : 0 ≤ x), max (rexp (|t| * x)) (rexp (-|t| * x)) = rexp (|t| * |x|)
Tactic: rcases le_total 0 x with hx | hx
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
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|)
⊢ max (rexp (|t| * x)) (rexp (-|t| * x)) = rexp (|t| * |x|)
have refine_2₁ : ∀ (hx : x ≤ 0), max (rexp (|t| * x)) (rexp (-|t| * x)) = rexp (|t| * |x|)
Tactic: rcases le_total 0 x with hx | hx
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
x t p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
hx : 0 ≤ x
⊢ max (rexp (|t| * x)) (rexp (-|t| * x)) = rexp (|t| * |x|)
have refine_2 : max (rexp (|t| * x)) (rexp (-|t| * x)) = rexp (|t| * x)
Tactic: rw [abs_of_nonneg hx]
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
x t p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
hx : 0 ≤ x
⊢ max (rexp (|t| * x)) (rexp (-|t| * x)) = rexp (|t| * x)
have refine_2 : 0 ≤ |t| * x
Tactic: simp only [neg_mul, sup_eq_left, exp_le_exp, neg_le_self_iff]
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
x t p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
hx : x ≤ 0
⊢ max (rexp (|t| * x)) (rexp (-|t| * x)) = rexp (|t| * |x|)
have refine_2 : max (rexp (|t| * x)) (rexp (-|t| * x)) = rexp (|t| * -x)
Tactic: rw [abs_of_nonpos hx]
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
x t p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
hx : x ≤ 0
⊢ max (rexp (|t| * x)) (rexp (-|t| * x)) = rexp (|t| * -x)
have refine_2 : |t| * x ≤ 0
Tactic: simp only [neg_mul, mul_neg, sup_eq_right, exp_le_exp, le_neg_self_iff]
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
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
have suffices : |t| ≠ 0
Tactic: suffices |t| ≠ 0 by simpa
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (hypothesis)
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
⊢ Integrable (ε := ℝ) (fun (a : Ω) ↦ |X a| ^ p * rexp (v * X a + x * |X a|)) μ
have ht : t ≠ 0
Tactic: have ht : t ≠ 0 := by
    suffices |t| ≠ 0 by simpa
    exact (h_nonneg.trans_lt hx).ne'
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
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
⊢ Integrable (ε := ℝ) (fun (a : Ω) ↦ |X a| ^ p * rexp (v * X a + x * |X a|)) μ
have refine_2 : ∀ (hX : AEMeasurable X μ), 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
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
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|)) μ
⊢ Integrable (ε := ℝ) (fun (a : Ω) ↦ |X a| ^ p * rexp (v * X a + x * |X a|)) μ
have refine_1 : v + t ≠ v - t
Tactic: have hX : AEMeasurable X μ := aemeasurable_of_integrable_exp_mul ?_ h_int_pos h_int_neg
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
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
have refine_1 : v + t - (v - t) ≠ 0
Tactic: rw [← sub_ne_zero]
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
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 μ
⊢ Integrable (ε := ℝ) (fun (a : Ω) ↦ |X a| ^ p * rexp (v * X a + x * |X a|)) μ
have refine_2 : Integrable (ε := ℝ) (fun (a : Ω) ↦ ‖|X a| ^ p * rexp (v * X a + x * |X a|)‖) μ
Tactic: rw [← integrable_norm_iff]
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
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|)) μ
have refine_2₁ : AEStronglyMeasurable (β := ℝ) (fun (a : Ω) ↦ |X a| ^ p * rexp (v * X a + x * |X a|)) μ
Tactic: rw [← integrable_norm_iff]
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
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 μ
⊢ Integrable (ε := ℝ) (fun (a : Ω) ↦ ‖|X a| ^ p * rexp (v * X a + x * |X a|)‖) μ
have refine_2 : Integrable (ε := ℝ) (fun (a : Ω) ↦ ||X a| ^ p| * rexp (v * X a + x * |X a|)) μ
Tactic: simp only [norm_mul, norm_eq_abs, abs_exp]
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
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|)
have 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)
Tactic: simp_rw [exp_add, mul_comm (exp (v * X a)), ← mul_assoc]
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
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 (x * |X a|) * rexp (v * X a) ≤ (p / (|t| - x)) ^ p * rexp (|t| * |X a|) * rexp (v * X a)
have hbc : |X a| ^ p * rexp (x * |X a|) ≤ (p / (|t| - x)) ^ p * rexp (|t| * |X a|)
Tactic: gcongr ?_ * _
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (hypothesis)
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 (x * |X a|) ≤ (p / (|t| - x)) ^ p * rexp (|t| * |X a|)
have this : |t| = |t| - x + x
Tactic: have : |t| = |t| - x + x := by simp
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
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 * rexp (x * |X a|) ≤ (p / (|t| - x)) ^ p * rexp (|t| * |X a|)
have hbc : |X a| ^ p * rexp (x * |X a|) ≤ (p / (|t| - x)) ^ p * rexp ((|t| - x + x) * |X a|)
Tactic: nth_rw 2 [this]
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
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 * rexp (x * |X a|) ≤ (p / (|t| - x)) ^ p * rexp ((|t| - x + x) * |X a|)
have hbc : |X a| ^ p * rexp (x * |X a|) ≤ (p / (|t| - x)) ^ p * rexp ((|t| - x) * |X a|) * rexp (x * |X a|)
Tactic: rw [add_mul, exp_add, ← mul_assoc]