awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
h : ∀ (x : Ω), (↑(X x) : ℂ) ^ n = (↑(HPow.hPow (β := ℝ) (X x) (↑n : ℝ)) : ℂ)
⊢ Integrable (ε := ℂ) (fun (ω : Ω) ↦ (↑(X ω) : ℂ) ^ n * cexp (z * (↑(X ω) : ℂ))) μ

Tactic:
convert! integrable_rpow_mul_cexp_of_re_mem_interior_integrableExpSet hz (Nat.cast_nonneg n)

Premises used: ProbabilityTheory.integrable_rpow_mul_cexp_of_re_mem_interior_integrableExpSet, Nat.cast_nonneg
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
x : Ω
⊢ (↑(X x) : ℂ) ^ n = (↑(HPow.hPow (β := ℝ) (X x) (↑n : ℝ)) : ℂ)

Tactic:
simp
-- Module: Mathlib.Probability.Moments.MGFAnalytic
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 ω) ∂μ)
rw₁ : Integrable (ε := ℂ) (fun (ω : Ω) ↦ (↑(X ω) : ℂ) ^ n * Complex.exp ((↑t : ℂ) * (↑(X ω) : ℂ))) μ
⊢ Complex.re (∫ (ω : Ω), (↑(X ω) : ℂ) ^ n * Complex.exp ((↑t : ℂ) * (↑(X ω) : ℂ)) ∂μ) =
    ∫ (ω : Ω), X ω ^ n * rexp (t * X ω) ∂μ

Tactic:
rw [← RCLike.re_eq_complex_re, ← integral_re]

Premises used: RCLike.re_eq_complex_re, integral_re
-- Module: Mathlib.Probability.Moments.MGFAnalytic
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 μ)
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ :
  Eq (α := ℝ) (∫ (x : Ω), (RCLike.re : (a : ℂ) → ℝ) (↑(X x ^ n * rexp (t * X x)) : ℂ) ∂μ)
    (∫ (ω : Ω), X ω ^ n * rexp (t * X ω) ∂μ)
⊢ Eq (α := ℝ) (∫ (x : Ω), (RCLike.re : (a : ℂ) → ℝ) ((↑(X x) : ℂ) ^ n * Complex.exp ((↑t : ℂ) * (↑(X x) : ℂ))) ∂μ)
    (∫ (ω : Ω), X ω ^ n * rexp (t * X ω) ∂μ)

Tactic:
norm_cast
-- Module: Mathlib.Probability.Moments.MGFAnalytic
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 ω) : ℂ))) μ

Tactic:
integrable_pow_mul_cexp_of_re_mem_interior_integrableExpSet ?_ n

Premises used: ProbabilityTheory.integrable_pow_mul_cexp_of_re_mem_interior_integrableExpSet
-- Module: Mathlib.Probability.Moments.MGFAnalytic
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 μ)
refine : (↑t : ℂ).re ∈ interior (integrableExpSet X μ)
⊢ Integrable (ε := ℂ) (fun (ω : Ω) ↦ (↑(X ω) : ℂ) ^ n * Complex.exp ((↑t : ℂ) * (↑(X ω) : ℂ))) μ

Tactic:
refine integrable_pow_mul_cexp_of_re_mem_interior_integrableExpSet ?_ n

Premises used: ProbabilityTheory.integrable_pow_mul_cexp_of_re_mem_interior_integrableExpSet
-- Module: Mathlib.Probability.Moments.MGFAnalytic
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 μ)
⊢ (↑t : ℂ).re ∈ interior (integrableExpSet X μ)

