awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
Y : Ω → ℝ
h : X =ᶠ[ae μ] Y
ω : Ω
hω : X ω = Y ω
⊢ rexp (t * X ω) = rexp (t * Y ω)
have rw : rexp (t * Y ω) = rexp (t * Y ω)
Tactic: rw [hω]
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
Y : Ω → ℝ
h : X =ᶠ[ae μ] Y
⊢ (ae μ).EventuallyEq (β := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) fun (ω : Ω) ↦ rexp (t * Y ω)
have h₁ : ∀ (a : Ω),
  Membership.mem (γ := Set Ω)
    {x : Ω |
      Membership.mem (γ := Set Ω) {x : Ω | (fun (x : Ω) ↦ X x = Y x) x} x →
        Membership.mem (γ := Set Ω)
          {x : Ω | (fun (x : Ω) ↦ Eq (α := ℝ) ((fun (ω : Ω) ↦ rexp (t * X ω)) x) ((fun (ω : Ω) ↦ rexp (t * Y ω)) x)) x}
          x}
    a
Tactic: filter_upwards [h] with ω hω using by rw [hω]
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
Y : Ω → ℝ
h : X =ᶠ[ae μ] Y
h₁ :
  ∀ (a : Ω),
    Membership.mem (γ := Set Ω)
      {x : Ω |
        Membership.mem (γ := Set Ω) {x : Ω | (fun (x : Ω) ↦ X x = Y x) x} x →
          Membership.mem (γ := Set Ω)
            {x : Ω |
              (fun (x : Ω) ↦ Eq (α := ℝ) ((fun (ω : Ω) ↦ rexp (t * X ω)) x) ((fun (ω : Ω) ↦ rexp (t * Y ω)) x)) x}
            x}
      a
