awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X : ι → Ω → ℝ
h_indep : iIndepFun (β := fun (x : ι) ↦ ℝ) X μ
h_meas : ∀ (i : ι), AEMeasurable (X i) μ
s : Finset ι
this : IsProbabilityMeasure μ
⊢ mgf (∑ i ∈ s, X i) μ t = ∏ i ∈ s, mgf (X i) μ t
have empty : mgf (∑ i ∈ ∅, X i) μ t = ∏ i ∈ ∅, mgf (X i) μ t
Tactic: classical
  induction s using Finset.induction_on with
  | empty => simp
  | insert i s hi_notin_s h_rec =>
    have h_int' : ∀ i : ι, AEStronglyMeasurable (fun ω : Ω => exp (t * X i ω)) μ := fun i =>
      ((h_meas i).const_mul t).exp.aestronglyMeasurable
    rw [sum_insert hi_notin_s,
      IndepFun.mgf_add (h_indep.indepFun_finsetSum_of_notMem₀ h_meas hi_notin_s).symm (h_int' i)
        (aestronglyMeasurable_exp_mul_sum fun i _ => h_int' i),
      h_rec, prod_insert hi_notin_s]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X : ι → Ω → ℝ
h_indep : iIndepFun (β := fun (x : ι) ↦ ℝ) X μ
h_meas : ∀ (i : ι), AEMeasurable (X i) μ
s : Finset ι
this : IsProbabilityMeasure μ
empty : mgf (∑ i ∈ ∅, X i) μ t = ∏ i ∈ ∅, mgf (X i) μ t
⊢ mgf (∑ i ∈ s, X i) μ t = ∏ i ∈ s, mgf (X i) μ t
have insert : ∀ (i : ι) (s : Finset ι) (hi_notin_s : i ∉ s) (h_rec : mgf (∑ i ∈ s, X i) μ t = ∏ i ∈ s, mgf (X i) μ t),
  mgf (∑ i ∈ insert i s, X i) μ t = ∏ i ∈ insert i s, mgf (X i) μ t
Tactic: classical
  induction s using Finset.induction_on with
  | empty => simp
  | insert i s hi_notin_s h_rec =>
    have h_int' : ∀ i : ι, AEStronglyMeasurable (fun ω : Ω => exp (t * X i ω)) μ := fun i =>
      ((h_meas i).const_mul t).exp.aestronglyMeasurable
    rw [sum_insert hi_notin_s,
      IndepFun.mgf_add (h_indep.indepFun_finsetSum_of_notMem₀ h_meas hi_notin_s).symm (h_int' i)
        (aestronglyMeasurable_exp_mul_sum fun i _ => h_int' i),
      h_rec, prod_insert hi_notin_s]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (hypothesis)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X : ι → Ω → ℝ
h_indep : iIndepFun (β := fun (x : ι) ↦ ℝ) X μ
h_meas : ∀ (i : ι), AEMeasurable (X i) μ
s : Finset ι
h_int : ∀ i ∈ s, Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X i ω)) μ
⊢ cgf (∑ i ∈ s, X i) μ t = ∑ i ∈ s, cgf (X i) μ t
have this : IsProbabilityMeasure μ
Tactic: have : IsProbabilityMeasure μ := h_indep.isProbabilityMeasure
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X : ι → Ω → ℝ
h_indep : iIndepFun (β := fun (x : ι) ↦ ℝ) X μ
h_meas : ∀ (i : ι), AEMeasurable (X i) μ
s : Finset ι
h_int : ∀ i ∈ s, Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X i ω)) μ
this : IsProbabilityMeasure μ
⊢ log (mgf (∑ i ∈ s, X i) μ t) = ∑ x ∈ s, log (mgf (X x) μ t)
have rw : log (mgf (∑ i ∈ s, X i) μ t) = log (∏ i ∈ s, mgf (X i) μ t)
Tactic: rw [← log_prod fun j hj => ?_]
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X : ι → Ω → ℝ
h_indep : iIndepFun (β := fun (x : ι) ↦ ℝ) X μ
h_meas : ∀ (i : ι), AEMeasurable (X i) μ
s : Finset ι
h_int : ∀ i ∈ s, Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X i ω)) μ
this : IsProbabilityMeasure μ
rw : log (mgf (∑ i ∈ s, X i) μ t) = log (∏ i ∈ s, mgf (X i) μ t)
⊢ log (mgf (∑ i ∈ s, X i) μ t) = ∑ x ∈ s, log (mgf (X x) μ t)
have rw₁ : ∀ (j : ι) (hj : j ∈ s), mgf (X j) μ t ≠ 0
Tactic: rw [← log_prod fun j hj => ?_]
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X : ι → Ω → ℝ
h_indep : iIndepFun (β := fun (x : ι) ↦ ℝ) X μ
h_meas : ∀ (i : ι), AEMeasurable (X i) μ
s : Finset ι
h_int : ∀ i ∈ s, Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X i ω)) μ
this : IsProbabilityMeasure μ
⊢ log (mgf (∑ i ∈ s, X i) μ t) = log (∏ i ∈ s, mgf (X i) μ t)
have rw : log (∏ i ∈ s, mgf (X i) μ t) = log (∏ i ∈ s, mgf (X i) μ t)
Tactic: rw [h_indep.mgf_sum₀ h_meas]
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
X : ι → Ω → ℝ
s : Finset ι
j : ι
h_meas : ∀ (i : ι), AEMeasurable (X i) μ
h_indep : iIndepFun (β := fun (x : ι) ↦ ℝ) X μ
hident : ∀ i ∈ s, ∀ j ∈ s, IdentDistrib (X i) (X j) μ μ
hj : j ∈ s
t : ℝ
⊢ mgf (∑ i ∈ s, X i) μ t = mgf (X j) μ t ^ #s
have rw : ∏ i ∈ s, mgf (X i) μ t = mgf (X j) μ t ^ #s
Tactic: rw [h_indep.mgf_sum₀ h_meas]
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst : IsFiniteMeasure μ
ε : ℝ
ht : 0 ≤ t
h_int : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
⊢ μ.real {ω : Ω | ε ≤ X ω} ≤ rexp (-t * ε) * mgf X μ t
have inl : ∀ (ht_zero_eq : 0 = t), μ.real {ω : Ω | ε ≤ X ω} ≤ rexp (-t * ε) * mgf X μ t
Tactic: rcases ht.eq_or_lt with ht_zero_eq | ht_pos
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst : IsFiniteMeasure μ
ε : ℝ
ht : 0 ≤ t
h_int : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
inl : ∀ (ht_zero_eq : 0 = t), μ.real {ω : Ω | ε ≤ X ω} ≤ rexp (-t * ε) * mgf X μ t
⊢ μ.real {ω : Ω | ε ≤ X ω} ≤ rexp (-t * ε) * mgf X μ t
have inr : ∀ (ht_pos : 0 < t), μ.real {ω : Ω | ε ≤ X ω} ≤ rexp (-t * ε) * mgf X μ t
Tactic: rcases ht.eq_or_lt with ht_zero_eq | ht_pos
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst : IsFiniteMeasure μ
ε : ℝ
ht : 0 ≤ t
h_int : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
ht_zero_eq : 0 = t
⊢ μ.real {ω : Ω | ε ≤ X ω} ≤ rexp (-t * ε) * mgf X μ t
have inl : μ.real {ω : Ω | ε ≤ X ω} ≤ rexp (-0 * ε) * mgf X μ 0
Tactic: rw [ht_zero_eq.symm]
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst : IsFiniteMeasure μ
ε : ℝ
ht : 0 ≤ t
h_int : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
ht_zero_eq : 0 = t
⊢ μ.real {ω : Ω | ε ≤ X ω} ≤ rexp (-0 * ε) * mgf X μ 0
have inl : μ.real {ω : Ω | ε ≤ X ω} ≤ μ.real Set.univ
Tactic: simp only [neg_zero, zero_mul, exp_zero, mgf_zero', one_mul]
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst : IsFiniteMeasure μ
ε : ℝ
ht : 0 ≤ t
h_int : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
ht_zero_eq : 0 = t
⊢ μ.real {ω : Ω | ε ≤ X ω} ≤ μ.real Set.univ
have inl : autoParam (Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)) measureReal_mono._auto_1
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst : IsFiniteMeasure μ
ε : ℝ
ht : 0 ≤ t
h_int : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
ht_zero_eq : 0 = t
inl : autoParam (Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)) measureReal_mono._auto_1
⊢ μ.real {ω : Ω | ε ≤ X ω} ≤ μ.real Set.univ
have inl₁ : Subset.{u_1} (α := Set Ω) {ω : Ω | ε ≤ X ω} Set.univ
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst : IsFiniteMeasure μ
ε : ℝ
ht : 0 ≤ t
h_int : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
ht_pos : 0 < t
⊢ μ.real {ω : Ω | ε ≤ X ω} = μ.real {ω : Ω | rexp (t * ε) ≤ rexp (t * X ω)}
have e_s : ∀ (ω : Ω),
  Membership.mem (γ := Set Ω) {ω : Ω | ε ≤ X ω} ω ↔
    Membership.mem (γ := Set Ω) {ω : Ω | rexp (t * ε) ≤ rexp (t * X ω)} ω
