awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
⊢ AnalyticOnNhd ℝ (mgf X μ) (interior (integrableExpSet X μ))

Tactic:
fun _ hx ↦ analyticAt_mgf hx

Premises used: AnalyticOnNhd, ProbabilityTheory.analyticAt_mgf
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
⊢ AnalyticOn ℝ (mgf X μ) (interior (integrableExpSet X μ))

Tactic:
analyticOnNhd_mgf.analyticOn

Premises used: AnalyticOnNhd.analyticOn, ProbabilityTheory.analyticOnNhd_mgf
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
hv : v ∈ interior (integrableExpSet X μ)
⊢ HasFPowerSeriesAt (𝕜 := ℝ) (mgf X μ)
    (FormalMultilinearSeries.ofScalars ℝ fun (n : ℕ) ↦ iteratedDeriv n (mgf X μ) v / (↑n ! : ℝ)) v

Tactic:
(analyticAt_mgf hv).hasFPowerSeriesAt

Premises used: ProbabilityTheory.analyticAt_mgf, AnalyticAt.hasFPowerSeriesAt
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
hv : v ∈ interior (integrableExpSet X μ)
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
⊢ HasFPowerSeriesAt (𝕜 := ℝ) (mgf X μ)
    (FormalMultilinearSeries.ofScalars ℝ fun (n : ℕ) ↦
      HDiv.hDiv (α := ℝ) (∫ (x : Ω), (fun (ω : Ω) ↦ X ω ^ n * rexp (v * X ω)) x ∂μ) (↑n ! : ℝ))
    v

Tactic:
convert! (analyticAt_mgf hv).hasFPowerSeriesAt

Premises used: ProbabilityTheory.analyticAt_mgf, AnalyticAt.hasFPowerSeriesAt
-- Module: Mathlib.Probability.Moments.MGFAnalytic
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 : ℕ
h h₁ :
  Eq (α := ℝ) (∫ (x_1 : Ω), (fun (ω : Ω) ↦ X ω ^ x * rexp (v * X ω)) x_1 ∂μ)
    (∫ (x_1 : Ω), (fun (ω : Ω) ↦ X ω ^ x * rexp (v * X ω)) x_1 ∂μ)
⊢ ∫ (x_1 : Ω), (fun (ω : Ω) ↦ X ω ^ x * rexp (v * X ω)) x_1 ∂μ = iteratedDeriv x (mgf X μ) v

Tactic:
rw [iteratedDeriv_mgf hv]

Premises used: ProbabilityTheory.iteratedDeriv_mgf
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
⊢ DifferentiableAt ℝ (mgf X μ) t

Tactic:
(analyticAt_mgf ht).differentiableAt

Premises used: ProbabilityTheory.analyticAt_mgf, AnalyticAt.differentiableAt
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
⊢ DifferentiableOn ℝ (mgf X μ) (interior (integrableExpSet X μ))

Tactic:
fun _ hx ↦ (differentiableAt_mgf hx).differentiableWithinAt

Premises used: ProbabilityTheory.differentiableAt_mgf, DifferentiableAt.differentiableWithinAt, DifferentiableOn
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
⊢ ContinuousOn (mgf X μ) (interior (integrableExpSet X μ))

Tactic:
differentiableOn_mgf.continuousOn

Premises used: DifferentiableOn.continuousOn, ProbabilityTheory.differentiableOn_mgf
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
h : ∀ (t : ℝ), Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
rw : ContinuousOn (mgf X μ) Set.univ
⊢ Continuous (mgf X μ)

Tactic:
rw [← continuousOn_univ]

Premises used: continuousOn_univ
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
h : ∀ (t : ℝ), Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
⊢ ContinuousOn (mgf X μ) (interior (integrableExpSet X μ))

Tactic:
continuousOn_mgf

Premises used: ProbabilityTheory.continuousOn_mgf
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
h : ∀ (t : ℝ), Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
h₁ : Set.univ = interior (integrableExpSet X μ)
⊢ ContinuousOn (mgf X μ) Set.univ

Tactic:
convert! continuousOn_mgf