⊢ (ae μ).EventuallyEq (β := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) fun (ω : Ω) ↦ rexp (t * Y ω)
have h₂ : ∀ (a : Ω), X a = Y a → rexp (t * X a) = rexp (t * Y a)
Tactic: filter_upwards [h] with ω hω using by rw [hω]
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
μ' : Measure Ω'
Y : Ω' → ℝ
h : IdentDistrib X Y μ μ'
⊢ mgf X μ = mgf Y μ'
have rw : mgf (m := measurableSpace) id (Measure.map X μ) = mgf Y μ'
Tactic: rw [← mgf_id_map h.aemeasurable_fst, ← mgf_id_map h.aemeasurable_snd, h.map_eq]
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
μ' : Measure Ω'
Y : Ω' → ℝ
h : IdentDistrib X Y μ μ'
rw : mgf (m := measurableSpace) id (Measure.map X μ) = mgf Y μ'
⊢ mgf X μ = mgf Y μ'
have rw₁ : mgf (m := measurableSpace) id (Measure.map X μ) = mgf (m := measurableSpace) id (Measure.map Y μ')
Tactic: rw [← mgf_id_map h.aemeasurable_fst, ← mgf_id_map h.aemeasurable_snd, h.map_eq]
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
μ' : Measure Ω'
Y : Ω' → ℝ
h : IdentDistrib X Y μ μ'
rw : mgf (m := measurableSpace) id (Measure.map X μ) = mgf Y μ'
rw₁ : mgf (m := measurableSpace) id (Measure.map X μ) = mgf (m := measurableSpace) id (Measure.map Y μ')
⊢ mgf X μ = mgf Y μ'
have rw₂ : mgf (m := measurableSpace) id (Measure.map Y μ') = mgf (m := measurableSpace) id (Measure.map Y μ')
Tactic: rw [← mgf_id_map h.aemeasurable_fst, ← mgf_id_map h.aemeasurable_snd, h.map_eq]
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
⊢ mgf (-X) μ t = mgf X μ (-t)
have simp_rw : Eq (α := ℝ) (∫ (x : Ω), rexp (t * (-X) x) ∂μ) (∫ (x : Ω), rexp (-t * X x) ∂μ)
Tactic: simp_rw [mgf, Pi.neg_apply, mul_neg, neg_mul]
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
simp_rw : Eq (α := ℝ) (∫ (x : Ω), rexp (t * (-X) x) ∂μ) (∫ (x : Ω), rexp (-t * X x) ∂μ)
⊢ mgf (-X) μ t = mgf X μ (-t)
have simp_rw₁ : Eq (α := ℝ) (∫ (x : Ω), rexp (t * -X x) ∂μ) (∫ (x : Ω), rexp (-t * X x) ∂μ)
Tactic: simp_rw [mgf, Pi.neg_apply, mul_neg, neg_mul]
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
simp_rw : Eq (α := ℝ) (∫ (x : Ω), rexp (t * (-X) x) ∂μ) (∫ (x : Ω), rexp (-t * X x) ∂μ)
simp_rw₁ : Eq (α := ℝ) (∫ (x : Ω), rexp (t * -X x) ∂μ) (∫ (x : Ω), rexp (-t * X x) ∂μ)
⊢ mgf (-X) μ t = mgf X μ (-t)
have simp_rw₂ : Eq (α := ℝ) (∫ (x : Ω), rexp (-(t * X x)) ∂μ) (∫ (x : Ω), rexp (-t * X x) ∂μ)
Tactic: simp_rw [mgf, Pi.neg_apply, mul_neg, neg_mul]
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t α : ℝ
⊢ mgf (α • X) μ t = mgf X μ (α * t)
have simp_rw : Eq (α := ℝ) (∫ (x : Ω), rexp (t * (α • X) x) ∂μ) (∫ (x : Ω), rexp (α * t * X x) ∂μ)
Tactic: simp_rw [mgf, Pi.smul_apply, smul_eq_mul, mul_comm α t, mul_assoc]
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t α : ℝ
simp_rw : Eq (α := ℝ) (∫ (x : Ω), rexp (t * (α • X) x) ∂μ) (∫ (x : Ω), rexp (α * t * X x) ∂μ)
⊢ mgf (α • X) μ t = mgf X μ (α * t)
have simp_rw₁ : Eq (α := ℝ) (∫ (x : Ω), rexp (t * α • X x) ∂μ) (∫ (x : Ω), rexp (α * t * X x) ∂μ)
Tactic: simp_rw [mgf, Pi.smul_apply, smul_eq_mul, mul_comm α t, mul_assoc]
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t α : ℝ
simp_rw : Eq (α := ℝ) (∫ (x : Ω), rexp (t * (α • X) x) ∂μ) (∫ (x : Ω), rexp (α * t * X x) ∂μ)
simp_rw₁ : Eq (α := ℝ) (∫ (x : Ω), rexp (t * α • X x) ∂μ) (∫ (x : Ω), rexp (α * t * X x) ∂μ)
⊢ mgf (α • X) μ t = mgf X μ (α * t)
have simp_rw₂ : Eq (α := ℝ) (∫ (x : Ω), rexp (t * (α * X x)) ∂μ) (∫ (x : Ω), rexp (α * t * X x) ∂μ)
Tactic: simp_rw [mgf, Pi.smul_apply, smul_eq_mul, mul_comm α t, mul_assoc]
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t α : ℝ
simp_rw : Eq (α := ℝ) (∫ (x : Ω), rexp (t * (α • X) x) ∂μ) (∫ (x : Ω), rexp (α * t * X x) ∂μ)
simp_rw₁ : Eq (α := ℝ) (∫ (x : Ω), rexp (t * α • X x) ∂μ) (∫ (x : Ω), rexp (α * t * X x) ∂μ)
simp_rw₂ : Eq (α := ℝ) (∫ (x : Ω), rexp (t * (α * X x)) ∂μ) (∫ (x : Ω), rexp (α * t * X x) ∂μ)
⊢ mgf (α • X) μ t = mgf X μ (α * t)
have simp_rw₃ : Eq (α := ℝ) (∫ (x : Ω), rexp (t * (α * X x)) ∂μ) (∫ (x : Ω), rexp (t * α * X x) ∂μ)
Tactic: simp_rw [mgf, Pi.smul_apply, smul_eq_mul, mul_comm α t, mul_assoc]
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t α : ℝ
⊢ mgf (fun (ω : Ω) ↦ α + X ω) μ t = rexp (t * α) * mgf X μ t
have rw : Eq (α := ℝ) (∫ (x : Ω), (fun (ω : Ω) ↦ rexp (t * (α + X ω))) x ∂μ) (∫ (a : Ω), rexp (t * α) * rexp (t * X a) ∂μ)
Tactic: rw [mgf, mgf, ← integral_const_mul]
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t α : ℝ
⊢ Eq (α := ℝ) (∫ (x : Ω), (fun (ω : Ω) ↦ rexp (t * (α + X ω))) x ∂μ) (∫ (a : Ω), rexp (t * α) * rexp (t * X a) ∂μ)
have e_f : ∀ (x : Ω), (fun (ω : Ω) ↦ rexp (t * (α + X ω))) x = rexp (t * α) * rexp (t * X x)
Tactic: congr with x
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t α : ℝ
x : Ω
⊢ rexp (t * (α + X x)) = rexp (t * α) * rexp (t * X x)
have e_f : rexp (t * α + t * X x) = rexp (t * α) * rexp (t * X x)
Tactic: rw [mul_add, exp_add]
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t α : ℝ
x : Ω
e_f : rexp (t * α + t * X x) = rexp (t * α) * rexp (t * X x)
⊢ rexp (t * (α + X x)) = rexp (t * α) * rexp (t * X x)
have e_f₁ : rexp (t * α) * rexp (t * X x) = rexp (t * α) * rexp (t * X x)
Tactic: rw [mul_add, exp_add]
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ν : Measure Ω
hμ : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
hν : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) ν
⊢ mgf X (μ + ν) t = mgf X μ t + mgf X ν t
have rw : ∫ (x : Ω), (fun (ω : Ω) ↦ rexp (t * X ω)) x ∂(μ + ν) = mgf X μ t + mgf X ν t
Tactic: rw [mgf, integral_add_measure hμ hν, mgf, mgf]
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ν : Measure Ω
hμ : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
hν : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) ν
rw : ∫ (x : Ω), (fun (ω : Ω) ↦ rexp (t * X ω)) x ∂(μ + ν) = mgf X μ t + mgf X ν t
⊢ mgf X (μ + ν) t = mgf X μ t + mgf X ν t
have rw₁ : HAdd.hAdd (α := ℝ) (∫ (x : Ω), rexp (t * X x) ∂μ) (∫ (x : Ω), rexp (t * X x) ∂ν) = mgf X μ t + mgf X ν t
Tactic: rw [mgf, integral_add_measure hμ hν, mgf, mgf]
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ν : Measure Ω
hμ : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
hν : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) ν
rw : ∫ (x : Ω), (fun (ω : Ω) ↦ rexp (t * X ω)) x ∂(μ + ν) = mgf X μ t + mgf X ν t
rw₁ : HAdd.hAdd (α := ℝ) (∫ (x : Ω), rexp (t * X x) ∂μ) (∫ (x : Ω), rexp (t * X x) ∂ν) = mgf X μ t + mgf X ν t
⊢ mgf X (μ + ν) t = mgf X μ t + mgf X ν t
have rw₂ : HAdd.hAdd (α := ℝ) (∫ (x : Ω), rexp (t * X x) ∂μ) (∫ (x : Ω), rexp (t * X x) ∂ν) =
  ∫ (x : Ω), (fun (ω : Ω) ↦ rexp (t * X ω)) x ∂μ + mgf X ν t
