awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
h_int : Integrable (ε := ℝ) (fun (ω : Ω) ↦ 2 * X ω * deriv (cgf X μ) v * rexp (v * X ω)) μ
e_a :
  ∫ (ω : Ω), HPow.hPow (β := ℕ) (X ω) 2 * rexp (v * X ω) ∂μ -
        HMul.hMul (α := ℝ) 2 (∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) * deriv (cgf X μ) v +
      HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2 * mgf X μ v =
    HAdd.hAdd (α := ℝ)
      (∫ (a : Ω), HPow.hPow (β := ℕ) (X a) 2 * rexp (v * X a) - 2 * X a * deriv (cgf X μ) v * rexp (v * X a) ∂μ)
      (∫ (a : Ω), HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2 * rexp (v * X a) ∂μ)
e_a₁ :
  Integrable (ε := ℝ)
    (fun (ω : Ω) ↦ HPow.hPow (β := ℕ) (X ω) 2 * rexp (v * X ω) - 2 * X ω * deriv (cgf X μ) v * rexp (v * X ω)) μ
e_a₂ : Integrable (ε := ℝ) (fun (ω : Ω) ↦ HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2 * rexp (v * X ω)) μ
⊢ ∫ (ω : Ω), HPow.hPow (β := ℕ) (X ω) 2 * rexp (v * X ω) ∂μ -
        HMul.hMul (α := ℝ) 2 (∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) * deriv (cgf X μ) v +
      HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2 * mgf X μ v =
    ∫ (ω : Ω),
      HPow.hPow (β := ℕ) (X ω) 2 * rexp (v * X ω) - 2 * X ω * deriv (cgf X μ) v * rexp (v * X ω) +
        HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2 * rexp (v * X ω) ∂μ

Tactic:
rw [integral_add]

Premises used: MeasureTheory.integral_add
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
h_int : Integrable (ε := ℝ) (fun (ω : Ω) ↦ 2 * X ω * deriv (cgf X μ) v * rexp (v * X ω)) μ
⊢ Integrable (ε := ℝ)
    (fun (ω : Ω) ↦ HPow.hPow (β := ℕ) (X ω) 2 * rexp (v * X ω) - 2 * X ω * deriv (cgf X μ) v * rexp (v * X ω)) μ

Tactic:
(integrable_pow_mul_exp_of_mem_interior_integrableExpSet h 2).sub h_int

Premises used: MeasureTheory.Integrable.sub, ProbabilityTheory.integrable_pow_mul_exp_of_mem_interior_integrableExpSet, OfNat.ofNat
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
h_int : Integrable (ε := ℝ) (fun (ω : Ω) ↦ 2 * X ω * deriv (cgf X μ) v * rexp (v * X ω)) μ
⊢ Integrable (ε := ℝ)
    (fun (ω : Ω) ↦ HPow.hPow (β := ℕ) (X ω) 2 * rexp (v * X ω) - 2 * X ω * deriv (cgf X μ) v * rexp (v * X ω)) μ

Tactic:
exact (integrable_pow_mul_exp_of_mem_interior_integrableExpSet h 2).sub h_int

Premises used: MeasureTheory.Integrable.sub, ProbabilityTheory.integrable_pow_mul_exp_of_mem_interior_integrableExpSet, OfNat.ofNat
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
h_int : Integrable (ε := ℝ) (fun (ω : Ω) ↦ 2 * X ω * deriv (cgf X μ) v * rexp (v * X ω)) μ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2 * rexp (v * X ω)) μ

Tactic:
(interior_subset (s := integrableExpSet X μ) h).const_mul _

Premises used: interior_subset, MeasureTheory.Integrable.const_mul
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
h_int : Integrable (ε := ℝ) (fun (ω : Ω) ↦ 2 * X ω * deriv (cgf X μ) v * rexp (v * X ω)) μ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2 * rexp (v * X ω)) μ

Tactic:
exact (interior_subset (s := integrableExpSet X μ) h).const_mul _

