awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
Ω_1 : Type u_1
m_1 : MeasurableSpace Ω_1
X_1 : Ω_1 → ℝ
μ_1 : Measure Ω_1
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t₁ : ℝ
ht₁ : t₁ ∈ integrableExpSet X μ
t₂ : ℝ
ht₂ : t₂ ∈ integrableExpSet X μ
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h_le : t₁ ≤ t₂
refine_1 : t₁ ≤ a • t₁ + b • t₂
⊢ a • t₁ + b • t₂ ∈ integrableExpSet X μ
have refine_2 : a • t₁ + b • t₂ ≤ t₂
Tactic: refine integrable_exp_mul_of_le_of_le ht₁ ht₂ ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
Ω_1 : Type u_1
m_1 : MeasurableSpace Ω_1
X_1 : Ω_1 → ℝ
μ_1 : Measure Ω_1
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t₁ : ℝ
ht₁ : t₁ ∈ integrableExpSet X μ
t₂ : ℝ
ht₂ : t₂ ∈ integrableExpSet X μ
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h_le : t₁ ≤ t₂
⊢ t₁ = a * t₁ + b * t₁
have rw : t₁ = (a + b) * t₁
Tactic: rw [← add_mul, hab, one_mul]
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
Ω_1 : Type u_1
m_1 : MeasurableSpace Ω_1
X_1 : Ω_1 → ℝ
μ_1 : Measure Ω_1
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t₁ : ℝ
ht₁ : t₁ ∈ integrableExpSet X μ
t₂ : ℝ
ht₂ : t₂ ∈ integrableExpSet X μ
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h_le : t₁ ≤ t₂
rw : t₁ = (a + b) * t₁
⊢ t₁ = a * t₁ + b * t₁
have rw₁ : t₁ = 1 * t₁
Tactic: rw [← add_mul, hab, one_mul]
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
Ω_1 : Type u_1
m_1 : MeasurableSpace Ω_1
X_1 : Ω_1 → ℝ
μ_1 : Measure Ω_1
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t₁ : ℝ
ht₁ : t₁ ∈ integrableExpSet X μ
t₂ : ℝ
ht₂ : t₂ ∈ integrableExpSet X μ
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h_le : t₁ ≤ t₂
rw : t₁ = (a + b) * t₁
rw₁ : t₁ = 1 * t₁
⊢ t₁ = a * t₁ + b * t₁
have rw₂ : t₁ = t₁
Tactic: rw [← add_mul, hab, one_mul]
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
Ω_1 : Type u_1
m_1 : MeasurableSpace Ω_1
X_1 : Ω_1 → ℝ
μ_1 : Measure Ω_1
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t₁ : ℝ
ht₁ : t₁ ∈ integrableExpSet X μ
t₂ : ℝ
ht₂ : t₂ ∈ integrableExpSet X μ
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h_le : t₁ ≤ t₂
⊢ t₁ ≤ a * t₁ + b * t₂
have calc : t₁ = a * t₁ + b * t₁
Tactic: calc t₁
    _ = a * t₁ + b * t₁ := by rw [← add_mul, hab, one_mul]
    _ ≤ a * t₁ + b * t₂ := by gcongr
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
Ω_1 : Type u_1
m_1 : MeasurableSpace Ω_1
X_1 : Ω_1 → ℝ
μ_1 : Measure Ω_1
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t₁ : ℝ
ht₁ : t₁ ∈ integrableExpSet X μ
t₂ : ℝ
ht₂ : t₂ ∈ integrableExpSet X μ
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h_le : t₁ ≤ t₂
calc : t₁ = a * t₁ + b * t₁
⊢ t₁ ≤ a * t₁ + b * t₂
have calc₁ : a * t₁ + b * t₁ ≤ a * t₁ + b * t₂
Tactic: calc t₁
    _ = a * t₁ + b * t₁ := by rw [← add_mul, hab, one_mul]
    _ ≤ a * t₁ + b * t₂ := by gcongr
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
Ω_1 : Type u_1
m_1 : MeasurableSpace Ω_1
X_1 : Ω_1 → ℝ
μ_1 : Measure Ω_1
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t₁ : ℝ
ht₁ : t₁ ∈ integrableExpSet X μ
t₂ : ℝ
ht₂ : t₂ ∈ integrableExpSet X μ
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h_le : t₁ ≤ t₂
⊢ a * t₂ + b * t₂ = t₂
have rw : (a + b) * t₂ = t₂
Tactic: rw [← add_mul, hab, one_mul]
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
Ω_1 : Type u_1
m_1 : MeasurableSpace Ω_1
X_1 : Ω_1 → ℝ
μ_1 : Measure Ω_1
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t₁ : ℝ
ht₁ : t₁ ∈ integrableExpSet X μ
t₂ : ℝ
ht₂ : t₂ ∈ integrableExpSet X μ
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h_le : t₁ ≤ t₂
rw : (a + b) * t₂ = t₂
⊢ a * t₂ + b * t₂ = t₂
have rw₁ : 1 * t₂ = t₂
Tactic: rw [← add_mul, hab, one_mul]
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
Ω_1 : Type u_1
m_1 : MeasurableSpace Ω_1
X_1 : Ω_1 → ℝ
μ_1 : Measure Ω_1
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t₁ : ℝ
ht₁ : t₁ ∈ integrableExpSet X μ
t₂ : ℝ
ht₂ : t₂ ∈ integrableExpSet X μ
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h_le : t₁ ≤ t₂
rw : (a + b) * t₂ = t₂
rw₁ : 1 * t₂ = t₂
⊢ a * t₂ + b * t₂ = t₂
have rw₂ : t₂ = t₂
Tactic: rw [← add_mul, hab, one_mul]
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
Ω_1 : Type u_1
m_1 : MeasurableSpace Ω_1
X_1 : Ω_1 → ℝ
μ_1 : Measure Ω_1
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t₁ : ℝ
ht₁ : t₁ ∈ integrableExpSet X μ
t₂ : ℝ
ht₂ : t₂ ∈ integrableExpSet X μ
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h_le : t₁ ≤ t₂
⊢ a * t₁ + b * t₂ ≤ t₂
have calc : a * t₁ + b * t₂ ≤ a * t₂ + b * t₂
Tactic: calc a * t₁ + b * t₂
    _ ≤ a * t₂ + b * t₂ := by gcongr
    _ = t₂ := by rw [← add_mul, hab, one_mul]
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
Ω_1 : Type u_1
m_1 : MeasurableSpace Ω_1
X_1 : Ω_1 → ℝ
μ_1 : Measure Ω_1
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t₁ : ℝ
ht₁ : t₁ ∈ integrableExpSet X μ
t₂ : ℝ
ht₂ : t₂ ∈ integrableExpSet X μ
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h_le : t₁ ≤ t₂
calc : a * t₁ + b * t₂ ≤ a * t₂ + b * t₂
⊢ a * t₁ + b * t₂ ≤ t₂
have calc₁ : a * t₂ + b * t₂ = t₂
Tactic: calc a * t₁ + b * t₂
    _ ≤ a * t₂ + b * t₂ := by gcongr
    _ = t₂ := by rw [← add_mul, hab, one_mul]
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
u v : ℝ
huv : u ≠ v
hu_int : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (u * X ω)) μ
hv_int : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (v * X ω)) μ
⊢ AEMeasurable X μ
have pos : ∀ (hu : u = 0), AEMeasurable X μ
Tactic: by_cases hu : u = 0
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
u v : ℝ
huv : u ≠ v
hu_int : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (u * X ω)) μ
hv_int : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (v * X ω)) μ
pos : ∀ (hu : u = 0), AEMeasurable X μ
⊢ AEMeasurable X μ
have neg : ∀ (hu : ¬u = 0), AEMeasurable X μ
Tactic: by_cases hu : u = 0
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (hypothesis)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
u v : ℝ
huv : u ≠ v
hu_int : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (u * X ω)) μ
hv_int : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (v * X ω)) μ
hu : u = 0
⊢ AEMeasurable X μ
have hv : v ≠ 0
Tactic: have hv : v ≠ 0 := ne_of_ne_of_eq huv.symm hu
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (hypothesis)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v : ℝ
ht_int_pos : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp ((v + t) * X ω)) μ
ht_int_neg : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp ((v - t) * X ω)) μ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * |X ω| + v * X ω)) μ
have h_int_add : Integrable (ε := ℝ) (fun (a : Ω) ↦ rexp ((v + t) * X a) + rexp ((v - t) * X a)) μ
Tactic: have h_int_add : Integrable (fun a ↦ exp ((v + t) * X a) + exp ((v - t) * X a)) μ :=
    ht_int_pos.add <| by simpa using ht_int_neg
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v : ℝ
ht_int_pos : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp ((v + t) * X ω)) μ
ht_int_neg : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp ((v - t) * X ω)) μ
h_int_add : Integrable (ε := ℝ) (fun (a : Ω) ↦ rexp ((v + t) * X a) + rexp ((v - t) * X a)) μ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * |X ω| + v * X ω)) μ
have refine_1 : AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * |X ω| + v * X ω)) μ
Tactic: refine Integrable.mono h_int_add ?_ (ae_of_all _ fun ω ↦ ?_)
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v : ℝ
ht_int_pos : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp ((v + t) * X ω)) μ
ht_int_neg : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp ((v - t) * X ω)) μ
h_int_add : Integrable (ε := ℝ) (fun (a : Ω) ↦ rexp ((v + t) * X a) + rexp ((v - t) * X a)) μ
refine_1 : AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * |X ω| + v * X ω)) μ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * |X ω| + v * X ω)) μ
have refine_2 : ∀ (ω : Ω), ‖rexp (t * |X ω| + v * X ω)‖ ≤ ‖rexp ((v + t) * X ω) + rexp ((v - t) * X ω)‖
Tactic: refine Integrable.mono h_int_add ?_ (ae_of_all _ fun ω ↦ ?_)
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v : ℝ
ht_int_pos : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp ((v + t) * X ω)) μ
ht_int_neg : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp ((v - t) * X ω)) μ
h_int_add : Integrable (ε := ℝ) (fun (a : Ω) ↦ rexp ((v + t) * X a) + rexp ((v - t) * X a)) μ
⊢ AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * |X ω| + v * X ω)) μ
have pos : ∀ (ht : t = 0), AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * |X ω| + v * X ω)) μ
Tactic: by_cases ht : t = 0
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v : ℝ
ht_int_pos : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp ((v + t) * X ω)) μ
ht_int_neg : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp ((v - t) * X ω)) μ
h_int_add : Integrable (ε := ℝ) (fun (a : Ω) ↦ rexp ((v + t) * X a) + rexp ((v - t) * X a)) μ
pos : ∀ (ht : t = 0), AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * |X ω| + v * X ω)) μ
⊢ AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * |X ω| + v * X ω)) μ
have neg : ∀ (ht : ¬t = 0), AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * |X ω| + v * X ω)) μ
Tactic: by_cases ht : t = 0
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v : ℝ
ht_int_pos : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp ((v + t) * X ω)) μ
ht_int_neg : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp ((v - t) * X ω)) μ
h_int_add : Integrable (ε := ℝ) (fun (a : Ω) ↦ rexp ((v + t) * X a) + rexp ((v - t) * X a)) μ
ht : t = 0
⊢ AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * |X ω| + v * X ω)) μ
have pos : ∀ (ht_int_pos : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (v * X ω)) μ),
  AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (v * X ω)) μ