Tactic: rw [mgf, integral_add_measure hμ hν, mgf, mgf]
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ν : Measure Ω
hμ : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
hν : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) ν
rw : ∫ (x : Ω), (fun (ω : Ω) ↦ rexp (t * X ω)) x ∂(μ + ν) = mgf X μ t + mgf X ν t
rw₁ : HAdd.hAdd (α := ℝ) (∫ (x : Ω), rexp (t * X x) ∂μ) (∫ (x : Ω), rexp (t * X x) ∂ν) = mgf X μ t + mgf X ν t
rw₂ :
  HAdd.hAdd (α := ℝ) (∫ (x : Ω), rexp (t * X x) ∂μ) (∫ (x : Ω), rexp (t * X x) ∂ν) =
    ∫ (x : Ω), (fun (ω : Ω) ↦ rexp (t * X ω)) x ∂μ + mgf X ν t
⊢ mgf X (μ + ν) t = mgf X μ t + mgf X ν t
have rw₃ : HAdd.hAdd (α := ℝ) (∫ (x : Ω), rexp (t * X x) ∂μ) (∫ (x : Ω), rexp (t * X x) ∂ν) =
  HAdd.hAdd (α := ℝ) (∫ (x : Ω), (fun (ω : Ω) ↦ rexp (t * X ω)) x ∂μ) (∫ (x : Ω), (fun (ω : Ω) ↦ rexp (t * X ω)) x ∂ν)
