awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.CentralLimitTheorem (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : IsProbabilityMeasure P
X : Ω → ℝ
hX : AEMeasurable X P
h0 : Eq (α := ℝ) (∫ (x : Ω), X x ∂P) 0
h1 : Eq (α := ℝ) (∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂P) 1
t : ℝ
this :
  Asymptotics.IsLittleO (E := ℂ) (F := ℝ) atTop
    (fun (n : ℕ) ↦
      charFun (mE := Real.measurableSpace) (Measure.map X P) ((√(↑n : ℝ))⁻¹ * t) -
        (1 + -(HPow.hPow (β := ℕ) ((↑(√(↑n : ℝ))⁻¹ : ℂ) * (↑t : ℂ)) 2 / 2)))
    fun (n : ℕ) ↦ HPow.hPow (β := ℕ) ((√(↑n : ℝ))⁻¹ * t) 2
aux :
  Eq (α := (n : ℕ) → ℝ) (fun (n : ℕ) ↦ ‖HDiv.hDiv (α := ℂ) 1 (↑n : ℂ)‖) fun (n : ℕ) ↦ ‖HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)‖
⊢ Asymptotics.IsLittleO (E := ℂ) (F := ℂ) atTop
    (fun (n : ℕ) ↦
      charFun (mE := Real.measurableSpace) (Measure.map X P) ((√(↑n : ℝ))⁻¹ * t) -
        (1 + -HPow.hPow (β := ℕ) (↑t : ℂ) 2 / 2 / (↑n : ℂ)))
    fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) 1 (↑n : ℂ)
have rw : Asymptotics.IsLittleO (E := ℂ) (F := ℝ) atTop
  (fun (n : ℕ) ↦
    charFun (mE := Real.measurableSpace) (Measure.map X P) ((√(↑n : ℝ))⁻¹ * t) -
      (1 + -HPow.hPow (β := ℕ) (↑t : ℂ) 2 / 2 / (↑n : ℂ)))
  fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)
Tactic: rw [← Asymptotics.isLittleO_norm_right, aux, Asymptotics.isLittleO_norm_right]
-- Lean 4 proof step from Mathlib.Probability.CentralLimitTheorem (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : IsProbabilityMeasure P
X : Ω → ℝ
hX : AEMeasurable X P
h0 : Eq (α := ℝ) (∫ (x : Ω), X x ∂P) 0
h1 : Eq (α := ℝ) (∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂P) 1
t : ℝ
this :
  Asymptotics.IsLittleO (E := ℂ) (F := ℝ) atTop
    (fun (n : ℕ) ↦
      charFun (mE := Real.measurableSpace) (Measure.map X P) ((√(↑n : ℝ))⁻¹ * t) -
        (1 + -(HPow.hPow (β := ℕ) ((↑(√(↑n : ℝ))⁻¹ : ℂ) * (↑t : ℂ)) 2 / 2)))
    fun (n : ℕ) ↦ HPow.hPow (β := ℕ) ((√(↑n : ℝ))⁻¹ * t) 2
aux :
  Eq (α := (n : ℕ) → ℝ) (fun (n : ℕ) ↦ ‖HDiv.hDiv (α := ℂ) 1 (↑n : ℂ)‖) fun (n : ℕ) ↦ ‖HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)‖
⊢ Asymptotics.IsLittleO (E := ℂ) (F := ℝ) atTop
    (fun (n : ℕ) ↦
      charFun (mE := Real.measurableSpace) (Measure.map X P) ((√(↑n : ℝ))⁻¹ * t) -
        (1 + -HPow.hPow (β := ℕ) (↑t : ℂ) 2 / 2 / (↑n : ℂ)))
    fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)
have refine : Asymptotics.IsLittleO (E := ℂ) (F := ℝ) atTop
  (fun (n : ℕ) ↦
    charFun (mE := Real.measurableSpace) (Measure.map X P) ((√(↑n : ℝ))⁻¹ * t) -
      (1 + -HPow.hPow (β := ℕ) (↑t : ℂ) 2 / 2 / (↑n : ℂ)))
  fun (x : ℕ) ↦ HPow.hPow (β := ℕ) t 2 * HDiv.hDiv (α := ℝ) 1 (↑x : ℝ)
Tactic: refine .of_const_mul_right (c := t ^ 2) ?_
-- Lean 4 proof step from Mathlib.Probability.CentralLimitTheorem (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : IsProbabilityMeasure P
X : Ω → ℝ
hX : AEMeasurable X P
h0 : Eq (α := ℝ) (∫ (x : Ω), X x ∂P) 0
h1 : Eq (α := ℝ) (∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂P) 1
t : ℝ
this :
  Asymptotics.IsLittleO (E := ℂ) (F := ℝ) atTop
    (fun (n : ℕ) ↦
      charFun (mE := Real.measurableSpace) (Measure.map X P) ((√(↑n : ℝ))⁻¹ * t) -
        (1 + -(HPow.hPow (β := ℕ) ((↑(√(↑n : ℝ))⁻¹ : ℂ) * (↑t : ℂ)) 2 / 2)))
    fun (n : ℕ) ↦ HPow.hPow (β := ℕ) ((√(↑n : ℝ))⁻¹ * t) 2
aux :
  Eq (α := (n : ℕ) → ℝ) (fun (n : ℕ) ↦ ‖HDiv.hDiv (α := ℂ) 1 (↑n : ℂ)‖) fun (n : ℕ) ↦ ‖HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)‖
