awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace ℝ E
inst_5 : NormedSpace 𝕜 F
inst_6 : NormedSpace ℝ F
inst_7 : CompleteSpace E
inst_8 : CompleteSpace F
inst_9 : MeasurableSpace E
μ : Measure E
h : Integrable id μ
L : E →L[𝕜] F
⊢ Eq.{u_3 + 1} (α := F) (∫ (x : E), (L : (a : E) → F) x ∂μ : F) ((L : (a : E) → F) (∫ (x : E), id x ∂μ) : F)
have change : Eq.{u_3 + 1} (α := F) (∫ (x : E), (L : (a : E) → F) (id x) ∂μ : F) ((L : (a : E) → F) (∫ (x : E), id x ∂μ) : F)
Tactic: change ∫ x, L (id x) ∂μ = _
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace ℝ E
inst_5 : NormedSpace 𝕜 F
inst_6 : NormedSpace ℝ F
inst_7 : CompleteSpace E
inst_8 : CompleteSpace F
inst_9 : MeasurableSpace E
μ : Measure E
h : Integrable id μ
L : E →L[𝕜] F
⊢ Eq.{u_3 + 1} (α := F) (∫ (x : E), (L : (a : E) → F) (id x) ∂μ : F) ((L : (a : E) → F) (∫ (x : E), id x ∂μ) : F)
have rw : Eq.{u_3 + 1} (α := F) ((L : (a : E) → F) (∫ (x : E), id x ∂μ) : F) ((L : (a : E) → F) (∫ (x : E), id x ∂μ) : F)
Tactic: rw [L.integral_comp_comm h]
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace ℝ E
inst_5 : NormedSpace 𝕜 F
inst_6 : NormedSpace ℝ F
inst_7 : CompleteSpace E
inst_8 : CompleteSpace F
inst_9 : MeasurableSpace E
μ : Measure E
inst_10 : OpensMeasurableSpace E
inst_11 : MeasurableSpace F
inst_12 : BorelSpace F
inst_13 : SecondCountableTopology F
h : Integrable id μ
L : E →L[𝕜] F
⊢ Eq.{u_3 + 1} (α := F) (@integral _ _ _ _ inst_11 (Measure.map (⇑L : (a : E) → F) μ) fun (x : F) ↦ x : F)
    ((L : (a : E) → F) (∫ (x : E), x ∂μ) : F)
