awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
n : ℕ
zero :
  ∀ {t : ℝ} (ht : t ∈ interior (integrableExpSet X μ)),
    HasDerivAt (iteratedDeriv 0 (mgf X μ))
      (∫ (x : Ω), (fun (ω : Ω) ↦ X ω ^ HAdd.hAdd (α := ℕ) 0 1 * rexp (t * X ω)) x ∂μ) t
⊢ HasDerivAt (iteratedDeriv n (mgf X μ)) (∫ (x : Ω), (fun (ω : Ω) ↦ X ω ^ (n + 1) * rexp (t * X ω)) x ∂μ) t
have succ : ∀ (n : ℕ)
  (hn :
    ∀ {t : ℝ} (ht : t ∈ interior (integrableExpSet X μ)),
      HasDerivAt (iteratedDeriv n (mgf X μ)) (∫ (x : Ω), (fun (ω : Ω) ↦ X ω ^ (n + 1) * rexp (t * X ω)) x ∂μ) t)
  {t : ℝ} (ht : t ∈ interior (integrableExpSet X μ)),
  HasDerivAt (iteratedDeriv (n + 1) (mgf X μ)) (∫ (x : Ω), (fun (ω : Ω) ↦ X ω ^ (n + 1 + 1) * rexp (t * X ω)) x ∂μ) t
Tactic: induction n generalizing t with
  | zero => simp [hasDerivAt_mgf ht]
  | succ n hn =>
    rw [iteratedDeriv_succ]
    have : deriv (iteratedDeriv n (mgf X μ))
        =ᶠ[𝓝 t] fun t ↦ μ[fun ω ↦ X ω ^ (n + 1) * exp (t * X ω)] := by
      have h_mem : ∀ᶠ y in 𝓝 t, y ∈ interior (integrableExpSet X μ) :=
        isOpen_interior.eventually_mem ht
      filter_upwards [h_mem] with y hy using HasDerivAt.deriv (hn hy)
    rw [EventuallyEq.hasDerivAt_iff this]
    exact hasDerivAt_integral_pow_mul_exp_real ht (n + 1)
Cleared hypotheses: t, ht, n
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
n : ℕ
hn :
  ∀ {t : ℝ} (ht : t ∈ interior (integrableExpSet X μ)),
    iteratedDeriv n (mgf X μ) t = ∫ (x : Ω), (fun (ω : Ω) ↦ X ω ^ n * rexp (t * X ω)) x ∂μ
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
⊢ iteratedDeriv (n + 1) (mgf X μ) t = ∫ (x : Ω), (fun (ω : Ω) ↦ X ω ^ (n + 1) * rexp (t * X ω)) x ∂μ
have succ : deriv (iteratedDeriv n (mgf X μ)) t = ∫ (x : Ω), (fun (ω : Ω) ↦ X ω ^ (n + 1) * rexp (t * X ω)) x ∂μ
Tactic: rw [iteratedDeriv_succ]
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
n : ℕ
⊢ iteratedDeriv n (mgf X μ) t = ∫ (x : Ω), (fun (ω : Ω) ↦ X ω ^ n * rexp (t * X ω)) x ∂μ
have zero : ∀ {t : ℝ} (ht : t ∈ interior (integrableExpSet X μ)),
  iteratedDeriv 0 (mgf X μ) t = ∫ (x : Ω), (fun (ω : Ω) ↦ HPow.hPow (β := ℕ) (X ω) 0 * rexp (t * X ω)) x ∂μ
Tactic: induction n generalizing t with
  | zero => simp [mgf]
  | succ n hn =>
    rw [iteratedDeriv_succ]
    exact (hasDerivAt_iteratedDeriv_mgf ht n).deriv
Cleared hypotheses: t, ht, n
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
n : ℕ
zero :
  ∀ {t : ℝ} (ht : t ∈ interior (integrableExpSet X μ)),
    iteratedDeriv 0 (mgf X μ) t = ∫ (x : Ω), (fun (ω : Ω) ↦ HPow.hPow (β := ℕ) (X ω) 0 * rexp (t * X ω)) x ∂μ
