-- Mathlib/Probability/Moments/ComplexMGF.lean
lemma hasDerivAt_iteratedDeriv_complexMGF (hz : z.re ∈ interior (integrableExpSet X μ)) (n : ℕ) :
    HasDerivAt (iteratedDeriv n (complexMGF X μ)) μ[fun ω ↦ X ω ^ (n + 1) * cexp (z * X ω)] z

Proof state:
case succ
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
n : ℕ
hn :
  ∀ {z : ℂ},
    z.re ∈ interior (integrableExpSet X μ) →
      HasDerivAt (iteratedDeriv n (complexMGF X μ)) (∫ (x : Ω), (fun ω => ↑(X ω) ^ (n + 1) * cexp (z * ↑(X ω))) x ∂μ) z
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
⊢ HasDerivAt (deriv (iteratedDeriv n (complexMGF X μ)))
    (∫ (x : Ω), (fun ω => ↑(X ω) ^ (n + 1 + 1) * cexp (z * ↑(X ω))) x ∂μ) z

Tactic:
have : deriv (iteratedDeriv n (complexMGF X μ))
    =ᶠ[𝓝 z] fun z ↦ μ[fun ω ↦ X ω ^ (n + 1) * cexp (z * X ω)] := by
  have h_mem : ∀ᶠ y in 𝓝 z, y.re ∈ interior (integrableExpSet X μ) := by
    refine IsOpen.eventually_mem ?_ hz
    exact isOpen_interior.preimage Complex.continuous_re
  filter_upwards [h_mem] with y hy using HasDerivAt.deriv (hn hy)

Result:
case succ
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
n : ℕ
hn :
  ∀ {z : ℂ},
    z.re ∈ interior (integrableExpSet X μ) →
      HasDerivAt (iteratedDeriv n (complexMGF X μ)) (∫ (x : Ω), (fun ω => ↑(X ω) ^ (n + 1) * cexp (z * ↑(X ω))) x ∂μ) z
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
this :
  deriv (iteratedDeriv n (complexMGF X μ)) =ᶠ[𝓝 z] fun z =>
    ∫ (x : Ω), (fun ω => ↑(X ω) ^ (n + 1) * cexp (z * ↑(X ω))) x ∂μ
⊢ HasDerivAt (deriv (iteratedDeriv n (complexMGF X μ)))
    (∫ (x : Ω), (fun ω => ↑(X ω) ^ (n + 1 + 1) * cexp (z * ↑(X ω))) x ∂μ) z

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
⊢ HasDerivAt (iteratedDeriv n (complexMGF X μ)) (∫ (x : Ω), (fun ω => ↑(X ω) ^ (n + 1) * cexp (z * ↑(X ω))) x ∂μ) z

Tactic:
induction n generalizing z with
| zero => simp [hasDerivAt_complexMGF hz]
| succ n hn =>
  rw [iteratedDeriv_succ]
  have : deriv (iteratedDeriv n (complexMGF X μ))
      =ᶠ[𝓝 z] fun z ↦ μ[fun ω ↦ X ω ^ (n + 1) * cexp (z * X ω)] := by
    have h_mem : ∀ᶠ y in 𝓝 z, y.re ∈ interior (integrableExpSet X μ) := by
      refine IsOpen.eventually_mem ?_ hz
      exact isOpen_interior.preimage Complex.continuous_re
    filter_upwards [h_mem] with y hy using HasDerivAt.deriv (hn hy)
  rw [EventuallyEq.hasDerivAt_iff this]
  exact hasDerivAt_integral_pow_mul_exp hz (n + 1)

Result:
no goals

Proof state:
case succ
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
n : ℕ
hn :
  ∀ {z : ℂ},
    z.re ∈ interior (integrableExpSet X μ) →
      HasDerivAt (iteratedDeriv n (complexMGF X μ)) (∫ (x : Ω), (fun ω => ↑(X ω) ^ (n + 1) * cexp (z * ↑(X ω))) x ∂μ) z
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
this :
  deriv (iteratedDeriv n (complexMGF X μ)) =ᶠ[𝓝 z] fun z =>
    ∫ (x : Ω), (fun ω => ↑(X ω) ^ (n + 1) * cexp (z * ↑(X ω))) x ∂μ
⊢ HasDerivAt (fun z => ∫ (x : Ω), (fun ω => ↑(X ω) ^ (n + 1) * cexp (z * ↑(X ω))) x ∂μ)
    (∫ (x : Ω), (fun ω => ↑(X ω) ^ (n + 1 + 1) * cexp (z * ↑(X ω))) x ∂μ) z

Tactic:
exact hasDerivAt_integral_pow_mul_exp hz (n + 1)

Result:
no goals

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
n : ℕ
hn :
  ∀ {z : ℂ},
    z.re ∈ interior (integrableExpSet X μ) →
      HasDerivAt (iteratedDeriv n (complexMGF X μ)) (∫ (x : Ω), (fun ω => ↑(X ω) ^ (n + 1) * cexp (z * ↑(X ω))) x ∂μ) z
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
h_mem : ∀ᶠ (y : ℂ) in 𝓝 z, y.re ∈ interior (integrableExpSet X μ)
⊢ deriv (iteratedDeriv n (complexMGF X μ)) =ᶠ[𝓝 z] fun z =>
    ∫ (x : Ω), (fun ω => ↑(X ω) ^ (n + 1) * cexp (z * ↑(X ω))) x ∂μ

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