Tactic:
simpa using ht'
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
n : ℕ
⊢ ∀ (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'
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t_1 : ℝ
ht : t_1 ∈ 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 : ℝ
ht' : t ∈ interior (integrableExpSet X μ)
⊢ Complex.re (∫ (ω : Ω), (↑(X ω) : ℂ) ^ n * Complex.exp ((↑t : ℂ) * (↑(X ω) : ℂ)) ∂μ) =
    ∫ (ω : Ω), X ω ^ n * rexp (t * X ω) ∂μ

Tactic:
h_re_of_mem n t ht'
-- Module: Mathlib.Probability.Moments.MGFAnalytic
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
h₁ h₂ :
  ∀ (t : ℝ) (ht' : t ∈ interior (integrableExpSet X μ)),
    Complex.re (∫ (ω : Ω), (↑(X ω) : ℂ) ^ n * Complex.exp ((↑t : ℂ) * (↑(X ω) : ℂ)) ∂μ) =
      ∫ (ω : Ω), X ω ^ n * rexp (t * X ω) ∂μ
⊢ ∀ᶠ (t' : ℝ) in 𝓝 t,
    Complex.re (∫ (ω : Ω), (↑(X ω) : ℂ) ^ n * Complex.exp ((↑t' : ℂ) * (↑(X ω) : ℂ)) ∂μ) =
      ∫ (ω : Ω), X ω ^ n * rexp (t' * X ω) ∂μ

Tactic:
filter_upwards [isOpen_interior.eventually_mem ht] with t ht' using h_re_of_mem n t ht'

Premises used: IsOpen.eventually_mem, isOpen_interior
-- Module: Mathlib.Probability.Moments.MGFAnalytic
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 ω) ∂μ
⊢ ∀ (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'
-- Module: Mathlib.Probability.Moments.MGFAnalytic
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 ω) ∂μ
rw :
  HasDerivAt (fun (x : ℝ) ↦ Complex.re (∫ (ω : Ω), (↑(X ω) : ℂ) ^ n * Complex.exp ((↑x : ℂ) * (↑(X ω) : ℂ)) ∂μ))
    (Complex.re (∫ (ω : Ω), (↑(X ω) : ℂ) ^ (n + 1) * Complex.exp ((↑t : ℂ) * (↑(X ω) : ℂ)) ∂μ)) t
⊢ HasDerivAt (F := ℝ) (fun (t : ℝ) ↦ ∫ (x : Ω), (fun (ω : Ω) ↦ X ω ^ n * rexp (t * X ω)) x ∂μ)
    (∫ (x : Ω), (fun (ω : Ω) ↦ X ω ^ (n + 1) * rexp (t * X ω)) x ∂μ) t

Tactic:
rw [← EventuallyEq.hasDerivAt_iff (h_re _), ← h_re_of_mem _ t ht]

Premises used: Filter.EventuallyEq.hasDerivAt_iff
-- Module: Mathlib.Probability.Moments.MGFAnalytic
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 ω) ∂μ
⊢ (↑t : ℂ).re ∈ interior (integrableExpSet X μ)

Tactic:
simp [ht]
-- Module: Mathlib.Probability.Moments.MGFAnalytic
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 (fun (x : ℝ) ↦ Complex.re (∫ (ω : Ω), (↑(X ω) : ℂ) ^ n * Complex.exp ((↑x : ℂ) * (↑(X ω) : ℂ)) ∂μ))
    (Complex.re (∫ (ω : Ω), (↑(X ω) : ℂ) ^ (n + 1) * Complex.exp ((↑t : ℂ) * (↑(X ω) : ℂ)) ∂μ)) t

Tactic:
exact (hasDerivAt_integral_pow_mul_exp (by simp [ht]) n).real_of_complex

Premises used: ProbabilityTheory.hasDerivAt_integral_pow_mul_exp, HasDerivAt.real_of_complex
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
h : t ∈ interior (integrableExpSet X μ)
⊢ HasDerivAt (F := ℝ) (fun (t : ℝ) ↦ ∫ (x : Ω), (fun (ω : Ω) ↦ HPow.hPow (β := ℕ) (X ω) 0 * rexp (t * X ω)) x ∂μ)
    (∫ (x : Ω), (fun (ω : Ω) ↦ X ω ^ HAdd.hAdd (α := ℕ) 0 1 * rexp (t * X ω)) x ∂μ) t

Tactic:
hasDerivAt_integral_pow_mul_exp_real h 0

Premises used: ProbabilityTheory.hasDerivAt_integral_pow_mul_exp_real, OfNat.ofNat
-- Module: Mathlib.Probability.Moments.MGFAnalytic
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 ∂μ
h₂ : ∀ (x x : Ω), X x = X x ^ HAdd.hAdd (α := ℕ) 0 1
⊢ HasDerivAt (mgf X μ) (∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (t * X ω)) x ∂μ) t

Tactic:
convert! hasDerivAt_integral_pow_mul_exp_real h 0

Premises used: ProbabilityTheory.hasDerivAt_integral_pow_mul_exp_real, OfNat.ofNat
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
h : t ∈ interior (integrableExpSet X μ)
x : ℝ
⊢ mgf X μ x = ∫ (x_1 : Ω), (fun (ω : Ω) ↦ HPow.hPow (β := ℕ) (X ω) 0 * rexp (x * X ω)) x_1 ∂μ

Tactic:
simp [mgf]

Premises used: ProbabilityTheory.mgf
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
h : t ∈ interior (integrableExpSet X μ)
x x_1 : Ω
⊢ X x_1 = X x_1 ^ HAdd.hAdd (α := ℕ) 0 1

Tactic:
simp
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
⊢ HasDerivAt (iteratedDeriv 0 (mgf X μ)) (∫ (x : Ω), (fun (ω : Ω) ↦ X ω ^ HAdd.hAdd (α := ℕ) 0 1 * rexp (t * X ω)) x ∂μ)
    t

Tactic:
simp [hasDerivAt_mgf ht]

Premises used: ProbabilityTheory.hasDerivAt_mgf
-- Module: Mathlib.Probability.Moments.MGFAnalytic
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 μ)
succ :
  HasDerivAt (deriv (iteratedDeriv n (mgf X μ))) (∫ (x : Ω), (fun (ω : Ω) ↦ X ω ^ (n + 1 + 1) * rexp (t * X ω)) x ∂μ) t
⊢ HasDerivAt (iteratedDeriv (n + 1) (mgf X μ)) (∫ (x : Ω), (fun (ω : Ω) ↦ X ω ^ (n + 1 + 1) * rexp (t * X ω)) x ∂μ) t

Tactic:
rw [iteratedDeriv_succ]

Premises used: iteratedDeriv_succ
-- Module: Mathlib.Probability.Moments.MGFAnalytic
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 μ)
⊢ ∀ᶠ (y : ℝ) in 𝓝 t, y ∈ interior (integrableExpSet X μ)

Tactic:
have h_mem : ∀ᶠ y in 𝓝 t, y ∈ interior (integrableExpSet X μ) :=
        isOpen_interior.eventually_mem ht
-- Module: Mathlib.Probability.Moments.MGFAnalytic
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 μ)
y : ℝ
hy : y ∈ interior (integrableExpSet X μ)
⊢ deriv (iteratedDeriv n (mgf X μ)) y = ∫ (x : Ω), X x ^ (n + 1) * rexp (y * X x) ∂μ

Tactic:
HasDerivAt.deriv (hn hy)

Premises used: HasDerivAt.deriv
-- Module: Mathlib.Probability.Moments.MGFAnalytic
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
h₁ h₂ :
  ∀ (y : ℝ) (hy : y ∈ interior (integrableExpSet X μ)),
    deriv (iteratedDeriv n (mgf X μ)) y = ∫ (x : Ω), X x ^ (n + 1) * rexp (y * X x) ∂μ
⊢ deriv (iteratedDeriv n (mgf X μ)) =ᶠ[𝓝 t] fun (t : ℝ) ↦ ∫ (x : Ω), (fun (ω : Ω) ↦ X ω ^ (n + 1) * rexp (t * X ω)) x ∂μ

Tactic:
filter_upwards [h_mem] with y hy using HasDerivAt.deriv (hn hy)
-- Module: Mathlib.Probability.Moments.MGFAnalytic
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 ∂μ

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)
-- Module: Mathlib.Probability.Moments.MGFAnalytic
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 ∂μ
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
⊢ HasDerivAt (deriv (iteratedDeriv n (mgf X μ))) (∫ (x : Ω), (fun (ω : Ω) ↦ X ω ^ (n + 1 + 1) * rexp (t * X ω)) x ∂μ) t