Tactic: simp only [ht, zero_mul, zero_add, add_zero] at ht_int_pos ⊢
Cleared hypotheses: ht_int_pos
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v : ℝ
ht_int_pos : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp ((v + t) * X ω)) μ
ht_int_neg : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp ((v - t) * X ω)) μ
h_int_add : Integrable (ε := ℝ) (fun (a : Ω) ↦ rexp ((v + t) * X a) + rexp ((v - t) * X a)) μ
ht : ¬t = 0
⊢ AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * |X ω| + v * X ω)) μ
have neg : ∀ (hX : AEMeasurable X μ), AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * |X ω| + v * X ω)) μ
Tactic: have hX : AEMeasurable X μ := aemeasurable_of_integrable_exp_mul ?_ ht_int_pos ht_int_neg
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v : ℝ
ht_int_pos : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp ((v + t) * X ω)) μ
ht_int_neg : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp ((v - t) * X ω)) μ
h_int_add : Integrable (ε := ℝ) (fun (a : Ω) ↦ rexp ((v + t) * X a) + rexp ((v - t) * X a)) μ
ht : ¬t = 0
neg : ∀ (hX : AEMeasurable X μ), AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * |X ω| + v * X ω)) μ
⊢ AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * |X ω| + v * X ω)) μ
have neg₁ : v + t ≠ v - t
Tactic: have hX : AEMeasurable X μ := aemeasurable_of_integrable_exp_mul ?_ ht_int_pos ht_int_neg
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v : ℝ
ht_int_pos : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp ((v + t) * X ω)) μ
ht_int_neg : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp ((v - t) * X ω)) μ
h_int_add : Integrable (ε := ℝ) (fun (a : Ω) ↦ rexp ((v + t) * X a) + rexp ((v - t) * X a)) μ
ht : ¬t = 0
⊢ v + t ≠ v - t
have neg : 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 : ℝ
ht_int_pos : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp ((v + t) * X ω)) μ
ht_int_neg : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp ((v - t) * X ω)) μ
h_int_add : Integrable (ε := ℝ) (fun (a : Ω) ↦ rexp ((v + t) * X a) + rexp ((v - t) * X a)) μ
ω : Ω
⊢ ‖rexp (t * |X ω| + v * X ω)‖ ≤ ‖rexp ((v + t) * X ω) + rexp ((v - t) * X ω)‖
have refine_2 : rexp (t * |X ω| + v * X ω) ≤ |rexp ((v + t) * X ω) + rexp ((v - t) * X ω)|
Tactic: simp only [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 : ℝ
ht_int_pos : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp ((v + t) * X ω)) μ
ht_int_neg : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp ((v - t) * X ω)) μ
h_int_add : Integrable (ε := ℝ) (fun (a : Ω) ↦ rexp ((v + t) * X a) + rexp ((v - t) * X a)) μ
ω : Ω
| |rexp ((v + t) * X ω) + rexp ((v - t) * X ω)|
have rw : rexp ((v + t) * X ω) + rexp ((v - t) * X ω)
Tactic: rw [abs_of_nonneg (by positivity)]
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v : ℝ
ht_int_pos : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp ((v + t) * X ω)) μ
ht_int_neg : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp ((v - t) * X ω)) μ
h_int_add : Integrable (ε := ℝ) (fun (a : Ω) ↦ rexp ((v + t) * X a) + rexp ((v - t) * X a)) μ
ω : Ω
⊢ rexp (t * |X ω| + v * X ω) ≤ |rexp ((v + t) * X ω) + rexp ((v - t) * X ω)|
have refine_2 : rexp (t * |X ω| + v * X ω) ≤ rexp ((v + t) * X ω) + rexp ((v - t) * X ω)
Tactic: conv_rhs => rw [abs_of_nonneg (by positivity)]
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v : ℝ
ht_int_pos : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp ((v + t) * X ω)) μ
ht_int_neg : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp ((v - t) * X ω)) μ
h_int_add : Integrable (ε := ℝ) (fun (a : Ω) ↦ rexp ((v + t) * X a) + rexp ((v - t) * X a)) μ
ω : Ω
⊢ rexp (t * |X ω| + v * X ω) ≤ rexp ((v + t) * X ω) + rexp ((v - t) * X ω)
have refine_2 : ∀ (h_nonneg : 0 ≤ X ω), rexp (t * |X ω| + v * X ω) ≤ rexp ((v + t) * X ω) + rexp ((v - t) * X ω)
Tactic: rcases le_total 0 (X ω) with h_nonneg | h_nonpos
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v : ℝ
ht_int_pos : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp ((v + t) * X ω)) μ
ht_int_neg : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp ((v - t) * X ω)) μ
h_int_add : Integrable (ε := ℝ) (fun (a : Ω) ↦ rexp ((v + t) * X a) + rexp ((v - t) * X a)) μ
ω : Ω
refine_2 : ∀ (h_nonneg : 0 ≤ X ω), rexp (t * |X ω| + v * X ω) ≤ rexp ((v + t) * X ω) + rexp ((v - t) * X ω)
⊢ rexp (t * |X ω| + v * X ω) ≤ rexp ((v + t) * X ω) + rexp ((v - t) * X ω)
have refine_2₁ : ∀ (h_nonpos : X ω ≤ 0), rexp (t * |X ω| + v * X ω) ≤ rexp ((v + t) * X ω) + rexp ((v - t) * X ω)
Tactic: rcases le_total 0 (X ω) with h_nonneg | h_nonpos
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v : ℝ
ht_int_pos : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp ((v + t) * X ω)) μ
ht_int_neg : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp ((v - t) * X ω)) μ
h_int_add : Integrable (ε := ℝ) (fun (a : Ω) ↦ rexp ((v + t) * X a) + rexp ((v - t) * X a)) μ
ω : Ω
h_nonneg : 0 ≤ X ω
⊢ rexp (t * |X ω| + v * X ω) ≤ rexp ((v + t) * X ω) + rexp ((v - t) * X ω)
have refine_2 : 0 ≤ rexp ((v - t) * X ω)
Tactic: rw [abs_of_nonneg h_nonneg, ← add_mul, add_comm, le_add_iff_nonneg_right]
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v : ℝ
ht_int_pos : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp ((v + t) * X ω)) μ
ht_int_neg : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp ((v - t) * X ω)) μ
h_int_add : Integrable (ε := ℝ) (fun (a : Ω) ↦ rexp ((v + t) * X a) + rexp ((v - t) * X a)) μ
ω : Ω
h_nonpos : X ω ≤ 0
⊢ rexp (t * |X ω| + v * X ω) ≤ rexp ((v + t) * X ω) + rexp ((v - t) * X ω)
have refine_2 : 0 ≤ rexp ((v + t) * X ω)
Tactic: rw [abs_of_nonpos h_nonpos, mul_neg, mul_comm, ← mul_neg, mul_comm, ← add_mul, add_comm,
        ← sub_eq_add_neg, le_add_iff_nonneg_left]
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht_int_pos : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
ht_int_neg : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (-t * X ω)) μ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * |X ω|)) μ
have refine_3 : ∀ (h : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * |X ω| + 0 * X ω)) μ),
  Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * |X ω|)) μ