Premises used: ProbabilityTheory.continuousOn_mgf
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
h : ∀ (t : ℝ), Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
h₁ : interior (integrableExpSet X μ) = Set.univ
⊢ Set.univ = interior (integrableExpSet X μ)

Tactic:
symm
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
h : ∀ (t : ℝ), Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
h₁ : integrableExpSet X μ = Set.univ
⊢ interior (integrableExpSet X μ) = Set.univ

Tactic:
rw [interior_eq_univ]

Premises used: interior_eq_univ
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
h : ∀ (t : ℝ), Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
h₁ : ∀ (t : ℝ), t ∈ integrableExpSet X μ ↔ Membership.mem (γ := Set ℝ) Set.univ t
⊢ integrableExpSet X μ = Set.univ

Tactic:
ext t
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
h : ∀ (t : ℝ), Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
t : ℝ
⊢ t ∈ integrableExpSet X μ ↔ Membership.mem (γ := Set ℝ) Set.univ t

Tactic:
simpa using h t
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
n : ℕ
rw : AnalyticOnNhd ℝ (deriv^[n] (mgf X μ)) (interior (integrableExpSet X μ))
⊢ AnalyticOnNhd ℝ (iteratedDeriv n (mgf X μ)) (interior (integrableExpSet X μ))

Tactic:
rw [iteratedDeriv_eq_iterate]

Premises used: iteratedDeriv_eq_iterate
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
n : ℕ
⊢ AnalyticOnNhd ℝ (deriv^[n] (mgf X μ)) (interior (integrableExpSet X μ))

Tactic:
analyticOnNhd_mgf.iterated_deriv n

Premises used: ProbabilityTheory.analyticOnNhd_mgf, AnalyticOnNhd.iterated_deriv
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
n : ℕ
⊢ AnalyticOnNhd ℝ (deriv^[n] (mgf X μ)) (interior (integrableExpSet X μ))

Tactic:
exact analyticOnNhd_mgf.iterated_deriv n

Premises used: ProbabilityTheory.analyticOnNhd_mgf, AnalyticOnNhd.iterated_deriv
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
n : ℕ
⊢ AnalyticOn ℝ (iteratedDeriv n (mgf X μ)) (interior (integrableExpSet X μ))

Tactic:
(analyticOnNhd_iteratedDeriv_mgf n).analyticOn

Premises used: AnalyticOnNhd.analyticOn, ProbabilityTheory.analyticOnNhd_iteratedDeriv_mgf
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
hv : v ∈ interior (integrableExpSet X μ)
n : ℕ
⊢ AnalyticAt ℝ (iteratedDeriv n (mgf X μ)) v

Tactic:
analyticOnNhd_iteratedDeriv_mgf n v hv

Premises used: ProbabilityTheory.analyticOnNhd_iteratedDeriv_mgf
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
hv : v ∈ interior (integrableExpSet X μ)
n : ℕ
⊢ DifferentiableAt ℝ (iteratedDeriv n (mgf X μ)) v

Tactic:
(analyticAt_iteratedDeriv_mgf hv n).differentiableAt

Premises used: AnalyticAt.differentiableAt, ProbabilityTheory.analyticAt_iteratedDeriv_mgf
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
pos : ∀ (hμ : μ = 0), AnalyticAt ℝ (cgf X μ) v
neg : ∀ (hμ : ¬μ = 0), AnalyticAt ℝ (cgf X μ) v
⊢ AnalyticAt ℝ (cgf X μ) v

Tactic:
by_cases hμ : μ = 0
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : μ = 0
pos : AnalyticAt ℝ (F := ℝ) 0 v
⊢ AnalyticAt ℝ (cgf X μ) v

Tactic:
simp only [hμ, cgf_zero_measure]

Premises used: ProbabilityTheory.cgf_zero_measure
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : μ = 0
⊢ AnalyticAt ℝ (F := ℝ) 0 v

Tactic:
analyticAt_const

Premises used: analyticAt_const
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : μ = 0
⊢ AnalyticAt ℝ (F := ℝ) 0 v

Tactic:
exact analyticAt_const

Premises used: analyticAt_const
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
⊢ AnalyticAt ℝ (cgf X μ) v

