awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Moments.ComplexMGF (goal)
Goal:
Ω : 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 : ℝ := min (z.re - l) (u - z.re) / 2
h_pos : 0 < min (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 ω|)
have refine_4 : |X ω| ^ (n + 1) * rexp (ε.re * X ω) ≤ |X ω| ^ (n + 1) * rexp (z.re * X ω + t / 2 * |X ω|)
Tactic: simp only [mul_re, ofReal_re, ofReal_im, mul_zero, sub_zero]
-- Lean 4 proof step from Mathlib.Probability.Moments.ComplexMGF (goal)
Goal:
Ω : 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 : ℝ := min (z.re - l) (u - z.re) / 2
h_pos : 0 < min (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 ω|)
have refine_4 : ε.re * X ω ≤ z.re * X ω + t / 2 * |X ω|
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Probability.Moments.ComplexMGF (hypothesis)
Goal:
Ω : 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 : ℝ := min (z.re - l) (u - z.re) / 2
h_pos : 0 < min (z.re - l) (u - z.re)
ht : 0 < t
ω : Ω
ε : ℂ
hε : ε ∈ Metric.ball z (t / 2)
⊢ ε.re * X ω ≤ z.re * X ω + t / 2 * |X ω|
have this : ε = z + (ε - z)
Tactic: have : ε = z + (ε - z) := by simp
-- Lean 4 proof step from Mathlib.Probability.Moments.ComplexMGF (goal)
Goal:
Ω : 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 : ℝ := min (z.re - l) (u - z.re) / 2
h_pos : 0 < min (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 ω|
have refine_4 : z.re * X ω + (ε - z).re * X ω ≤ z.re * X ω + t / 2 * |X ω|
Tactic: rw [this, add_re, add_mul]
-- Lean 4 proof step from Mathlib.Probability.Moments.ComplexMGF (goal)
Goal:
Ω : 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 : ℝ := min (z.re - l) (u - z.re) / 2
h_pos : 0 < min (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 ω|
have refine_4 : (ε - z).re * X ω ≤ t / 2 * |X ω|
Tactic: gcongr _ + ?_
-- Lean 4 proof step from Mathlib.Probability.Moments.ComplexMGF (goal)
Goal:
Ω : 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 : ℝ := min (z.re - l) (u - z.re) / 2
h_pos : 0 < min (z.re - l) (u - z.re)
ht : 0 < t
ω : Ω
ε : ℂ
hε : ε ∈ Metric.ball z (t / 2)
this : ε = z + (ε - z)
⊢ (ε - z).re * X ω ≤ t / 2 * |X ω|
have refine_4 : |(ε - z).re * X ω| ≤ t / 2 * |X ω|
Tactic: refine (le_abs_self _).trans ?_
-- Lean 4 proof step from Mathlib.Probability.Moments.ComplexMGF (goal)
Goal:
Ω : 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 : ℝ := min (z.re - l) (u - z.re) / 2
h_pos : 0 < min (z.re - l) (u - z.re)
ht : 0 < t
ω : Ω
ε : ℂ
hε : ε ∈ Metric.ball z (t / 2)
this : ε = z + (ε - z)
⊢ |(ε - z).re * X ω| ≤ t / 2 * |X ω|
have refine_4 : |(ε - z).re| * |X ω| ≤ t / 2 * |X ω|
Tactic: rw [abs_mul]
-- Lean 4 proof step from Mathlib.Probability.Moments.ComplexMGF (goal)
Goal:
Ω : 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 : ℝ := min (z.re - l) (u - z.re) / 2
h_pos : 0 < min (z.re - l) (u - z.re)
ht : 0 < t
ω : Ω
ε : ℂ
hε : ε ∈ Metric.ball z (t / 2)
this : ε = z + (ε - z)
⊢ |(ε - z).re| * |X ω| ≤ t / 2 * |X ω|
have refine_4 : |(ε - z).re| ≤ t / 2
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Probability.Moments.ComplexMGF (hypothesis)
Goal:
Ω : 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 : ℝ := min (z.re - l) (u - z.re) / 2
h_pos : 0 < min (z.re - l) (u - z.re)
ht : 0 < t
ω : Ω
ε : ℂ
hε : ε ∈ Metric.ball z (t / 2)
this : ε = z + (ε - z)
⊢ ‖ε - z‖ ≤ t / 2
have hε₁ : ‖ε - z‖ < t / 2
Tactic: simp only [Metric.mem_ball, dist_eq_norm] at hε
Cleared hypotheses: hε
-- Lean 4 proof step from Mathlib.Probability.Moments.ComplexMGF (goal)
Goal:
Ω : 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 : ℝ := min (z.re - l) (u - z.re) / 2
h_pos : 0 < min (z.re - l) (u - z.re)
ht : 0 < t
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ |X ω| ^ (n + 1) * rexp (z.re * X ω + t / 2 * |X ω|)) μ
have refine_5 : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp ((z.re + t) * X ω)) μ
Tactic: refine integrable_pow_abs_mul_exp_add_of_integrable_exp_mul ?_ ?_ ?_ ?_ (t := t) (n + 1)
-- Lean 4 proof step from Mathlib.Probability.Moments.ComplexMGF (goal)
Goal:
Ω : 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 : ℝ := min (z.re - l) (u - z.re) / 2
h_pos : 0 < min (z.re - l) (u - z.re)
ht : 0 < t
refine_5 : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp ((z.re + t) * X ω)) μ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ |X ω| ^ (n + 1) * rexp (z.re * X ω + t / 2 * |X ω|)) μ
have refine_5₁ : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp ((z.re - t) * X ω)) μ
Tactic: refine integrable_pow_abs_mul_exp_add_of_integrable_exp_mul ?_ ?_ ?_ ?_ (t := t) (n + 1)
-- Lean 4 proof step from Mathlib.Probability.Moments.ComplexMGF (goal)
Goal:
Ω : 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 : ℝ := min (z.re - l) (u - z.re) / 2
h_pos : 0 < min (z.re - l) (u - z.re)
ht : 0 < t
refine_5 : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp ((z.re + t) * X ω)) μ
refine_5₁ : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp ((z.re - t) * X ω)) μ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ |X ω| ^ (n + 1) * rexp (z.re * X ω + t / 2 * |X ω|)) μ
have refine_5₂ : 0 ≤ t / 2
Tactic: refine integrable_pow_abs_mul_exp_add_of_integrable_exp_mul ?_ ?_ ?_ ?_ (t := t) (n + 1)
-- Lean 4 proof step from Mathlib.Probability.Moments.ComplexMGF (goal)
Goal:
Ω : 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 : ℝ := min (z.re - l) (u - z.re) / 2
h_pos : 0 < min (z.re - l) (u - z.re)
ht : 0 < t
refine_5 : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp ((z.re + t) * X ω)) μ
refine_5₁ : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp ((z.re - t) * X ω)) μ
refine_5₂ : 0 ≤ t / 2
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ |X ω| ^ (n + 1) * rexp (z.re * X ω + t / 2 * |X ω|)) μ
have refine_5₃ : t / 2 < |t|
Tactic: refine integrable_pow_abs_mul_exp_add_of_integrable_exp_mul ?_ ?_ ?_ ?_ (t := t) (n + 1)
-- Lean 4 proof step from Mathlib.Probability.Moments.ComplexMGF (goal)
Goal:
Ω : 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 : ℝ := min (z.re - l) (u - z.re) / 2
h_pos : 0 < min (z.re - l) (u - z.re)
ht : 0 < t
⊢ ∀ᵐ (a : Ω) ∂μ,
    ∀ x ∈ Metric.ball z (t / 2),
      HasDerivAt (F := ℂ) (fun (x : ℂ) ↦ (fun (z : ℂ) (ω : Ω) ↦ (↑(X ω) : ℂ) ^ n * cexp (z * (↑(X ω) : ℂ))) x a)
        ((fun (z : ℂ) (ω : Ω) ↦ (↑(X ω) : ℂ) ^ (n + 1) * cexp (z * (↑(X ω) : ℂ))) x a) x