⊢ iteratedDeriv n (mgf X μ) t = ∫ (x : Ω), (fun (ω : Ω) ↦ X ω ^ n * rexp (t * X ω)) x ∂μ
have succ : ∀ (n : ℕ)
  (hn :
    ∀ {t : ℝ} (ht : t ∈ interior (integrableExpSet X μ)),
      iteratedDeriv n (mgf X μ) t = ∫ (x : Ω), (fun (ω : Ω) ↦ X ω ^ n * rexp (t * X ω)) x ∂μ)
  {t : ℝ} (ht : t ∈ interior (integrableExpSet X μ)),
  iteratedDeriv (n + 1) (mgf X μ) t = ∫ (x : Ω), (fun (ω : Ω) ↦ X ω ^ (n + 1) * rexp (t * X ω)) x ∂μ
Tactic: induction n generalizing t with
  | zero => simp [mgf]
  | succ n hn =>
    rw [iteratedDeriv_succ]
    exact (hasDerivAt_iteratedDeriv_mgf ht n).deriv
Cleared hypotheses: t, ht, n
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
⊢ AnalyticAt ℝ (mgf X μ) t
have rw : AnalyticAt ℝ (F := ℝ) (fun (x : ℝ) ↦ (complexMGF X μ (↑x : ℂ)).re) t
Tactic: rw [← re_complexMGF_ofReal']
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
hv : v ∈ interior (integrableExpSet X μ)
⊢ HasFPowerSeriesAt (𝕜 := ℝ) (mgf X μ)
    (FormalMultilinearSeries.ofScalars ℝ fun (n : ℕ) ↦
      HDiv.hDiv (α := ℝ) (∫ (x : Ω), (fun (ω : Ω) ↦ X ω ^ n * rexp (v * X ω)) x ∂μ) (↑n ! : ℝ))
    v
have h : normedAddCommGroup = NonUnitalNormedRing.toNormedAddCommGroup →
  HEq (α := NormedSpace ℝ ℝ) InnerProductSpace.toNormedSpace (β := NormedSpace ℝ ℝ) NormedField.toNormedSpace →
    ∀ (x : ℕ), ∫ (x_1 : Ω), (fun (ω : Ω) ↦ X ω ^ x * rexp (v * X ω)) x_1 ∂μ = iteratedDeriv x (mgf X μ) v
Tactic: convert! (analyticAt_mgf hv).hasFPowerSeriesAt
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
hv : v ∈ interior (integrableExpSet X μ)
e_5 : normedAddCommGroup = NonUnitalNormedRing.toNormedAddCommGroup
e_6 : HEq (α := NormedSpace ℝ ℝ) InnerProductSpace.toNormedSpace (β := NormedSpace ℝ ℝ) NormedField.toNormedSpace
x : ℕ
⊢ ∫ (x_1 : Ω), (fun (ω : Ω) ↦ X ω ^ x * rexp (v * X ω)) x_1 ∂μ = iteratedDeriv x (mgf X μ) v
have h : Eq (α := ℝ) (∫ (x_1 : Ω), (fun (ω : Ω) ↦ X ω ^ x * rexp (v * X ω)) x_1 ∂μ)
  (∫ (x_1 : Ω), (fun (ω : Ω) ↦ X ω ^ x * rexp (v * X ω)) x_1 ∂μ)
Tactic: rw [iteratedDeriv_mgf hv]
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
h : ∀ (t : ℝ), Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
⊢ Continuous (mgf X μ)
have rw : ContinuousOn (mgf X μ) Set.univ
Tactic: rw [← continuousOn_univ]
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
h : ∀ (t : ℝ), Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
⊢ ContinuousOn (mgf X μ) Set.univ
have h₁ : Set.univ = interior (integrableExpSet X μ)
Tactic: convert! continuousOn_mgf
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
h : ∀ (t : ℝ), Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
⊢ Set.univ = interior (integrableExpSet X μ)
have h₁ : interior (integrableExpSet X μ) = Set.univ
Tactic: symm
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
h : ∀ (t : ℝ), Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
⊢ interior (integrableExpSet X μ) = Set.univ
have h₁ : integrableExpSet X μ = Set.univ
Tactic: rw [interior_eq_univ]
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
h : ∀ (t : ℝ), Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
⊢ integrableExpSet X μ = Set.univ
have h₁ : ∀ (t : ℝ), t ∈ integrableExpSet X μ ↔ Membership.mem (γ := Set ℝ) Set.univ t
Tactic: ext t
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
n : ℕ
⊢ AnalyticOnNhd ℝ (iteratedDeriv n (mgf X μ)) (interior (integrableExpSet X μ))
have rw : AnalyticOnNhd ℝ (deriv^[n] (mgf X μ)) (interior (integrableExpSet X μ))
Tactic: rw [iteratedDeriv_eq_iterate]
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
⊢ AnalyticAt ℝ (cgf X μ) v
have pos : ∀ (hμ : μ = 0), AnalyticAt ℝ (cgf X μ) v
Tactic: by_cases hμ : μ = 0
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
pos : ∀ (hμ : μ = 0), AnalyticAt ℝ (cgf X μ) v
⊢ AnalyticAt ℝ (cgf X μ) v
have neg : ∀ (hμ : ¬μ = 0), AnalyticAt ℝ (cgf X μ) v
Tactic: by_cases hμ : μ = 0
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : μ = 0
⊢ AnalyticAt ℝ (cgf X μ) v
have pos : AnalyticAt ℝ (F := ℝ) 0 v
Tactic: simp only [hμ, cgf_zero_measure]
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
⊢ deriv (cgf X μ) v = (∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (v * X ω)) x ∂μ) / mgf X μ v
have pos : ∀ (hμ : μ = 0), deriv (cgf X μ) v = (∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (v * X ω)) x ∂μ) / mgf X μ v
Tactic: by_cases hμ : μ = 0
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
pos : ∀ (hμ : μ = 0), deriv (cgf X μ) v = (∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (v * X ω)) x ∂μ) / mgf X μ v
⊢ deriv (cgf X μ) v = (∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (v * X ω)) x ∂μ) / mgf X μ v
have neg : ∀ (hμ : ¬μ = 0), deriv (cgf X μ) v = (∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (v * X ω)) x ∂μ) / mgf X μ v
Tactic: by_cases hμ : μ = 0
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : μ = 0
⊢ deriv (cgf X μ) v = (∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (v * X ω)) x ∂μ) / mgf X μ v
have pos : Eq (α := ℝ) (deriv 0 v) 0
Tactic: simp only [hμ, cgf_zero_measure, integral_zero_measure, mgf_zero_measure, div_zero,
      Pi.zero_apply]
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (hypothesis)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
⊢ deriv (cgf X μ) v = (∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (v * X ω)) x ∂μ) / mgf X μ v
have hv : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (v * X ω)) μ
Tactic: have hv : Integrable (fun ω ↦ exp (v * X ω)) μ := interior_subset (s := integrableExpSet X μ) h
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
hv : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (v * X ω)) μ
⊢ deriv (fun (x : ℝ) ↦ log (mgf X μ x)) v = deriv (mgf X μ) v / mgf X μ v
have rw : deriv (mgf X μ) v / mgf X μ v = deriv (mgf X μ) v / mgf X μ v
Tactic: rw [deriv.log (differentiableAt_mgf h) ((mgf_pos' hμ hv).ne')]
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
hv : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (v * X ω)) μ
⊢ deriv (mgf X μ) v / mgf X μ v = (∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (v * X ω)) x ∂μ) / mgf X μ v
have rw : (∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (v * X ω)) x ∂μ) / mgf X μ v =
  (∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (v * X ω)) x ∂μ) / mgf X μ v
