-- Mathlib/Probability/Moments/MGFAnalytic.lean
/-- For `t : ℝ` with `t ∈ interior (integrableExpSet X μ)`, the derivative of the function
`x ↦ μ[X ^ n * exp (x * X)]` at `t` is `μ[X ^ (n + 1) * exp (t * X)]`. -/
lemma hasDerivAt_integral_pow_mul_exp_real (ht : t ∈ interior (integrableExpSet X μ)) (n : ℕ) :
    HasDerivAt (fun t ↦ μ[fun ω ↦ X ω ^ n * exp (t * X ω)])
      μ[fun ω ↦ X ω ^ (n + 1) * exp (t * X ω)] t

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
n : ℕ
h_re_of_mem :
  ∀ (n : ℕ),
    ∀ t ∈ interior (integrableExpSet X μ),
      (∫ (ω : Ω), ↑(X ω) ^ n * Complex.exp (↑t * ↑(X ω)) ∂μ).re = ∫ (ω : Ω), X ω ^ n * rexp (t * X ω) ∂μ
⊢ HasDerivAt (fun t => ∫ (x : Ω), (fun ω => X ω ^ n * rexp (t * X ω)) x ∂μ)
    (∫ (x : Ω), (fun ω => X ω ^ (n + 1) * rexp (t * X ω)) x ∂μ) t

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'

Result:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
n : ℕ
h_re_of_mem :
  ∀ (n : ℕ),
    ∀ t ∈ interior (integrableExpSet X μ),
      (∫ (ω : Ω), ↑(X ω) ^ n * Complex.exp (↑t * ↑(X ω)) ∂μ).re = ∫ (ω : Ω), X ω ^ n * rexp (t * X ω) ∂μ
