-- 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 μ
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
⊢ 0 < (z.re - l) ⊓ (u - z.re)

Tactic:
simp [hlu.1, hlu.2]

Result:
no goals

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

Tactic:
rw [abs_mul]

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

Tactic:
simp only

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

Proof state:
Ω : 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
⊢ AEMeasurable ((fun z ω => ↑(X ω) ^ (n + 1) * cexp (z * ↑(X ω))) z) μ

Tactic:
fun_prop

Result:
no goals

Proof state:
case intro.intro.intro.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
⊢ AEStronglyMeasurable ((fun z ω => ↑(X ω) ^ (n + 1) * cexp (z * ↑(X ω))) z) μ

Tactic:
exact AEMeasurable.aestronglyMeasurable (by fun_prop)

Result:
no goals

Proof state:
case intro.intro.intro.refine_2
Ω : 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 z ω => ↑(X ω) ^ n * cexp (z * ↑(X ω))) z) μ

Tactic:
exact integrable_pow_mul_cexp_of_re_mem_interior_integrableExpSet hz n

Result:
no goals

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)
⊢ |X ω| ^ (n + 1) * rexp (ε * ↑(X ω)).re ≤ |X ω| ^ (n + 1) * rexp (z.re * X ω + t / 2 * |X ω|)

Tactic:
simp only [mul_re, ofReal_re, ofReal_im, mul_zero, sub_zero]

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

Tactic:
rw [Complex.norm_exp]

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) * rexp (ε * ↑(X ω)).re ≤ |X ω| ^ (n + 1) * rexp (z.re * X ω + t / 2 * |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)
⊢ |X ω| ^ (n + 1) * rexp (ε.re * X ω) ≤ |X ω| ^ (n + 1) * rexp (z.re * X ω + t / 2 * |X ω|)

Tactic:
gcongr

Result:
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)
⊢ ε.re * X ω ≤ z.re * X ω + t / 2 * |X ω|

Proof state:
Ω : 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
z : ℂ
⊢ AEMeasurable ((fun z ω => ↑(X ω) ^ n * cexp (z * ↑(X ω))) z) μ

Tactic:
fun_prop

Result:
no goals