Tactic: rw [deriv_mgf h]
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
hv : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (v * X ω)) μ
⊢ deriv (cgf X μ) v = (∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (v * X ω)) x ∂μ) / mgf X μ v
have calc : deriv (fun (x : ℝ) ↦ log (mgf X μ x)) v = deriv (mgf X μ) v / mgf X μ v
Tactic: calc deriv (fun x ↦ log (mgf X μ x)) v
  _ = deriv (mgf X μ) v / mgf X μ v := by
    rw [deriv.log (differentiableAt_mgf h) ((mgf_pos' hμ hv).ne')]
  _ = μ[fun ω ↦ X ω * exp (v * X ω)] / mgf X μ v := by rw [deriv_mgf h]
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
hv : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (v * X ω)) μ
calc : deriv (fun (x : ℝ) ↦ log (mgf X μ x)) v = deriv (mgf X μ) v / mgf X μ v
⊢ deriv (cgf X μ) v = (∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (v * X ω)) x ∂μ) / mgf X μ v
have calc₁ : deriv (mgf X μ) v / mgf X μ v = (∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (v * X ω)) x ∂μ) / mgf X μ v
Tactic: calc deriv (fun x ↦ log (mgf X μ x)) v
  _ = deriv (mgf X μ) v / mgf X μ v := by
    rw [deriv.log (differentiableAt_mgf h) ((mgf_pos' hμ hv).ne')]
  _ = μ[fun ω ↦ X ω * exp (v * X ω)] / mgf X μ v := by rw [deriv_mgf h]
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
⊢ iteratedDeriv 2 (cgf X μ) v =
    (∫ (x : Ω), (fun (ω : Ω) ↦ HPow.hPow (β := ℕ) (X ω) 2 * rexp (v * X ω)) x ∂μ) / mgf X μ v -
      HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2
have rw : deriv (deriv (cgf X μ)) v =
  (∫ (x : Ω), (fun (ω : Ω) ↦ HPow.hPow (β := ℕ) (X ω) 2 * rexp (v * X ω)) x ∂μ) / mgf X μ v -
    HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2
Tactic: rw [iteratedDeriv_succ, iteratedDeriv_one]
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
⊢ deriv (deriv (cgf X μ)) v =
    (∫ (x : Ω), (fun (ω : Ω) ↦ HPow.hPow (β := ℕ) (X ω) 2 * rexp (v * X ω)) x ∂μ) / mgf X μ v -
      HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2
have pos : ∀ (hμ : μ = 0),
  deriv (deriv (cgf X μ)) v =
    (∫ (x : Ω), (fun (ω : Ω) ↦ HPow.hPow (β := ℕ) (X ω) 2 * rexp (v * X ω)) x ∂μ) / mgf X μ v -
      HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2
Tactic: by_cases hμ : μ = 0
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
pos :
  ∀ (hμ : μ = 0),
    deriv (deriv (cgf X μ)) v =
      (∫ (x : Ω), (fun (ω : Ω) ↦ HPow.hPow (β := ℕ) (X ω) 2 * rexp (v * X ω)) x ∂μ) / mgf X μ v -
        HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2
⊢ deriv (deriv (cgf X μ)) v =
    (∫ (x : Ω), (fun (ω : Ω) ↦ HPow.hPow (β := ℕ) (X ω) 2 * rexp (v * X ω)) x ∂μ) / mgf X μ v -
      HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2
have neg : ∀ (hμ : ¬μ = 0),
  deriv (deriv (cgf X μ)) v =
    (∫ (x : Ω), (fun (ω : Ω) ↦ HPow.hPow (β := ℕ) (X ω) 2 * rexp (v * X ω)) x ∂μ) / mgf X μ v -
      HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2
Tactic: by_cases hμ : μ = 0
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (hypothesis)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
⊢ deriv (deriv (cgf X μ)) v =
    (∫ (x : Ω), (fun (ω : Ω) ↦ HPow.hPow (β := ℕ) (X ω) 2 * rexp (v * X ω)) x ∂μ) / mgf X μ v -
      HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2
have h_mem : ∀ᶠ (y : ℝ) in 𝓝 v, y ∈ interior (integrableExpSet X μ)
Tactic: have h_mem : ∀ᶠ y in 𝓝 v, y ∈ interior (integrableExpSet X μ) :=
    isOpen_interior.eventually_mem h
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
h_mem : ∀ᶠ (y : ℝ) in 𝓝 v, y ∈ interior (integrableExpSet X μ)
⊢ deriv (cgf X μ) =ᶠ[𝓝 v] fun (u : ℝ) ↦ (∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (u * X ω)) x ∂μ) / mgf X μ u
have h₁ : ∀ (a : ℝ),
  Membership.mem (γ := Set ℝ)
    {x : ℝ |
      Membership.mem (γ := Set ℝ) {x : ℝ | (fun (y : ℝ) ↦ y ∈ interior (integrableExpSet X μ)) x} x →
        Membership.mem (γ := Set ℝ)
          {x : ℝ |
            (fun (x : ℝ) ↦
                deriv (cgf X μ) x =
                  (fun (u : ℝ) ↦ (∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (u * X ω)) x ∂μ) / mgf X μ u) x)
              x}
          x}
    a
