-- Mathlib/Probability/Moments/ComplexMGF.lean
/-- For `z : ℂ` with `z.re ∈ interior (integrableExpSet X μ)`, the derivative of the function
`z' ↦ μ[X ^ n * cexp (z' * X)]` at `z` is `μ[X ^ (n + 1) * cexp (z * X)]`. -/
lemma hasDerivAt_integral_pow_mul_exp (hz : z.re ∈ interior (integrableExpSet X μ)) (n : ℕ) :
    HasDerivAt (fun z ↦ μ[fun ω ↦ X ω ^ n * cexp (z * X ω)])
        μ[fun ω ↦ X ω ^ (n + 1) * cexp (z * X ω)] z

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

Tactic:
have hz' := hz

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

Proof state:
case h.e'_9
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
hX : AEMeasurable X μ
l u : ℝ
hlu : z.re ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := ((z.re - l) ⊓ (u - z.re)) / 2
h_pos : 0 < (z.re - l) ⊓ (u - z.re)
ht : 0 < t
ω : Ω
ε : ℂ
hε : ε ∈ Metric.ball z (t / 2)
⊢ ↑(X ω) • NormedSpace.exp ℂ (ε • ↑(X ω)) = NormedSpace.exp ℂ (ε • ↑(X ω)) * ↑(X ω)

Tactic:
rw [smul_eq_mul, mul_comm]

Result:
no goals

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
hX : AEMeasurable X μ
hz' : ∃ l u, z.re ∈ Set.Ioo l u ∧ Set.Ioo l u ⊆ integrableExpSet X μ
⊢ HasDerivAt (fun z => ∫ (x : Ω), (fun ω => ↑(X ω) ^ n * cexp (z * ↑(X ω))) x ∂μ)
    (∫ (x : Ω), (fun ω => ↑(X ω) ^ (n + 1) * cexp (z * ↑(X ω))) x ∂μ) z

Tactic:
obtain ⟨l, u, hlu, h_subset⟩ := hz'

Result:
case intro.intro.intro
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
hX : AEMeasurable X μ
l u : ℝ
hlu : z.re ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
⊢ HasDerivAt (fun z => ∫ (x : Ω), (fun ω => ↑(X ω) ^ n * cexp (z * ↑(X ω))) x ∂μ)
    (∫ (x : Ω), (fun ω => ↑(X ω) ^ (n + 1) * cexp (z * ↑(X ω))) x ∂μ) z

Proof state:
case intro.intro.intro.refine_6
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
hX : AEMeasurable X μ
l u : ℝ
hlu : z.re ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := ((z.re - l) ⊓ (u - z.re)) / 2
h_pos : 0 < (z.re - l) ⊓ (u - z.re)
ht : 0 < t
ω : Ω
ε : ℂ
hε : ε ∈ Metric.ball z (t / 2)
⊢ HasDerivAt (fun x => ↑(X ω) ^ n * cexp (x * ↑(X ω))) (↑(X ω) ^ n * (↑(X ω) * cexp (ε * ↑(X ω)))) ε

Tactic:
refine HasDerivAt.const_mul _ ?_

Result:
case intro.intro.intro.refine_6
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
hX : AEMeasurable X μ
l u : ℝ
hlu : z.re ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := ((z.re - l) ⊓ (u - z.re)) / 2
h_pos : 0 < (z.re - l) ⊓ (u - z.re)
ht : 0 < t
ω : Ω
ε : ℂ
hε : ε ∈ Metric.ball z (t / 2)
⊢ HasDerivAt (fun x => cexp (x * ↑(X ω))) (↑(X ω) * cexp (ε * ↑(X ω))) ε

Proof state:
case intro.intro.intro
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
hX : AEMeasurable X μ
l u : ℝ
hlu : z.re ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
⊢ HasDerivAt (fun z => ∫ (x : Ω), (fun ω => ↑(X ω) ^ n * cexp (z * ↑(X ω))) x ∂μ)
    (∫ (x : Ω), (fun ω => ↑(X ω) ^ (n + 1) * cexp (z * ↑(X ω))) x ∂μ) z

Tactic:
let t := ((z.re - l) ⊓ (u - z.re)) / 2

