-- 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:
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 ω))) ε

Tactic:
simp_rw [← smul_eq_mul, Complex.exp_eq_exp_ℂ]

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 => NormedSpace.exp ℂ (x • ↑(X ω))) (↑(X ω) • NormedSpace.exp ℂ (ε • ↑(X ω))) ε

Proof state:
case intro.intro.intro.refine_4
Ω : 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)
⊢ ‖(fun z ω => ↑(X ω) ^ (n + 1) * cexp (z * ↑(X ω))) ε ω‖ ≤
    (fun ω => |X ω| ^ (n + 1) * rexp (z.re * X ω + t / 2 * |X ω|)) ω

Tactic:
simp only [norm_mul, norm_pow, norm_real, Real.norm_eq_abs]

Result:
case intro.intro.intro.refine_4
Ω : 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 ω| ^ (n + 1) * ‖cexp (ε * ↑(X ω))‖ ≤ |X ω| ^ (n + 1) * rexp (z.re * X ω + t / 2 * |X ω|)

Proof state:
case intro.intro.intro.refine_5.refine_3
Ω : 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
⊢ 0 ≤ t / 2

Tactic:
positivity

Result:
no goals

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

Tactic:
have hX : AEMeasurable X μ := aemeasurable_of_mem_interior_integrableExpSet hz

Result:
Ω : 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

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 μ
t : ℝ := ((z.re - l) ⊓ (u - z.re)) / 2
h_pos : 0 < (z.re - l) ⊓ (u - z.re)
⊢ HasDerivAt (fun z => ∫ (x : Ω), (fun ω => ↑(X ω) ^ n * cexp (z * ↑(X ω))) x ∂μ)
    (∫ (x : Ω), (fun ω => ↑(X ω) ^ (n + 1) * cexp (z * ↑(X ω))) x ∂μ) z

Tactic:
have ht : 0 < t := half_pos h_pos

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
h_pos : 0 < (z.re - l) ⊓ (u - z.re)
ht : 0 < t
⊢ HasDerivAt (fun z => ∫ (x : Ω), (fun ω => ↑(X ω) ^ n * cexp (z * ↑(X ω))) x ∂μ)
    (∫ (x : Ω), (fun ω => ↑(X ω) ^ (n + 1) * cexp (z * ↑(X ω))) x ∂μ) z

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

Tactic:
rw [mem_interior_iff_mem_nhds, mem_nhds_iff_exists_Ioo_subset] at hz'

Result:
Ω : 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

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 + 1) * cexp (ε * ↑(X ω))) ε

Tactic:
simp_rw [pow_succ, mul_assoc]

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 => ↑(X ω) ^ n * cexp (x * ↑(X ω))) (↑(X ω) ^ n * (↑(X ω) * cexp (ε * ↑(X ω)))) ε

Proof state:
case intro.intro.intro.refine_4.h.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 * X ω + (ε - z).re * X ω ≤ z.re * X ω + t / 2 * |X ω|

Tactic:
gcongr _ + ?_

Result:
case intro.intro.intro.refine_4.h.h.bc
Ω : 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 * X ω ≤ t / 2 * |X ω|

Proof state:
case intro.intro.intro.refine_5.refine_4
Ω : 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
⊢ t / 2 < |t|

Tactic:
exact lt_of_lt_of_le (by simp [ht]) (le_abs_self _)

Result:
no goals