Tactic: filter_upwards [h_mem] with u hu using deriv_cgf hu
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
h_mem : ∀ᶠ (y : ℝ) in 𝓝 v, y ∈ interior (integrableExpSet X μ)
h₁ :
  ∀ (a : ℝ),
    Membership.mem (γ := Set ℝ)
      {x : ℝ |
        Membership.mem (γ := Set ℝ) {x : ℝ | (fun (y : ℝ) ↦ y ∈ interior (integrableExpSet X μ)) x} x →
          Membership.mem (γ := Set ℝ)
            {x : ℝ |
              (fun (x : ℝ) ↦
                  deriv (cgf X μ) x =
                    (fun (u : ℝ) ↦ (∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (u * X ω)) x ∂μ) / mgf X μ u) x)
                x}
            x}
      a
⊢ deriv (cgf X μ) =ᶠ[𝓝 v] fun (u : ℝ) ↦ (∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (u * X ω)) x ∂μ) / mgf X μ u
have h₂ : ∀ a ∈ interior (integrableExpSet X μ), deriv (cgf X μ) a = (∫ (x : Ω), X x * rexp (a * X x) ∂μ) / mgf X μ a
Tactic: filter_upwards [h_mem] with u hu using deriv_cgf hu
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (hypothesis)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
h_mem : ∀ᶠ (y : ℝ) in 𝓝 v, y ∈ interior (integrableExpSet X μ)
⊢ deriv (deriv (cgf X μ)) v =
    (∫ (x : Ω), (fun (ω : Ω) ↦ HPow.hPow (β := ℕ) (X ω) 2 * rexp (v * X ω)) x ∂μ) / mgf X μ v -
      HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2