Premises used: interior_subset, MeasureTheory.Integrable.const_mul
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
h_int : Integrable (ε := ℝ) (fun (ω : Ω) ↦ 2 * X ω * deriv (cgf X μ) v * rexp (v * X ω)) μ
e_a :
  ∫ (ω : Ω), HPow.hPow (β := ℕ) (X ω) 2 * rexp (v * X ω) ∂μ -
        HMul.hMul (α := ℝ) 2 (∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) * deriv (cgf X μ) v +
      HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2 * mgf X μ v =
    HSub.hSub (α := ℝ) (∫ (a : Ω), HPow.hPow (β := ℕ) (X a) 2 * rexp (v * X a) ∂μ)
        (∫ (a : Ω), 2 * X a * deriv (cgf X μ) v * rexp (v * X a) ∂μ) +
      ∫ (a : Ω), HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2 * rexp (v * X a) ∂μ
⊢ ∫ (ω : Ω), HPow.hPow (β := ℕ) (X ω) 2 * rexp (v * X ω) ∂μ -
        HMul.hMul (α := ℝ) 2 (∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) * deriv (cgf X μ) v +
      HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2 * mgf X μ v =
    HAdd.hAdd (α := ℝ)
      (∫ (a : Ω), HPow.hPow (β := ℕ) (X a) 2 * rexp (v * X a) - 2 * X a * deriv (cgf X μ) v * rexp (v * X a) ∂μ)
      (∫ (a : Ω), HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2 * rexp (v * X a) ∂μ)

Tactic:
rw [integral_sub (integrable_pow_mul_exp_of_mem_interior_integrableExpSet h 2) h_int]

Premises used: MeasureTheory.integral_sub, ProbabilityTheory.integrable_pow_mul_exp_of_mem_interior_integrableExpSet, OfNat.ofNat
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
h_int : Integrable (ε := ℝ) (fun (ω : Ω) ↦ 2 * X ω * deriv (cgf X μ) v * rexp (v * X ω)) μ
e_a :
  HMul.hMul (α := ℝ) 2 (∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) * deriv (cgf X μ) v =
    ∫ (a : Ω), 2 * X a * deriv (cgf X μ) v * rexp (v * X a) ∂μ
e_a₁ :
  HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2 * mgf X μ v =
    ∫ (a : Ω), HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2 * rexp (v * X a) ∂μ
⊢ ∫ (ω : Ω), HPow.hPow (β := ℕ) (X ω) 2 * rexp (v * X ω) ∂μ -
        HMul.hMul (α := ℝ) 2 (∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) * deriv (cgf X μ) v +
      HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2 * mgf X μ v =
    HSub.hSub (α := ℝ) (∫ (a : Ω), HPow.hPow (β := ℕ) (X a) 2 * rexp (v * X a) ∂μ)
        (∫ (a : Ω), 2 * X a * deriv (cgf X μ) v * rexp (v * X a) ∂μ) +
      ∫ (a : Ω), HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2 * rexp (v * X a) ∂μ

Tactic:
congr
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
h_int : Integrable (ε := ℝ) (fun (ω : Ω) ↦ 2 * X ω * deriv (cgf X μ) v * rexp (v * X ω)) μ
e_a :
  Eq (α := ℝ) (∫ (a : Ω), 2 * (X a * rexp (v * X a)) * deriv (cgf X μ) v ∂μ)
    (∫ (a : Ω), 2 * X a * deriv (cgf X μ) v * rexp (v * X a) ∂μ)
⊢ HMul.hMul (α := ℝ) 2 (∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) * deriv (cgf X μ) v =
    ∫ (a : Ω), 2 * X a * deriv (cgf X μ) v * rexp (v * X a) ∂μ

Tactic:
rw [← integral_const_mul, ← integral_mul_const]

Premises used: MeasureTheory.integral_const_mul, MeasureTheory.integral_mul_const
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
h_int : Integrable (ε := ℝ) (fun (ω : Ω) ↦ 2 * X ω * deriv (cgf X μ) v * rexp (v * X ω)) μ
e_a : ∀ (ω : Ω), 2 * (X ω * rexp (v * X ω)) * deriv (cgf X μ) v = 2 * X ω * deriv (cgf X μ) v * rexp (v * X ω)
⊢ Eq (α := ℝ) (∫ (a : Ω), 2 * (X a * rexp (v * X a)) * deriv (cgf X μ) v ∂μ)
    (∫ (a : Ω), 2 * X a * deriv (cgf X μ) v * rexp (v * X a) ∂μ)