Tactic: rw [mgf, integral_add_measure hμ hν, mgf, mgf]
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
c : ℝ≥0∞
⊢ mgf X (c • μ) t = c.toReal * mgf X μ t
have rw : ∫ (x : Ω), (fun (ω : Ω) ↦ rexp (t * X ω)) x ∂c • μ = c.toReal * mgf X μ t
Tactic: rw [mgf, integral_smul_measure, mgf, smul_eq_mul]
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
c : ℝ≥0∞
rw : ∫ (x : Ω), (fun (ω : Ω) ↦ rexp (t * X ω)) x ∂c • μ = c.toReal * mgf X μ t
⊢ mgf X (c • μ) t = c.toReal * mgf X μ t
have rw₁ : HSMul.hSMul (β := ℝ) c.toReal (∫ (x : Ω), rexp (t * X x) ∂μ) = c.toReal * mgf X μ t
Tactic: rw [mgf, integral_smul_measure, mgf, smul_eq_mul]
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
c : ℝ≥0∞
rw : ∫ (x : Ω), (fun (ω : Ω) ↦ rexp (t * X ω)) x ∂c • μ = c.toReal * mgf X μ t
rw₁ : HSMul.hSMul (β := ℝ) c.toReal (∫ (x : Ω), rexp (t * X x) ∂μ) = c.toReal * mgf X μ t
⊢ mgf X (c • μ) t = c.toReal * mgf X μ t
have rw₂ : HSMul.hSMul (β := ℝ) c.toReal (∫ (x : Ω), rexp (t * X x) ∂μ) = c.toReal * ∫ (x : Ω), (fun (ω : Ω) ↦ rexp (t * X ω)) x ∂μ
Tactic: rw [mgf, integral_smul_measure, mgf, smul_eq_mul]
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
c : ℝ≥0∞
rw : ∫ (x : Ω), (fun (ω : Ω) ↦ rexp (t * X ω)) x ∂c • μ = c.toReal * mgf X μ t
rw₁ : HSMul.hSMul (β := ℝ) c.toReal (∫ (x : Ω), rexp (t * X x) ∂μ) = c.toReal * mgf X μ t
rw₂ :
  HSMul.hSMul (β := ℝ) c.toReal (∫ (x : Ω), rexp (t * X x) ∂μ) =
    c.toReal * ∫ (x : Ω), (fun (ω : Ω) ↦ rexp (t * X ω)) x ∂μ
