-- Mathlib/Probability/Moments/MGFAnalytic.lean
lemma hasDerivAt_iteratedDeriv_mgf (ht : t ∈ interior (integrableExpSet X μ)) (n : ℕ) :
    HasDerivAt (iteratedDeriv n (mgf X μ)) μ[fun ω ↦ X ω ^ (n + 1) * exp (t * X ω)] t

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
n : ℕ
hn :
  ∀ {t : ℝ},
    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 h_mem : ∀ᶠ y in 𝓝 t, y ∈ interior (integrableExpSet X μ) :=
  isOpen_interior.eventually_mem ht

Result:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
n : ℕ
hn :
  ∀ {t : ℝ},
    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 ∂μ

Proof state:
Ω : 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

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)

Result:
no goals

Proof state:
case zero
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
⊢ HasDerivAt (iteratedDeriv 0 (mgf X μ)) (∫ (x : Ω), (fun ω => X ω ^ (0 + 1) * rexp (t * X ω)) x ∂μ) t

Tactic:
simp [hasDerivAt_mgf ht]

Result:
no goals

Proof state:
case succ
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
n : ℕ
hn :
  ∀ {t : ℝ},
    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

Tactic:
rw [iteratedDeriv_succ]

Result:
case succ
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
n : ℕ
hn :
  ∀ {t : ℝ},
    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

Proof state:
case succ
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
n : ℕ
hn :
  ∀ {t : ℝ},
    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 (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)

Result:
no goals

Proof state:
case succ
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
n : ℕ
hn :
  ∀ {t : ℝ},
    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

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)

Result:
case succ
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
n : ℕ
hn :
  ∀ {t : ℝ},
    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

Proof state:
case succ
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
n : ℕ
hn :
  ∀ {t : ℝ},
    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

Tactic:
rw [EventuallyEq.hasDerivAt_iff this]

Result:
case succ
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
n : ℕ
hn :
  ∀ {t : ℝ},
    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 (fun t => ∫ (x : Ω), (fun ω => X ω ^ (n + 1) * rexp (t * X ω)) x ∂μ)
    (∫ (x : Ω), (fun ω => X ω ^ (n + 1 + 1) * rexp (t * X ω)) x ∂μ) t

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
n : ℕ
hn :
  ∀ {t : ℝ},
    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 ∂μ

Tactic:
filter_upwards [h_mem] with y hy using HasDerivAt.deriv (hn hy)

Result:
no goals