Tactic:
rw [EventuallyEq.hasDerivAt_iff this]

Premises used: Filter.EventuallyEq.hasDerivAt_iff
-- Module: Mathlib.Probability.Moments.MGFAnalytic
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 (F := ℝ) (fun (t : ℝ) ↦ ∫ (x : Ω), (fun (ω : Ω) ↦ X ω ^ (n + 1) * rexp (t * X ω)) x ∂μ)
    (∫ (x : Ω), (fun (ω : Ω) ↦ X ω ^ (n + 1 + 1) * rexp (t * X ω)) x ∂μ) t

Tactic:
hasDerivAt_integral_pow_mul_exp_real ht (n + 1)

Premises used: HAdd.hAdd, ProbabilityTheory.hasDerivAt_integral_pow_mul_exp_real, OfNat.ofNat
-- Module: Mathlib.Probability.Moments.MGFAnalytic
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 (F := ℝ) (fun (t : ℝ) ↦ ∫ (x : Ω), (fun (ω : Ω) ↦ X ω ^ (n + 1) * rexp (t * X ω)) x ∂μ)
    (∫ (x : Ω), (fun (ω : Ω) ↦ X ω ^ (n + 1 + 1) * rexp (t * X ω)) x ∂μ) t

Tactic:
exact hasDerivAt_integral_pow_mul_exp_real ht (n + 1)

