awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
h : 0 ∈ interior (integrableExpSet X μ)
p : ℝ≥0
hX : AEMeasurable X μ
hp_zero : ¬p = 0
⊢ MemLp X (↑p : ℝ≥0∞) μ
have neg : Integrable (ε := ℝ) (fun (x : Ω) ↦ ‖X x‖ ^ (↑p : ℝ≥0∞).toReal) μ
Tactic: rw [← integrable_norm_rpow_iff hX.aestronglyMeasurable (mod_cast hp_zero) (by simp)]
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
h : 0 ∈ interior (integrableExpSet X μ)
p : ℝ≥0
hX : AEMeasurable X μ
hp_zero : ¬p = 0
⊢ Integrable (ε := ℝ) (fun (x : Ω) ↦ ‖X x‖ ^ (↑p : ℝ≥0∞).toReal) μ
have neg : Integrable (ε := ℝ) (fun (x : Ω) ↦ |X x| ^ (↑p : ℝ)) μ
Tactic: simp only [norm_eq_abs, ENNReal.coe_toReal]
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hX : AEMeasurable X μ
hz : z.re ∈ integrableExpSet X μ
⊢ Integrable (ε := ℂ) (fun (ω : Ω) ↦ cexp (z * (↑(X ω) : ℂ))) μ
have rw : Integrable (ε := ℝ) (fun (a : Ω) ↦ ‖cexp (z * (↑(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 Ω
z : ℂ
hX : AEMeasurable X μ
hz : z.re ∈ integrableExpSet X μ
rw : Integrable (ε := ℝ) (fun (a : Ω) ↦ ‖cexp (z * (↑(X a) : ℂ))‖) μ
⊢ Integrable (ε := ℂ) (fun (ω : Ω) ↦ cexp (z * (↑(X ω) : ℂ))) μ
have rw₁ : AEStronglyMeasurable (β := ℂ) (fun (ω : Ω) ↦ cexp (z * (↑(X ω) : ℂ))) μ
Tactic: rw [← integrable_norm_iff]
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (hypothesis)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
p : ℝ
hp : 0 ≤ p
⊢ Integrable (ε := ℂ) (fun (ω : Ω) ↦ (↑(|X ω| ^ p) : ℂ) * cexp (z * (↑(X ω) : ℂ))) μ
have hX : AEMeasurable X μ
Tactic: have hX : AEMeasurable X μ := aemeasurable_of_mem_interior_integrableExpSet hz
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
p : ℝ
hp : 0 ≤ p
hX : AEMeasurable X μ
⊢ Integrable (ε := ℂ) (fun (ω : Ω) ↦ (↑(|X ω| ^ p) : ℂ) * cexp (z * (↑(X ω) : ℂ))) μ
have rw : Integrable (ε := ℝ) (fun (a : Ω) ↦ ‖(↑(|X a| ^ p) : ℂ) * cexp (z * (↑(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 Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
p : ℝ
hp : 0 ≤ p
hX : AEMeasurable X μ
rw : Integrable (ε := ℝ) (fun (a : Ω) ↦ ‖(↑(|X a| ^ p) : ℂ) * cexp (z * (↑(X a) : ℂ))‖) μ
⊢ Integrable (ε := ℂ) (fun (ω : Ω) ↦ (↑(|X ω| ^ p) : ℂ) * cexp (z * (↑(X ω) : ℂ))) μ
have rw₁ : AEStronglyMeasurable (β := ℂ) (fun (ω : Ω) ↦ (↑(|X ω| ^ p) : ℂ) * cexp (z * (↑(X ω) : ℂ))) μ
Tactic: rw [← integrable_norm_iff]
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
⊢ Integrable (ε := ℂ) (fun (ω : Ω) ↦ (↑|X ω| : ℂ) ^ n * cexp (z * (↑(X ω) : ℂ))) μ
have h : ∀ (x : Ω), (↑|X x| : ℂ) ^ n = (↑(HPow.hPow (β := ℝ) |X x| (↑n : ℝ)) : ℂ)
Tactic: convert! integrable_rpow_abs_mul_cexp_of_re_mem_interior_integrableExpSet hz (Nat.cast_nonneg n)
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (hypothesis)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
p : ℝ
hp : 0 ≤ p
⊢ Integrable (ε := ℂ) (fun (ω : Ω) ↦ (↑(X ω ^ p) : ℂ) * cexp (z * (↑(X ω) : ℂ))) μ
have hX : AEMeasurable X μ
Tactic: have hX : AEMeasurable X μ := aemeasurable_of_mem_interior_integrableExpSet hz
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
p : ℝ
hp : 0 ≤ p
hX : AEMeasurable X μ
⊢ Integrable (ε := ℂ) (fun (ω : Ω) ↦ (↑(X ω ^ p) : ℂ) * cexp (z * (↑(X ω) : ℂ))) μ
have rw : Integrable (ε := ℝ) (fun (a : Ω) ↦ ‖(↑(X a ^ p) : ℂ) * cexp (z * (↑(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 Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
p : ℝ
hp : 0 ≤ p
hX : AEMeasurable X μ
rw : Integrable (ε := ℝ) (fun (a : Ω) ↦ ‖(↑(X a ^ p) : ℂ) * cexp (z * (↑(X a) : ℂ))‖) μ
⊢ Integrable (ε := ℂ) (fun (ω : Ω) ↦ (↑(X ω ^ p) : ℂ) * cexp (z * (↑(X ω) : ℂ))) μ
have rw₁ : AEStronglyMeasurable (β := ℂ) (fun (ω : Ω) ↦ (↑(X ω ^ p) : ℂ) * cexp (z * (↑(X ω) : ℂ))) μ
Tactic: rw [← integrable_norm_iff]
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
p : ℝ
hp : 0 ≤ p
hX : AEMeasurable X μ
⊢ Integrable (ε := ℝ) (fun (a : Ω) ↦ ‖(↑(X a ^ p) : ℂ) * cexp (z * (↑(X a) : ℂ))‖) μ
have simp : Integrable (ε := ℝ) (fun (a : Ω) ↦ ‖X a ^ p‖ * rexp (z.re * X a)) μ
Tactic: simp only [norm_mul, norm_real, Complex.norm_exp, mul_re, ofReal_re,
    ofReal_im, mul_zero, sub_zero]
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
p : ℝ
hp : 0 ≤ p
hX : AEMeasurable X μ
⊢ Integrable (ε := ℝ) (fun (a : Ω) ↦ ‖X a ^ p‖ * rexp (z.re * X a)) μ
have refine_1 : AEStronglyMeasurable (β := ℝ) (fun (a : Ω) ↦ ‖X a ^ p‖ * rexp (z.re * X a)) μ
Tactic: refine (integrable_rpow_abs_mul_exp_of_mem_interior_integrableExpSet hz hp).mono ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
p : ℝ
hp : 0 ≤ p
hX : AEMeasurable X μ
refine_1 : AEStronglyMeasurable (β := ℝ) (fun (a : Ω) ↦ ‖X a ^ p‖ * rexp (z.re * X a)) μ
⊢ Integrable (ε := ℝ) (fun (a : Ω) ↦ ‖X a ^ p‖ * rexp (z.re * X a)) μ
have refine_2 : ∀ᵐ (a : Ω) ∂μ, ‖‖X a ^ p‖ * rexp (z.re * X a)‖ ≤ ‖|X a| ^ p * rexp (z.re * X a)‖
Tactic: refine (integrable_rpow_abs_mul_exp_of_mem_interior_integrableExpSet hz hp).mono ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
p : ℝ
hp : 0 ≤ p
hX : AEMeasurable X μ
⊢ ∀ᵐ (a : Ω) ∂μ, ‖‖X a ^ p‖ * rexp (z.re * X a)‖ ≤ ‖|X a| ^ p * rexp (z.re * X a)‖
have refine_2 : ∀ (ω : Ω), ‖‖X ω ^ p‖ * rexp (z.re * X ω)‖ ≤ ‖|X ω| ^ p * rexp (z.re * X ω)‖
Tactic: refine ae_of_all _ fun ω ↦ ?_
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
p : ℝ
hp : 0 ≤ p
hX : AEMeasurable X μ
ω : Ω
⊢ ‖‖X ω ^ p‖ * rexp (z.re * X ω)‖ ≤ ‖|X ω| ^ p * rexp (z.re * X ω)‖
have refine_2 : |(|X ω ^ p|)| * rexp (z.re * X ω) ≤ ||X ω| ^ p| * rexp (z.re * X ω)
Tactic: simp only [norm_mul, Real.norm_eq_abs, Real.abs_exp]
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
p : ℝ
hp : 0 ≤ p
hX : AEMeasurable X μ
ω : Ω
⊢ |(|X ω ^ p|)| * rexp (z.re * X ω) ≤ ||X ω| ^ p| * rexp (z.re * X ω)
have refine_2 : |X ω ^ p| ≤ |X ω| ^ p
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
⊢ Integrable (ε := ℂ) (fun (ω : Ω) ↦ (↑(X ω) : ℂ) ^ n * cexp (z * (↑(X ω) : ℂ))) μ
have h : ∀ (x : Ω), (↑(X x) : ℂ) ^ n = (↑(HPow.hPow (β := ℝ) (X x) (↑n : ℝ)) : ℂ)
Tactic: convert! integrable_rpow_mul_cexp_of_re_mem_interior_integrableExpSet hz (Nat.cast_nonneg n)
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t_1 : ℝ
ht : t_1 ∈ interior (integrableExpSet X μ)
n_1 n : ℕ
t : ℝ
ht' : t ∈ interior (integrableExpSet X μ)
⊢ Complex.re (∫ (ω : Ω), (↑(X ω) : ℂ) ^ n * Complex.exp ((↑t : ℂ) * (↑(X ω) : ℂ)) ∂μ) =
    ∫ (ω : Ω), X ω ^ n * rexp (t * X ω) ∂μ
have rw : Eq (α := ℝ) (∫ (x : Ω), (RCLike.re : (a : ℂ) → ℝ) ((↑(X x) : ℂ) ^ n * Complex.exp ((↑t : ℂ) * (↑(X x) : ℂ))) ∂μ)
  (∫ (ω : Ω), X ω ^ n * rexp (t * X ω) ∂μ)
Tactic: rw [← RCLike.re_eq_complex_re, ← integral_re]
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t_1 : ℝ
ht : t_1 ∈ interior (integrableExpSet X μ)
n_1 n : ℕ
t : ℝ
ht' : t ∈ interior (integrableExpSet X μ)
rw :
  Eq (α := ℝ) (∫ (x : Ω), (RCLike.re : (a : ℂ) → ℝ) ((↑(X x) : ℂ) ^ n * Complex.exp ((↑t : ℂ) * (↑(X x) : ℂ))) ∂μ)
    (∫ (ω : Ω), X ω ^ n * rexp (t * X ω) ∂μ)
⊢ Complex.re (∫ (ω : Ω), (↑(X ω) : ℂ) ^ n * Complex.exp ((↑t : ℂ) * (↑(X ω) : ℂ)) ∂μ) =
    ∫ (ω : Ω), X ω ^ n * rexp (t * X ω) ∂μ
have rw₁ : Integrable (ε := ℂ) (fun (ω : Ω) ↦ (↑(X ω) : ℂ) ^ n * Complex.exp ((↑t : ℂ) * (↑(X ω) : ℂ))) μ
Tactic: rw [← RCLike.re_eq_complex_re, ← integral_re]
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t_1 : ℝ
ht : t_1 ∈ interior (integrableExpSet X μ)
n_1 n : ℕ
t : ℝ
ht' : t ∈ interior (integrableExpSet X μ)
⊢ Eq (α := ℝ) (∫ (x : Ω), (RCLike.re : (a : ℂ) → ℝ) ((↑(X x) : ℂ) ^ n * Complex.exp ((↑t : ℂ) * (↑(X x) : ℂ))) ∂μ)
    (∫ (ω : Ω), X ω ^ n * rexp (t * X ω) ∂μ)
have norm_cast : Eq (α := ℝ) (∫ (x : Ω), (RCLike.re : (a : ℂ) → ℝ) (↑(X x ^ n * rexp (t * X x)) : ℂ) ∂μ)
  (∫ (ω : Ω), X ω ^ n * rexp (t * X ω) ∂μ)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t_1 : ℝ
ht : t_1 ∈ interior (integrableExpSet X μ)
n_1 n : ℕ
t : ℝ
ht' : t ∈ interior (integrableExpSet X μ)
⊢ Integrable (ε := ℂ) (fun (ω : Ω) ↦ (↑(X ω) : ℂ) ^ n * Complex.exp ((↑t : ℂ) * (↑(X ω) : ℂ))) μ
have refine : (↑t : ℂ).re ∈ interior (integrableExpSet X μ)
Tactic: refine integrable_pow_mul_cexp_of_re_mem_interior_integrableExpSet ?_ n
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (hypothesis)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
n : ℕ
⊢ HasDerivAt (F := ℝ) (fun (t : ℝ) ↦ ∫ (x : Ω), (fun (ω : Ω) ↦ X ω ^ n * rexp (t * X ω)) x ∂μ)
    (∫ (x : Ω), (fun (ω : Ω) ↦ X ω ^ (n + 1) * rexp (t * X ω)) x ∂μ) t
have h_re_of_mem : ∀ (n : ℕ) (t : ℝ) (ht' : t ∈ interior (integrableExpSet X μ)),
  Complex.re (∫ (ω : Ω), (↑(X ω) : ℂ) ^ n * Complex.exp ((↑t : ℂ) * (↑(X ω) : ℂ)) ∂μ) =
    ∫ (ω : Ω), X ω ^ n * rexp (t * X ω) ∂μ
Tactic: have h_re_of_mem n t (ht' : t ∈ interior (integrableExpSet X μ)) :
      (∫ ω, X ω ^ n * Complex.exp (t * X ω) ∂μ).re = ∫ ω, X ω ^ n * exp (t * X ω) ∂μ := by
    rw [← RCLike.re_eq_complex_re, ← integral_re]
    · norm_cast
    · refine integrable_pow_mul_cexp_of_re_mem_interior_integrableExpSet ?_ n
      simpa using ht'
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
n_1 : ℕ
h_re_of_mem :
  ∀ (n : ℕ) (t : ℝ) (ht' : t ∈ interior (integrableExpSet X μ)),
    Complex.re (∫ (ω : Ω), (↑(X ω) : ℂ) ^ n * Complex.exp ((↑t : ℂ) * (↑(X ω) : ℂ)) ∂μ) =
      ∫ (ω : Ω), X ω ^ n * rexp (t * X ω) ∂μ
n : ℕ
⊢ ∀ᶠ (t' : ℝ) in 𝓝 t,
    Complex.re (∫ (ω : Ω), (↑(X ω) : ℂ) ^ n * Complex.exp ((↑t' : ℂ) * (↑(X ω) : ℂ)) ∂μ) =
      ∫ (ω : Ω), X ω ^ n * rexp (t' * X ω) ∂μ
have h : ∀ (a : ℝ),
  Membership.mem (γ := Set ℝ)
    {x : ℝ |
      Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ x ∈ interior (integrableExpSet X μ)) x} x →
        Membership.mem (γ := Set ℝ)
          {x : ℝ |
            (fun (t' : ℝ) ↦
                Complex.re (∫ (ω : Ω), (↑(X ω) : ℂ) ^ n * Complex.exp ((↑t' : ℂ) * (↑(X ω) : ℂ)) ∂μ) =
                  ∫ (ω : Ω), X ω ^ n * rexp (t' * X ω) ∂μ)
              x}
          x}
    a
Tactic: filter_upwards [isOpen_interior.eventually_mem ht] with t ht' using h_re_of_mem n t ht'
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
n_1 : ℕ
h_re_of_mem :
  ∀ (n : ℕ) (t : ℝ) (ht' : t ∈ interior (integrableExpSet X μ)),
    Complex.re (∫ (ω : Ω), (↑(X ω) : ℂ) ^ n * Complex.exp ((↑t : ℂ) * (↑(X ω) : ℂ)) ∂μ) =
      ∫ (ω : Ω), X ω ^ n * rexp (t * X ω) ∂μ
n : ℕ
h :
  ∀ (a : ℝ),
    Membership.mem (γ := Set ℝ)
      {x : ℝ |
        Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ x ∈ interior (integrableExpSet X μ)) x} x →
          Membership.mem (γ := Set ℝ)
            {x : ℝ |
              (fun (t' : ℝ) ↦
                  Complex.re (∫ (ω : Ω), (↑(X ω) : ℂ) ^ n * Complex.exp ((↑t' : ℂ) * (↑(X ω) : ℂ)) ∂μ) =
                    ∫ (ω : Ω), X ω ^ n * rexp (t' * X ω) ∂μ)
                x}
            x}
      a
⊢ ∀ᶠ (t' : ℝ) in 𝓝 t,
    Complex.re (∫ (ω : Ω), (↑(X ω) : ℂ) ^ n * Complex.exp ((↑t' : ℂ) * (↑(X ω) : ℂ)) ∂μ) =
      ∫ (ω : Ω), X ω ^ n * rexp (t' * X ω) ∂μ
have h₁ : ∀ a ∈ interior (integrableExpSet X μ),
  Complex.re (∫ (ω : Ω), (↑(X ω) : ℂ) ^ n * Complex.exp ((↑a : ℂ) * (↑(X ω) : ℂ)) ∂μ) =
    ∫ (ω : Ω), X ω ^ n * rexp (a * X ω) ∂μ
Tactic: filter_upwards [isOpen_interior.eventually_mem ht] with t ht' using h_re_of_mem n t ht'
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (hypothesis)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
n : ℕ
h_re_of_mem :
  ∀ (n : ℕ) (t : ℝ) (ht' : t ∈ interior (integrableExpSet X μ)),
    Complex.re (∫ (ω : Ω), (↑(X ω) : ℂ) ^ n * Complex.exp ((↑t : ℂ) * (↑(X ω) : ℂ)) ∂μ) =
      ∫ (ω : Ω), X ω ^ n * rexp (t * X ω) ∂μ
⊢ HasDerivAt (F := ℝ) (fun (t : ℝ) ↦ ∫ (x : Ω), (fun (ω : Ω) ↦ X ω ^ n * rexp (t * X ω)) x ∂μ)
    (∫ (x : Ω), (fun (ω : Ω) ↦ X ω ^ (n + 1) * rexp (t * X ω)) x ∂μ) t
have h_re : ∀ (n : ℕ),
  ∀ᶠ (t' : ℝ) in 𝓝 t,
    Complex.re (∫ (ω : Ω), (↑(X ω) : ℂ) ^ n * Complex.exp ((↑t' : ℂ) * (↑(X ω) : ℂ)) ∂μ) =
      ∫ (ω : Ω), X ω ^ n * rexp (t' * X ω) ∂μ
Tactic: have h_re n : ∀ᶠ t' : ℝ in 𝓝 t, (∫ ω, X ω ^ n * Complex.exp (t' * X ω) ∂μ).re
      = ∫ ω, X ω ^ n * exp (t' * X ω) ∂μ := by
    filter_upwards [isOpen_interior.eventually_mem ht] with t ht' using h_re_of_mem n t ht'
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
n : ℕ
h_re_of_mem :
  ∀ (n : ℕ) (t : ℝ) (ht' : t ∈ interior (integrableExpSet X μ)),
    Complex.re (∫ (ω : Ω), (↑(X ω) : ℂ) ^ n * Complex.exp ((↑t : ℂ) * (↑(X ω) : ℂ)) ∂μ) =
      ∫ (ω : Ω), X ω ^ n * rexp (t * X ω) ∂μ
h_re :
  ∀ (n : ℕ),
    ∀ᶠ (t' : ℝ) in 𝓝 t,
      Complex.re (∫ (ω : Ω), (↑(X ω) : ℂ) ^ n * Complex.exp ((↑t' : ℂ) * (↑(X ω) : ℂ)) ∂μ) =
        ∫ (ω : Ω), X ω ^ n * rexp (t' * X ω) ∂μ
⊢ HasDerivAt (F := ℝ) (fun (t : ℝ) ↦ ∫ (x : Ω), (fun (ω : Ω) ↦ X ω ^ n * rexp (t * X ω)) x ∂μ)
    (∫ (x : Ω), (fun (ω : Ω) ↦ X ω ^ (n + 1) * rexp (t * X ω)) x ∂μ) t
have rw : HasDerivAt (fun (x : ℝ) ↦ Complex.re (∫ (ω : Ω), (↑(X ω) : ℂ) ^ n * Complex.exp ((↑x : ℂ) * (↑(X ω) : ℂ)) ∂μ))
  (Complex.re (∫ (ω : Ω), (↑(X ω) : ℂ) ^ (n + 1) * Complex.exp ((↑t : ℂ) * (↑(X ω) : ℂ)) ∂μ)) t
Tactic: rw [← EventuallyEq.hasDerivAt_iff (h_re _), ← h_re_of_mem _ t ht]
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
h : t ∈ interior (integrableExpSet X μ)
⊢ HasDerivAt (mgf X μ) (∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (t * X ω)) x ∂μ) t
have h₁ : ∀ (x : ℝ), mgf X μ x = ∫ (x_1 : Ω), (fun (ω : Ω) ↦ HPow.hPow (β := ℕ) (X ω) 0 * rexp (x * X ω)) x_1 ∂μ
Tactic: convert! hasDerivAt_integral_pow_mul_exp_real h 0
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
h : t ∈ interior (integrableExpSet X μ)
h₁ : ∀ (x : ℝ), mgf X μ x = ∫ (x_1 : Ω), (fun (ω : Ω) ↦ HPow.hPow (β := ℕ) (X ω) 0 * rexp (x * X ω)) x_1 ∂μ
⊢ HasDerivAt (mgf X μ) (∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (t * X ω)) x ∂μ) t
have h₂ : ∀ (x x : Ω), X x = X x ^ HAdd.hAdd (α := ℕ) 0 1
Tactic: convert! hasDerivAt_integral_pow_mul_exp_real h 0
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
n : ℕ
hn :
  ∀ {t : ℝ} (ht : t ∈ interior (integrableExpSet X μ)),
    HasDerivAt (iteratedDeriv n (mgf X μ)) (∫ (x : Ω), (fun (ω : Ω) ↦ X ω ^ (n + 1) * rexp (t * X ω)) x ∂μ) t
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
⊢ HasDerivAt (iteratedDeriv (n + 1) (mgf X μ)) (∫ (x : Ω), (fun (ω : Ω) ↦ X ω ^ (n + 1 + 1) * rexp (t * X ω)) x ∂μ) t
have succ : HasDerivAt (deriv (iteratedDeriv n (mgf X μ))) (∫ (x : Ω), (fun (ω : Ω) ↦ X ω ^ (n + 1 + 1) * rexp (t * X ω)) x ∂μ) t
Tactic: rw [iteratedDeriv_succ]
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (hypothesis)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
n : ℕ
hn :
  ∀ {t : ℝ} (ht : t ∈ interior (integrableExpSet X μ)),
    HasDerivAt (iteratedDeriv n (mgf X μ)) (∫ (x : Ω), (fun (ω : Ω) ↦ X ω ^ (n + 1) * rexp (t * X ω)) x ∂μ) t
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
⊢ deriv (iteratedDeriv n (mgf X μ)) =ᶠ[𝓝 t] fun (t : ℝ) ↦ ∫ (x : Ω), (fun (ω : Ω) ↦ X ω ^ (n + 1) * rexp (t * X ω)) x ∂μ
have h_mem : ∀ᶠ (y : ℝ) in 𝓝 t, y ∈ interior (integrableExpSet X μ)
Tactic: have h_mem : ∀ᶠ y in 𝓝 t, y ∈ interior (integrableExpSet X μ) :=
        isOpen_interior.eventually_mem ht
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
n : ℕ
hn :
  ∀ {t : ℝ} (ht : t ∈ interior (integrableExpSet X μ)),
    HasDerivAt (iteratedDeriv n (mgf X μ)) (∫ (x : Ω), (fun (ω : Ω) ↦ X ω ^ (n + 1) * rexp (t * X ω)) x ∂μ) t
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
h_mem : ∀ᶠ (y : ℝ) in 𝓝 t, y ∈ interior (integrableExpSet X μ)
⊢ deriv (iteratedDeriv n (mgf X μ)) =ᶠ[𝓝 t] fun (t : ℝ) ↦ ∫ (x : Ω), (fun (ω : Ω) ↦ X ω ^ (n + 1) * rexp (t * X ω)) x ∂μ
have h : ∀ (a : ℝ),
  Membership.mem (γ := Set ℝ)
    {x : ℝ |
      Membership.mem (γ := Set ℝ) {x : ℝ | (fun (y : ℝ) ↦ y ∈ interior (integrableExpSet X μ)) x} x →
        Membership.mem (γ := Set ℝ)
          {x : ℝ |
            (fun (x : ℝ) ↦
                deriv (iteratedDeriv n (mgf X μ)) x =
                  (fun (t : ℝ) ↦ (∫ (x : Ω), (fun (ω : Ω) ↦ X ω ^ (n + 1) * rexp (t * X ω)) x ∂μ : ℝ)) x)
              x}
          x}
    a
Tactic: filter_upwards [h_mem] with y hy using HasDerivAt.deriv (hn hy)
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
n : ℕ
hn :
  ∀ {t : ℝ} (ht : t ∈ interior (integrableExpSet X μ)),
    HasDerivAt (iteratedDeriv n (mgf X μ)) (∫ (x : Ω), (fun (ω : Ω) ↦ X ω ^ (n + 1) * rexp (t * X ω)) x ∂μ) t
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
h_mem : ∀ᶠ (y : ℝ) in 𝓝 t, y ∈ interior (integrableExpSet X μ)
h :
  ∀ (a : ℝ),
    Membership.mem (γ := Set ℝ)
      {x : ℝ |
        Membership.mem (γ := Set ℝ) {x : ℝ | (fun (y : ℝ) ↦ y ∈ interior (integrableExpSet X μ)) x} x →
          Membership.mem (γ := Set ℝ)
            {x : ℝ |
              (fun (x : ℝ) ↦
                  deriv (iteratedDeriv n (mgf X μ)) x =
                    (fun (t : ℝ) ↦ (∫ (x : Ω), (fun (ω : Ω) ↦ X ω ^ (n + 1) * rexp (t * X ω)) x ∂μ : ℝ)) x)
                x}
            x}
      a
⊢ deriv (iteratedDeriv n (mgf X μ)) =ᶠ[𝓝 t] fun (t : ℝ) ↦ ∫ (x : Ω), (fun (ω : Ω) ↦ X ω ^ (n + 1) * rexp (t * X ω)) x ∂μ
have h₁ : ∀ a ∈ interior (integrableExpSet X μ),
  deriv (iteratedDeriv n (mgf X μ)) a = ∫ (x : Ω), X x ^ (n + 1) * rexp (a * X x) ∂μ
Tactic: filter_upwards [h_mem] with y hy using HasDerivAt.deriv (hn hy)
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (hypothesis)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
n : ℕ
hn :
  ∀ {t : ℝ} (ht : t ∈ interior (integrableExpSet X μ)),
    HasDerivAt (iteratedDeriv n (mgf X μ)) (∫ (x : Ω), (fun (ω : Ω) ↦ X ω ^ (n + 1) * rexp (t * X ω)) x ∂μ) t
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
⊢ HasDerivAt (deriv (iteratedDeriv n (mgf X μ))) (∫ (x : Ω), (fun (ω : Ω) ↦ X ω ^ (n + 1 + 1) * rexp (t * X ω)) x ∂μ) t
have this : deriv (iteratedDeriv n (mgf X μ)) =ᶠ[𝓝 t] fun (t : ℝ) ↦ ∫ (x : Ω), (fun (ω : Ω) ↦ X ω ^ (n + 1) * rexp (t * X ω)) x ∂μ
Tactic: have : deriv (iteratedDeriv n (mgf X μ))
        =ᶠ[𝓝 t] fun t ↦ μ[fun ω ↦ X ω ^ (n + 1) * exp (t * X ω)] := by
      have h_mem : ∀ᶠ y in 𝓝 t, y ∈ interior (integrableExpSet X μ) :=
        isOpen_interior.eventually_mem ht
      filter_upwards [h_mem] with y hy using HasDerivAt.deriv (hn hy)
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
n : ℕ
hn :
  ∀ {t : ℝ} (ht : t ∈ interior (integrableExpSet X μ)),
    HasDerivAt (iteratedDeriv n (mgf X μ)) (∫ (x : Ω), (fun (ω : Ω) ↦ X ω ^ (n + 1) * rexp (t * X ω)) x ∂μ) t
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
this :
  deriv (iteratedDeriv n (mgf X μ)) =ᶠ[𝓝 t] fun (t : ℝ) ↦ ∫ (x : Ω), (fun (ω : Ω) ↦ X ω ^ (n + 1) * rexp (t * X ω)) x ∂μ
⊢ HasDerivAt (deriv (iteratedDeriv n (mgf X μ))) (∫ (x : Ω), (fun (ω : Ω) ↦ X ω ^ (n + 1 + 1) * rexp (t * X ω)) x ∂μ) t
have succ : HasDerivAt (F := ℝ) (fun (t : ℝ) ↦ ∫ (x : Ω), (fun (ω : Ω) ↦ X ω ^ (n + 1) * rexp (t * X ω)) x ∂μ)
  (∫ (x : Ω), (fun (ω : Ω) ↦ X ω ^ (n + 1 + 1) * rexp (t * X ω)) x ∂μ) t
Tactic: rw [EventuallyEq.hasDerivAt_iff this]
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
n : ℕ
⊢ HasDerivAt (iteratedDeriv n (mgf X μ)) (∫ (x : Ω), (fun (ω : Ω) ↦ X ω ^ (n + 1) * rexp (t * X ω)) x ∂μ) t
have zero : ∀ {t : ℝ} (ht : t ∈ interior (integrableExpSet X μ)),
  HasDerivAt (iteratedDeriv 0 (mgf X μ)) (∫ (x : Ω), (fun (ω : Ω) ↦ X ω ^ HAdd.hAdd (α := ℕ) 0 1 * rexp (t * X ω)) x ∂μ)
    t
Tactic: induction n generalizing t with
  | zero => simp [hasDerivAt_mgf ht]
  | succ n hn =>
    rw [iteratedDeriv_succ]
    have : deriv (iteratedDeriv n (mgf X μ))
        =ᶠ[𝓝 t] fun t ↦ μ[fun ω ↦ X ω ^ (n + 1) * exp (t * X ω)] := by
      have h_mem : ∀ᶠ y in 𝓝 t, y ∈ interior (integrableExpSet X μ) :=
        isOpen_interior.eventually_mem ht
      filter_upwards [h_mem] with y hy using HasDerivAt.deriv (hn hy)
    rw [EventuallyEq.hasDerivAt_iff this]
    exact hasDerivAt_integral_pow_mul_exp_real ht (n + 1)
Cleared hypotheses: t, ht, n