have rw : Eq.{u_3 + 1} (α := F) (∫ (x : E), (L : (a : E) → F) x ∂μ : F) ((L : (a : E) → F) (∫ (x : E), x ∂μ) : F)
Tactic: rw [integral_map (by fun_prop) (by fun_prop)]
-- Lean 4 proof step from Mathlib.Probability.Moments.ComplexMGF (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hX : AEMeasurable X μ
h : ¬Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (z.re * X ω)) μ
⊢ complexMGF X μ z = 0
have rw : ¬Integrable (ε := ℂ) (fun (ω : Ω) ↦ cexp (z * (↑(X ω) : ℂ))) μ
Tactic: rw [complexMGF, integral_undef]
-- Lean 4 proof step from Mathlib.Probability.Moments.ComplexMGF (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hX : AEMeasurable X μ
h : ¬Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (z.re * X ω)) μ
⊢ ¬Integrable (ε := ℂ) (fun (ω : Ω) ↦ cexp (z * (↑(X ω) : ℂ))) μ
have rw : ¬Integrable (ε := ℝ) (fun (a : Ω) ↦ ‖cexp (z * (↑(X a) : ℂ))‖) μ
Tactic: rw [← integrable_norm_iff (by fun_prop)]
-- Lean 4 proof step from Mathlib.Probability.Moments.ComplexMGF (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hX : AEMeasurable X μ
⊢ complexMGF (m := Real.measurableSpace) id (Measure.map X μ) = complexMGF X μ
have h : ∀ (t : ℂ), complexMGF (m := Real.measurableSpace) id (Measure.map X μ) t = complexMGF X μ t
Tactic: ext t
-- Lean 4 proof step from Mathlib.Probability.Moments.ComplexMGF (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hX : AEMeasurable X μ
t : ℂ
⊢ complexMGF (m := Real.measurableSpace) id (Measure.map X μ) t = complexMGF X μ t
have h : ∫ (x : Ω), cexp (t * (↑(id (X x)) : ℂ)) ∂μ = complexMGF X μ t
Tactic: rw [complexMGF, integral_map hX]
-- Lean 4 proof step from Mathlib.Probability.Moments.ComplexMGF (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hX : AEMeasurable X μ
t : ℂ
h : ∫ (x : Ω), cexp (t * (↑(id (X x)) : ℂ)) ∂μ = complexMGF X μ t
⊢ complexMGF (m := Real.measurableSpace) id (Measure.map X μ) t = complexMGF X μ t
have h₁ : AEStronglyMeasurable (β := ℂ) (m₀ := Real.measurableSpace) (fun (ω : ℝ) ↦ cexp (t * (↑(id ω) : ℂ))) (Measure.map X μ)
Tactic: rw [complexMGF, integral_map hX]
-- Lean 4 proof step from Mathlib.Probability.Moments.ComplexMGF (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
μ' : Measure Ω'
Y : Ω' → ℝ
h : IdentDistrib X Y μ μ'
⊢ complexMGF X μ = complexMGF Y μ'
have rw : complexMGF (m := Real.measurableSpace) id (Measure.map X μ) = complexMGF Y μ'
Tactic: rw [← complexMGF_id_map h.aemeasurable_fst, ← complexMGF_id_map h.aemeasurable_snd, h.map_eq]
-- Lean 4 proof step from Mathlib.Probability.Moments.ComplexMGF (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
μ' : Measure Ω'
Y : Ω' → ℝ
h : IdentDistrib X Y μ μ'
rw : complexMGF (m := Real.measurableSpace) id (Measure.map X μ) = complexMGF Y μ'
⊢ complexMGF X μ = complexMGF Y μ'
have rw₁ : complexMGF (m := Real.measurableSpace) id (Measure.map X μ) =
  complexMGF (m := Real.measurableSpace) id (Measure.map Y μ')
Tactic: rw [← complexMGF_id_map h.aemeasurable_fst, ← complexMGF_id_map h.aemeasurable_snd, h.map_eq]
-- Lean 4 proof step from Mathlib.Probability.Moments.ComplexMGF (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
μ' : Measure Ω'
Y : Ω' → ℝ
h : IdentDistrib X Y μ μ'
rw : complexMGF (m := Real.measurableSpace) id (Measure.map X μ) = complexMGF Y μ'
rw₁ :
  complexMGF (m := Real.measurableSpace) id (Measure.map X μ) =
    complexMGF (m := Real.measurableSpace) id (Measure.map Y μ')
⊢ complexMGF X μ = complexMGF Y μ'
have rw₂ : complexMGF (m := Real.measurableSpace) id (Measure.map Y μ') =
  complexMGF (m := Real.measurableSpace) id (Measure.map Y μ')
Tactic: rw [← complexMGF_id_map h.aemeasurable_fst, ← complexMGF_id_map h.aemeasurable_snd, h.map_eq]
-- Lean 4 proof step from Mathlib.Probability.Moments.ComplexMGF (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
⊢ ‖complexMGF X μ z‖ ≤ mgf X μ z.re
have rw : Norm.norm (E := ℂ) (∫ (ω : Ω), cexp (((↑z.re : ℂ) + (↑z.im : ℂ) * I) * (↑(X ω) : ℂ)) ∂μ) ≤
  mgf X μ ((↑z.re : ℂ) + (↑z.im : ℂ) * I).re
Tactic: rw [complexMGF, ← re_add_im z]
-- Lean 4 proof step from Mathlib.Probability.Moments.ComplexMGF (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
⊢ Norm.norm (E := ℂ) (∫ (ω : Ω), cexp (((↑z.re : ℂ) + (↑z.im : ℂ) * I) * (↑(X ω) : ℂ)) ∂μ) ≤
    mgf X μ ((↑z.re : ℂ) + (↑z.im : ℂ) * I).re
have simp_rw : Norm.norm (E := ℂ) (∫ (ω : Ω), cexp ((↑z.re : ℂ) * (↑(X ω) : ℂ)) * cexp ((↑z.im : ℂ) * I * (↑(X ω) : ℂ)) ∂μ) ≤
  mgf X μ z.re
Tactic: simp_rw [add_mul, Complex.exp_add, re_add_im]
-- Lean 4 proof step from Mathlib.Probability.Moments.ComplexMGF (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
⊢ Norm.norm (E := ℂ) (∫ (ω : Ω), cexp ((↑z.re : ℂ) * (↑(X ω) : ℂ)) * cexp ((↑z.im : ℂ) * I * (↑(X ω) : ℂ)) ∂μ) ≤
    mgf X μ z.re
have calc : Eq (α := ℝ) (∫ (ω : Ω), ‖cexp ((↑z.re : ℂ) * (↑(X ω) : ℂ)) * cexp ((↑z.im : ℂ) * I * (↑(X ω) : ℂ))‖ ∂μ)
  (∫ (ω : Ω), rexp (z.re * X ω) ∂μ)
Tactic: calc ‖∫ ω, cexp (z.re * X ω) * cexp (z.im * I * X ω) ∂μ‖
  _ ≤ ∫ ω, ‖cexp (z.re * X ω) * cexp (z.im * I * X ω)‖ ∂μ := norm_integral_le_integral_norm _
  _ = ∫ ω, rexp (z.re * X ω) ∂μ := by simp [Complex.norm_exp]
-- Lean 4 proof step from Mathlib.Probability.Moments.ComplexMGF (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
x : ℝ
⊢ ∫ (ω : Ω), cexp ((↑x : ℂ) * (↑(X ω) : ℂ)) ∂μ = (↑(∫ (x_1 : Ω), (fun (ω : Ω) ↦ rexp (x * X ω)) x_1 ∂μ) : ℂ)
have norm_cast : Eq (α := ℝ) (∫ (x_1 : Ω), rexp (x * X x_1) ∂μ) (∫ (x_1 : Ω), (fun (x_2 : Ω) ↦ rexp (x * X x_2)) x_1 ∂μ)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Probability.Moments.ComplexMGF (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
⊢ (fun (x : ℝ) ↦ (complexMGF X μ (↑x : ℂ)).re) = mgf X μ
have h : ∀ (x : ℝ), (complexMGF X μ (↑x : ℂ)).re = mgf X μ x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Probability.Moments.ComplexMGF (goal)
Goal:
μ : Measure ℝ
t : ℝ
⊢ complexMGF id μ ((↑t : ℂ) * I) = charFun μ t
have simp : Eq (α := ℂ) (∫ (ω : ℝ), cexp ((↑t : ℂ) * I * (↑ω : ℂ)) ∂μ) (∫ (x : ℝ), cexp ((↑t : ℂ) * (↑x : ℂ) * I) ∂μ)
Tactic: simp only [complexMGF, id_eq, charFun, RCLike.inner_apply, conj_trivial, ofReal_mul]
-- Lean 4 proof step from Mathlib.Probability.Moments.ComplexMGF (goal)
Goal:
μ : Measure ℝ
t : ℝ
⊢ Eq (α := ℂ) (∫ (ω : ℝ), cexp ((↑t : ℂ) * I * (↑ω : ℂ)) ∂μ) (∫ (x : ℝ), cexp ((↑t : ℂ) * (↑x : ℂ) * I) ∂μ)
have e_f : ∀ (x : ℝ), cexp ((↑t : ℂ) * I * (↑x : ℂ)) = cexp ((↑t : ℂ) * (↑x : ℂ) * I)
Tactic: congr with x
-- Lean 4 proof step from Mathlib.Probability.Moments.ComplexMGF (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hX : AEMeasurable X μ
t : ℝ
⊢ complexMGF X μ ((↑t : ℂ) * I) = charFun (mE := Real.measurableSpace) (Measure.map X μ) t
have rw : complexMGF (m := Real.measurableSpace) id (Measure.map X μ) ((↑t : ℂ) * I) =
  charFun (mE := Real.measurableSpace) (Measure.map X μ) t
Tactic: rw [← complexMGF_id_map hX, complexMGF_id_mul_I]
-- Lean 4 proof step from Mathlib.Probability.Moments.ComplexMGF (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hX : AEMeasurable X μ
t : ℝ
rw :
  complexMGF (m := Real.measurableSpace) id (Measure.map X μ) ((↑t : ℂ) * I) =
    charFun (mE := Real.measurableSpace) (Measure.map X μ) t
⊢ complexMGF X μ ((↑t : ℂ) * I) = charFun (mE := Real.measurableSpace) (Measure.map X μ) t
have rw₁ : charFun (mE := Real.measurableSpace) (Measure.map X μ) t = charFun (mE := Real.measurableSpace) (Measure.map X μ) t
Tactic: rw [← complexMGF_id_map hX, complexMGF_id_mul_I]
-- 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 : ℕ
⊢ HasDerivAt (F := ℂ) (fun (z : ℂ) ↦ ∫ (x : Ω), (fun (ω : Ω) ↦ (↑(X ω) : ℂ) ^ n * cexp (z * (↑(X ω) : ℂ))) x ∂μ)
    (∫ (x : Ω), (fun (ω : Ω) ↦ (↑(X ω) : ℂ) ^ (n + 1) * cexp (z * (↑(X ω) : ℂ))) x ∂μ) z
have hX : AEMeasurable X μ
Tactic: have hX : AEMeasurable X μ := aemeasurable_of_mem_interior_integrableExpSet hz
-- 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 μ
hz' : z.re ∈ interior (integrableExpSet X μ)
⊢ HasDerivAt (F := ℂ) (fun (z : ℂ) ↦ ∫ (x : Ω), (fun (ω : Ω) ↦ (↑(X ω) : ℂ) ^ n * cexp (z * (↑(X ω) : ℂ))) x ∂μ)
    (∫ (x : Ω), (fun (ω : Ω) ↦ (↑(X ω) : ℂ) ^ (n + 1) * cexp (z * (↑(X ω) : ℂ))) x ∂μ) z
have hz'₁ : ∃ (l : ℝ) (u : ℝ), z.re ∈ Set.Ioo l u ∧ Set.Ioo l u ⊆ integrableExpSet X μ
Tactic: rw [mem_interior_iff_mem_nhds, mem_nhds_iff_exists_Ioo_subset] at hz'
Cleared hypotheses: hz'
-- 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 μ
hz' : ∃ (l : ℝ) (u : ℝ), z.re ∈ Set.Ioo l u ∧ Set.Ioo l u ⊆ integrableExpSet X μ
⊢ HasDerivAt (F := ℂ) (fun (z : ℂ) ↦ ∫ (x : Ω), (fun (ω : Ω) ↦ (↑(X ω) : ℂ) ^ n * cexp (z * (↑(X ω) : ℂ))) x ∂μ)
    (∫ (x : Ω), (fun (ω : Ω) ↦ (↑(X ω) : ℂ) ^ (n + 1) * cexp (z * (↑(X ω) : ℂ))) x ∂μ) z
have obtain : ∀ (l u : ℝ) (hlu : z.re ∈ Set.Ioo l u) (h_subset : Set.Ioo l u ⊆ integrableExpSet X μ),
  HasDerivAt (F := ℂ) (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'
Cleared hypotheses: hz'
-- 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
⊢ HasDerivAt (F := ℂ) (fun (z : ℂ) ↦ ∫ (x : Ω), (fun (ω : Ω) ↦ (↑(X ω) : ℂ) ^ n * cexp (z * (↑(X ω) : ℂ))) x ∂μ)
    (∫ (x : Ω), (fun (ω : Ω) ↦ (↑(X ω) : ℂ) ^ (n + 1) * cexp (z * (↑(X ω) : ℂ))) x ∂μ) z
have h_pos : 0 < min (z.re - l) (u - z.re)
Tactic: have h_pos : 0 < (z.re - l) ⊓ (u - z.re) := by simp [hlu.1, hlu.2]
-- 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)
⊢ HasDerivAt (F := ℂ) (fun (z : ℂ) ↦ ∫ (x : Ω), (fun (ω : Ω) ↦ (↑(X ω) : ℂ) ^ n * cexp (z * (↑(X ω) : ℂ))) x ∂μ)
    (∫ (x : Ω), (fun (ω : Ω) ↦ (↑(X ω) : ℂ) ^ (n + 1) * cexp (z * (↑(X ω) : ℂ))) x ∂μ) z
have ht : 0 < t
Tactic: have ht : 0 < t := half_pos h_pos
-- 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
⊢ HasDerivAt (F := ℂ) (fun (z : ℂ) ↦ ∫ (x : Ω), (fun (ω : Ω) ↦ (↑(X ω) : ℂ) ^ n * cexp (z * (↑(X ω) : ℂ))) x ∂μ)
    (∫ (x : Ω), (fun (ω : Ω) ↦ (↑(X ω) : ℂ) ^ (n + 1) * cexp (z * (↑(X ω) : ℂ))) x ∂μ) z
have refine_1 : ∀ᶠ (x : ℂ) in 𝓝 z,
  AEStronglyMeasurable (β := ℂ) ((fun (z : ℂ) (ω : Ω) ↦ (↑(X ω) : ℂ) ^ n * cexp (z * (↑(X ω) : ℂ))) x) μ
Tactic: refine (hasDerivAt_integral_of_dominated_loc_of_deriv_le
    (bound := fun ω ↦ |X ω| ^ (n + 1) * rexp (z.re * X ω + t / 2 * |X ω|))
    (F := fun z ω ↦ X ω ^ n * cexp (z * X ω))
    (F' := fun z ω ↦ X ω ^ (n + 1) * cexp (z * X ω)) (Metric.ball_mem_nhds _ (half_pos ht))
    ?_ ?_ ?_ ?_ ?_ ?_).2
-- 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_1 :
  ∀ᶠ (x : ℂ) in 𝓝 z,
    AEStronglyMeasurable (β := ℂ) ((fun (z : ℂ) (ω : Ω) ↦ (↑(X ω) : ℂ) ^ n * cexp (z * (↑(X ω) : ℂ))) x) μ
⊢ HasDerivAt (F := ℂ) (fun (z : ℂ) ↦ ∫ (x : Ω), (fun (ω : Ω) ↦ (↑(X ω) : ℂ) ^ n * cexp (z * (↑(X ω) : ℂ))) x ∂μ)
    (∫ (x : Ω), (fun (ω : Ω) ↦ (↑(X ω) : ℂ) ^ (n + 1) * cexp (z * (↑(X ω) : ℂ))) x ∂μ) z
have refine_2 : Integrable (ε := ℂ) ((fun (z : ℂ) (ω : Ω) ↦ (↑(X ω) : ℂ) ^ n * cexp (z * (↑(X ω) : ℂ))) z) μ
Tactic: refine (hasDerivAt_integral_of_dominated_loc_of_deriv_le
    (bound := fun ω ↦ |X ω| ^ (n + 1) * rexp (z.re * X ω + t / 2 * |X ω|))
    (F := fun z ω ↦ X ω ^ n * cexp (z * X ω))
    (F' := fun z ω ↦ X ω ^ (n + 1) * cexp (z * X ω)) (Metric.ball_mem_nhds _ (half_pos ht))
    ?_ ?_ ?_ ?_ ?_ ?_).2
-- 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_1 :
  ∀ᶠ (x : ℂ) in 𝓝 z,
    AEStronglyMeasurable (β := ℂ) ((fun (z : ℂ) (ω : Ω) ↦ (↑(X ω) : ℂ) ^ n * cexp (z * (↑(X ω) : ℂ))) x) μ
refine_2 : Integrable (ε := ℂ) ((fun (z : ℂ) (ω : Ω) ↦ (↑(X ω) : ℂ) ^ n * cexp (z * (↑(X ω) : ℂ))) z) μ
⊢ HasDerivAt (F := ℂ) (fun (z : ℂ) ↦ ∫ (x : Ω), (fun (ω : Ω) ↦ (↑(X ω) : ℂ) ^ n * cexp (z * (↑(X ω) : ℂ))) x ∂μ)
    (∫ (x : Ω), (fun (ω : Ω) ↦ (↑(X ω) : ℂ) ^ (n + 1) * cexp (z * (↑(X ω) : ℂ))) x ∂μ) z
have refine_3 : AEStronglyMeasurable (β := ℂ) ((fun (z : ℂ) (ω : Ω) ↦ (↑(X ω) : ℂ) ^ (n + 1) * cexp (z * (↑(X ω) : ℂ))) z) μ
Tactic: refine (hasDerivAt_integral_of_dominated_loc_of_deriv_le
    (bound := fun ω ↦ |X ω| ^ (n + 1) * rexp (z.re * X ω + t / 2 * |X ω|))
    (F := fun z ω ↦ X ω ^ n * cexp (z * X ω))
    (F' := fun z ω ↦ X ω ^ (n + 1) * cexp (z * X ω)) (Metric.ball_mem_nhds _ (half_pos ht))
    ?_ ?_ ?_ ?_ ?_ ?_).2
-- 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_1 :
  ∀ᶠ (x : ℂ) in 𝓝 z,
    AEStronglyMeasurable (β := ℂ) ((fun (z : ℂ) (ω : Ω) ↦ (↑(X ω) : ℂ) ^ n * cexp (z * (↑(X ω) : ℂ))) x) μ
refine_2 : Integrable (ε := ℂ) ((fun (z : ℂ) (ω : Ω) ↦ (↑(X ω) : ℂ) ^ n * cexp (z * (↑(X ω) : ℂ))) z) μ
refine_3 : AEStronglyMeasurable (β := ℂ) ((fun (z : ℂ) (ω : Ω) ↦ (↑(X ω) : ℂ) ^ (n + 1) * cexp (z * (↑(X ω) : ℂ))) z) μ
⊢ HasDerivAt (F := ℂ) (fun (z : ℂ) ↦ ∫ (x : Ω), (fun (ω : Ω) ↦ (↑(X ω) : ℂ) ^ n * cexp (z * (↑(X ω) : ℂ))) x ∂μ)
    (∫ (x : Ω), (fun (ω : Ω) ↦ (↑(X ω) : ℂ) ^ (n + 1) * cexp (z * (↑(X ω) : ℂ))) x ∂μ) z
have refine_4 : ∀ᵐ (a : Ω) ∂μ,
  ∀ x ∈ Metric.ball z (t / 2),
    Norm.norm (E := ℂ) ((fun (z : ℂ) (ω : Ω) ↦ (↑(X ω) : ℂ) ^ (n + 1) * cexp (z * (↑(X ω) : ℂ))) x a) ≤
      (fun (ω : Ω) ↦ |X ω| ^ (n + 1) * rexp (z.re * X ω + t / 2 * |X ω|)) a
Tactic: refine (hasDerivAt_integral_of_dominated_loc_of_deriv_le
    (bound := fun ω ↦ |X ω| ^ (n + 1) * rexp (z.re * X ω + t / 2 * |X ω|))
    (F := fun z ω ↦ X ω ^ n * cexp (z * X ω))
    (F' := fun z ω ↦ X ω ^ (n + 1) * cexp (z * X ω)) (Metric.ball_mem_nhds _ (half_pos ht))
    ?_ ?_ ?_ ?_ ?_ ?_).2
-- 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_1 :
  ∀ᶠ (x : ℂ) in 𝓝 z,
    AEStronglyMeasurable (β := ℂ) ((fun (z : ℂ) (ω : Ω) ↦ (↑(X ω) : ℂ) ^ n * cexp (z * (↑(X ω) : ℂ))) x) μ
refine_2 : Integrable (ε := ℂ) ((fun (z : ℂ) (ω : Ω) ↦ (↑(X ω) : ℂ) ^ n * cexp (z * (↑(X ω) : ℂ))) z) μ
refine_3 : AEStronglyMeasurable (β := ℂ) ((fun (z : ℂ) (ω : Ω) ↦ (↑(X ω) : ℂ) ^ (n + 1) * cexp (z * (↑(X ω) : ℂ))) z) μ
refine_4 :
  ∀ᵐ (a : Ω) ∂μ,
    ∀ x ∈ Metric.ball z (t / 2),
      Norm.norm (E := ℂ) ((fun (z : ℂ) (ω : Ω) ↦ (↑(X ω) : ℂ) ^ (n + 1) * cexp (z * (↑(X ω) : ℂ))) x a) ≤
        (fun (ω : Ω) ↦ |X ω| ^ (n + 1) * rexp (z.re * X ω + t / 2 * |X ω|)) a
⊢ HasDerivAt (F := ℂ) (fun (z : ℂ) ↦ ∫ (x : Ω), (fun (ω : Ω) ↦ (↑(X ω) : ℂ) ^ n * cexp (z * (↑(X ω) : ℂ))) x ∂μ)
    (∫ (x : Ω), (fun (ω : Ω) ↦ (↑(X ω) : ℂ) ^ (n + 1) * cexp (z * (↑(X ω) : ℂ))) x ∂μ) z
have refine_5 : Integrable (ε := ℝ) (fun (ω : Ω) ↦ |X ω| ^ (n + 1) * rexp (z.re * X ω + t / 2 * |X ω|)) μ
Tactic: refine (hasDerivAt_integral_of_dominated_loc_of_deriv_le
    (bound := fun ω ↦ |X ω| ^ (n + 1) * rexp (z.re * X ω + t / 2 * |X ω|))
    (F := fun z ω ↦ X ω ^ n * cexp (z * X ω))
    (F' := fun z ω ↦ X ω ^ (n + 1) * cexp (z * X ω)) (Metric.ball_mem_nhds _ (half_pos ht))
    ?_ ?_ ?_ ?_ ?_ ?_).2
-- 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_1 :
  ∀ᶠ (x : ℂ) in 𝓝 z,
    AEStronglyMeasurable (β := ℂ) ((fun (z : ℂ) (ω : Ω) ↦ (↑(X ω) : ℂ) ^ n * cexp (z * (↑(X ω) : ℂ))) x) μ
refine_2 : Integrable (ε := ℂ) ((fun (z : ℂ) (ω : Ω) ↦ (↑(X ω) : ℂ) ^ n * cexp (z * (↑(X ω) : ℂ))) z) μ
refine_3 : AEStronglyMeasurable (β := ℂ) ((fun (z : ℂ) (ω : Ω) ↦ (↑(X ω) : ℂ) ^ (n + 1) * cexp (z * (↑(X ω) : ℂ))) z) μ
refine_4 :
  ∀ᵐ (a : Ω) ∂μ,
    ∀ x ∈ Metric.ball z (t / 2),
      Norm.norm (E := ℂ) ((fun (z : ℂ) (ω : Ω) ↦ (↑(X ω) : ℂ) ^ (n + 1) * cexp (z * (↑(X ω) : ℂ))) x a) ≤
        (fun (ω : Ω) ↦ |X ω| ^ (n + 1) * rexp (z.re * X ω + t / 2 * |X ω|)) a
refine_5 : Integrable (ε := ℝ) (fun (ω : Ω) ↦ |X ω| ^ (n + 1) * rexp (z.re * X ω + t / 2 * |X ω|)) μ
⊢ HasDerivAt (F := ℂ) (fun (z : ℂ) ↦ ∫ (x : Ω), (fun (ω : Ω) ↦ (↑(X ω) : ℂ) ^ n * cexp (z * (↑(X ω) : ℂ))) x ∂μ)
    (∫ (x : Ω), (fun (ω : Ω) ↦ (↑(X ω) : ℂ) ^ (n + 1) * cexp (z * (↑(X ω) : ℂ))) x ∂μ) z
have refine_6 : ∀ᵐ (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
Tactic: refine (hasDerivAt_integral_of_dominated_loc_of_deriv_le
    (bound := fun ω ↦ |X ω| ^ (n + 1) * rexp (z.re * X ω + t / 2 * |X ω|))
    (F := fun z ω ↦ X ω ^ n * cexp (z * X ω))
    (F' := fun z ω ↦ X ω ^ (n + 1) * cexp (z * X ω)) (Metric.ball_mem_nhds _ (half_pos ht))
    ?_ ?_ ?_ ?_ ?_ ?_).2
-- 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),
      Norm.norm (E := ℂ) ((fun (z : ℂ) (ω : Ω) ↦ (↑(X ω) : ℂ) ^ (n + 1) * cexp (z * (↑(X ω) : ℂ))) x a) ≤
        (fun (ω : Ω) ↦ |X ω| ^ (n + 1) * rexp (z.re * X ω + t / 2 * |X ω|)) a
have refine_4 : ∀ (ω : Ω) (ε : ℂ) (hε : ε ∈ Metric.ball z (t / 2)),
  Norm.norm (E := ℂ) ((fun (z : ℂ) (ω : Ω) ↦ (↑(X ω) : ℂ) ^ (n + 1) * cexp (z * (↑(X ω) : ℂ))) ε ω) ≤
    (fun (ω : Ω) ↦ |X ω| ^ (n + 1) * rexp (z.re * X ω + t / 2 * |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)
⊢ Norm.norm (E := ℂ) ((fun (z : ℂ) (ω : Ω) ↦ (↑(X ω) : ℂ) ^ (n + 1) * cexp (z * (↑(X ω) : ℂ))) ε ω) ≤
    (fun (ω : Ω) ↦ |X ω| ^ (n + 1) * rexp (z.re * X ω + t / 2 * |X ω|)) ω
have refine_4 : |X ω| ^ (n + 1) * ‖cexp (ε * (↑(X ω) : ℂ))‖ ≤ |X ω| ^ (n + 1) * rexp (z.re * X ω + t / 2 * |X ω|)
Tactic: simp only [norm_mul, norm_pow, norm_real, Real.norm_eq_abs]
-- 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) * ‖cexp (ε * (↑(X ω) : ℂ))‖ ≤ |X ω| ^ (n + 1) * rexp (z.re * X ω + t / 2 * |X ω|)
have refine_4 : |X ω| ^ (n + 1) * rexp (ε * (↑(X ω) : ℂ)).re ≤ |X ω| ^ (n + 1) * rexp (z.re * X ω + t / 2 * |X ω|)
Tactic: rw [Complex.norm_exp]