Tactic: congr 1 with ω
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst : IsFiniteMeasure μ
ε : ℝ
ht : 0 ≤ t
h_int : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
ht_pos : 0 < t
ω : Ω
⊢ Membership.mem (γ := Set Ω) {ω : Ω | ε ≤ X ω} ω ↔
    Membership.mem (γ := Set Ω) {ω : Ω | rexp (t * ε) ≤ rexp (t * X ω)} ω
have e_s : ε ≤ X ω ↔ t * ε ≤ t * X ω
Tactic: simp only [Set.mem_setOf_eq, exp_le_exp]
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (hypothesis)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst : IsFiniteMeasure μ
ε : ℝ
ht : 0 ≤ t
h_int : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
ht_pos : 0 < t
⊢ μ.real {ω : Ω | rexp (t * ε) ≤ rexp (t * X ω)} ≤ (rexp (t * ε))⁻¹ * ∫ (x : Ω), (fun (ω : Ω) ↦ rexp (t * X ω)) x ∂μ
have this : rexp (t * ε) * μ.real {ω : Ω | rexp (t * ε) ≤ rexp (t * X ω)} ≤ ∫ (x : Ω), (fun (ω : Ω) ↦ rexp (t * X ω)) x ∂μ
Tactic: have : exp (t * ε) * μ.real {ω | exp (t * ε) ≤ exp (t * X ω)} ≤
          μ[fun ω => exp (t * X ω)] :=
        mul_meas_ge_le_integral_of_nonneg (ae_of_all _ fun x => (exp_pos _).le) h_int _
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst : IsFiniteMeasure μ
ε : ℝ
ht : 0 ≤ t
h_int : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
ht_pos : 0 < t
this : rexp (t * ε) * μ.real {ω : Ω | rexp (t * ε) ≤ rexp (t * X ω)} ≤ ∫ (x : Ω), (fun (ω : Ω) ↦ rexp (t * X ω)) x ∂μ
⊢ μ.real {ω : Ω | rexp (t * ε) ≤ rexp (t * X ω)} ≤ (rexp (t * ε))⁻¹ * ∫ (x : Ω), (fun (ω : Ω) ↦ rexp (t * X ω)) x ∂μ
have rwa : μ.real {ω : Ω | rexp (t * ε) ≤ rexp (t * X ω)} ≤ (∫ (x : Ω), (fun (ω : Ω) ↦ rexp (t * X ω)) x ∂μ) * (rexp (t * ε))⁻¹
Tactic: rwa [mul_comm (exp (t * ε))⁻¹, ← div_eq_mul_inv, le_div_iff₀' (exp_pos _)]
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst : IsFiniteMeasure μ
ε : ℝ
ht : 0 ≤ t
h_int : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
ht_pos : 0 < t
this : rexp (t * ε) * μ.real {ω : Ω | rexp (t * ε) ≤ rexp (t * X ω)} ≤ ∫ (x : Ω), (fun (ω : Ω) ↦ rexp (t * X ω)) x ∂μ
rwa :
  μ.real {ω : Ω | rexp (t * ε) ≤ rexp (t * X ω)} ≤ (∫ (x : Ω), (fun (ω : Ω) ↦ rexp (t * X ω)) x ∂μ) * (rexp (t * ε))⁻¹
⊢ μ.real {ω : Ω | rexp (t * ε) ≤ rexp (t * X ω)} ≤ (rexp (t * ε))⁻¹ * ∫ (x : Ω), (fun (ω : Ω) ↦ rexp (t * X ω)) x ∂μ
have rwa₁ : μ.real {ω : Ω | rexp (t * ε) ≤ rexp (t * X ω)} ≤ (∫ (x : Ω), (fun (ω : Ω) ↦ rexp (t * X ω)) x ∂μ) / rexp (t * ε)
Tactic: rwa [mul_comm (exp (t * ε))⁻¹, ← div_eq_mul_inv, le_div_iff₀' (exp_pos _)]
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst : IsFiniteMeasure μ
ε : ℝ
ht : 0 ≤ t
h_int : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
ht_pos : 0 < t
⊢ (rexp (t * ε))⁻¹ * ∫ (x : Ω), (fun (ω : Ω) ↦ rexp (t * X ω)) x ∂μ = rexp (-t * ε) * mgf X μ t
have rw : (rexp (t * ε))⁻¹ * ∫ (x : Ω), (fun (ω : Ω) ↦ rexp (t * X ω)) x ∂μ = (rexp (t * ε))⁻¹ * mgf X μ t
Tactic: rw [neg_mul, exp_neg]
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst : IsFiniteMeasure μ
ε : ℝ
ht : 0 ≤ t
h_int : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
ht_pos : 0 < t
⊢ μ.real {ω : Ω | ε ≤ X ω} ≤ rexp (-t * ε) * mgf X μ t
have ε₁ : μ.real {ω : Ω | ε ≤ X ω} = μ.real {ω : Ω | rexp (t * ε) ≤ rexp (t * X ω)}
Tactic: calc
    μ.real {ω | ε ≤ X ω} = μ.real {ω | exp (t * ε) ≤ exp (t * X ω)} := by
      congr 1 with ω
      simp only [Set.mem_setOf_eq, exp_le_exp]
      exact ⟨fun h => mul_le_mul_of_nonneg_left h ht_pos.le,
        fun h => le_of_mul_le_mul_left h ht_pos⟩
    _ ≤ (exp (t * ε))⁻¹ * μ[fun ω => exp (t * X ω)] := by
      have : exp (t * ε) * μ.real {ω | exp (t * ε) ≤ exp (t * X ω)} ≤
          μ[fun ω => exp (t * X ω)] :=
        mul_meas_ge_le_integral_of_nonneg (ae_of_all _ fun x => (exp_pos _).le) h_int _
      rwa [mul_comm (exp (t * ε))⁻¹, ← div_eq_mul_inv, le_div_iff₀' (exp_pos _)]
    _ = exp (-t * ε) * mgf X μ t := by rw [neg_mul, exp_neg]; rfl
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst : IsFiniteMeasure μ
ε : ℝ
ht : 0 ≤ t
h_int : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
ht_pos : 0 < t
ε₁ : μ.real {ω : Ω | ε ≤ X ω} = μ.real {ω : Ω | rexp (t * ε) ≤ rexp (t * X ω)}
⊢ μ.real {ω : Ω | ε ≤ X ω} ≤ rexp (-t * ε) * mgf X μ t
have ε₂ : μ.real {ω : Ω | rexp (t * ε) ≤ rexp (t * X ω)} ≤ (rexp (t * ε))⁻¹ * ∫ (x : Ω), (fun (ω : Ω) ↦ rexp (t * X ω)) x ∂μ
Tactic: calc
    μ.real {ω | ε ≤ X ω} = μ.real {ω | exp (t * ε) ≤ exp (t * X ω)} := by
      congr 1 with ω
      simp only [Set.mem_setOf_eq, exp_le_exp]
      exact ⟨fun h => mul_le_mul_of_nonneg_left h ht_pos.le,
        fun h => le_of_mul_le_mul_left h ht_pos⟩
    _ ≤ (exp (t * ε))⁻¹ * μ[fun ω => exp (t * X ω)] := by
      have : exp (t * ε) * μ.real {ω | exp (t * ε) ≤ exp (t * X ω)} ≤
          μ[fun ω => exp (t * X ω)] :=
        mul_meas_ge_le_integral_of_nonneg (ae_of_all _ fun x => (exp_pos _).le) h_int _
      rwa [mul_comm (exp (t * ε))⁻¹, ← div_eq_mul_inv, le_div_iff₀' (exp_pos _)]
    _ = exp (-t * ε) * mgf X μ t := by rw [neg_mul, exp_neg]; rfl
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst : IsFiniteMeasure μ
ε : ℝ
ht : 0 ≤ t
h_int : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
ht_pos : 0 < t
ε₁ : μ.real {ω : Ω | ε ≤ X ω} = μ.real {ω : Ω | rexp (t * ε) ≤ rexp (t * X ω)}
ε₂ : μ.real {ω : Ω | rexp (t * ε) ≤ rexp (t * X ω)} ≤ (rexp (t * ε))⁻¹ * ∫ (x : Ω), (fun (ω : Ω) ↦ rexp (t * X ω)) x ∂μ
⊢ μ.real {ω : Ω | ε ≤ X ω} ≤ rexp (-t * ε) * mgf X μ t
have ε₃ : (rexp (t * ε))⁻¹ * ∫ (x : Ω), (fun (ω : Ω) ↦ rexp (t * X ω)) x ∂μ = rexp (-t * ε) * mgf X μ t
Tactic: calc
    μ.real {ω | ε ≤ X ω} = μ.real {ω | exp (t * ε) ≤ exp (t * X ω)} := by
      congr 1 with ω
      simp only [Set.mem_setOf_eq, exp_le_exp]
      exact ⟨fun h => mul_le_mul_of_nonneg_left h ht_pos.le,
        fun h => le_of_mul_le_mul_left h ht_pos⟩
    _ ≤ (exp (t * ε))⁻¹ * μ[fun ω => exp (t * X ω)] := by
      have : exp (t * ε) * μ.real {ω | exp (t * ε) ≤ exp (t * X ω)} ≤
          μ[fun ω => exp (t * X ω)] :=
        mul_meas_ge_le_integral_of_nonneg (ae_of_all _ fun x => (exp_pos _).le) h_int _
      rwa [mul_comm (exp (t * ε))⁻¹, ← div_eq_mul_inv, le_div_iff₀' (exp_pos _)]
    _ = exp (-t * ε) * mgf X μ t := by rw [neg_mul, exp_neg]; rfl
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst : IsFiniteMeasure μ
ε : ℝ
ht : t ≤ 0
h_int : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
⊢ μ.real {ω : Ω | X ω ≤ ε} ≤ rexp (-t * ε) * mgf X μ t
have rw : μ.real {ω : Ω | X ω ≤ ε} ≤ rexp (- -t * -ε) * mgf (-X) μ (-t)
Tactic: rw [← neg_neg t, ← mgf_neg, neg_neg, ← neg_mul_neg (-t)]
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst : IsFiniteMeasure μ
ε : ℝ
ht : t ≤ 0
h_int : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
⊢ μ.real {ω : Ω | X ω ≤ ε} ≤ rexp (- -t * -ε) * mgf (-X) μ (-t)
have refine_1 : μ.real {ω : Ω | X ω ≤ ε} = μ.real {ω : Ω | -ε ≤ (-X) ω}
Tactic: refine Eq.trans_le ?_ (measure_ge_le_exp_mul_mgf (-ε) (neg_nonneg.mpr ht) ?_)
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst : IsFiniteMeasure μ
ε : ℝ
ht : t ≤ 0
h_int : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
refine_1 : μ.real {ω : Ω | X ω ≤ ε} = μ.real {ω : Ω | -ε ≤ (-X) ω}
⊢ μ.real {ω : Ω | X ω ≤ ε} ≤ rexp (- -t * -ε) * mgf (-X) μ (-t)
have refine_2 : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (-t * (-X) ω)) μ
Tactic: refine Eq.trans_le ?_ (measure_ge_le_exp_mul_mgf (-ε) (neg_nonneg.mpr ht) ?_)
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst : IsFiniteMeasure μ
ε : ℝ
ht : 0 ≤ t
h_int : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
⊢ μ.real {ω : Ω | ε ≤ X ω} ≤ rexp (-t * ε + cgf X μ t)
have refine : rexp (-t * ε) * mgf X μ t ≤ rexp (-t * ε + cgf X μ t)
Tactic: refine (measure_ge_le_exp_mul_mgf ε ht h_int).trans ?_
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst : IsFiniteMeasure μ
ε : ℝ
ht : 0 ≤ t
h_int : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
⊢ rexp (-t * ε) * mgf X μ t ≤ rexp (-t * ε + cgf X μ t)
have rw : rexp (-t * ε) * mgf X μ t ≤ rexp (-t * ε) * rexp (cgf X μ t)
Tactic: rw [exp_add]
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst : IsFiniteMeasure μ
ε : ℝ
ht : t ≤ 0
h_int : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
⊢ μ.real {ω : Ω | X ω ≤ ε} ≤ rexp (-t * ε + cgf X μ t)
have refine : rexp (-t * ε) * mgf X μ t ≤ rexp (-t * ε + cgf X μ t)
Tactic: refine (measure_le_le_exp_mul_mgf ε ht h_int).trans ?_
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst : IsFiniteMeasure μ
ε : ℝ
ht : t ≤ 0
h_int : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
⊢ rexp (-t * ε) * mgf X μ t ≤ rexp (-t * ε + cgf X μ t)
have rw : rexp (-t * ε) * mgf X μ t ≤ rexp (-t * ε) * rexp (cgf X μ t)
Tactic: rw [exp_add]
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
x : ℝ
hX : Eq (α := Measure ℝ) (Measure.map X μ) (Measure.dirac x)
t : ℝ
⊢ IsProbabilityMeasure (m0 := measurableSpace) (Measure.map X μ)
have rw : IsProbabilityMeasure (m0 := measurableSpace) (Measure.dirac x)
Tactic: rw [hX]
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (hypothesis)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
x : ℝ
hX : Eq (α := Measure ℝ) (Measure.map X μ) (Measure.dirac x)
t : ℝ
⊢ mgf X μ t = rexp (x * t)
have this : IsProbabilityMeasure (m0 := measurableSpace) (Measure.map X μ)
Tactic: have : IsProbabilityMeasure (μ.map X) := by rw [hX]; infer_instance
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
x : ℝ
hX : Eq (α := Measure ℝ) (Measure.map X μ) (Measure.dirac x)
t : ℝ
this : IsProbabilityMeasure (m0 := measurableSpace) (Measure.map X μ)
⊢ mgf X μ t = rexp (x * t)
have rw : mgf (m := measurableSpace) id (Measure.map X μ) t = rexp (x * t)
Tactic: rw [← mgf_id_map (.of_map_ne_zero <| IsProbabilityMeasure.ne_zero _), mgf, hX, integral_dirac,
    mul_comm, id_def]
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
x : ℝ
hX : Eq (α := Measure ℝ) (Measure.map X μ) (Measure.dirac x)
t : ℝ
this : IsProbabilityMeasure (m0 := measurableSpace) (Measure.map X μ)
rw : mgf (m := measurableSpace) id (Measure.map X μ) t = rexp (x * t)
⊢ mgf X μ t = rexp (x * t)
have rw₁ : (@integral _ _ _ _ measurableSpace (Measure.map X μ) fun (x : ℝ) ↦ (fun (ω : ℝ) ↦ rexp (t * id ω)) x) = rexp (x * t)
Tactic: rw [← mgf_id_map (.of_map_ne_zero <| IsProbabilityMeasure.ne_zero _), mgf, hX, integral_dirac,
    mul_comm, id_def]
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
x : ℝ
hX : Eq (α := Measure ℝ) (Measure.map X μ) (Measure.dirac x)
t : ℝ
this : IsProbabilityMeasure (m0 := measurableSpace) (Measure.map X μ)
rw : mgf (m := measurableSpace) id (Measure.map X μ) t = rexp (x * t)
rw₁ :
  (@integral _ _ _ _ measurableSpace (Measure.map X μ) fun (x : ℝ) ↦ (fun (ω : ℝ) ↦ rexp (t * id ω)) x) = rexp (x * t)
⊢ mgf X μ t = rexp (x * t)
have rw₂ : (@integral _ _ _ _ measurableSpace (Measure.dirac x) fun (x : ℝ) ↦ (fun (ω : ℝ) ↦ rexp (t * id ω)) x) = rexp (x * t)
Tactic: rw [← mgf_id_map (.of_map_ne_zero <| IsProbabilityMeasure.ne_zero _), mgf, hX, integral_dirac,
    mul_comm, id_def]
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
x : ℝ
hX : Eq (α := Measure ℝ) (Measure.map X μ) (Measure.dirac x)
t : ℝ
this : IsProbabilityMeasure (m0 := measurableSpace) (Measure.map X μ)
rw : mgf (m := measurableSpace) id (Measure.map X μ) t = rexp (x * t)
rw₁ :
  (@integral _ _ _ _ measurableSpace (Measure.map X μ) fun (x : ℝ) ↦ (fun (ω : ℝ) ↦ rexp (t * id ω)) x) = rexp (x * t)
rw₂ :
  (@integral _ _ _ _ measurableSpace (Measure.dirac x) fun (x : ℝ) ↦ (fun (ω : ℝ) ↦ rexp (t * id ω)) x) = rexp (x * t)
⊢ mgf X μ t = rexp (x * t)
have rw₃ : rexp (t * id x) = rexp (x * t)
Tactic: rw [← mgf_id_map (.of_map_ne_zero <| IsProbabilityMeasure.ne_zero _), mgf, hX, integral_dirac,
    mul_comm, id_def]
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
x : ℝ
hX : Eq (α := Measure ℝ) (Measure.map X μ) (Measure.dirac x)
t : ℝ
this : IsProbabilityMeasure (m0 := measurableSpace) (Measure.map X μ)
rw : mgf (m := measurableSpace) id (Measure.map X μ) t = rexp (x * t)
rw₁ :
  (@integral _ _ _ _ measurableSpace (Measure.map X μ) fun (x : ℝ) ↦ (fun (ω : ℝ) ↦ rexp (t * id ω)) x) = rexp (x * t)
rw₂ :
  (@integral _ _ _ _ measurableSpace (Measure.dirac x) fun (x : ℝ) ↦ (fun (ω : ℝ) ↦ rexp (t * id ω)) x) = rexp (x * t)
rw₃ : rexp (t * id x) = rexp (x * t)
⊢ mgf X μ t = rexp (x * t)
have rw₄ : rexp (id x * t) = rexp (x * t)
Tactic: rw [← mgf_id_map (.of_map_ne_zero <| IsProbabilityMeasure.ne_zero _), mgf, hX, integral_dirac,
    mul_comm, id_def]
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
x : ℝ
hX : Eq (α := Measure ℝ) (Measure.map X μ) (Measure.dirac x)
t : ℝ
this : IsProbabilityMeasure (m0 := measurableSpace) (Measure.map X μ)
rw : mgf (m := measurableSpace) id (Measure.map X μ) t = rexp (x * t)
rw₁ :
  (@integral _ _ _ _ measurableSpace (Measure.map X μ) fun (x : ℝ) ↦ (fun (ω : ℝ) ↦ rexp (t * id ω)) x) = rexp (x * t)
rw₂ :
  (@integral _ _ _ _ measurableSpace (Measure.dirac x) fun (x : ℝ) ↦ (fun (ω : ℝ) ↦ rexp (t * id ω)) x) = rexp (x * t)
rw₃ : rexp (t * id x) = rexp (x * t)
rw₄ : rexp (id x * t) = rexp (x * t)
⊢ mgf X μ t = rexp (x * t)
have rw₅ : rexp (x * t) = rexp (x * t)
Tactic: rw [← mgf_id_map (.of_map_ne_zero <| IsProbabilityMeasure.ne_zero _), mgf, hX, integral_dirac,
    mul_comm, id_def]
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
t : ℝ
inst : MeasurableSingletonClass Ω
ω : Ω
⊢ mgf (m := m) X (Measure.dirac ω) t = rexp (t * X ω)
have rw : (@integral _ _ _ _ m (Measure.dirac ω) fun (x : Ω) ↦ (fun (ω : Ω) ↦ rexp (t * X ω)) x) = rexp (t * X ω)
Tactic: rw [mgf, integral_dirac]
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
t : ℝ
inst : MeasurableSingletonClass Ω
ω : Ω
rw : (@integral _ _ _ _ m (Measure.dirac ω) fun (x : Ω) ↦ (fun (ω : Ω) ↦ rexp (t * X ω)) x) = rexp (t * X ω)
⊢ mgf (m := m) X (Measure.dirac ω) t = rexp (t * X ω)
have rw₁ : rexp (t * X ω) = rexp (t * X ω)
Tactic: rw [mgf, integral_dirac]
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
inst : IsFiniteMeasure μ
X : Ω → ℝ
t b : ℝ
ht : 0 ≤ t
hX : AEMeasurable X μ
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ≤ b
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
have refine : ∀ᵐ (ω : Ω) ∂μ, rexp (t * X ω) ∈ Set.Icc 0 (rexp (t * b))
Tactic: refine .of_mem_Icc 0 (rexp (t * b)) (measurable_exp.comp_aemeasurable (hX.const_mul t)) ?_
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
inst : IsFiniteMeasure μ
X : Ω → ℝ
t b : ℝ
ht : 0 ≤ t
hX : AEMeasurable X μ
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ≤ b
⊢ ∀ᵐ (ω : Ω) ∂μ, rexp (t * X ω) ∈ Set.Icc 0 (rexp (t * b))
have h : ∀ (ω : Ω) (hb : X ω ≤ b), rexp (t * X ω) ∈ Set.Icc 0 (rexp (t * b))
Tactic: filter_upwards [hb] with ω hb