have h_d_cgf : deriv (cgf X μ) =ᶠ[𝓝 v] fun (u : ℝ) ↦ (∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (u * X ω)) x ∂μ) / mgf X μ u
Tactic: have h_d_cgf : deriv (cgf X μ) =ᶠ[𝓝 v] fun u ↦ μ[fun ω ↦ X ω * exp (u * X ω)] / mgf X μ u := by
    filter_upwards [h_mem] with u hu using deriv_cgf hu
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
h_mem : ∀ᶠ (y : ℝ) in 𝓝 v, y ∈ interior (integrableExpSet X μ)
h_d_cgf : deriv (cgf X μ) =ᶠ[𝓝 v] fun (u : ℝ) ↦ (∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (u * X ω)) x ∂μ) / mgf X μ u
⊢ deriv (mgf X μ) =ᶠ[𝓝 v] fun (u : ℝ) ↦ ∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (u * X ω)) x ∂μ
have h₁ : ∀ (a : ℝ),
  Membership.mem (γ := Set ℝ)
    {x : ℝ |
      Membership.mem (γ := Set ℝ) {x : ℝ | (fun (y : ℝ) ↦ y ∈ interior (integrableExpSet X μ)) x} x →
        Membership.mem (γ := Set ℝ)
          {x : ℝ |
            (fun (x : ℝ) ↦
                deriv (mgf X μ) x = (fun (u : ℝ) ↦ (∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (u * X ω)) x ∂μ : ℝ)) x)
              x}
          x}
    a