⊢ mgf X (c • μ) t = c.toReal * mgf X μ t
have rw₃ : c.toReal * ∫ (x : Ω), rexp (t * X x) ∂μ = c.toReal * ∫ (x : Ω), (fun (ω : Ω) ↦ rexp (t * X ω)) x ∂μ
Tactic: rw [mgf, integral_smul_measure, mgf, smul_eq_mul]
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
Y : Ω → ℝ
hXY : X ≤ᶠ[ae μ] Y
ht : 0 ≤ t
htY : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * Y ω)) μ
⊢ mgf X μ t ≤ mgf Y μ t
have pos : ∀ (htX : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ), mgf X μ t ≤ mgf Y μ t
Tactic: by_cases htX : Integrable (fun ω ↦ exp (t * X ω)) μ
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
Y : Ω → ℝ
hXY : X ≤ᶠ[ae μ] Y
ht : 0 ≤ t
htY : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * Y ω)) μ
pos : ∀ (htX : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ), mgf X μ t ≤ mgf Y μ t
⊢ mgf X μ t ≤ mgf Y μ t
have neg : ∀ (htX : ¬Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ), mgf X μ t ≤ mgf Y μ t
Tactic: by_cases htX : Integrable (fun ω ↦ exp (t * X ω)) μ
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
Y : Ω → ℝ
hXY : X ≤ᶠ[ae μ] Y
ht : 0 ≤ t
htY : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * Y ω)) μ
htX : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
⊢ mgf X μ t ≤ mgf Y μ t
have pos : (ae μ).EventuallyLE (β := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) fun (ω : Ω) ↦ rexp (t * Y ω)
Tactic: refine integral_mono_ae htX htY ?_
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
Y : Ω → ℝ
hXY : X ≤ᶠ[ae μ] Y
ht : 0 ≤ t
htY : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * Y ω)) μ
htX : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
⊢ (ae μ).EventuallyLE (β := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) fun (ω : Ω) ↦ rexp (t * Y ω)
have h : ∀ (a : Ω),
  Membership.mem (γ := Set Ω)
    {x : Ω |
      Membership.mem (γ := Set Ω) {x : Ω | (fun (x : Ω) ↦ X x ≤ Y x) x} x →
        Membership.mem (γ := Set Ω)
          {x : Ω |
            (fun (x : Ω) ↦ LE.le (α := ℝ) ((fun (ω : Ω) ↦ rexp (t * X ω)) x) ((fun (ω : Ω) ↦ rexp (t * Y ω)) x)) x}
          x}
    a
Tactic: filter_upwards [hXY] with ω hω using by gcongr
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
Y : Ω → ℝ
hXY : X ≤ᶠ[ae μ] Y
ht : 0 ≤ t
htY : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * Y ω)) μ
htX : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
h :
  ∀ (a : Ω),
    Membership.mem (γ := Set Ω)
      {x : Ω |
        Membership.mem (γ := Set Ω) {x : Ω | (fun (x : Ω) ↦ X x ≤ Y x) x} x →
          Membership.mem (γ := Set Ω)
            {x : Ω |
              (fun (x : Ω) ↦ LE.le (α := ℝ) ((fun (ω : Ω) ↦ rexp (t * X ω)) x) ((fun (ω : Ω) ↦ rexp (t * Y ω)) x)) x}
            x}
      a