Tactic:
congr with ω
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
h_int : Integrable (ε := ℝ) (fun (ω : Ω) ↦ 2 * X ω * deriv (cgf X μ) v * rexp (v * X ω)) μ
ω : Ω
⊢ 2 * (X ω * rexp (v * X ω)) * deriv (cgf X μ) v = 2 * X ω * deriv (cgf X μ) v * rexp (v * X ω)

Tactic:
ring
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
h_int : Integrable (ε := ℝ) (fun (ω : Ω) ↦ 2 * X ω * deriv (cgf X μ) v * rexp (v * X ω)) μ
e_a :
  HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2 * mgf X μ v =
    HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2 * ∫ (a : Ω), rexp (v * X a) ∂μ
e_a₁ e_a₂ :
  HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2 * ∫ (x : Ω), (fun (ω : Ω) ↦ rexp (v * X ω)) x ∂μ =
    HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2 * ∫ (a : Ω), rexp (v * X a) ∂μ
⊢ HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2 * mgf X μ v =
    ∫ (a : Ω), HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2 * rexp (v * X a) ∂μ

Tactic:
rw [integral_const_mul, mgf]

Premises used: MeasureTheory.integral_const_mul, ProbabilityTheory.mgf
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
e_a :
  ∀ (ω : Ω),
    (HPow.hPow (β := ℕ) (X ω) 2 - 2 * X ω * deriv (cgf X μ) v + HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2) *
        rexp (v * X ω) =
      HPow.hPow (β := ℕ) (X ω - deriv (cgf X μ) v) 2 * rexp (v * X ω)
⊢ (∫ (ω : Ω),
        (HPow.hPow (β := ℕ) (X ω) 2 - 2 * X ω * deriv (cgf X μ) v + HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2) *
          rexp (v * X ω) ∂μ) /
      mgf X μ v =
    (∫ (ω : Ω), HPow.hPow (β := ℕ) (X ω - deriv (cgf X μ) v) 2 * rexp (v * X ω) ∂μ) / mgf X μ v

Tactic:
congr with ω
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
ω : Ω
⊢ (HPow.hPow (β := ℕ) (X ω) 2 - 2 * X ω * deriv (cgf X μ) v + HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2) *
      rexp (v * X ω) =
    HPow.hPow (β := ℕ) (X ω - deriv (cgf X μ) v) 2 * rexp (v * X ω)

Tactic:
ring
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
calc :
  (∫ (ω : Ω), HPow.hPow (β := ℕ) (X ω) 2 * rexp (v * X ω) ∂μ) / mgf X μ v - HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2 =
    (∫ (ω : Ω), HPow.hPow (β := ℕ) (X ω) 2 * rexp (v * X ω) ∂μ -
          HMul.hMul (α := ℝ) 2 (∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) * deriv (cgf X μ) v +
        HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2 * mgf X μ v) /
      mgf X μ v
calc₁ :
  (∫ (ω : Ω), HPow.hPow (β := ℕ) (X ω) 2 * rexp (v * X ω) ∂μ -
          HMul.hMul (α := ℝ) 2 (∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) * deriv (cgf X μ) v +
        HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2 * mgf X μ v) /
      mgf X μ v =
    (∫ (ω : Ω),
        (HPow.hPow (β := ℕ) (X ω) 2 - 2 * X ω * deriv (cgf X μ) v + HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2) *
          rexp (v * X ω) ∂μ) /
      mgf X μ v
calc₂ :
  (∫ (ω : Ω),
        (HPow.hPow (β := ℕ) (X ω) 2 - 2 * X ω * deriv (cgf X μ) v + HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2) *
          rexp (v * X ω) ∂μ) /
      mgf X μ v =
    (∫ (ω : Ω), HPow.hPow (β := ℕ) (X ω - deriv (cgf X μ) v) 2 * rexp (v * X ω) ∂μ) / mgf X μ v
⊢ (∫ (x : Ω), (fun (ω : Ω) ↦ HPow.hPow (β := ℕ) (X ω) 2 * rexp (v * X ω)) x ∂μ) / mgf X μ v -
      HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2 =
    (∫ (x : Ω), (fun (ω : Ω) ↦ HPow.hPow (β := ℕ) (X ω - deriv (cgf X μ) v) 2 * rexp (v * X ω)) x ∂μ) / mgf X μ v