Result:
case intro.intro.intro
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
hX : AEMeasurable X μ
l u : ℝ
hlu : z.re ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := ((z.re - l) ⊓ (u - z.re)) / 2
⊢ HasDerivAt (fun z => ∫ (x : Ω), (fun ω => ↑(X ω) ^ n * cexp (z * ↑(X ω))) x ∂μ)
    (∫ (x : Ω), (fun ω => ↑(X ω) ^ (n + 1) * cexp (z * ↑(X ω))) x ∂μ) z

Proof state:
case intro.intro.intro.refine_6
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
hX : AEMeasurable X μ
l u : ℝ
hlu : z.re ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := ((z.re - l) ⊓ (u - z.re)) / 2
h_pos : 0 < (z.re - l) ⊓ (u - z.re)
ht : 0 < t
⊢ ∀ᵐ (a : Ω) ∂μ,
    ∀ x ∈ Metric.ball z (t / 2),
      HasDerivAt (fun x => (fun z ω => ↑(X ω) ^ n * cexp (z * ↑(X ω))) x a)
        ((fun z ω => ↑(X ω) ^ (n + 1) * cexp (z * ↑(X ω))) x a) x

Tactic:
refine ae_of_all _ fun ω ε hε ↦ ?_

Result:
case intro.intro.intro.refine_6
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
hX : AEMeasurable X μ
l u : ℝ
hlu : z.re ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := ((z.re - l) ⊓ (u - z.re)) / 2
h_pos : 0 < (z.re - l) ⊓ (u - z.re)
ht : 0 < t
ω : Ω
ε : ℂ
hε : ε ∈ Metric.ball z (t / 2)
⊢ HasDerivAt (fun x => (fun z ω => ↑(X ω) ^ n * cexp (z * ↑(X ω))) x ω)
    ((fun z ω => ↑(X ω) ^ (n + 1) * cexp (z * ↑(X ω))) ε ω) ε

Proof state:
case intro.intro.intro.refine_4.h.h.bc.h
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
hX : AEMeasurable X μ
l u : ℝ
hlu : z.re ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := ((z.re - l) ⊓ (u - z.re)) / 2
h_pos : 0 < (z.re - l) ⊓ (u - z.re)
ht : 0 < t
ω : Ω
ε : ℂ
hε : ε ∈ Metric.ball z (t / 2)
this : ε = z + (ε - z)
⊢ ‖ε - z‖ ≤ t / 2

Tactic:
simp only [Metric.mem_ball, dist_eq_norm] at hε

Result:
case intro.intro.intro.refine_4.h.h.bc.h
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
hX : AEMeasurable X μ
l u : ℝ
hlu : z.re ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := ((z.re - l) ⊓ (u - z.re)) / 2
h_pos : 0 < (z.re - l) ⊓ (u - z.re)
ht : 0 < t
ω : Ω
ε : ℂ
this : ε = z + (ε - z)
hε : ‖ε - z‖ < t / 2
⊢ ‖ε - z‖ ≤ t / 2

Proof state:
case intro.intro.intro.refine_4.h.h.bc.h
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
hX : AEMeasurable X μ
l u : ℝ
hlu : z.re ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := ((z.re - l) ⊓ (u - z.re)) / 2
h_pos : 0 < (z.re - l) ⊓ (u - z.re)
ht : 0 < t
ω : Ω
ε : ℂ
hε : ε ∈ Metric.ball z (t / 2)
this : ε = z + (ε - z)
⊢ |(ε - z).re| ≤ t / 2

Tactic:
refine (abs_re_le_norm _).trans ?_

Result:
case intro.intro.intro.refine_4.h.h.bc.h
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
hX : AEMeasurable X μ
l u : ℝ
hlu : z.re ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := ((z.re - l) ⊓ (u - z.re)) / 2
h_pos : 0 < (z.re - l) ⊓ (u - z.re)
ht : 0 < t
ω : Ω
ε : ℂ
hε : ε ∈ Metric.ball z (t / 2)
this : ε = z + (ε - z)
⊢ ‖ε - z‖ ≤ t / 2

Proof state:
case intro.intro.intro.refine_5.refine_1
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
hX : AEMeasurable X μ
l u : ℝ
hlu : z.re ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := ((z.re - l) ⊓ (u - z.re)) / 2
h_pos : 0 < (z.re - l) ⊓ (u - z.re)
ht : 0 < t
⊢ Integrable (fun ω => rexp ((z.re + t) * X ω)) μ

Tactic:
exact h_subset (add_half_inf_sub_mem_Ioo hlu)

Result:
no goals