⊢ (ae μ).EventuallyLE (β := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) fun (ω : Ω) ↦ rexp (t * Y ω)
have h₁ : ∀ (a : Ω), X a ≤ Y a → rexp (t * X a) ≤ rexp (t * Y a)
Tactic: filter_upwards [hXY] with ω hω using by gcongr
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
Y : Ω → ℝ
hXY : X ≤ᶠ[ae μ] Y
ht : 0 ≤ t
htY : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * Y ω)) μ
htX : ¬Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
⊢ mgf X μ t ≤ mgf Y μ t
have neg : 0 ≤ mgf Y μ t
Tactic: rw [mgf_undef htX]
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
Y : Ω → ℝ
hXY : X ≤ᶠ[ae μ] Y
ht : t ≤ 0
htX : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
⊢ mgf Y μ t ≤ mgf X μ t
have pos : ∀ (htY : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * Y ω)) μ), mgf Y μ t ≤ mgf X μ t
Tactic: by_cases htY : Integrable (fun ω ↦ exp (t * Y ω)) μ
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
Y : Ω → ℝ
hXY : X ≤ᶠ[ae μ] Y
ht : t ≤ 0
htX : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
pos : ∀ (htY : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * Y ω)) μ), mgf Y μ t ≤ mgf X μ t
⊢ mgf Y μ t ≤ mgf X μ t
have neg : ∀ (htY : ¬Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * Y ω)) μ), mgf Y μ t ≤ mgf X μ t
Tactic: by_cases htY : Integrable (fun ω ↦ exp (t * Y ω)) μ
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
Y : Ω → ℝ
hXY : X ≤ᶠ[ae μ] Y
ht : t ≤ 0
htX : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
htY : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * Y ω)) μ
⊢ mgf Y μ t ≤ mgf X μ t
have pos : (ae μ).EventuallyLE (β := ℝ) (fun (ω : Ω) ↦ rexp (t * Y ω)) fun (ω : Ω) ↦ rexp (t * X ω)
Tactic: refine integral_mono_ae htY htX ?_
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
Y : Ω → ℝ
hXY : X ≤ᶠ[ae μ] Y
ht : t ≤ 0
htX : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
htY : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * Y ω)) μ
⊢ (ae μ).EventuallyLE (β := ℝ) (fun (ω : Ω) ↦ rexp (t * Y ω)) fun (ω : Ω) ↦ rexp (t * X ω)
have h : ∀ (a : Ω),
  Membership.mem (γ := Set Ω)
    {x : Ω |
      Membership.mem (γ := Set Ω) {x : Ω | (fun (x : Ω) ↦ X x ≤ Y x) x} x →
        Membership.mem (γ := Set Ω)
          {x : Ω |
            (fun (x : Ω) ↦ LE.le (α := ℝ) ((fun (ω : Ω) ↦ rexp (t * Y ω)) x) ((fun (ω : Ω) ↦ rexp (t * X ω)) x)) x}
          x}
    a
Tactic: filter_upwards [hXY] with ω hω using exp_monotone <| mul_le_mul_of_nonpos_left hω ht
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
Y : Ω → ℝ
hXY : X ≤ᶠ[ae μ] Y
ht : t ≤ 0
htX : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
htY : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * Y ω)) μ
h :
  ∀ (a : Ω),
    Membership.mem (γ := Set Ω)
      {x : Ω |
        Membership.mem (γ := Set Ω) {x : Ω | (fun (x : Ω) ↦ X x ≤ Y x) x} x →
          Membership.mem (γ := Set Ω)
            {x : Ω |
              (fun (x : Ω) ↦ LE.le (α := ℝ) ((fun (ω : Ω) ↦ rexp (t * Y ω)) x) ((fun (ω : Ω) ↦ rexp (t * X ω)) x)) x}
            x}
      a
⊢ (ae μ).EventuallyLE (β := ℝ) (fun (ω : Ω) ↦ rexp (t * Y ω)) fun (ω : Ω) ↦ rexp (t * X ω)
have h₁ : ∀ (a : Ω), X a ≤ Y a → rexp (t * Y a) ≤ rexp (t * X a)
Tactic: filter_upwards [hXY] with ω hω using exp_monotone <| mul_le_mul_of_nonpos_left hω ht
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
Y : Ω → ℝ
hXY : X ≤ᶠ[ae μ] Y
ht : t ≤ 0
htX : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
htY : ¬Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * Y ω)) μ
⊢ mgf Y μ t ≤ mgf X μ t
have neg : 0 ≤ mgf X μ t
Tactic: rw [mgf_undef htY]
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (hypothesis)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
h_indep : X ⟂ᵢ[μ] Y
s t : ℝ
⊢ (fun (ω : Ω) ↦ rexp (s * X ω)) ⟂ᵢ[μ] fun (ω : Ω) ↦ rexp (t * Y ω)
have h_meas : ∀ (t : ℝ), Measurable (β := ℝ) fun (x : ℝ) ↦ rexp (t * x)
Tactic: have h_meas : ∀ t, Measurable fun x => exp (t * x) := fun t => (measurable_id'.const_mul t).exp
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X Y : Ω → ℝ
h_indep : X ⟂ᵢ[μ] Y
hX : AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
hY : AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * Y ω)) μ
⊢ mgf (X + Y) μ t = mgf X μ t * mgf Y μ t
have simp_rw : ∫ (x : Ω), rexp (t * X x) * rexp (t * Y x) ∂μ =
  HMul.hMul (α := ℝ) (∫ (x : Ω), rexp (t * X x) ∂μ) (∫ (x : Ω), rexp (t * Y x) ∂μ)