Tactic:
(analyticAt_mgf h).log <| mgf_pos' hμ (interior_subset (s := integrableExpSet X μ) h)

Premises used: interior_subset, ProbabilityTheory.cgf, AnalyticAt.log, ProbabilityTheory.analyticAt_mgf, ProbabilityTheory.mgf_pos'
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
⊢ AnalyticAt ℝ (cgf X μ) v

Tactic:
exact (analyticAt_mgf h).log <| mgf_pos' hμ (interior_subset (s := integrableExpSet X μ) h)

Premises used: interior_subset, AnalyticAt.log, ProbabilityTheory.analyticAt_mgf, ProbabilityTheory.mgf_pos'
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
⊢ AnalyticOnNhd ℝ (cgf X μ) (interior (integrableExpSet X μ))

Tactic:
fun _ hx ↦ analyticAt_cgf hx

Premises used: AnalyticOnNhd, ProbabilityTheory.analyticAt_cgf
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
⊢ AnalyticOn ℝ (cgf X μ) (interior (integrableExpSet X μ))

Tactic:
analyticOnNhd_cgf.analyticOn

Premises used: ProbabilityTheory.analyticOnNhd_cgf, AnalyticOnNhd.analyticOn
-- Module: Mathlib.Probability.Moments.MGFAnalytic
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
neg : ∀ (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

Tactic:
by_cases hμ : μ = 0
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : μ = 0
pos : Eq (α := ℝ) (deriv 0 v) 0
⊢ deriv (cgf X μ) v = (∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (v * X ω)) x ∂μ) / mgf X μ v

Tactic:
simp only [hμ, cgf_zero_measure, integral_zero_measure, mgf_zero_measure, div_zero,
      Pi.zero_apply]

Premises used: Pi.zero_apply, ProbabilityTheory.mgf_zero_measure, MeasureTheory.integral_zero_measure, ProbabilityTheory.cgf_zero_measure, div_zero
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : μ = 0
⊢ Eq (α := ℝ) (deriv 0 v) 0

Tactic:
deriv_const v 0

Premises used: deriv_const, OfNat.ofNat
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : μ = 0
⊢ Eq (α := ℝ) (deriv 0 v) 0

Tactic:
exact deriv_const v 0

Premises used: deriv_const, OfNat.ofNat
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (v * X ω)) μ

Tactic:
have hv : Integrable (fun ω ↦ exp (v * X ω)) μ := interior_subset (s := integrableExpSet X μ) h
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
hv : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (v * X ω)) μ
rw rw₁ : deriv (mgf X μ) v / mgf X μ v = deriv (mgf X μ) v / mgf X μ v
⊢ deriv (fun (x : ℝ) ↦ log (mgf X μ x)) v = deriv (mgf X μ) v / mgf X μ v

Tactic:
rw [deriv.log (differentiableAt_mgf h) ((mgf_pos' hμ hv).ne')]

Premises used: deriv.log, ProbabilityTheory.differentiableAt_mgf, ProbabilityTheory.mgf_pos', LT.lt.ne'
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
hv : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (v * X ω)) μ
rw rw₁ :
  (∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (v * X ω)) x ∂μ) / mgf X μ v =
    (∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (v * X ω)) x ∂μ) / mgf X μ v
⊢ deriv (mgf X μ) v / mgf X μ v = (∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (v * X ω)) x ∂μ) / mgf X μ v

Tactic:
rw [deriv_mgf h]

Premises used: ProbabilityTheory.deriv_mgf
-- Module: Mathlib.Probability.Moments.MGFAnalytic
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
calc₁ : deriv (mgf X μ) v / mgf 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

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]

Premises used: HMul.hMul, deriv, Real.exp, Real.log, ProbabilityTheory.mgf
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
h : 0 ∈ interior (integrableExpSet X μ)
⊢ deriv (cgf X μ) 0 = (∫ (x : Ω), X x ∂μ) / μ.real Set.univ

Tactic:
simp [deriv_cgf h]

Premises used: ProbabilityTheory.deriv_cgf
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
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
⊢ 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