⊢ Asymptotics.IsLittleO (E := ℂ) (F := ℝ) atTop
    (fun (n : ℕ) ↦
      charFun (mE := Real.measurableSpace) (Measure.map X P) ((√(↑n : ℝ))⁻¹ * t) -
        (1 + -HPow.hPow (β := ℕ) (↑t : ℂ) 2 / 2 / (↑n : ℂ)))
    fun (x : ℕ) ↦ HPow.hPow (β := ℕ) t 2 * HDiv.hDiv (α := ℝ) 1 (↑x : ℝ)
have h : ∀ (n : ℕ), -HPow.hPow (β := ℕ) (↑t : ℂ) 2 / 2 / (↑n : ℂ) = -(HPow.hPow (β := ℕ) ((↑(√(↑n : ℝ))⁻¹ : ℂ) * (↑t : ℂ)) 2 / 2)
Tactic: convert! this using 4 with n
-- Lean 4 proof step from Mathlib.Probability.CentralLimitTheorem (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : IsProbabilityMeasure P
X : Ω → ℝ
hX : AEMeasurable X P
h0 : Eq (α := ℝ) (∫ (x : Ω), X x ∂P) 0
h1 : Eq (α := ℝ) (∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂P) 1
t : ℝ
this :
  Asymptotics.IsLittleO (E := ℂ) (F := ℝ) atTop
    (fun (n : ℕ) ↦
      charFun (mE := Real.measurableSpace) (Measure.map X P) ((√(↑n : ℝ))⁻¹ * t) -
        (1 + -(HPow.hPow (β := ℕ) ((↑(√(↑n : ℝ))⁻¹ : ℂ) * (↑t : ℂ)) 2 / 2)))
    fun (n : ℕ) ↦ HPow.hPow (β := ℕ) ((√(↑n : ℝ))⁻¹ * t) 2
aux :
  Eq (α := (n : ℕ) → ℝ) (fun (n : ℕ) ↦ ‖HDiv.hDiv (α := ℂ) 1 (↑n : ℂ)‖) fun (n : ℕ) ↦ ‖HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)‖
h :
  ∀ (n : ℕ),
    -HPow.hPow (β := ℕ) (↑t : ℂ) 2 / 2 / (↑n : ℂ) = -(HPow.hPow (β := ℕ) ((↑(√(↑n : ℝ))⁻¹ : ℂ) * (↑t : ℂ)) 2 / 2)
⊢ Asymptotics.IsLittleO (E := ℂ) (F := ℝ) atTop
    (fun (n : ℕ) ↦
      charFun (mE := Real.measurableSpace) (Measure.map X P) ((√(↑n : ℝ))⁻¹ * t) -
        (1 + -HPow.hPow (β := ℕ) (↑t : ℂ) 2 / 2 / (↑n : ℂ)))
    fun (x : ℕ) ↦ HPow.hPow (β := ℕ) t 2 * HDiv.hDiv (α := ℝ) 1 (↑x : ℝ)
have h₁ : ∀ (x : ℕ), HPow.hPow (β := ℕ) t 2 * HDiv.hDiv (α := ℝ) 1 (↑x : ℝ) = HPow.hPow (β := ℕ) ((√(↑x : ℝ))⁻¹ * t) 2
Tactic: convert! this using 4 with n
-- Lean 4 proof step from Mathlib.Probability.CentralLimitTheorem (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : IsProbabilityMeasure P
X : Ω → ℝ
hX : AEMeasurable X P
h0 : Eq (α := ℝ) (∫ (x : Ω), X x ∂P) 0
h1 : Eq (α := ℝ) (∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂P) 1
t : ℝ
this :
  Asymptotics.IsLittleO (E := ℂ) (F := ℝ) atTop
    (fun (n : ℕ) ↦
      charFun (mE := Real.measurableSpace) (Measure.map X P) ((√(↑n : ℝ))⁻¹ * t) -
        (1 + -(HPow.hPow (β := ℕ) ((↑(√(↑n : ℝ))⁻¹ : ℂ) * (↑t : ℂ)) 2 / 2)))
    fun (n : ℕ) ↦ HPow.hPow (β := ℕ) ((√(↑n : ℝ))⁻¹ * t) 2
aux :
  Eq (α := (n : ℕ) → ℝ) (fun (n : ℕ) ↦ ‖HDiv.hDiv (α := ℂ) 1 (↑n : ℂ)‖) fun (n : ℕ) ↦ ‖HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)‖