Tactic: filter_upwards [h_mem] with u hu using deriv_mgf hu
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
h_mem : ∀ᶠ (y : ℝ) in 𝓝 v, y ∈ interior (integrableExpSet X μ)
h_d_cgf : deriv (cgf X μ) =ᶠ[𝓝 v] fun (u : ℝ) ↦ (∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (u * X ω)) x ∂μ) / mgf X μ u
h₁ :
  ∀ (a : ℝ),
    Membership.mem (γ := Set ℝ)
      {x : ℝ |
        Membership.mem (γ := Set ℝ) {x : ℝ | (fun (y : ℝ) ↦ y ∈ interior (integrableExpSet X μ)) x} x →
          Membership.mem (γ := Set ℝ)
            {x : ℝ |
              (fun (x : ℝ) ↦
                  deriv (mgf X μ) x = (fun (u : ℝ) ↦ (∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (u * X ω)) x ∂μ : ℝ)) x)
                x}
            x}
      a
⊢ deriv (mgf X μ) =ᶠ[𝓝 v] fun (u : ℝ) ↦ ∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (u * X ω)) x ∂μ
have h₂ : ∀ a ∈ interior (integrableExpSet X μ), deriv (mgf X μ) a = ∫ (x : Ω), X x * rexp (a * X x) ∂μ
Tactic: filter_upwards [h_mem] with u hu using deriv_mgf hu
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (hypothesis)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
h_mem : ∀ᶠ (y : ℝ) in 𝓝 v, y ∈ interior (integrableExpSet X μ)
h_d_cgf : deriv (cgf X μ) =ᶠ[𝓝 v] fun (u : ℝ) ↦ (∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (u * X ω)) x ∂μ) / mgf X μ u
⊢ deriv (deriv (cgf X μ)) v =
    (∫ (x : Ω), (fun (ω : Ω) ↦ HPow.hPow (β := ℕ) (X ω) 2 * rexp (v * X ω)) x ∂μ) / mgf X μ v -
      HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2
have h_d_mgf : deriv (mgf X μ) =ᶠ[𝓝 v] fun (u : ℝ) ↦ ∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (u * X ω)) x ∂μ
Tactic: have h_d_mgf : deriv (mgf X μ) =ᶠ[𝓝 v] fun u ↦ μ[fun ω ↦ X ω * exp (u * X ω)] := by
    filter_upwards [h_mem] with u hu using deriv_mgf hu
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
h_mem : ∀ᶠ (y : ℝ) in 𝓝 v, y ∈ interior (integrableExpSet X μ)
h_d_cgf : deriv (cgf X μ) =ᶠ[𝓝 v] fun (u : ℝ) ↦ (∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (u * X ω)) x ∂μ) / mgf X μ u
h_d_mgf : deriv (mgf X μ) =ᶠ[𝓝 v] fun (u : ℝ) ↦ ∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (u * X ω)) x ∂μ
⊢ deriv (deriv (cgf X μ)) v =
    (∫ (x : Ω), (fun (ω : Ω) ↦ HPow.hPow (β := ℕ) (X ω) 2 * rexp (v * X ω)) x ∂μ) / mgf X μ v -
      HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2