Tactic:
rw [iteratedDeriv_succ, iteratedDeriv_one]

Premises used: iteratedDeriv_succ, iteratedDeriv_one
-- Module: Mathlib.Probability.Moments.MGFAnalytic
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
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
⊢ 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
-- Module: Mathlib.Probability.Moments.MGFAnalytic
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

Tactic:
simp [hμ]
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
⊢ ∀ᶠ (y : ℝ) in 𝓝 v, y ∈ interior (integrableExpSet X μ)

Tactic:
have h_mem : ∀ᶠ y in 𝓝 v, y ∈ interior (integrableExpSet X μ) :=
    isOpen_interior.eventually_mem h
-- Module: Mathlib.Probability.Moments.MGFAnalytic
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 μ)
u : ℝ
hu : u ∈ interior (integrableExpSet X μ)
⊢ deriv (cgf X μ) u = (∫ (x : Ω), X x * rexp (u * X x) ∂μ) / mgf X μ u

Tactic:
deriv_cgf hu

Premises used: ProbabilityTheory.deriv_cgf
-- Module: Mathlib.Probability.Moments.MGFAnalytic
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
h₂ h₃ :
  ∀ (u : ℝ) (hu : u ∈ interior (integrableExpSet X μ)),
    deriv (cgf X μ) u = (∫ (x : Ω), X x * rexp (u * X x) ∂μ) / mgf X μ u
⊢ deriv (cgf X μ) =ᶠ[𝓝 v] fun (u : ℝ) ↦ (∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (u * X ω)) x ∂μ) / mgf X μ u

Tactic:
filter_upwards [h_mem] with u hu using deriv_cgf hu
-- Module: Mathlib.Probability.Moments.MGFAnalytic
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

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
-- Module: Mathlib.Probability.Moments.MGFAnalytic
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
u : ℝ
hu : u ∈ interior (integrableExpSet X μ)
⊢ deriv (mgf X μ) u = ∫ (x : Ω), X x * rexp (u * X x) ∂μ

Tactic:
deriv_mgf hu

Premises used: ProbabilityTheory.deriv_mgf
-- Module: Mathlib.Probability.Moments.MGFAnalytic
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
h₂ h₃ : ∀ (u : ℝ) (hu : u ∈ interior (integrableExpSet X μ)), deriv (mgf X μ) u = ∫ (x : Ω), X x * rexp (u * X x) ∂μ
⊢ deriv (mgf X μ) =ᶠ[𝓝 v] fun (u : ℝ) ↦ ∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (u * X ω)) x ∂μ

Tactic:
filter_upwards [h_mem] with u hu using deriv_mgf hu
-- Module: Mathlib.Probability.Moments.MGFAnalytic
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 ∂μ

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
-- Module: Mathlib.Probability.Moments.MGFAnalytic
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 ∂μ
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
⊢ 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 [h_d_cgf.deriv_eq]

Premises used: Filter.EventuallyEq.deriv_eq
-- Module: Mathlib.Probability.Moments.MGFAnalytic
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
hx : mgf X μ v ≠ 0
⊢ 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

Tactic:
rw [deriv_fun_div]

Premises used: deriv_fun_div
-- Module: Mathlib.Probability.Moments.MGFAnalytic
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 ℝ (iteratedDeriv 1 (mgf X μ)) v
⊢ DifferentiableAt ℝ (F := ℝ) (fun (u : ℝ) ↦ ∫ (ω : Ω), X ω * rexp (u * X ω) ∂μ) v

Tactic:
rw [h_d_mgf.symm.differentiableAt_iff, ← iteratedDeriv_one]

Premises used: Filter.EventuallyEq.differentiableAt_iff, iteratedDeriv_one, Filter.EventuallyEq.symm
-- Module: Mathlib.Probability.Moments.MGFAnalytic
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 ∂μ
⊢ DifferentiableAt ℝ (iteratedDeriv 1 (mgf X μ)) v

Tactic:
differentiableAt_iteratedDeriv_mgf h 1

Premises used: ProbabilityTheory.differentiableAt_iteratedDeriv_mgf, OfNat.ofNat