n : ℕ
⊢ -HPow.hPow (β := ℕ) (↑t : ℂ) 2 / 2 / (↑n : ℂ) = -(HPow.hPow (β := ℕ) ((↑(√(↑n : ℝ))⁻¹ : ℂ) * (↑t : ℂ)) 2 / 2)
have h : -HPow.hPow (β := ℕ) t 2 / 2 / (↑n : ℝ) = -(HPow.hPow (β := ℕ) ((√(↑n : ℝ))⁻¹ * t) 2 / 2)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Probability.CentralLimitTheorem (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : IsProbabilityMeasure P
X : Ω → ℝ
hX : AEMeasurable X P
h0 : Eq (α := ℝ) (∫ (x : Ω), X x ∂P) 0
h1 : Eq (α := ℝ) (∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂P) 1
t : ℝ
⊢ Asymptotics.IsLittleO (E := ℂ) (F := ℂ) atTop
    (fun (n : ℕ) ↦
      charFun (mE := Real.measurableSpace) (Measure.map X P) ((√(↑n : ℝ))⁻¹ * t) -
        (1 + -HPow.hPow (β := ℕ) (↑t : ℂ) 2 / 2 / (↑n : ℂ)))
    fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) 1 (↑n : ℂ)
have hf : Asymptotics.IsLittleO (E := ℂ) (F := ℝ) atTop
  (fun (n : ℕ) ↦
    charFun (mE := Real.measurableSpace) (Measure.map X P) ((√(↑n : ℝ))⁻¹ * t) -
      (1 + -(HPow.hPow (β := ℕ) ((↑(√(↑n : ℝ))⁻¹ : ℂ) * (↑t : ℂ)) 2 / 2)))
  fun (n : ℕ) ↦ HPow.hPow (β := ℕ) ((√(↑n : ℝ))⁻¹ * t) 2
Tactic: suffices (fun (n : ℕ) ↦ charFun (Measure.map X P) ((√n)⁻¹ * t) -
      (1 + (-(((√n)⁻¹ * t) ^ 2 / 2) : ℂ))) =o[atTop] fun n ↦ ((√n)⁻¹ * t) ^ 2 by
    have aux : (fun (n : ℕ) ↦ ‖(1 / n : ℂ)‖) = fun (n : ℕ) ↦ ‖(1 / n : ℝ)‖ := by simp
    rw [← Asymptotics.isLittleO_norm_right, aux, Asymptotics.isLittleO_norm_right]
    refine .of_const_mul_right (c := t ^ 2) ?_
    convert! this using 4 with n <;> norm_cast <;> simp [field]
-- Lean 4 proof step from Mathlib.Probability.CentralLimitTheorem (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : IsProbabilityMeasure P
X : Ω → ℝ
hX : AEMeasurable X P
h0 : Eq (α := ℝ) (∫ (x : Ω), X x ∂P) 0
h1 : Eq (α := ℝ) (∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂P) 1
t : ℝ
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ (√(↑n : ℝ))⁻¹ * t) atTop (𝓝 0)
have rw : Tendsto (fun (n : ℕ) ↦ (√(↑n : ℝ))⁻¹ * t) atTop (𝓝 (0 * t))
Tactic: rw [← zero_mul t]
-- Lean 4 proof step from Mathlib.Probability.CentralLimitTheorem (hypothesis)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : IsProbabilityMeasure P
X : Ω → ℝ
hX : AEMeasurable X P
h0 : Eq (α := ℝ) (∫ (x : Ω), X x ∂P) 0
h1 : Eq (α := ℝ) (∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂P) 1
t : ℝ
⊢ Asymptotics.IsLittleO (E := ℂ) (F := ℝ) atTop
    (fun (n : ℕ) ↦
      charFun (mE := Real.measurableSpace) (Measure.map X P) ((√(↑n : ℝ))⁻¹ * t) -
        (1 + -(HPow.hPow (β := ℕ) ((↑(√(↑n : ℝ))⁻¹ : ℂ) * (↑t : ℂ)) 2 / 2)))
    fun (n : ℕ) ↦ HPow.hPow (β := ℕ) ((√(↑n : ℝ))⁻¹ * t) 2
have this : Tendsto (β := ℝ) (fun (n : ℕ) ↦ (√(↑n : ℝ))⁻¹ * t) atTop (𝓝 0)
Tactic: have : Tendsto (fun (n : ℕ) ↦ (√n)⁻¹ * t) atTop (𝓝 0) := by
    rw [← zero_mul t]
    exact .mul_const t (tendsto_inv_atTop_zero.comp <| Real.tendsto_sqrt_atTop.comp <|
      tendsto_natCast_atTop_atTop)