have neg : deriv (fun (u : ℝ) ↦ (∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (u * X ω)) x ∂μ) / mgf X μ u) v =
  (∫ (x : Ω), (fun (ω : Ω) ↦ HPow.hPow (β := ℕ) (X ω) 2 * rexp (v * X ω)) x ∂μ) / mgf X μ v -
    HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2
Tactic: rw [h_d_cgf.deriv_eq]
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
h_mem : ∀ᶠ (y : ℝ) in 𝓝 v, y ∈ interior (integrableExpSet X μ)
h_d_cgf : deriv (cgf X μ) =ᶠ[𝓝 v] fun (u : ℝ) ↦ (∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (u * X ω)) x ∂μ) / mgf X μ u
h_d_mgf : deriv (mgf X μ) =ᶠ[𝓝 v] fun (u : ℝ) ↦ ∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (u * X ω)) x ∂μ
⊢ deriv (fun (u : ℝ) ↦ (∫ (ω : Ω), X ω * rexp (u * X ω) ∂μ) / mgf X μ u) v =
    (deriv (fun (u : ℝ) ↦ ∫ (ω : Ω), X ω * rexp (u * X ω) ∂μ) v * mgf X μ v -
        (∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) * deriv (mgf X μ) v) /
      HPow.hPow (β := ℕ) (mgf X μ v) 2
have hc : DifferentiableAt ℝ (F := ℝ) (fun (u : ℝ) ↦ ∫ (ω : Ω), X ω * rexp (u * X ω) ∂μ) v
Tactic: rw [deriv_fun_div]
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
h_mem : ∀ᶠ (y : ℝ) in 𝓝 v, y ∈ interior (integrableExpSet X μ)
h_d_cgf : deriv (cgf X μ) =ᶠ[𝓝 v] fun (u : ℝ) ↦ (∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (u * X ω)) x ∂μ) / mgf X μ u
h_d_mgf : deriv (mgf X μ) =ᶠ[𝓝 v] fun (u : ℝ) ↦ ∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (u * X ω)) x ∂μ
hc : DifferentiableAt ℝ (F := ℝ) (fun (u : ℝ) ↦ ∫ (ω : Ω), X ω * rexp (u * X ω) ∂μ) v
⊢ deriv (fun (u : ℝ) ↦ (∫ (ω : Ω), X ω * rexp (u * X ω) ∂μ) / mgf X μ u) v =
    (deriv (fun (u : ℝ) ↦ ∫ (ω : Ω), X ω * rexp (u * X ω) ∂μ) v * mgf X μ v -
        (∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) * deriv (mgf X μ) v) /
      HPow.hPow (β := ℕ) (mgf X μ v) 2
have hd : DifferentiableAt ℝ (mgf X μ) v
Tactic: rw [deriv_fun_div]
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
h_mem : ∀ᶠ (y : ℝ) in 𝓝 v, y ∈ interior (integrableExpSet X μ)
h_d_cgf : deriv (cgf X μ) =ᶠ[𝓝 v] fun (u : ℝ) ↦ (∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (u * X ω)) x ∂μ) / mgf X μ u
h_d_mgf : deriv (mgf X μ) =ᶠ[𝓝 v] fun (u : ℝ) ↦ ∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (u * X ω)) x ∂μ
hc : DifferentiableAt ℝ (F := ℝ) (fun (u : ℝ) ↦ ∫ (ω : Ω), X ω * rexp (u * X ω) ∂μ) v
hd : DifferentiableAt ℝ (mgf X μ) v
⊢ deriv (fun (u : ℝ) ↦ (∫ (ω : Ω), X ω * rexp (u * X ω) ∂μ) / mgf X μ u) v =
    (deriv (fun (u : ℝ) ↦ ∫ (ω : Ω), X ω * rexp (u * X ω) ∂μ) v * mgf X μ v -
        (∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) * deriv (mgf X μ) v) /
      HPow.hPow (β := ℕ) (mgf X μ v) 2
have hx : mgf X μ v ≠ 0
Tactic: rw [deriv_fun_div]