h_re :
  ∀ (n : ℕ),
    ∀ᶠ (t' : ℝ) in 𝓝 t,
      (∫ (ω : Ω), ↑(X ω) ^ n * Complex.exp (↑t' * ↑(X ω)) ∂μ).re = ∫ (ω : Ω), X ω ^ n * rexp (t' * X ω) ∂μ
⊢ HasDerivAt (fun t => ∫ (x : Ω), (fun ω => X ω ^ n * rexp (t * X ω)) x ∂μ)
    (∫ (x : Ω), (fun ω => X ω ^ (n + 1) * rexp (t * X ω)) x ∂μ) t

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
n : ℕ
h_re_of_mem :
  ∀ (n : ℕ),
    ∀ t ∈ interior (integrableExpSet X μ),
      (∫ (ω : Ω), ↑(X ω) ^ n * Complex.exp (↑t * ↑(X ω)) ∂μ).re = ∫ (ω : Ω), X ω ^ n * rexp (t * X ω) ∂μ
h_re :
  ∀ (n : ℕ),
    ∀ᶠ (t' : ℝ) in 𝓝 t,
      (∫ (ω : Ω), ↑(X ω) ^ n * Complex.exp (↑t' * ↑(X ω)) ∂μ).re = ∫ (ω : Ω), X ω ^ n * rexp (t' * X ω) ∂μ
⊢ (↑t).re ∈ interior (integrableExpSet X μ)

Tactic:
simp [ht]

Result:
no goals

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
n✝ : ℕ
h_re_of_mem :
  ∀ (n : ℕ),
    ∀ t ∈ interior (integrableExpSet X μ),
      (∫ (ω : Ω), ↑(X ω) ^ n * Complex.exp (↑t * ↑(X ω)) ∂μ).re = ∫ (ω : Ω), X ω ^ n * rexp (t * X ω) ∂μ
n : ℕ
⊢ ∀ᶠ (t' : ℝ) in 𝓝 t,
    (∫ (ω : Ω), ↑(X ω) ^ n * Complex.exp (↑t' * ↑(X ω)) ∂μ).re = ∫ (ω : Ω), X ω ^ n * rexp (t' * X ω) ∂μ

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

Result:
no goals

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
n : ℕ
h_re_of_mem :
  ∀ (n : ℕ),
    ∀ t ∈ interior (integrableExpSet X μ),
      (∫ (ω : Ω), ↑(X ω) ^ n * Complex.exp (↑t * ↑(X ω)) ∂μ).re = ∫ (ω : Ω), X ω ^ n * rexp (t * X ω) ∂μ
h_re :
  ∀ (n : ℕ),
    ∀ᶠ (t' : ℝ) in 𝓝 t,
      (∫ (ω : Ω), ↑(X ω) ^ n * Complex.exp (↑t' * ↑(X ω)) ∂μ).re = ∫ (ω : Ω), X ω ^ n * rexp (t' * X ω) ∂μ
⊢ HasDerivAt (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]

Result:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
n : ℕ
h_re_of_mem :
  ∀ (n : ℕ),
    ∀ t ∈ interior (integrableExpSet X μ),
      (∫ (ω : Ω), ↑(X ω) ^ n * Complex.exp (↑t * ↑(X ω)) ∂μ).re = ∫ (ω : Ω), X ω ^ n * rexp (t * X ω) ∂μ
h_re :
  ∀ (n : ℕ),
    ∀ᶠ (t' : ℝ) in 𝓝 t,
      (∫ (ω : Ω), ↑(X ω) ^ n * Complex.exp (↑t' * ↑(X ω)) ∂μ).re = ∫ (ω : Ω), X ω ^ n * rexp (t' * X ω) ∂μ
⊢ HasDerivAt (fun x => (∫ (ω : Ω), ↑(X ω) ^ n * Complex.exp (↑x * ↑(X ω)) ∂μ).re)
    (∫ (ω : Ω), ↑(X ω) ^ (n + 1) * Complex.exp (↑t * ↑(X ω)) ∂μ).re t

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
n : ℕ
h_re_of_mem :
  ∀ (n : ℕ),
    ∀ t ∈ interior (integrableExpSet X μ),
      (∫ (ω : Ω), ↑(X ω) ^ n * Complex.exp (↑t * ↑(X ω)) ∂μ).re = ∫ (ω : Ω), X ω ^ n * rexp (t * X ω) ∂μ
h_re :
  ∀ (n : ℕ),
    ∀ᶠ (t' : ℝ) in 𝓝 t,
      (∫ (ω : Ω), ↑(X ω) ^ n * Complex.exp (↑t' * ↑(X ω)) ∂μ).re = ∫ (ω : Ω), X ω ^ n * rexp (t' * X ω) ∂μ
⊢ HasDerivAt (fun x => (∫ (ω : Ω), ↑(X ω) ^ n * Complex.exp (↑x * ↑(X ω)) ∂μ).re)
    (∫ (ω : Ω), ↑(X ω) ^ (n + 1) * Complex.exp (↑t * ↑(X ω)) ∂μ).re t

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

Result:
no goals

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t✝ : ℝ
ht : t✝ ∈ interior (integrableExpSet X μ)
n✝ n : ℕ
t : ℝ
ht' : t ∈ interior (integrableExpSet X μ)
⊢ (↑t).re ∈ interior (integrableExpSet X μ)

Tactic:
simpa using ht'

Result:
no goals

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t✝ : ℝ
ht : t✝ ∈ interior (integrableExpSet X μ)
n✝ n : ℕ
t : ℝ
ht' : t ∈ interior (integrableExpSet X μ)
⊢ Integrable (fun ω => ↑(X ω) ^ n * Complex.exp (↑t * ↑(X ω))) μ

Tactic:
refine integrable_pow_mul_cexp_of_re_mem_interior_integrableExpSet ?_ n

Result:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t✝ : ℝ
ht : t✝ ∈ interior (integrableExpSet X μ)
n✝ n : ℕ
t : ℝ
ht' : t ∈ interior (integrableExpSet X μ)
⊢ (↑t).re ∈ interior (integrableExpSet X μ)

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t✝ : ℝ
ht : t✝ ∈ interior (integrableExpSet X μ)
n✝ n : ℕ
t : ℝ
ht' : t ∈ interior (integrableExpSet X μ)
⊢ ∫ (x : Ω), RCLike.re (↑(X x) ^ n * Complex.exp (↑t * ↑(X x))) ∂μ = ∫ (ω : Ω), X ω ^ n * rexp (t * X ω) ∂μ

Tactic:
norm_cast

Result:
no goals

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t✝ : ℝ
ht : t✝ ∈ interior (integrableExpSet X μ)
n✝ n : ℕ
t : ℝ
ht' : t ∈ interior (integrableExpSet X μ)
⊢ (∫ (ω : Ω), ↑(X ω) ^ n * Complex.exp (↑t * ↑(X ω)) ∂μ).re = ∫ (ω : Ω), X ω ^ n * rexp (t * X ω) ∂μ

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

Result:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t✝ : ℝ
ht : t✝ ∈ interior (integrableExpSet X μ)
n✝ n : ℕ
t : ℝ
ht' : t ∈ interior (integrableExpSet X μ)
⊢ ∫ (x : Ω), RCLike.re (↑(X x) ^ n * Complex.exp (↑t * ↑(X x))) ∂μ = ∫ (ω : Ω), X ω ^ n * rexp (t * X ω) ∂μ

Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t✝ : ℝ
ht : t✝ ∈ interior (integrableExpSet X μ)
n✝ n : ℕ
t : ℝ
ht' : t ∈ interior (integrableExpSet X μ)
⊢ Integrable (fun ω => ↑(X ω) ^ n * Complex.exp (↑t * ↑(X ω))) μ