Tactic: simp_rw [mgf, Pi.add_apply, mul_add, exp_add]
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (hypothesis)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X Y : Ω → ℝ
h_indep : X ⟂ᵢ[μ] Y
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
⊢ mgf (X + Y) μ t = mgf X μ t * mgf Y μ t
have A : Continuous (Y := ℝ) fun (x : ℝ) ↦ rexp (t * x)
Tactic: have A : Continuous fun x : ℝ => exp (t * x) := by fun_prop
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (hypothesis)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X Y : Ω → ℝ
h_indep : X ⟂ᵢ[μ] Y
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
A : Continuous (Y := ℝ) fun (x : ℝ) ↦ rexp (t * x)
⊢ mgf (X + Y) μ t = mgf X μ t * mgf Y μ t
have h'X : AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
Tactic: have h'X : AEStronglyMeasurable (fun ω => exp (t * X ω)) μ :=
    A.aestronglyMeasurable.comp_aemeasurable hX.aemeasurable
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (hypothesis)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X Y : Ω → ℝ
h_indep : X ⟂ᵢ[μ] Y
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
A : Continuous (Y := ℝ) fun (x : ℝ) ↦ rexp (t * x)
h'X : AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
⊢ mgf (X + Y) μ t = mgf X μ t * mgf Y μ t
have h'Y : AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * Y ω)) μ
Tactic: have h'Y : AEStronglyMeasurable (fun ω => exp (t * Y ω)) μ :=
    A.aestronglyMeasurable.comp_aemeasurable hY.aemeasurable
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X Y : Ω → ℝ
h_indep : X ⟂ᵢ[μ] Y
h_int_X : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
h_int_Y : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * Y ω)) μ
⊢ cgf (X + Y) μ t = cgf X μ t + cgf Y μ t
have pos : ∀ (hμ : μ = 0), cgf (X + Y) μ t = cgf X μ t + cgf Y μ t
Tactic: by_cases hμ : μ = 0
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X Y : Ω → ℝ
h_indep : X ⟂ᵢ[μ] Y
h_int_X : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
h_int_Y : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * Y ω)) μ
pos : ∀ (hμ : μ = 0), cgf (X + Y) μ t = cgf X μ t + cgf Y μ t
⊢ cgf (X + Y) μ t = cgf X μ t + cgf Y μ t
have neg : ∀ (hμ : ¬μ = 0), cgf (X + Y) μ t = cgf X μ t + cgf Y μ t
Tactic: by_cases hμ : μ = 0
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X Y : Ω → ℝ
h_indep : X ⟂ᵢ[μ] Y
h_int_X : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
h_int_Y : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * Y ω)) μ
hμ : ¬μ = 0
⊢ cgf (X + Y) μ t = cgf X μ t + cgf Y μ t
have neg : log (mgf X μ t * mgf Y μ t) = log (mgf X μ t) + log (mgf Y μ t)
Tactic: simp only [cgf, h_indep.mgf_add h_int_X.aestronglyMeasurable h_int_Y.aestronglyMeasurable]
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X Y : Ω → ℝ
h_int_X : AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
h_int_Y : AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * Y ω)) μ
⊢ AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * (X + Y) ω)) μ
have simp_rw : AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω) * rexp (t * Y ω)) μ
Tactic: simp_rw [Pi.add_apply, mul_add, exp_add]
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X : ι → Ω → ℝ
h_int : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * X i ω)) μ
⊢ AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * (∑ i ∈ ∅, X i) ω)) μ
have empty : AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ 1) μ
Tactic: simp only [sum_apply, sum_empty, mul_zero, exp_zero]