Tactic: have h := integrable_exp_mul_abs_add (t := t) (μ := μ) (X := X) (v := 0) ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht_int_pos : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
ht_int_neg : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (-t * X ω)) μ
refine_3 :
  ∀ (h : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * |X ω| + 0 * X ω)) μ),
    Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * |X ω|)) μ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * |X ω|)) μ
have refine_1 : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp ((0 + t) * X ω)) μ
Tactic: have h := integrable_exp_mul_abs_add (t := t) (μ := μ) (X := X) (v := 0) ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht_int_pos : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
ht_int_neg : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (-t * X ω)) μ
refine_3 :
  ∀ (h : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * |X ω| + 0 * X ω)) μ),
    Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * |X ω|)) μ
refine_1 : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp ((0 + t) * X ω)) μ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * |X ω|)) μ
have refine_2 : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp ((0 - t) * X ω)) μ
Tactic: have h := integrable_exp_mul_abs_add (t := t) (μ := μ) (X := X) (v := 0) ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v : ℝ
ht_int_pos : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp ((v + t) * X ω)) μ
ht_int_neg : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp ((v - t) * X ω)) μ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (|t| * |X ω| + v * X ω)) μ
have inl : ∀ (ht_nonneg : 0 ≤ t), Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (|t| * |X ω| + v * X ω)) μ
Tactic: rcases le_total 0 t with ht_nonneg | ht_nonpos
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v : ℝ
ht_int_pos : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp ((v + t) * X ω)) μ
ht_int_neg : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp ((v - t) * X ω)) μ
inl : ∀ (ht_nonneg : 0 ≤ t), Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (|t| * |X ω| + v * X ω)) μ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (|t| * |X ω| + v * X ω)) μ
have inr : ∀ (ht_nonpos : t ≤ 0), Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (|t| * |X ω| + v * X ω)) μ
Tactic: rcases le_total 0 t with ht_nonneg | ht_nonpos
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v : ℝ
ht_int_pos : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp ((v + t) * X ω)) μ
ht_int_neg : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp ((v - t) * X ω)) μ
ht_nonneg : 0 ≤ t
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (|t| * |X ω| + v * X ω)) μ
have inl : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * |X ω| + v * X ω)) μ
Tactic: simp_rw [abs_of_nonneg ht_nonneg]
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v : ℝ
ht_int_pos : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp ((v + t) * X ω)) μ
ht_int_neg : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp ((v - t) * X ω)) μ
ht_nonpos : t ≤ 0
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (|t| * |X ω| + v * X ω)) μ
have inr : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (-t * |X ω| + v * X ω)) μ
Tactic: simp_rw [abs_of_nonpos ht_nonpos]
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht_int_pos : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
ht_int_neg : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (-t * X ω)) μ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (|t| * |X ω|)) μ
have inl : ∀ (ht_nonneg : 0 ≤ t), Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (|t| * |X ω|)) μ
Tactic: rcases le_total 0 t with ht_nonneg | ht_nonpos
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht_int_pos : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
ht_int_neg : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (-t * X ω)) μ
inl : ∀ (ht_nonneg : 0 ≤ t), Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (|t| * |X ω|)) μ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (|t| * |X ω|)) μ
have inr : ∀ (ht_nonpos : t ≤ 0), Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (|t| * |X ω|)) μ
Tactic: rcases le_total 0 t with ht_nonneg | ht_nonpos
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht_int_pos : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
ht_int_neg : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (-t * X ω)) μ
ht_nonneg : 0 ≤ t
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (|t| * |X ω|)) μ
have inl : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * |X ω|)) μ
Tactic: simp_rw [abs_of_nonneg ht_nonneg]
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht_int_pos : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
ht_int_neg : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (-t * X ω)) μ
ht_nonpos : t ≤ 0
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (|t| * |X ω|)) μ
have inr : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (-t * |X ω|)) μ
Tactic: simp_rw [abs_of_nonpos ht_nonpos]
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
x t p : ℝ
hp : 0 ≤ p
ht : 0 < t
⊢ |x| ^ p ≤ (p / t) ^ p * max (rexp (t * x)) (rexp (-t * x))
have pos : ∀ (hp_zero : p = 0), |x| ^ p ≤ (p / t) ^ p * max (rexp (t * x)) (rexp (-t * x))
Tactic: by_cases hp_zero : p = 0
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
x t p : ℝ
hp : 0 ≤ p
ht : 0 < t
pos : ∀ (hp_zero : p = 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 neg : ∀ (hp_zero : ¬p = 0), |x| ^ p ≤ (p / t) ^ p * max (rexp (t * x)) (rexp (-t * x))
Tactic: by_cases hp_zero : p = 0
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
x t p : ℝ
hp : 0 ≤ p
ht : 0 < t
hp_zero : p = 0
⊢ |x| ^ p ≤ (p / t) ^ p * max (rexp (t * x)) (rexp (-t * x))
have pos : 0 ≤ t * x ∨ t * x ≤ 0
Tactic: simp only [hp_zero, rpow_zero, zero_div, neg_mul, one_mul, le_sup_iff, one_le_exp_iff,
      Left.nonneg_neg_iff]
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (hypothesis)
Goal:
x t p : ℝ
hp : 0 ≤ p
ht : 0 < t
hp_zero : ¬p = 0
⊢ |x| ^ p ≤ (p / t) ^ p * max (rexp (t * x)) (rexp (-t * x))
have h_x_le : ∀ (c : ℝ) (hc : 0 < c), x ≤ c⁻¹ * rexp (c * x)
Tactic: have h_x_le c (hc : 0 < c) : x ≤ c⁻¹ * exp (c * x) := le_inv_mul_exp x hc