awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.CentralLimitTheorem
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)
h₁ : ∀ (x : ℕ), HPow.hPow (β := ℕ) t 2 * HDiv.hDiv (α := ℝ) 1 (↑x : ℝ) = HPow.hPow (β := ℕ) ((√(↑x : ℝ))⁻¹ * t) 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 : ℝ)

Tactic:
convert! this using 4 with n
-- Module: Mathlib.Probability.CentralLimitTheorem
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 : ℕ
h : -HPow.hPow (β := ℕ) t 2 / 2 / (↑n : ℝ) = -(HPow.hPow (β := ℕ) ((√(↑n : ℝ))⁻¹ * t) 2 / 2)
⊢ -HPow.hPow (β := ℕ) (↑t : ℂ) 2 / 2 / (↑n : ℂ) = -(HPow.hPow (β := ℕ) ((↑(√(↑n : ℝ))⁻¹ : ℂ) * (↑t : ℂ)) 2 / 2)

Tactic:
norm_cast
-- Module: Mathlib.Probability.CentralLimitTheorem
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)

Tactic:
simp [field]
-- Module: Mathlib.Probability.CentralLimitTheorem
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 : ℝ)‖
x : ℕ
⊢ HPow.hPow (β := ℕ) t 2 * HDiv.hDiv (α := ℝ) 1 (↑x : ℝ) = HPow.hPow (β := ℕ) ((√(↑x : ℝ))⁻¹ * t) 2

Tactic:
simp [field]
-- Module: Mathlib.Probability.CentralLimitTheorem
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 : ℝ
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
⊢ 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:
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]
-- Module: Mathlib.Probability.CentralLimitTheorem
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 : ℝ
rw : Tendsto (fun (n : ℕ) ↦ (√(↑n : ℝ))⁻¹ * t) atTop (𝓝 (0 * t))
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ (√(↑n : ℝ))⁻¹ * t) atTop (𝓝 0)

Tactic:
rw [← zero_mul t]

Premises used: MulZeroClass.zero_mul
-- Module: Mathlib.Probability.CentralLimitTheorem
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 * t))

Tactic:
.mul_const t (tendsto_inv_atTop_zero.comp <| Real.tendsto_sqrt_atTop.comp <|
      tendsto_natCast_atTop_atTop)

Premises used: tendsto_inv_atTop_zero, Filter.Tendsto.mul_const, tendsto_natCast_atTop_atTop, Real.tendsto_sqrt_atTop, Filter.Tendsto.comp
-- Module: Mathlib.Probability.CentralLimitTheorem
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 * t))

Tactic:
exact .mul_const t (tendsto_inv_atTop_zero.comp <| Real.tendsto_sqrt_atTop.comp <|
      tendsto_natCast_atTop_atTop)
-- Module: Mathlib.Probability.CentralLimitTheorem
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)

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)
-- Module: Mathlib.Probability.CentralLimitTheorem
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 (t : ℝ) ↦
        charFun (mE := Real.measurableSpace) (Measure.map X P) t - (1 - HPow.hPow (β := ℕ) (↑t : ℂ) 2 / 2)) ∘
      fun (n : ℕ) ↦ (√(↑n : ℝ))⁻¹ * t)
    ((fun (t : ℝ) ↦ HPow.hPow (β := ℕ) t 2) ∘ fun (n : ℕ) ↦ (√(↑n : ℝ))⁻¹ * t)

Tactic:
(taylor_charFun_two hX h0 h1).comp_tendsto this

Premises used: MeasureTheory.taylor_charFun_two, Asymptotics.IsLittleO.comp_tendsto
-- Module: Mathlib.Probability.CentralLimitTheorem
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)
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
⊢ 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:
convert! (taylor_charFun_two hX h0 h1).comp_tendsto this using 2

Premises used: MeasureTheory.taylor_charFun_two, Asymptotics.IsLittleO.comp_tendsto
-- Module: Mathlib.Probability.CentralLimitTheorem
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 : ℕ
h :
  1 + -(HPow.hPow (β := ℕ) ((↑√(↑x : ℝ) : ℂ)⁻¹ * (↑t : ℂ)) 2 / 2) =
    1 - HPow.hPow (β := ℕ) ((↑√(↑x : ℝ) : ℂ)⁻¹ * (↑t : ℂ)) 2 / 2