-- Lean 4 proof step from Mathlib.Probability.CentralLimitTheorem (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : IsProbabilityMeasure P
X : Ω → ℝ
hX : AEMeasurable X P
h0 : Eq (α := ℝ) (∫ (x : Ω), X x ∂P) 0
h1 : Eq (α := ℝ) (∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂P) 1
t : ℝ
this : Tendsto (β := ℝ) (fun (n : ℕ) ↦ (√(↑n : ℝ))⁻¹ * t) atTop (𝓝 0)
⊢ Asymptotics.IsLittleO (E := ℂ) (F := ℝ) atTop
    (fun (n : ℕ) ↦
      charFun (mE := Real.measurableSpace) (Measure.map X P) ((√(↑n : ℝ))⁻¹ * t) -
        (1 + -(HPow.hPow (β := ℕ) ((↑(√(↑n : ℝ))⁻¹ : ℂ) * (↑t : ℂ)) 2 / 2)))
    fun (n : ℕ) ↦ HPow.hPow (β := ℕ) ((√(↑n : ℝ))⁻¹ * t) 2
have h : ∀ (x : ℕ),
  charFun (mE := Real.measurableSpace) (Measure.map X P) ((√(↑x : ℝ))⁻¹ * t) -
      (1 + -(HPow.hPow (β := ℕ) ((↑(√(↑x : ℝ))⁻¹ : ℂ) * (↑t : ℂ)) 2 / 2)) =
    ((fun (t : ℝ) ↦
          charFun (mE := Real.measurableSpace) (Measure.map X P) t - (1 - HPow.hPow (β := ℕ) (↑t : ℂ) 2 / 2)) ∘
        fun (n : ℕ) ↦ (√(↑n : ℝ))⁻¹ * t)
      x
Tactic: convert! (taylor_charFun_two hX h0 h1).comp_tendsto this using 2
-- Lean 4 proof step from Mathlib.Probability.CentralLimitTheorem (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : IsProbabilityMeasure P
X : Ω → ℝ
hX : AEMeasurable X P
h0 : Eq (α := ℝ) (∫ (x : Ω), X x ∂P) 0
h1 : Eq (α := ℝ) (∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂P) 1
t : ℝ
this : Tendsto (β := ℝ) (fun (n : ℕ) ↦ (√(↑n : ℝ))⁻¹ * t) atTop (𝓝 0)
x : ℕ
⊢ charFun (mE := Real.measurableSpace) (Measure.map X P) ((√(↑x : ℝ))⁻¹ * t) -
      (1 + -(HPow.hPow (β := ℕ) ((↑(√(↑x : ℝ))⁻¹ : ℂ) * (↑t : ℂ)) 2 / 2)) =
    ((fun (t : ℝ) ↦
          charFun (mE := Real.measurableSpace) (Measure.map X P) t - (1 - HPow.hPow (β := ℕ) (↑t : ℂ) 2 / 2)) ∘
        fun (n : ℕ) ↦ (√(↑n : ℝ))⁻¹ * t)
      x
have h : 1 + -(HPow.hPow (β := ℕ) ((↑√(↑x : ℝ) : ℂ)⁻¹ * (↑t : ℂ)) 2 / 2) =
  1 - HPow.hPow (β := ℕ) ((↑√(↑x : ℝ) : ℂ)⁻¹ * (↑t : ℂ)) 2 / 2
Tactic: simp
-- Lean 4 proof step from Mathlib.Probability.CentralLimitTheorem (goal)
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
P : Measure Ω
P' : Measure Ω'
X : ℕ → Ω → ℝ
Y : Ω' → ℝ
inst : IsProbabilityMeasure P
inst_1 : IsProbabilityMeasure P'
hY : HasLaw Y (gaussianReal 0 1) P'
h0 : Eq (α := ℝ) (∫ (x : Ω), X 0 x ∂P) 0
h1 : Eq (α := ℝ) (∫ (x : Ω), HPow.hPow (β := ℕ) (X 0) 2 x ∂P) 1
hindep : iIndepFun (β := fun (x : ℕ) ↦ ℝ) X P
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) P P
⊢ Tendsto
    (fun (n : ℕ) ↦
      Subtype.mk (p := fun (μ : Measure ℝ) ↦ IsProbabilityMeasure μ)
        (Measure.map (fun (ω : Ω) ↦ (√(↑n : ℝ))⁻¹ * ∑ k ∈ Finset.range n, X k ω) P) ⋯)
    atTop (𝓝 (Subtype.mk (p := fun (μ : Measure ℝ) ↦ IsProbabilityMeasure μ) (Measure.map Y P') ⋯))
have refine : ∀ (t : ℝ),
  Tendsto
    (fun (n : ℕ) ↦
      charFun (mE := Real.measurableSpace)
        (↑(Subtype.mk (p := fun (μ : Measure ℝ) ↦ IsProbabilityMeasure μ)
              (Measure.map (fun (ω : Ω) ↦ (√(↑n : ℝ))⁻¹ * ∑ k ∈ Finset.range n, X k ω) P) sorry) :
          Measure ℝ)
        t)
    atTop
    (𝓝 (charFun (↑(Subtype.mk (p := fun (μ : Measure ℝ) ↦ IsProbabilityMeasure μ) (Measure.map Y P') sorry) : Measure ℝ) t))
Tactic: refine ProbabilityMeasure.tendsto_iff_tendsto_charFun.2 fun t ↦ ?_
-- Lean 4 proof step from Mathlib.Probability.CentralLimitTheorem (goal)
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
P : Measure Ω
P' : Measure Ω'
X : ℕ → Ω → ℝ
Y : Ω' → ℝ
inst : IsProbabilityMeasure P
inst_1 : IsProbabilityMeasure P'
hY : HasLaw Y (gaussianReal 0 1) P'
h0 : Eq (α := ℝ) (∫ (x : Ω), X 0 x ∂P) 0
h1 : Eq (α := ℝ) (∫ (x : Ω), HPow.hPow (β := ℕ) (X 0) 2 x ∂P) 1
hindep : iIndepFun (β := fun (x : ℕ) ↦ ℝ) X P
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) P P
t : ℝ
⊢ Tendsto
    (fun (n : ℕ) ↦
      charFun (mE := Real.measurableSpace)
        (↑(Subtype.mk (p := fun (μ : Measure ℝ) ↦ IsProbabilityMeasure μ)
              (Measure.map (fun (ω : Ω) ↦ (√(↑n : ℝ))⁻¹ * ∑ k ∈ Finset.range n, X k ω) P) ⋯) :
          Measure ℝ)
        t)
    atTop
    (𝓝 (charFun (↑(Subtype.mk (p := fun (μ : Measure ℝ) ↦ IsProbabilityMeasure μ) (Measure.map Y P') ⋯) : Measure ℝ) t))
have rw! : Tendsto
  (fun (n : ℕ) ↦
    charFun (mE := Real.measurableSpace)
      (↑(Subtype.mk (p := fun (μ : Measure ℝ) ↦ IsProbabilityMeasure μ)
            (Measure.map (fun (ω : Ω) ↦ (√(↑n : ℝ))⁻¹ * ∑ k ∈ Finset.range n, X k ω) P) sorry) :
        Measure ℝ)
      t)
  atTop
  (𝓝 (charFun (↑(Subtype.mk (p := fun (μ : Measure ℝ) ↦ IsProbabilityMeasure μ) (gaussianReal 0 1) sorry) : Measure ℝ) t))
Tactic: rw! [hY.map_eq]
-- Lean 4 proof step from Mathlib.Probability.CentralLimitTheorem (hypothesis)
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
P : Measure Ω
P' : Measure Ω'
X : ℕ → Ω → ℝ
Y : Ω' → ℝ
inst : IsProbabilityMeasure P
inst_1 : IsProbabilityMeasure P'
hY : HasLaw Y (gaussianReal 0 1) P'
hX : Var[X 0; P] ≠ 0
hindep : iIndepFun (β := fun (x : ℕ) ↦ ℝ) X P
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) P P
⊢ TendstoInDistribution (Ω := fun (n : ℕ) ↦ Ω) (m := fun (i : ℕ) ↦ mΩ) (mE := Real.measurableSpace)
    (fun (n : ℕ) (ω : Ω) ↦
      (√((↑n : ℝ) * Var[X 0; P]))⁻¹ * (∑ k ∈ Finset.range n, X k ω - HMul.hMul (α := ℝ) (↑n : ℝ) (∫ (x : Ω), X 0 x ∂P)))
    atTop Y (fun (x : ℕ) ↦ P) P'
have mX0 : AEMeasurable (X 0) P
Tactic: have mX0 := (hident 0).aemeasurable_fst
-- Lean 4 proof step from Mathlib.Probability.CentralLimitTheorem (hypothesis)
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
P : Measure Ω
P' : Measure Ω'
X : ℕ → Ω → ℝ
Y : Ω' → ℝ
inst : IsProbabilityMeasure P
inst_1 : IsProbabilityMeasure P'
hY : HasLaw Y (gaussianReal 0 1) P'
hX : Var[X 0; P] ≠ 0
hindep : iIndepFun (β := fun (x : ℕ) ↦ ℝ) X P
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) P P
mX0 : AEMeasurable (X 0) P
⊢ TendstoInDistribution (Ω := fun (n : ℕ) ↦ Ω) (m := fun (i : ℕ) ↦ mΩ) (mE := Real.measurableSpace)
    (fun (n : ℕ) (ω : Ω) ↦
      (√((↑n : ℝ) * Var[X 0; P]))⁻¹ * (∑ k ∈ Finset.range n, X k ω - HMul.hMul (α := ℝ) (↑n : ℝ) (∫ (x : Ω), X 0 x ∂P)))
    atTop Y (fun (x : ℕ) ↦ P) P'
have intX0 : Integrable (X 0) P
Tactic: have intX0 : Integrable (X 0) P := memLp_one_iff_integrable.1 <|
    (memLp_two_of_variance_ne_zero mX0.aestronglyMeasurable hX).mono_exponent (by simp)
-- Lean 4 proof step from Mathlib.Probability.CentralLimitTheorem (goal)
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
P : Measure Ω
P' : Measure Ω'
X : ℕ → Ω → ℝ
Y : Ω' → ℝ
inst : IsProbabilityMeasure P
inst_1 : IsProbabilityMeasure P'
hY : HasLaw Y (gaussianReal 0 1) P'
hX : Var[X 0; P] ≠ 0
hindep : iIndepFun (β := fun (x : ℕ) ↦ ℝ) X P
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) P P
mX0 : AEMeasurable (X 0) P
intX0 : Integrable (X 0) P
n : ℕ
ω : Ω
⊢ (√((↑n : ℝ) * Var[X 0; P]))⁻¹ * (∑ k ∈ Finset.range n, X k ω - HMul.hMul (α := ℝ) (↑n : ℝ) (∫ (x : Ω), X 0 x ∂P)) =
    (√(↑n : ℝ))⁻¹ * ∑ k ∈ Finset.range n, (X k ω - ∫ (x : Ω), X 0 x ∂P) / √Var[X 0; P]
have rw : (√((↑n : ℝ) * Var[X 0; P]))⁻¹ * (∑ k ∈ Finset.range n, X k ω - HMul.hMul (α := ℝ) (↑n : ℝ) (∫ (x : Ω), X 0 x ∂P)) =
  (√(↑n : ℝ))⁻¹ *
    (HSub.hSub (α := ℝ) (∑ x ∈ Finset.range n, X x ω) (∑ x ∈ Finset.range n, ∫ (x : Ω), X 0 x ∂P) / √Var[X 0; P])
Tactic: rw [← Finset.sum_div, Finset.sum_sub_distrib]
-- Lean 4 proof step from Mathlib.Probability.CentralLimitTheorem (hypothesis)
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
P : Measure Ω
P' : Measure Ω'
X : ℕ → Ω → ℝ
Y : Ω' → ℝ
inst : IsProbabilityMeasure P
inst_1 : IsProbabilityMeasure P'
hY : HasLaw Y (gaussianReal 0 1) P'
hX : Var[X 0; P] ≠ 0
hindep : iIndepFun (β := fun (x : ℕ) ↦ ℝ) X P
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) P P
mX0 : AEMeasurable (X 0) P
intX0 : Integrable (X 0) P
⊢ TendstoInDistribution (Ω := fun (n : ℕ) ↦ Ω) (m := fun (i : ℕ) ↦ mΩ) (mE := Real.measurableSpace)
    (fun (n : ℕ) (ω : Ω) ↦
      (√((↑n : ℝ) * Var[X 0; P]))⁻¹ * (∑ k ∈ Finset.range n, X k ω - HMul.hMul (α := ℝ) (↑n : ℝ) (∫ (x : Ω), X 0 x ∂P)))
    atTop Y (fun (x : ℕ) ↦ P) P'
have this : ∀ (n : ℕ) (ω : Ω),
  (√((↑n : ℝ) * Var[X 0; P]))⁻¹ * (∑ k ∈ Finset.range n, X k ω - HMul.hMul (α := ℝ) (↑n : ℝ) (∫ (x : Ω), X 0 x ∂P)) =
    (√(↑n : ℝ))⁻¹ * ∑ k ∈ Finset.range n, (X k ω - ∫ (x : Ω), X 0 x ∂P) / √Var[X 0; P]
Tactic: have this (n : ℕ) ω : (√(n * Var[X 0; P]))⁻¹ * (∑ k ∈ Finset.range n, X k ω - n * P[X 0]) =
      (√n)⁻¹ * ∑ k ∈ Finset.range n, (X k ω - P[X 0]) / √Var[X 0; P] := by
    rw [← Finset.sum_div, Finset.sum_sub_distrib]
    simp [field]
-- Lean 4 proof step from Mathlib.Probability.CentralLimitTheorem (goal)
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
P : Measure Ω
P' : Measure Ω'
X : ℕ → Ω → ℝ
Y : Ω' → ℝ
inst : IsProbabilityMeasure P
inst_1 : IsProbabilityMeasure P'
hY : HasLaw Y (gaussianReal 0 1) P'
hX : Var[X 0; P] ≠ 0
hindep : iIndepFun (β := fun (x : ℕ) ↦ ℝ) X P
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) P P
mX0 : AEMeasurable (X 0) P
intX0 : Integrable (X 0) P
this :
  ∀ (n : ℕ) (ω : Ω),
    (√((↑n : ℝ) * Var[X 0; P]))⁻¹ * (∑ k ∈ Finset.range n, X k ω - HMul.hMul (α := ℝ) (↑n : ℝ) (∫ (x : Ω), X 0 x ∂P)) =
      (√(↑n : ℝ))⁻¹ * ∑ k ∈ Finset.range n, (X k ω - ∫ (x : Ω), X 0 x ∂P) / √Var[X 0; P]
⊢ TendstoInDistribution (Ω := fun (n : ℕ) ↦ Ω) (m := fun (i : ℕ) ↦ mΩ) (mE := Real.measurableSpace)
    (fun (n : ℕ) (ω : Ω) ↦
      (√((↑n : ℝ) * Var[X 0; P]))⁻¹ * (∑ k ∈ Finset.range n, X k ω - HMul.hMul (α := ℝ) (↑n : ℝ) (∫ (x : Ω), X 0 x ∂P)))
    atTop Y (fun (x : ℕ) ↦ P) P'
have simp_rw : TendstoInDistribution (Ω := fun (n : ℕ) ↦ Ω) (m := fun (i : ℕ) ↦ mΩ) (mE := Real.measurableSpace)
  (fun (n : ℕ) (ω : Ω) ↦ (√(↑n : ℝ))⁻¹ * ∑ k ∈ Finset.range n, (X k ω - ∫ (x : Ω), X 0 x ∂P) / √Var[X 0; P]) atTop Y
  (fun (x : ℕ) ↦ P) P'
Tactic: simp_rw [this]
-- Lean 4 proof step from Mathlib.Probability.CentralLimitTheorem (goal)
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
P : Measure Ω
P' : Measure Ω'
X : ℕ → Ω → ℝ
Y : Ω' → ℝ
inst : IsProbabilityMeasure P
inst_1 : IsProbabilityMeasure P'
hY : HasLaw Y (gaussianReal 0 1) P'
hX : Var[X 0; P] ≠ 0
hindep : iIndepFun (β := fun (x : ℕ) ↦ ℝ) X P
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) P P
mX0 : AEMeasurable (X 0) P
intX0 : Integrable (X 0) P
this :
  ∀ (n : ℕ) (ω : Ω),
    (√((↑n : ℝ) * Var[X 0; P]))⁻¹ * (∑ k ∈ Finset.range n, X k ω - HMul.hMul (α := ℝ) (↑n : ℝ) (∫ (x : Ω), X 0 x ∂P)) =
      (√(↑n : ℝ))⁻¹ * ∑ k ∈ Finset.range n, (X k ω - ∫ (x : Ω), X 0 x ∂P) / √Var[X 0; P]
⊢ TendstoInDistribution (Ω := fun (n : ℕ) ↦ Ω) (m := fun (i : ℕ) ↦ mΩ) (mE := Real.measurableSpace)
    (fun (n : ℕ) (ω : Ω) ↦ (√(↑n : ℝ))⁻¹ * ∑ k ∈ Finset.range n, (X k ω - ∫ (x : Ω), X 0 x ∂P) / √Var[X 0; P]) atTop Y
    (fun (x : ℕ) ↦ P) P'
have convert_6 : Eq (α := ℝ) (∫ (x : Ω), (X 0 x - ∫ (x : Ω), X 0 x ∂P) / √Var[X 0; P] ∂P) 0
Tactic: convert! tendstoInDistribution_inv_sqrt_mul_sum hY ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.CentralLimitTheorem (goal)
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
P : Measure Ω
P' : Measure Ω'
X : ℕ → Ω → ℝ
Y : Ω' → ℝ
inst : IsProbabilityMeasure P
inst_1 : IsProbabilityMeasure P'
hY : HasLaw Y (gaussianReal 0 1) P'
hX : Var[X 0; P] ≠ 0
hindep : iIndepFun (β := fun (x : ℕ) ↦ ℝ) X P
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) P P
mX0 : AEMeasurable (X 0) P
intX0 : Integrable (X 0) P
this :
  ∀ (n : ℕ) (ω : Ω),
    (√((↑n : ℝ) * Var[X 0; P]))⁻¹ * (∑ k ∈ Finset.range n, X k ω - HMul.hMul (α := ℝ) (↑n : ℝ) (∫ (x : Ω), X 0 x ∂P)) =
      (√(↑n : ℝ))⁻¹ * ∑ k ∈ Finset.range n, (X k ω - ∫ (x : Ω), X 0 x ∂P) / √Var[X 0; P]
convert_6 : Eq (α := ℝ) (∫ (x : Ω), (X 0 x - ∫ (x : Ω), X 0 x ∂P) / √Var[X 0; P] ∂P) 0
⊢ TendstoInDistribution (Ω := fun (n : ℕ) ↦ Ω) (m := fun (i : ℕ) ↦ mΩ) (mE := Real.measurableSpace)
    (fun (n : ℕ) (ω : Ω) ↦ (√(↑n : ℝ))⁻¹ * ∑ k ∈ Finset.range n, (X k ω - ∫ (x : Ω), X 0 x ∂P) / √Var[X 0; P]) atTop Y
    (fun (x : ℕ) ↦ P) P'
have convert_7 : Eq (α := ℝ)
  (∫ (x : Ω), HPow.hPow (α := Ω → ℝ) (β := ℕ) (fun (ω : Ω) ↦ (X 0 ω - ∫ (x : Ω), X 0 x ∂P) / √Var[X 0; P]) 2 x ∂P) 1
Tactic: convert! tendstoInDistribution_inv_sqrt_mul_sum hY ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.CentralLimitTheorem (goal)
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
P : Measure Ω
P' : Measure Ω'
X : ℕ → Ω → ℝ
Y : Ω' → ℝ
inst : IsProbabilityMeasure P
inst_1 : IsProbabilityMeasure P'
hY : HasLaw Y (gaussianReal 0 1) P'
hX : Var[X 0; P] ≠ 0
hindep : iIndepFun (β := fun (x : ℕ) ↦ ℝ) X P
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) P P
mX0 : AEMeasurable (X 0) P
intX0 : Integrable (X 0) P
this :
  ∀ (n : ℕ) (ω : Ω),
    (√((↑n : ℝ) * Var[X 0; P]))⁻¹ * (∑ k ∈ Finset.range n, X k ω - HMul.hMul (α := ℝ) (↑n : ℝ) (∫ (x : Ω), X 0 x ∂P)) =
      (√(↑n : ℝ))⁻¹ * ∑ k ∈ Finset.range n, (X k ω - ∫ (x : Ω), X 0 x ∂P) / √Var[X 0; P]
convert_6 : Eq (α := ℝ) (∫ (x : Ω), (X 0 x - ∫ (x : Ω), X 0 x ∂P) / √Var[X 0; P] ∂P) 0
convert_7 :
  Eq (α := ℝ)
    (∫ (x : Ω), HPow.hPow (α := Ω → ℝ) (β := ℕ) (fun (ω : Ω) ↦ (X 0 ω - ∫ (x : Ω), X 0 x ∂P) / √Var[X 0; P]) 2 x ∂P) 1
⊢ TendstoInDistribution (Ω := fun (n : ℕ) ↦ Ω) (m := fun (i : ℕ) ↦ mΩ) (mE := Real.measurableSpace)
    (fun (n : ℕ) (ω : Ω) ↦ (√(↑n : ℝ))⁻¹ * ∑ k ∈ Finset.range n, (X k ω - ∫ (x : Ω), X 0 x ∂P) / √Var[X 0; P]) atTop Y
    (fun (x : ℕ) ↦ P) P'
have convert_8 : iIndepFun (β := fun (x : ℕ) ↦ ℝ) (fun (k : ℕ) (ω : Ω) ↦ (X k ω - ∫ (x : Ω), X 0 x ∂P) / √Var[X 0; P]) P
Tactic: convert! tendstoInDistribution_inv_sqrt_mul_sum hY ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.CentralLimitTheorem (goal)
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
P : Measure Ω
P' : Measure Ω'
X : ℕ → Ω → ℝ
Y : Ω' → ℝ
inst : IsProbabilityMeasure P
inst_1 : IsProbabilityMeasure P'
hY : HasLaw Y (gaussianReal 0 1) P'
hX : Var[X 0; P] ≠ 0
hindep : iIndepFun (β := fun (x : ℕ) ↦ ℝ) X P
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) P P
mX0 : AEMeasurable (X 0) P
intX0 : Integrable (X 0) P
this :
  ∀ (n : ℕ) (ω : Ω),
    (√((↑n : ℝ) * Var[X 0; P]))⁻¹ * (∑ k ∈ Finset.range n, X k ω - HMul.hMul (α := ℝ) (↑n : ℝ) (∫ (x : Ω), X 0 x ∂P)) =
      (√(↑n : ℝ))⁻¹ * ∑ k ∈ Finset.range n, (X k ω - ∫ (x : Ω), X 0 x ∂P) / √Var[X 0; P]
convert_6 : Eq (α := ℝ) (∫ (x : Ω), (X 0 x - ∫ (x : Ω), X 0 x ∂P) / √Var[X 0; P] ∂P) 0
convert_7 :
  Eq (α := ℝ)
    (∫ (x : Ω), HPow.hPow (α := Ω → ℝ) (β := ℕ) (fun (ω : Ω) ↦ (X 0 ω - ∫ (x : Ω), X 0 x ∂P) / √Var[X 0; P]) 2 x ∂P) 1
convert_8 : iIndepFun (β := fun (x : ℕ) ↦ ℝ) (fun (k : ℕ) (ω : Ω) ↦ (X k ω - ∫ (x : Ω), X 0 x ∂P) / √Var[X 0; P]) P
⊢ TendstoInDistribution (Ω := fun (n : ℕ) ↦ Ω) (m := fun (i : ℕ) ↦ mΩ) (mE := Real.measurableSpace)
    (fun (n : ℕ) (ω : Ω) ↦ (√(↑n : ℝ))⁻¹ * ∑ k ∈ Finset.range n, (X k ω - ∫ (x : Ω), X 0 x ∂P) / √Var[X 0; P]) atTop Y
    (fun (x : ℕ) ↦ P) P'
have convert_9 : ∀ (i : ℕ),
  IdentDistrib (γ := ℝ) (fun (ω : Ω) ↦ (X i ω - ∫ (x : Ω), X 0 x ∂P) / √Var[X 0; P])
    (fun (ω : Ω) ↦ (X 0 ω - ∫ (x : Ω), X 0 x ∂P) / √Var[X 0; P]) P P
Tactic: convert! tendstoInDistribution_inv_sqrt_mul_sum hY ?_ ?_ ?_ ?_