Tactic:
calc (∫ ω, (X ω) ^ 2 * exp (v * X ω) ∂μ) / mgf X μ v - deriv (cgf X μ) v ^ 2
  _ = (∫ ω, (X ω) ^ 2 * exp (v * X ω) ∂μ - 2 * (∫ ω, X ω * exp (v * X ω) ∂μ) * deriv (cgf X μ) v
      + deriv (cgf X μ) v ^ 2 * mgf X μ v) / mgf X μ v := by
    rw [add_div, sub_div, sub_add]
    congr 1
    rw [mul_div_cancel_right₀, deriv_cgf h]
    · ring
    · exact (mgf_pos' hμ (interior_subset (s := integrableExpSet X μ) h)).ne'
  _ = (∫ ω, ((X ω) ^ 2 - 2 * X ω * deriv (cgf X μ) v + deriv (cgf X μ) v ^ 2) * exp (v * X ω) ∂μ)
      / mgf X μ v := by
    congr 1
    simp_rw [add_mul, sub_mul]
    have h_int : Integrable (fun ω ↦ 2 * X ω * deriv (cgf X μ) v * exp (v * X ω)) μ := by
      simp_rw [mul_assoc, mul_comm (deriv (cgf X μ) v)]
      refine Integrable.const_mul ?_ _
      simp_rw [← mul_assoc]
      refine Integrable.mul_const ?_ _
      convert! integrable_pow_mul_exp_of_mem_interior_integrableExpSet h 1
      simp
    rw [integral_add]
    rotate_left
    · exact (integrable_pow_mul_exp_of_mem_interior_integrableExpSet h 2).sub h_int
    · exact (interior_subset (s := integrableExpSet X μ) h).const_mul _
    rw [integral_sub (integrable_pow_mul_exp_of_mem_interior_integrableExpSet h 2) h_int]
    congr
    · rw [← integral_const_mul, ← integral_mul_const]
      congr with ω
      ring
    · rw [integral_const_mul, mgf]
  _ = (∫ ω, (X ω - deriv (cgf X μ) v) ^ 2 * exp (v * X ω) ∂μ) / mgf X μ v := by
    congr with ω
    ring

Premises used: HMul.hMul, ProbabilityTheory.cgf, deriv, HSub.hSub, Real.exp, HPow.hPow, HAdd.hAdd, MeasureTheory.integral, ProbabilityTheory.mgf, OfNat.ofNat
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst : IsZeroOrProbabilityMeasure μ
ht : 0 < t
hc : Eq (α := ℝ) (∫ (x : Ω), X x ∂μ) 0
hs : Set.Icc 0 t ⊆ interior (integrableExpSet X μ)
⊢ UniqueDiffOn ℝ (Set.Icc 0 t)

Tactic:
have hu : UniqueDiffOn ℝ (Set.Icc 0 t) := uniqueDiffOn_Icc ht
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst : IsZeroOrProbabilityMeasure μ
ht : 0 < t
hc : Eq (α := ℝ) (∫ (x : Ω), X x ∂μ) 0
hs : Set.Icc 0 t ⊆ interior (integrableExpSet X μ)
hu : UniqueDiffOn ℝ (Set.Icc 0 t)
rw : ∃ u ∈ Set.Ioo 0 t, cgf X μ t - 0 = iteratedDeriv 2 (cgf X μ) u * HPow.hPow (β := ℕ) t 2 / 2
⊢ ∃ u ∈ Set.Ioo 0 t, cgf X μ t = iteratedDeriv 2 (cgf X μ) u * HPow.hPow (β := ℕ) t 2 / 2

Tactic:
rw [← sub_zero (cgf X μ t)]

Premises used: ProbabilityTheory.cgf, sub_zero
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst : IsZeroOrProbabilityMeasure μ
ht : 0 < t
hc : Eq (α := ℝ) (∫ (x : Ω), X x ∂μ) 0
hs : Set.Icc 0 t ⊆ interior (integrableExpSet X μ)
hu : UniqueDiffOn ℝ (Set.Icc 0 t)
nth_rw : ∃ u ∈ Set.Ioo 0 t, cgf X μ t - 0 = iteratedDeriv 2 (cgf X μ) u * HPow.hPow (β := ℕ) (t - 0) 2 / 2
⊢ ∃ u ∈ Set.Ioo 0 t, cgf X μ t - 0 = iteratedDeriv 2 (cgf X μ) u * HPow.hPow (β := ℕ) t 2 / 2

Tactic:
nth_rw 3 [← sub_zero t]

Premises used: sub_zero
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst : IsZeroOrProbabilityMeasure μ
ht : 0 < t
hc : Eq (α := ℝ) (∫ (x : Ω), X x ∂μ) 0
hs : Set.Icc 0 t ⊆ interior (integrableExpSet X μ)
hu : UniqueDiffOn ℝ (Set.Icc 0 t)
rw : ∃ u ∈ Set.uIoo 0 t, cgf X μ t - 0 = iteratedDeriv 2 (cgf X μ) u * HPow.hPow (β := ℕ) (t - 0) 2 / 2
⊢ ∃ u ∈ Set.Ioo 0 t, cgf X μ t - 0 = iteratedDeriv 2 (cgf X μ) u * HPow.hPow (β := ℕ) (t - 0) 2 / 2

Tactic:
rw [← Set.uIoo_of_lt ht]

Premises used: Set.uIoo_of_lt
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst : IsZeroOrProbabilityMeasure μ
ht : 0 < t
hc : Eq (α := ℝ) (∫ (x : Ω), X x ∂μ) 0
hs : Set.Icc 0 t ⊆ interior (integrableExpSet X μ)
hu : UniqueDiffOn ℝ (Set.Icc 0 t)
⊢ ∃ x' ∈ Set.uIoo 0 t,
    cgf X μ t - taylorWithinEval (cgf X μ) 1 (Set.uIcc 0 t) 0 t =
      iteratedDeriv (HAdd.hAdd (α := ℕ) 1 1) (cgf X μ) x' * (t - 0) ^ HAdd.hAdd (α := ℕ) 1 1 /
        (↑(HAdd.hAdd (α := ℕ) 1 1)! : ℝ)

Tactic:
taylor_mean_remainder_lagrange_iteratedDeriv ht.ne ?_

Premises used: taylor_mean_remainder_lagrange_iteratedDeriv, LT.lt.ne
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst : IsZeroOrProbabilityMeasure μ
ht : 0 < t
hc : Eq (α := ℝ) (∫ (x : Ω), X x ∂μ) 0
hs : Set.Icc 0 t ⊆ interior (integrableExpSet X μ)
hu : UniqueDiffOn ℝ (Set.Icc 0 t)
h : ∀ (x : ℝ), 0 = taylorWithinEval (cgf X μ) 1 (Set.uIcc 0 t) 0 t
convert_3 : ContDiffOn ℝ (HAdd.hAdd (α := WithTop ℕ∞) (↑1 : WithTop ℕ∞) 1) (cgf X μ) (Set.uIcc 0 t)
⊢ ∃ u ∈ Set.uIoo 0 t, cgf X μ t - 0 = iteratedDeriv 2 (cgf X μ) u * HPow.hPow (β := ℕ) (t - 0) 2 / 2

Tactic:
convert! taylor_mean_remainder_lagrange_iteratedDeriv ht.ne ?_

Premises used: taylor_mean_remainder_lagrange_iteratedDeriv, LT.lt.ne
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst : IsZeroOrProbabilityMeasure μ
ht : 0 < t
hc : Eq (α := ℝ) (∫ (x : Ω), X x ∂μ) 0
hs : Set.Icc 0 t ⊆ interior (integrableExpSet X μ)
hu : UniqueDiffOn ℝ (Set.Icc 0 t)
x : ℝ
⊢ derivWithin (cgf X μ) (Set.Icc 0 t) 0 = deriv (cgf X μ) 0

Tactic:
(analyticAt_cgf (hs ⟨le_refl 0, le_of_lt ht⟩)).differentiableAt.derivWithin _

Premises used: le_refl, le_of_lt, ProbabilityTheory.analyticAt_cgf, DifferentiableAt.derivWithin, AnalyticAt.differentiableAt, And.intro, OfNat.ofNat
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst : IsZeroOrProbabilityMeasure μ
ht : 0 < t
hc : Eq (α := ℝ) (∫ (x : Ω), X x ∂μ) 0
hs : Set.Icc 0 t ⊆ interior (integrableExpSet X μ)
hu : UniqueDiffOn ℝ (Set.Icc 0 t)
x : ℝ
h : 0 = deriv (cgf X μ) 0
convert_2 : UniqueDiffWithinAt ℝ (Set.Icc 0 t) 0
⊢ derivWithin (cgf X μ) (Set.Icc 0 t) 0 = 0

Tactic:
convert! (analyticAt_cgf (hs ⟨le_refl 0, le_of_lt ht⟩)).differentiableAt.derivWithin _

Premises used: le_refl, le_of_lt, ProbabilityTheory.analyticAt_cgf, DifferentiableAt.derivWithin, AnalyticAt.differentiableAt, And.intro, OfNat.ofNat
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst : IsZeroOrProbabilityMeasure μ
ht : 0 < t
hc : Eq (α := ℝ) (∫ (x : Ω), X x ∂μ) 0
hs : Set.Icc 0 t ⊆ interior (integrableExpSet X μ)
hu : UniqueDiffOn ℝ (Set.Icc 0 t)
x : ℝ
⊢ 0 = deriv (cgf X μ) 0

Tactic:
simpa [hc] using (deriv_cgf_zero (hs ⟨le_refl 0, le_of_lt ht⟩)).symm

Premises used: le_refl, le_of_lt, And.intro, ProbabilityTheory.deriv_cgf_zero, OfNat.ofNat, Eq.symm
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst : IsZeroOrProbabilityMeasure μ
ht : 0 < t
hc : Eq (α := ℝ) (∫ (x : Ω), X x ∂μ) 0
hs : Set.Icc 0 t ⊆ interior (integrableExpSet X μ)
hu : UniqueDiffOn ℝ (Set.Icc 0 t)
x : ℝ
⊢ UniqueDiffWithinAt ℝ (Set.Icc 0 t) 0

Tactic:
hu 0 ⟨le_refl 0, le_of_lt ht⟩

Premises used: le_refl, le_of_lt, And.intro, OfNat.ofNat
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst : IsZeroOrProbabilityMeasure μ
ht : 0 < t
hc : Eq (α := ℝ) (∫ (x : Ω), X x ∂μ) 0
hs : Set.Icc 0 t ⊆ interior (integrableExpSet X μ)
hu : UniqueDiffOn ℝ (Set.Icc 0 t)
x : ℝ
⊢ UniqueDiffWithinAt ℝ (Set.Icc 0 t) 0

Tactic:
exact hu 0 ⟨le_refl 0, le_of_lt ht⟩

Premises used: le_refl, le_of_lt, And.intro, OfNat.ofNat
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst : IsZeroOrProbabilityMeasure μ
ht : 0 < t
hc : Eq (α := ℝ) (∫ (x : Ω), X x ∂μ) 0
hs : Set.Icc 0 t ⊆ interior (integrableExpSet X μ)
hu : UniqueDiffOn ℝ (Set.Icc 0 t)
x : ℝ
⊢ derivWithin (cgf X μ) (Set.Icc 0 t) 0 = 0

Tactic:
have hd : derivWithin (cgf X μ) (Set.Icc 0 t) 0 = 0 := by
      convert! (analyticAt_cgf (hs ⟨le_refl 0, le_of_lt ht⟩)).differentiableAt.derivWithin _
      · simpa [hc] using (deriv_cgf_zero (hs ⟨le_refl 0, le_of_lt ht⟩)).symm
      · exact hu 0 ⟨le_refl 0, le_of_lt ht⟩
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst : IsZeroOrProbabilityMeasure μ
ht : 0 < t
hc : Eq (α := ℝ) (∫ (x : Ω), X x ∂μ) 0
hs : Set.Icc 0 t ⊆ interior (integrableExpSet X μ)
hu : UniqueDiffOn ℝ (Set.Icc 0 t)
x : ℝ
hd : derivWithin (cgf X μ) (Set.Icc 0 t) 0 = 0
⊢ 0 = taylorWithinEval (cgf X μ) 1 (Set.uIcc 0 t) 0 t

Tactic:
simp [hd, Set.uIcc_of_lt ht]

Premises used: Set.uIcc_of_lt
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst : IsZeroOrProbabilityMeasure μ
ht : 0 < t
hc : Eq (α := ℝ) (∫ (x : Ω), X x ∂μ) 0
hs : Set.Icc 0 t ⊆ interior (integrableExpSet X μ)
hu : UniqueDiffOn ℝ (Set.Icc 0 t)
convert_3 : ContDiffOn ℝ (HAdd.hAdd (α := WithTop ℕ∞) (↑1 : WithTop ℕ∞) 1) (cgf X μ) (Set.Icc 0 t)
⊢ ContDiffOn ℝ (HAdd.hAdd (α := WithTop ℕ∞) (↑1 : WithTop ℕ∞) 1) (cgf X μ) (Set.uIcc 0 t)

Tactic:
rw [Set.uIcc_of_lt ht]

Premises used: Set.uIcc_of_lt
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst : IsZeroOrProbabilityMeasure μ
ht : 0 < t
hc : Eq (α := ℝ) (∫ (x : Ω), X x ∂μ) 0
hs : Set.Icc 0 t ⊆ interior (integrableExpSet X μ)
hu : UniqueDiffOn ℝ (Set.Icc 0 t)
⊢ ContDiffOn ℝ (HAdd.hAdd (α := WithTop ℕ∞) (↑1 : WithTop ℕ∞) 1) (cgf X μ) (Set.Icc 0 t)

Tactic:
(analyticOn_cgf.mono hs).contDiffOn hu

Premises used: ProbabilityTheory.analyticOn_cgf, AnalyticOn.contDiffOn, AnalyticOn.mono
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst : IsZeroOrProbabilityMeasure μ
ht : 0 < t
hc : Eq (α := ℝ) (∫ (x : Ω), X x ∂μ) 0
hs : Set.Icc 0 t ⊆ interior (integrableExpSet X μ)
hu : UniqueDiffOn ℝ (Set.Icc 0 t)
⊢ ContDiffOn ℝ (HAdd.hAdd (α := WithTop ℕ∞) (↑1 : WithTop ℕ∞) 1) (cgf X μ) (Set.Icc 0 t)

Tactic:
exact (analyticOn_cgf.mono hs).contDiffOn hu

Premises used: ProbabilityTheory.analyticOn_cgf, AnalyticOn.contDiffOn, AnalyticOn.mono
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
⊢ @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (1 * X ω)) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)