Premises used: HAdd.hAdd, ProbabilityTheory.hasDerivAt_integral_pow_mul_exp_real, OfNat.ofNat
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
n : ℕ
zero :
  ∀ {t : ℝ} (ht : t ∈ interior (integrableExpSet X μ)),
    HasDerivAt (iteratedDeriv 0 (mgf X μ))
      (∫ (x : Ω), (fun (ω : Ω) ↦ X ω ^ HAdd.hAdd (α := ℕ) 0 1 * rexp (t * X ω)) x ∂μ) t
succ :
  ∀ (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
⊢ HasDerivAt (iteratedDeriv n (mgf X μ)) (∫ (x : Ω), (fun (ω : Ω) ↦ X ω ^ (n + 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)

Premises used: iteratedDeriv_succ, HAdd.hAdd, ProbabilityTheory.hasDerivAt_integral_pow_mul_exp_real, ProbabilityTheory.hasDerivAt_mgf, OfNat.ofNat
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
⊢ iteratedDeriv 0 (mgf X μ) t = ∫ (x : Ω), (fun (ω : Ω) ↦ HPow.hPow (β := ℕ) (X ω) 0 * rexp (t * X ω)) x ∂μ

Tactic:
simp [mgf]

Premises used: ProbabilityTheory.mgf
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
n : ℕ
hn :
  ∀ {t : ℝ} (ht : t ∈ interior (integrableExpSet X μ)),
    iteratedDeriv n (mgf X μ) t = ∫ (x : Ω), (fun (ω : Ω) ↦ X ω ^ n * rexp (t * X ω)) x ∂μ
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
succ : deriv (iteratedDeriv n (mgf X μ)) t = ∫ (x : Ω), (fun (ω : Ω) ↦ X ω ^ (n + 1) * rexp (t * X ω)) x ∂μ
⊢ iteratedDeriv (n + 1) (mgf X μ) t = ∫ (x : Ω), (fun (ω : Ω) ↦ X ω ^ (n + 1) * rexp (t * X ω)) x ∂μ

Tactic:
rw [iteratedDeriv_succ]

Premises used: iteratedDeriv_succ
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
n : ℕ
hn :
  ∀ {t : ℝ} (ht : t ∈ interior (integrableExpSet X μ)),
    iteratedDeriv n (mgf X μ) t = ∫ (x : Ω), (fun (ω : Ω) ↦ X ω ^ n * rexp (t * X ω)) x ∂μ
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
⊢ deriv (iteratedDeriv n (mgf X μ)) t = ∫ (x : Ω), (fun (ω : Ω) ↦ X ω ^ (n + 1) * rexp (t * X ω)) x ∂μ

Tactic:
(hasDerivAt_iteratedDeriv_mgf ht n).deriv

Premises used: HasDerivAt.deriv, ProbabilityTheory.hasDerivAt_iteratedDeriv_mgf
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
n : ℕ
hn :
  ∀ {t : ℝ} (ht : t ∈ interior (integrableExpSet X μ)),
    iteratedDeriv n (mgf X μ) t = ∫ (x : Ω), (fun (ω : Ω) ↦ X ω ^ n * rexp (t * X ω)) x ∂μ
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
⊢ deriv (iteratedDeriv n (mgf X μ)) t = ∫ (x : Ω), (fun (ω : Ω) ↦ X ω ^ (n + 1) * rexp (t * X ω)) x ∂μ

Tactic:
exact (hasDerivAt_iteratedDeriv_mgf ht n).deriv

Premises used: HasDerivAt.deriv, ProbabilityTheory.hasDerivAt_iteratedDeriv_mgf
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
n : ℕ
zero :
  ∀ {t : ℝ} (ht : t ∈ interior (integrableExpSet X μ)),
    iteratedDeriv 0 (mgf X μ) t = ∫ (x : Ω), (fun (ω : Ω) ↦ HPow.hPow (β := ℕ) (X ω) 0 * rexp (t * X ω)) x ∂μ
succ :
  ∀ (n : ℕ)
    (hn :
      ∀ {t : ℝ} (ht : t ∈ interior (integrableExpSet X μ)),
        iteratedDeriv n (mgf X μ) t = ∫ (x : Ω), (fun (ω : Ω) ↦ X ω ^ n * rexp (t * X ω)) x ∂μ)
    {t : ℝ} (ht : t ∈ interior (integrableExpSet X μ)),
    iteratedDeriv (n + 1) (mgf X μ) t = ∫ (x : Ω), (fun (ω : Ω) ↦ X ω ^ (n + 1) * rexp (t * X ω)) x ∂μ
⊢ iteratedDeriv n (mgf X μ) t = ∫ (x : Ω), (fun (ω : Ω) ↦ X ω ^ n * rexp (t * X ω)) x ∂μ

Tactic:
induction n generalizing t with
  | zero => simp [mgf]
  | succ n hn =>
    rw [iteratedDeriv_succ]
    exact (hasDerivAt_iteratedDeriv_mgf ht n).deriv

Premises used: iteratedDeriv_succ, HasDerivAt.deriv, ProbabilityTheory.hasDerivAt_iteratedDeriv_mgf, ProbabilityTheory.mgf
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
h : 0 ∈ interior (integrableExpSet X μ)
n : ℕ
⊢ iteratedDeriv n (mgf X μ) 0 = ∫ (x : Ω), (X ^ n) x ∂μ

Tactic:
simp [iteratedDeriv_mgf h n]

Premises used: ProbabilityTheory.iteratedDeriv_mgf
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
h : t ∈ interior (integrableExpSet X μ)
⊢ deriv (mgf X μ) t = ∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (t * X ω)) x ∂μ

Tactic:
(hasDerivAt_mgf h).deriv

Premises used: HasDerivAt.deriv, ProbabilityTheory.hasDerivAt_mgf
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
h : 0 ∈ interior (integrableExpSet X μ)
⊢ deriv (mgf X μ) 0 = ∫ (x : Ω), X x ∂μ

Tactic:
simp [deriv_mgf h]

Premises used: ProbabilityTheory.deriv_mgf
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
rw : AnalyticAt ℝ (F := ℝ) (fun (x : ℝ) ↦ (complexMGF X μ (↑x : ℂ)).re) t
⊢ AnalyticAt ℝ (mgf X μ) t

Tactic:
rw [← re_complexMGF_ofReal']

Premises used: ProbabilityTheory.re_complexMGF_ofReal'
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
⊢ (↑t : ℂ).re ∈ interior (integrableExpSet X μ)

Tactic:
simp [ht]
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
⊢ AnalyticAt ℝ (F := ℝ) (fun (x : ℝ) ↦ (complexMGF X μ (↑x : ℂ)).re) t

Tactic:
exact (analyticAt_complexMGF (by simp [ht])).re_ofReal

Premises used: ProbabilityTheory.analyticAt_complexMGF, AnalyticAt.re_ofReal