have refine_6 : ∀ (ω : Ω) (ε : ℂ) (hε : ε ∈ Metric.ball z (t / 2)),
  HasDerivAt (F := ℂ) (fun (x : ℂ) ↦ (fun (z : ℂ) (ω : Ω) ↦ (↑(X ω) : ℂ) ^ n * cexp (z * (↑(X ω) : ℂ))) x ω)
    ((fun (z : ℂ) (ω : Ω) ↦ (↑(X ω) : ℂ) ^ (n + 1) * cexp (z * (↑(X ω) : ℂ))) ε ω) ε
Tactic: refine ae_of_all _ fun ω ε hε ↦ ?_
-- Lean 4 proof step from Mathlib.Probability.Moments.ComplexMGF (goal)
Goal:
Ω : 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 : ℝ := min (z.re - l) (u - z.re) / 2
h_pos : 0 < min (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 ω) : ℂ))) ε
have refine_6 : HasDerivAt (fun (x : ℂ) ↦ (↑(X ω) : ℂ) ^ n * cexp (x * (↑(X ω) : ℂ)))
  ((↑(X ω) : ℂ) ^ n * ((↑(X ω) : ℂ) * cexp (ε * (↑(X ω) : ℂ)))) ε
Tactic: simp_rw [pow_succ, mul_assoc]
-- Lean 4 proof step from Mathlib.Probability.Moments.ComplexMGF (goal)
Goal:
Ω : 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 : ℝ := min (z.re - l) (u - z.re) / 2
h_pos : 0 < min (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 ω) : ℂ)))) ε
have refine_6 : HasDerivAt (fun (x : ℂ) ↦ cexp (x * (↑(X ω) : ℂ))) ((↑(X ω) : ℂ) * cexp (ε * (↑(X ω) : ℂ))) ε
Tactic: refine HasDerivAt.const_mul _ ?_
-- Lean 4 proof step from Mathlib.Probability.Moments.ComplexMGF (goal)
Goal:
Ω : 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 : ℝ := min (z.re - l) (u - z.re) / 2
h_pos : 0 < min (z.re - l) (u - z.re)
ht : 0 < t
ω : Ω
ε : ℂ
hε : ε ∈ Metric.ball z (t / 2)
⊢ HasDerivAt (fun (x : ℂ) ↦ cexp (x * (↑(X ω) : ℂ))) ((↑(X ω) : ℂ) * cexp (ε * (↑(X ω) : ℂ))) ε
have refine_6 : HasDerivAt (fun (x : ℂ) ↦ NormedSpace.exp (x • (↑(X ω) : ℂ))) ((↑(X ω) : ℂ) • NormedSpace.exp (ε • (↑(X ω) : ℂ))) ε
Tactic: simp_rw [← smul_eq_mul, Complex.exp_eq_exp_ℂ]
-- Lean 4 proof step from Mathlib.Probability.Moments.ComplexMGF (goal)
Goal:
Ω : 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 : ℝ := min (z.re - l) (u - z.re) / 2
h_pos : 0 < min (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 ω) : ℂ))) ε
have h : (↑(X ω) : ℂ) • NormedSpace.exp (ε • (↑(X ω) : ℂ)) = NormedSpace.exp (ε • (↑(X ω) : ℂ)) * (↑(X ω) : ℂ)
Tactic: convert! hasDerivAt_exp_smul_const (X ω : ℂ) ε using 1
-- Lean 4 proof step from Mathlib.Probability.Moments.ComplexMGF (goal)
Goal:
Ω : 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 : ℝ := min (z.re - l) (u - z.re) / 2
h_pos : 0 < min (z.re - l) (u - z.re)
ht : 0 < t
ω : Ω
ε : ℂ
hε : ε ∈ Metric.ball z (t / 2)
⊢ (↑(X ω) : ℂ) • NormedSpace.exp (ε • (↑(X ω) : ℂ)) = NormedSpace.exp (ε • (↑(X ω) : ℂ)) * (↑(X ω) : ℂ)
have h : (↑(X ω) : ℂ) * NormedSpace.exp (ε • (↑(X ω) : ℂ)) = NormedSpace.exp (ε • (↑(X ω) : ℂ)) * (↑(X ω) : ℂ)
Tactic: rw [smul_eq_mul, mul_comm]
-- Lean 4 proof step from Mathlib.Probability.Moments.ComplexMGF (goal)
Goal:
Ω : 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 : ℝ := min (z.re - l) (u - z.re) / 2
h_pos : 0 < min (z.re - l) (u - z.re)
ht : 0 < t
ω : Ω
ε : ℂ
hε : ε ∈ Metric.ball z (t / 2)
h : (↑(X ω) : ℂ) * NormedSpace.exp (ε • (↑(X ω) : ℂ)) = NormedSpace.exp (ε • (↑(X ω) : ℂ)) * (↑(X ω) : ℂ)
⊢ (↑(X ω) : ℂ) • NormedSpace.exp (ε • (↑(X ω) : ℂ)) = NormedSpace.exp (ε • (↑(X ω) : ℂ)) * (↑(X ω) : ℂ)
have h₁ : NormedSpace.exp (ε • (↑(X ω) : ℂ)) * (↑(X ω) : ℂ) = NormedSpace.exp (ε • (↑(X ω) : ℂ)) * (↑(X ω) : ℂ)
Tactic: rw [smul_eq_mul, mul_comm]
-- Lean 4 proof step from Mathlib.Probability.Moments.ComplexMGF (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
⊢ HasDerivAt (complexMGF X μ) (∫ (x : Ω), (fun (ω : Ω) ↦ (↑(X ω) : ℂ) * cexp (z * (↑(X ω) : ℂ))) x ∂μ) z
have h : ∀ (x : ℂ),
  complexMGF X μ x = ∫ (x_1 : Ω), (fun (ω : Ω) ↦ HPow.hPow (β := ℕ) (↑(X ω) : ℂ) 0 * cexp (x * (↑(X ω) : ℂ))) x_1 ∂μ
Tactic: convert! hasDerivAt_integral_pow_mul_exp hz 0
-- Lean 4 proof step from Mathlib.Probability.Moments.ComplexMGF (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
h :
  ∀ (x : ℂ),
    complexMGF X μ x = ∫ (x_1 : Ω), (fun (ω : Ω) ↦ HPow.hPow (β := ℕ) (↑(X ω) : ℂ) 0 * cexp (x * (↑(X ω) : ℂ))) x_1 ∂μ
⊢ HasDerivAt (complexMGF X μ) (∫ (x : Ω), (fun (ω : Ω) ↦ (↑(X ω) : ℂ) * cexp (z * (↑(X ω) : ℂ))) x ∂μ) z
have h₁ : ∀ (x x : Ω), (↑(X x) : ℂ) = (↑(X x) : ℂ) ^ HAdd.hAdd (α := ℕ) 0 1
Tactic: convert! hasDerivAt_integral_pow_mul_exp hz 0
-- Lean 4 proof step from Mathlib.Probability.Moments.ComplexMGF (hypothesis)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : Membership.mem (γ := Set ℂ) {z : ℂ | z.re ∈ interior (integrableExpSet X μ)} z
⊢ DifferentiableWithinAt ℂ (complexMGF X μ) {z : ℂ | z.re ∈ interior (integrableExpSet X μ)} z
have h : HasDerivAt (complexMGF X μ) (∫ (x : Ω), (fun (ω : Ω) ↦ (↑(X ω) : ℂ) * cexp (z * (↑(X ω) : ℂ))) x ∂μ) z
Tactic: have h := hasDerivAt_complexMGF hz
-- Lean 4 proof step from Mathlib.Probability.Moments.ComplexMGF (hypothesis)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : Membership.mem (γ := Set ℂ) {z : ℂ | z.re ∈ interior (integrableExpSet X μ)} z
h : HasDerivAt (complexMGF X μ) (∫ (x : Ω), (fun (ω : Ω) ↦ (↑(X ω) : ℂ) * cexp (z * (↑(X ω) : ℂ))) x ∂μ) z
⊢ DifferentiableWithinAt ℂ (complexMGF X μ) {z : ℂ | z.re ∈ interior (integrableExpSet X μ)} z
have h₁ : HasFDerivAt (complexMGF X μ)
  (ContinuousLinearMap.toSpanSingleton ℂ (∫ (x : Ω), (fun (ω : Ω) ↦ (↑(X ω) : ℂ) * cexp (z * (↑(X ω) : ℂ))) x ∂μ)) z
Tactic: rw [hasDerivAt_iff_hasFDerivAt] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Probability.Moments.ComplexMGF (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
n : ℕ
hn :
  ∀ {z : ℂ} (hz : z.re ∈ interior (integrableExpSet X μ)),
    HasDerivAt (iteratedDeriv n (complexMGF X μ))
      (∫ (x : Ω), (fun (ω : Ω) ↦ (↑(X ω) : ℂ) ^ (n + 1) * cexp (z * (↑(X ω) : ℂ))) x ∂μ) z
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
⊢ HasDerivAt (iteratedDeriv (n + 1) (complexMGF X μ))
    (∫ (x : Ω), (fun (ω : Ω) ↦ (↑(X ω) : ℂ) ^ (n + 1 + 1) * cexp (z * (↑(X ω) : ℂ))) x ∂μ) z
have succ : HasDerivAt (deriv (iteratedDeriv n (complexMGF X μ)))
  (∫ (x : Ω), (fun (ω : Ω) ↦ (↑(X ω) : ℂ) ^ (n + 1 + 1) * cexp (z * (↑(X ω) : ℂ))) x ∂μ) z
Tactic: rw [iteratedDeriv_succ]
-- Lean 4 proof step from Mathlib.Probability.Moments.ComplexMGF (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
n : ℕ
hn :
  ∀ {z : ℂ} (hz : z.re ∈ interior (integrableExpSet X μ)),
    HasDerivAt (iteratedDeriv n (complexMGF X μ))
      (∫ (x : Ω), (fun (ω : Ω) ↦ (↑(X ω) : ℂ) ^ (n + 1) * cexp (z * (↑(X ω) : ℂ))) x ∂μ) z
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
⊢ ∀ᶠ (y : ℂ) in 𝓝 z, y.re ∈ interior (integrableExpSet X μ)
have refine : IsOpen (X := ℂ) fun (y : ℂ) ↦ interior (integrableExpSet X μ) y.re
Tactic: refine IsOpen.eventually_mem ?_ hz
-- Lean 4 proof step from Mathlib.Probability.Moments.ComplexMGF (hypothesis)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
n : ℕ
hn :
  ∀ {z : ℂ} (hz : z.re ∈ interior (integrableExpSet X μ)),
    HasDerivAt (iteratedDeriv n (complexMGF X μ))
      (∫ (x : Ω), (fun (ω : Ω) ↦ (↑(X ω) : ℂ) ^ (n + 1) * cexp (z * (↑(X ω) : ℂ))) x ∂μ) z
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
⊢ deriv (iteratedDeriv n (complexMGF X μ)) =ᶠ[𝓝 z] fun (z : ℂ) ↦
    ∫ (x : Ω), (fun (ω : Ω) ↦ (↑(X ω) : ℂ) ^ (n + 1) * cexp (z * (↑(X ω) : ℂ))) x ∂μ
have h_mem : ∀ᶠ (y : ℂ) in 𝓝 z, y.re ∈ interior (integrableExpSet X μ)
Tactic: have h_mem : ∀ᶠ y in 𝓝 z, y.re ∈ interior (integrableExpSet X μ) := by
        refine IsOpen.eventually_mem ?_ hz
        exact isOpen_interior.preimage Complex.continuous_re
-- Lean 4 proof step from Mathlib.Probability.Moments.ComplexMGF (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
n : ℕ
hn :
  ∀ {z : ℂ} (hz : z.re ∈ interior (integrableExpSet X μ)),
    HasDerivAt (iteratedDeriv n (complexMGF X μ))
      (∫ (x : Ω), (fun (ω : Ω) ↦ (↑(X ω) : ℂ) ^ (n + 1) * cexp (z * (↑(X ω) : ℂ))) x ∂μ) z
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
h_mem : ∀ᶠ (y : ℂ) in 𝓝 z, y.re ∈ interior (integrableExpSet X μ)
⊢ deriv (iteratedDeriv n (complexMGF X μ)) =ᶠ[𝓝 z] fun (z : ℂ) ↦
    ∫ (x : Ω), (fun (ω : Ω) ↦ (↑(X ω) : ℂ) ^ (n + 1) * cexp (z * (↑(X ω) : ℂ))) x ∂μ
have h : ∀ (a : ℂ),
  Membership.mem (γ := Set ℂ)
    {x : ℂ |
      Membership.mem (γ := Set ℂ) {x : ℂ | (fun (y : ℂ) ↦ y.re ∈ interior (integrableExpSet X μ)) x} x →
        Membership.mem (γ := Set ℂ)
          {x : ℂ |
            (fun (x : ℂ) ↦
                deriv (iteratedDeriv n (complexMGF X μ)) x =
                  (fun (z : ℂ) ↦ (∫ (x : Ω), (fun (ω : Ω) ↦ (↑(X ω) : ℂ) ^ (n + 1) * cexp (z * (↑(X ω) : ℂ))) x ∂μ : ℂ))
                    x)
              x}
          x}
    a
Tactic: filter_upwards [h_mem] with y hy using HasDerivAt.deriv (hn hy)
-- Lean 4 proof step from Mathlib.Probability.Moments.ComplexMGF (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
n : ℕ
hn :
  ∀ {z : ℂ} (hz : z.re ∈ interior (integrableExpSet X μ)),
    HasDerivAt (iteratedDeriv n (complexMGF X μ))
      (∫ (x : Ω), (fun (ω : Ω) ↦ (↑(X ω) : ℂ) ^ (n + 1) * cexp (z * (↑(X ω) : ℂ))) x ∂μ) z
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
h_mem : ∀ᶠ (y : ℂ) in 𝓝 z, y.re ∈ interior (integrableExpSet X μ)
h :
  ∀ (a : ℂ),
    Membership.mem (γ := Set ℂ)
      {x : ℂ |
        Membership.mem (γ := Set ℂ) {x : ℂ | (fun (y : ℂ) ↦ y.re ∈ interior (integrableExpSet X μ)) x} x →
          Membership.mem (γ := Set ℂ)
            {x : ℂ |
              (fun (x : ℂ) ↦
                  deriv (iteratedDeriv n (complexMGF X μ)) x =
                    (fun (z : ℂ) ↦
                        (∫ (x : Ω), (fun (ω : Ω) ↦ (↑(X ω) : ℂ) ^ (n + 1) * cexp (z * (↑(X ω) : ℂ))) x ∂μ : ℂ))
                      x)
                x}
            x}
      a
⊢ deriv (iteratedDeriv n (complexMGF X μ)) =ᶠ[𝓝 z] fun (z : ℂ) ↦
    ∫ (x : Ω), (fun (ω : Ω) ↦ (↑(X ω) : ℂ) ^ (n + 1) * cexp (z * (↑(X ω) : ℂ))) x ∂μ
have h₁ : ∀ (a : ℂ),
  a.re ∈ interior (integrableExpSet X μ) →
    deriv (iteratedDeriv n (complexMGF X μ)) a = ∫ (x : Ω), (↑(X x) : ℂ) ^ (n + 1) * cexp (a * (↑(X x) : ℂ)) ∂μ
Tactic: filter_upwards [h_mem] with y hy using HasDerivAt.deriv (hn hy)
-- Lean 4 proof step from Mathlib.Probability.Moments.ComplexMGF (hypothesis)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
n : ℕ
hn :
  ∀ {z : ℂ} (hz : z.re ∈ interior (integrableExpSet X μ)),
    HasDerivAt (iteratedDeriv n (complexMGF X μ))
      (∫ (x : Ω), (fun (ω : Ω) ↦ (↑(X ω) : ℂ) ^ (n + 1) * cexp (z * (↑(X ω) : ℂ))) x ∂μ) z
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
⊢ HasDerivAt (deriv (iteratedDeriv n (complexMGF X μ)))
    (∫ (x : Ω), (fun (ω : Ω) ↦ (↑(X ω) : ℂ) ^ (n + 1 + 1) * cexp (z * (↑(X ω) : ℂ))) x ∂μ) z
have this : deriv (iteratedDeriv n (complexMGF X μ)) =ᶠ[𝓝 z] fun (z : ℂ) ↦
  ∫ (x : Ω), (fun (ω : Ω) ↦ (↑(X ω) : ℂ) ^ (n + 1) * cexp (z * (↑(X ω) : ℂ))) x ∂μ
Tactic: have : deriv (iteratedDeriv n (complexMGF X μ))
        =ᶠ[𝓝 z] fun z ↦ μ[fun ω ↦ X ω ^ (n + 1) * cexp (z * X ω)] := by
      have h_mem : ∀ᶠ y in 𝓝 z, y.re ∈ interior (integrableExpSet X μ) := by
        refine IsOpen.eventually_mem ?_ hz
        exact isOpen_interior.preimage Complex.continuous_re
      filter_upwards [h_mem] with y hy using HasDerivAt.deriv (hn hy)
-- Lean 4 proof step from Mathlib.Probability.Moments.ComplexMGF (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
n : ℕ
hn :
  ∀ {z : ℂ} (hz : z.re ∈ interior (integrableExpSet X μ)),
    HasDerivAt (iteratedDeriv n (complexMGF X μ))
      (∫ (x : Ω), (fun (ω : Ω) ↦ (↑(X ω) : ℂ) ^ (n + 1) * cexp (z * (↑(X ω) : ℂ))) x ∂μ) z
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
this :
  deriv (iteratedDeriv n (complexMGF X μ)) =ᶠ[𝓝 z] fun (z : ℂ) ↦
    ∫ (x : Ω), (fun (ω : Ω) ↦ (↑(X ω) : ℂ) ^ (n + 1) * cexp (z * (↑(X ω) : ℂ))) x ∂μ
⊢ HasDerivAt (deriv (iteratedDeriv n (complexMGF X μ)))
    (∫ (x : Ω), (fun (ω : Ω) ↦ (↑(X ω) : ℂ) ^ (n + 1 + 1) * cexp (z * (↑(X ω) : ℂ))) x ∂μ) z
have succ : HasDerivAt (F := ℂ) (fun (z : ℂ) ↦ ∫ (x : Ω), (fun (ω : Ω) ↦ (↑(X ω) : ℂ) ^ (n + 1) * cexp (z * (↑(X ω) : ℂ))) x ∂μ)
  (∫ (x : Ω), (fun (ω : Ω) ↦ (↑(X ω) : ℂ) ^ (n + 1 + 1) * cexp (z * (↑(X ω) : ℂ))) x ∂μ) z
Tactic: rw [EventuallyEq.hasDerivAt_iff this]
-- Lean 4 proof step from Mathlib.Probability.Moments.ComplexMGF (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
⊢ HasDerivAt (iteratedDeriv n (complexMGF X μ))
    (∫ (x : Ω), (fun (ω : Ω) ↦ (↑(X ω) : ℂ) ^ (n + 1) * cexp (z * (↑(X ω) : ℂ))) x ∂μ) z
have zero : ∀ {z : ℂ} (hz : z.re ∈ interior (integrableExpSet X μ)),
  HasDerivAt (iteratedDeriv 0 (complexMGF X μ))
    (∫ (x : Ω), (fun (ω : Ω) ↦ (↑(X ω) : ℂ) ^ HAdd.hAdd (α := ℕ) 0 1 * cexp (z * (↑(X ω) : ℂ))) x ∂μ) z
Tactic: induction n generalizing z with
  | zero => simp [hasDerivAt_complexMGF hz]
  | succ n hn =>
    rw [iteratedDeriv_succ]
    have : deriv (iteratedDeriv n (complexMGF X μ))
        =ᶠ[𝓝 z] fun z ↦ μ[fun ω ↦ X ω ^ (n + 1) * cexp (z * X ω)] := by
      have h_mem : ∀ᶠ y in 𝓝 z, y.re ∈ interior (integrableExpSet X μ) := by
        refine IsOpen.eventually_mem ?_ hz
        exact isOpen_interior.preimage Complex.continuous_re
      filter_upwards [h_mem] with y hy using HasDerivAt.deriv (hn hy)
    rw [EventuallyEq.hasDerivAt_iff this]
    exact hasDerivAt_integral_pow_mul_exp hz (n + 1)
Cleared hypotheses: z, hz, n