Tactic:
have h_int := h.integrable_exp_mul 1
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
h_int : @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (1 * X ω)) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)
⊢ AEStronglyMeasurable (m₀ := mΩ) X ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)

Tactic:
simpa using (aemeasurable_of_aemeasurable_exp h_int.1.aemeasurable).aestronglyMeasurable

Premises used: AEMeasurable.aestronglyMeasurable, MeasureTheory.AEStronglyMeasurable.aemeasurable, And.left, Real.aemeasurable_of_aemeasurable_exp
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
t : ℝ
⊢ ∀ᵐ (ω' : Ω') ∂ν, @Integrable ℝ _ _ _ mΩ (fun (y : Ω) ↦ rexp (t * X y)) ((κ : (a : Ω') → Measure Ω) ω')

Tactic:
Measure.ae_integrable_of_integrable_comp (h.integrable_exp_mul t)

Premises used: ProbabilityTheory.Kernel.HasSubgaussianMGF.integrable_exp_mul, MeasureTheory.Measure.ae_integrable_of_integrable_comp
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
⊢ ∀ᵐ (ω' : Ω') ∂ν, @Integrable ℝ _ _ _ mΩ (fun (y : Ω) ↦ rexp (1 * X y)) ((κ : (a : Ω') → Measure Ω) ω')

Tactic:
have h_int := h.ae_integrable_exp_mul 1
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
h_int : ∀ᵐ (ω' : Ω') ∂ν, @Integrable ℝ _ _ _ mΩ (fun (y : Ω) ↦ rexp (1 * X y)) ((κ : (a : Ω') → Measure Ω) ω')
h₁ :
  ∀ (ω : Ω') (h_int : @Integrable ℝ _ _ _ mΩ (fun (y : Ω) ↦ rexp (1 * X y)) ((κ : (a : Ω') → Measure Ω) ω)),
    AEStronglyMeasurable (m₀ := mΩ) X ((κ : (a : Ω') → Measure Ω) ω)
⊢ ∀ᵐ (ω' : Ω') ∂ν, AEStronglyMeasurable (m₀ := mΩ) X ((κ : (a : Ω') → Measure Ω) ω')

Tactic:
filter_upwards [h_int] with ω h_int