Result:
no goals

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
n : ℕ
hn :
  ∀ {z : ℂ},
    z.re ∈ interior (integrableExpSet X μ) →
      HasDerivAt (iteratedDeriv n (complexMGF X μ)) (∫ (x : Ω), (fun ω => ↑(X ω) ^ (n + 1) * cexp (z * ↑(X ω))) x ∂μ) z
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
⊢ ∀ᶠ (y : ℂ) in 𝓝 z, y.re ∈ interior (integrableExpSet X μ)

Tactic:
refine IsOpen.eventually_mem ?_ hz

Result:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
n : ℕ
hn :
  ∀ {z : ℂ},
    z.re ∈ interior (integrableExpSet X μ) →
      HasDerivAt (iteratedDeriv n (complexMGF X μ)) (∫ (x : Ω), (fun ω => ↑(X ω) ^ (n + 1) * cexp (z * ↑(X ω))) x ∂μ) z
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
⊢ IsOpen fun y => interior (integrableExpSet X μ) y.re

Proof state:
case succ
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
n : ℕ
hn :
  ∀ {z : ℂ},
    z.re ∈ interior (integrableExpSet X μ) →
      HasDerivAt (iteratedDeriv n (complexMGF X μ)) (∫ (x : Ω), (fun ω => ↑(X ω) ^ (n + 1) * cexp (z * ↑(X ω))) x ∂μ) z
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
⊢ HasDerivAt (iteratedDeriv (n + 1) (complexMGF X μ))
    (∫ (x : Ω), (fun ω => ↑(X ω) ^ (n + 1 + 1) * cexp (z * ↑(X ω))) x ∂μ) z

Tactic:
rw [iteratedDeriv_succ]

Result:
case succ
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
n : ℕ
hn :
  ∀ {z : ℂ},
    z.re ∈ interior (integrableExpSet X μ) →
      HasDerivAt (iteratedDeriv n (complexMGF X μ)) (∫ (x : Ω), (fun ω => ↑(X ω) ^ (n + 1) * cexp (z * ↑(X ω))) x ∂μ) z
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
⊢ HasDerivAt (deriv (iteratedDeriv n (complexMGF X μ)))
    (∫ (x : Ω), (fun ω => ↑(X ω) ^ (n + 1 + 1) * cexp (z * ↑(X ω))) x ∂μ) z

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
n : ℕ
hn :
  ∀ {z : ℂ},
    z.re ∈ interior (integrableExpSet X μ) →
      HasDerivAt (iteratedDeriv n (complexMGF X μ)) (∫ (x : Ω), (fun ω => ↑(X ω) ^ (n + 1) * cexp (z * ↑(X ω))) x ∂μ) z
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
⊢ deriv (iteratedDeriv n (complexMGF X μ)) =ᶠ[𝓝 z] fun z =>
    ∫ (x : Ω), (fun ω => ↑(X ω) ^ (n + 1) * cexp (z * ↑(X ω))) x ∂μ

Tactic:
have h_mem : ∀ᶠ y in 𝓝 z, y.re ∈ interior (integrableExpSet X μ) := by
  refine IsOpen.eventually_mem ?_ hz
  exact isOpen_interior.preimage Complex.continuous_re

Result:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
n : ℕ
hn :
  ∀ {z : ℂ},
    z.re ∈ interior (integrableExpSet X μ) →
      HasDerivAt (iteratedDeriv n (complexMGF X μ)) (∫ (x : Ω), (fun ω => ↑(X ω) ^ (n + 1) * cexp (z * ↑(X ω))) x ∂μ) z
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
h_mem : ∀ᶠ (y : ℂ) in 𝓝 z, y.re ∈ interior (integrableExpSet X μ)
⊢ deriv (iteratedDeriv n (complexMGF X μ)) =ᶠ[𝓝 z] fun z =>
    ∫ (x : Ω), (fun ω => ↑(X ω) ^ (n + 1) * cexp (z * ↑(X ω))) x ∂μ

Proof state:
case succ
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
n : ℕ
hn :
  ∀ {z : ℂ},
    z.re ∈ interior (integrableExpSet X μ) →
      HasDerivAt (iteratedDeriv n (complexMGF X μ)) (∫ (x : Ω), (fun ω => ↑(X ω) ^ (n + 1) * cexp (z * ↑(X ω))) x ∂μ) z
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
this :
  deriv (iteratedDeriv n (complexMGF X μ)) =ᶠ[𝓝 z] fun z =>
    ∫ (x : Ω), (fun ω => ↑(X ω) ^ (n + 1) * cexp (z * ↑(X ω))) x ∂μ
⊢ HasDerivAt (deriv (iteratedDeriv n (complexMGF X μ)))
    (∫ (x : Ω), (fun ω => ↑(X ω) ^ (n + 1 + 1) * cexp (z * ↑(X ω))) x ∂μ) z

Tactic:
rw [EventuallyEq.hasDerivAt_iff this]

Result:
case succ
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
n : ℕ
hn :
  ∀ {z : ℂ},
    z.re ∈ interior (integrableExpSet X μ) →
      HasDerivAt (iteratedDeriv n (complexMGF X μ)) (∫ (x : Ω), (fun ω => ↑(X ω) ^ (n + 1) * cexp (z * ↑(X ω))) x ∂μ) z
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
this :
  deriv (iteratedDeriv n (complexMGF X μ)) =ᶠ[𝓝 z] fun z =>
    ∫ (x : Ω), (fun ω => ↑(X ω) ^ (n + 1) * cexp (z * ↑(X ω))) x ∂μ
⊢ HasDerivAt (fun z => ∫ (x : Ω), (fun ω => ↑(X ω) ^ (n + 1) * cexp (z * ↑(X ω))) x ∂μ)
    (∫ (x : Ω), (fun ω => ↑(X ω) ^ (n + 1 + 1) * cexp (z * ↑(X ω))) x ∂μ) z