⊢ 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:
simp
-- Module: Mathlib.Probability.CentralLimitTheorem
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 : ℕ
⊢ 1 + -(HPow.hPow (β := ℕ) ((↑√(↑x : ℝ) : ℂ)⁻¹ * (↑t : ℂ)) 2 / 2) =
    1 - HPow.hPow (β := ℕ) ((↑√(↑x : ℝ) : ℂ)⁻¹ * (↑t : ℂ)) 2 / 2

Tactic:
ring
-- Module: Mathlib.Probability.CentralLimitTheorem
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') ⋯))

Tactic:
ProbabilityMeasure.tendsto_iff_tendsto_charFun.2 fun t ↦ ?_

Premises used: Iff.mpr, MeasureTheory.ProbabilityMeasure.tendsto_iff_tendsto_charFun
-- Module: Mathlib.Probability.CentralLimitTheorem
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
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) ⋯) :
            Measure ℝ)
          t)
      atTop
      (𝓝
        (charFun (↑(Subtype.mk (p := fun (μ : Measure ℝ) ↦ IsProbabilityMeasure μ) (Measure.map Y P') ⋯) : Measure ℝ)
          t))
⊢ 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') ⋯))

Tactic:
refine ProbabilityMeasure.tendsto_iff_tendsto_charFun.2 fun t ↦ ?_

Premises used: Iff.mpr, MeasureTheory.ProbabilityMeasure.tendsto_iff_tendsto_charFun
-- Module: Mathlib.Probability.CentralLimitTheorem
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 : ℝ
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) ⋯) :
          Measure ℝ)
        t)
    atTop
    (𝓝 (charFun (↑(Subtype.mk (p := fun (μ : Measure ℝ) ↦ IsProbabilityMeasure μ) (gaussianReal 0 1) ⋯) : Measure ℝ) 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))

Tactic:
rw! [hY.map_eq]

Premises used: ProbabilityTheory.HasLaw.map_eq
-- Module: Mathlib.Probability.CentralLimitTheorem
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 μ) (gaussianReal 0 1) ⋯) : Measure ℝ) t))

Tactic:
simpa [charFun_inv_sqrt_mul_sum hindep hident, charFun_gaussianReal, neg_div] using
      tendsto_charFun_inv_sqrt_mul_pow (hident 0).aemeasurable_fst h0 h1 t

Premises used: neg_div, ProbabilityTheory.IdentDistrib.aemeasurable_fst, ProbabilityTheory.charFun_inv_sqrt_mul_sum, ProbabilityTheory.tendsto_charFun_inv_sqrt_mul_pow, OfNat.ofNat, ProbabilityTheory.charFun_gaussianReal
-- Module: Mathlib.Probability.CentralLimitTheorem
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
⊢ AEMeasurable (X 0) P

Tactic:
have mX0 := (hident 0).aemeasurable_fst
-- Module: Mathlib.Probability.CentralLimitTheorem
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
⊢ LE.le (α := ENNReal) 1 2

Tactic:
simp
-- Module: Mathlib.Probability.CentralLimitTheorem
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
⊢ 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)
-- Module: Mathlib.Probability.CentralLimitTheorem
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 : ℕ
ω : Ω
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])
⊢ (√((↑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:
rw [← Finset.sum_div, Finset.sum_sub_distrib]

Premises used: Finset.sum_div, Finset.sum_sub_distrib
-- Module: Mathlib.Probability.CentralLimitTheorem
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 : ℝ))⁻¹ *
      (HSub.hSub (α := ℝ) (∑ x ∈ Finset.range n, X x ω) (∑ x ∈ Finset.range n, ∫ (x : Ω), X 0 x ∂P) / √Var[X 0; P])

Tactic:
simp [field]
-- Module: Mathlib.Probability.CentralLimitTheorem
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]

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]
-- Module: Mathlib.Probability.CentralLimitTheorem
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]
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'
⊢ 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'

Tactic:
simp_rw [this]
-- Module: Mathlib.Probability.CentralLimitTheorem
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'

Tactic:
tendstoInDistribution_inv_sqrt_mul_sum hY ?_ ?_ ?_ ?_

Premises used: ProbabilityTheory.tendstoInDistribution_inv_sqrt_mul_sum
-- Module: Mathlib.Probability.CentralLimitTheorem
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
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
⊢ 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:
convert! tendstoInDistribution_inv_sqrt_mul_sum hY ?_ ?_ ?_ ?_

Premises used: ProbabilityTheory.tendstoInDistribution_inv_sqrt_mul_sum
-- Module: Mathlib.Probability.CentralLimitTheorem
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]
⊢ Integrable (ε := ℝ) (fun (a : Ω) ↦ ∫ (x : Ω), X 0 x ∂P) P

Tactic:
simp