-- 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_5
Ω : 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 ω => |X ω| ^ (n + 1) * rexp (z.re * X ω + t / 2 * |X ω|)) μ

Tactic:
refine integrable_pow_abs_mul_exp_add_of_integrable_exp_mul ?_ ?_ ?_ ?_ (t := t) (n + 1)

Result:
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 ω)) μ

case intro.intro.intro.refine_5.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 ω => rexp ((z.re - t) * X ω)) μ

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

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|

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
ω : Ω
ε : ℂ
hε : ε ∈ Metric.ball z (t / 2)
⊢ ε = z + (ε - z)

Tactic:
simp

Result:
no goals

Proof state:
case intro.intro.intro.refine_5.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 ω => rexp ((z.re - t) * X ω)) μ

Tactic:
exact h_subset (sub_half_inf_sub_mem_Ioo hlu)

Result:
no goals

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

Tactic:
have : ε = z + (ε - z) := by simp

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)
this : ε = z + (ε - z)
⊢ ε.re * X ω ≤ 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
⊢ ∀ᵐ (a : Ω) ∂μ,
    ∀ x ∈ Metric.ball z (t / 2),
      ‖(fun z ω => ↑(X ω) ^ (n + 1) * cexp (z * ↑(X ω))) x a‖ ≤
        (fun ω => |X ω| ^ (n + 1) * rexp (z.re * X ω + t / 2 * |X ω|)) a

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

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

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:
gcongr

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).re| ≤ t / 2

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

Tactic:
convert hasDerivAt_exp_smul_const (X ω : ℂ) ε using 1

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