awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : HSub.hSub (α := ℝ) (∫ (a : Ω), X 0 a ∂P) (∫ (a : Ω), ∫ (x : Ω), X 0 x ∂P ∂P) / √Var[X 0; P] = 0
⊢ Eq (α := ℝ) (∫ (x : Ω), (X 0 x - ∫ (x : Ω), X 0 x ∂P) / √Var[X 0; P] ∂P) 0

Tactic:
rw [integral_div, integral_sub intX0 (by simp)]

Premises used: MeasureTheory.integral_div, MeasureTheory.integral_sub
-- 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]
⊢ HSub.hSub (α := ℝ) (∫ (a : Ω), X 0 a ∂P) (∫ (a : Ω), ∫ (x : Ω), X 0 x ∂P ∂P) / √Var[X 0; P] = 0

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
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_7 :
  Eq (α := ℝ) (∫ (x : Ω), HPow.hPow (β := ℕ) (X 0 x - ∫ (x : Ω), X 0 x ∂P) 2 / HPow.hPow (β := ℕ) (√Var[X 0; P]) 2 ∂P) 1
⊢ Eq (α := ℝ)
    (∫ (x : Ω), HPow.hPow (α := Ω → ℝ) (β := ℕ) (fun (ω : Ω) ↦ (X 0 ω - ∫ (x : Ω), X 0 x ∂P) / √Var[X 0; P]) 2 x ∂P) 1

Tactic:
simp only [Pi.pow_apply, div_pow]

Premises used: Pi.pow_apply, div_pow
-- 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_7 : (∫ (a : Ω), HPow.hPow (β := ℕ) (X 0 a - ∫ (x : Ω), X 0 x ∂P) 2 ∂P) / HPow.hPow (β := ℕ) (√Var[X 0; P]) 2 = 1
convert_7₁ : Var[X 0; P] / HPow.hPow (β := ℕ) (√Var[X 0; P]) 2 = 1
convert_7₂ : Var[X 0; P] / Var[X 0; P] = 1
convert_7₃ convert_7₄ : Eq (α := ℝ) 1 1
⊢ Eq (α := ℝ) (∫ (x : Ω), HPow.hPow (β := ℕ) (X 0 x - ∫ (x : Ω), X 0 x ∂P) 2 / HPow.hPow (β := ℕ) (√Var[X 0; P]) 2 ∂P) 1

Tactic:
rw [integral_div, ← variance_eq_integral mX0, Real.sq_sqrt (variance_nonneg _ _), div_self hX]

Premises used: ProbabilityTheory.variance_eq_integral, MeasureTheory.integral_div, Real.sq_sqrt, ProbabilityTheory.variance_nonneg, div_self
-- 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]
⊢ ∀ (i : ℕ), Measurable (α := ℝ) (β := ℝ) ((fun (x : ℕ) (x_1 : ℝ) ↦ (x_1 - ∫ (x : Ω), X 0 x ∂P) / √Var[X 0; P]) i)

Tactic:
fun_prop
-- 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]
⊢ iIndepFun (β := fun (x : ℕ) ↦ ℝ) (fun (k : ℕ) (ω : Ω) ↦ (X k ω - ∫ (x : Ω), X 0 x ∂P) / √Var[X 0; P]) P

Tactic:
exact hindep.comp (fun _ x ↦ (x - P[X 0]) / √Var[X 0; P]) (by fun_prop)

Premises used: HSub.hSub, HDiv.hDiv, ProbabilityTheory.variance, MeasureTheory.integral, Real.sqrt, ProbabilityTheory.iIndepFun.comp, OfNat.ofNat
-- 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]
n : ℕ
⊢ Measurable (β := ℝ) fun (x : ℝ) ↦ (x - ∫ (x : Ω), X 0 x ∂P) / √Var[X 0; P]

Tactic:
fun_prop
-- 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]
⊢ ∀ (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! fun n ↦ (hident n).comp (u := fun x ↦ (x - P[X 0]) / √Var[X 0; P]) (by fun_prop)

Premises used: ProbabilityTheory.IdentDistrib.comp
-- 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 Var[X 0; P].toNNReal) P'
hX : MemLp (X 0) 2 P
hindep : iIndepFun (β := fun (x : ℕ) ↦ ℝ) X P
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) P P
inl :
  ∀ (h : Var[X 0; P] = 0),
    TendstoInDistribution (Ω := fun (n : ℕ) ↦ Ω) (m := fun (i : ℕ) ↦ mΩ) (mE := Real.measurableSpace)
      (fun (n : ℕ) (ω : Ω) ↦
        (√(↑n : ℝ))⁻¹ * (∑ k ∈ Finset.range n, X k ω - HMul.hMul (α := ℝ) (↑n : ℝ) (∫ (x : Ω), X 0 x ∂P)))
      atTop Y (fun (x : ℕ) ↦ P) P'
inr :
  ∀ (h : Var[X 0; P] ≠ 0),
    TendstoInDistribution (Ω := fun (n : ℕ) ↦ Ω) (m := fun (i : ℕ) ↦ mΩ) (mE := Real.measurableSpace)
      (fun (n : ℕ) (ω : Ω) ↦
        (√(↑n : ℝ))⁻¹ * (∑ k ∈ Finset.range n, X k ω - HMul.hMul (α := ℝ) (↑n : ℝ) (∫ (x : Ω), X 0 x ∂P)))
      atTop Y (fun (x : ℕ) ↦ P) P'
⊢ TendstoInDistribution (Ω := fun (n : ℕ) ↦ Ω) (m := fun (i : ℕ) ↦ mΩ) (mE := Real.measurableSpace)
    (fun (n : ℕ) (ω : Ω) ↦
      (√(↑n : ℝ))⁻¹ * (∑ k ∈ Finset.range n, X k ω - HMul.hMul (α := ℝ) (↑n : ℝ) (∫ (x : Ω), X 0 x ∂P)))
    atTop Y (fun (x : ℕ) ↦ P) P'

Tactic:
obtain h | h := eq_or_ne Var[X 0; P] 0

Premises used: ProbabilityTheory.variance, eq_or_ne, OfNat.ofNat
-- 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 Var[X 0; P].toNNReal) P'
hX : MemLp (X 0) 2 P
hindep : iIndepFun (β := fun (x : ℕ) ↦ ℝ) X P
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) P P
h : Var[X 0; P] = 0
⊢ ∀ᵐ (ω : Ω) ∂P, ∀ (n : ℕ), X n ω = ∫ (x : Ω), X 0 x ∂P

Tactic:
ae_all_iff.2 fun n ↦ ?_

Premises used: Iff.mpr, MeasureTheory.ae_all_iff
-- 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 Var[X 0; P].toNNReal) P'
hX : MemLp (X 0) 2 P
hindep : iIndepFun (β := fun (x : ℕ) ↦ ℝ) X P
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) P P
h : Var[X 0; P] = 0
refine : ∀ (n : ℕ), ∀ᵐ (a : Ω) ∂P, X n a = ∫ (x : Ω), X 0 x ∂P
⊢ ∀ᵐ (ω : Ω) ∂P, ∀ (n : ℕ), X n ω = ∫ (x : Ω), X 0 x ∂P

Tactic:
refine ae_all_iff.2 fun n ↦ ?_

Premises used: Iff.mpr, MeasureTheory.ae_all_iff
-- 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 Var[X 0; P].toNNReal) P'
hX : MemLp (X 0) 2 P
hindep : iIndepFun (β := fun (x : ℕ) ↦ ℝ) X P
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) P P
h : Var[X 0; P] = 0
n : ℕ
⊢ ∀ᵐ (ω : Ω) ∂P, X n ω = ∫ (x : Ω), X n x ∂P

Tactic:
(ae_eq_integral_of_variance_eq_zero ((hident n).memLp_iff.2 hX)) ?_

Premises used: Iff.mpr, ProbabilityTheory.IdentDistrib.memLp_iff, ProbabilityTheory.ae_eq_integral_of_variance_eq_zero
-- 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 Var[X 0; P].toNNReal) P'
hX : MemLp (X 0) 2 P
hindep : iIndepFun (β := fun (x : ℕ) ↦ ℝ) X P
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) P P
h : Var[X 0; P] = 0
n : ℕ
h₁ : ∀ (x : Ω), Eq (α := ℝ) (∫ (x : Ω), X 0 x ∂P) (∫ (x : Ω), X n x ∂P)
convert! : Var[X n; P] = 0
⊢ ∀ᵐ (a : Ω) ∂P, X n a = ∫ (x : Ω), X 0 x ∂P

Tactic:
convert! (ae_eq_integral_of_variance_eq_zero ((hident n).memLp_iff.2 hX)) ?_ using 3

Premises used: Iff.mpr, ProbabilityTheory.IdentDistrib.memLp_iff, ProbabilityTheory.ae_eq_integral_of_variance_eq_zero
-- 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 Var[X 0; P].toNNReal) P'
hX : MemLp (X 0) 2 P
hindep : iIndepFun (β := fun (x : ℕ) ↦ ℝ) X P
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) P P
h : Var[X 0; P] = 0
n : ℕ
x : Ω
h₁ h₂ : Eq (α := ℝ) (∫ (x : Ω), X 0 x ∂P) (∫ (x : Ω), X 0 x ∂P)
⊢ Eq (α := ℝ) (∫ (x : Ω), X 0 x ∂P) (∫ (x : Ω), X n x ∂P)

Tactic:
rw [(hident n).integral_eq]

Premises used: ProbabilityTheory.IdentDistrib.integral_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 Var[X 0; P].toNNReal) P'
hX : MemLp (X 0) 2 P
hindep : iIndepFun (β := fun (x : ℕ) ↦ ℝ) X P
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) P P
h : Var[X 0; P] = 0
n : ℕ
rwa rwa₁ rwa₂ rwa₃ : Var[X 0; P] = 0
⊢ Var[X n; P] = 0

Tactic:
rwa [(hident n).variance_eq]

Premises used: ProbabilityTheory.IdentDistrib.variance_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 Var[X 0; P].toNNReal) P'
hX : MemLp (X 0) 2 P
hindep : iIndepFun (β := fun (x : ℕ) ↦ ℝ) X P
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) P P
h : Var[X 0; P] = 0
⊢ ∀ᵐ (ω : Ω) ∂P, ∀ (n : ℕ), X n ω = ∫ (x : Ω), X 0 x ∂P

Tactic:
have : ∀ᵐ ω ∂P, ∀ n, X n ω = P[X 0] := by
      refine ae_all_iff.2 fun n ↦ ?_
      convert! (ae_eq_integral_of_variance_eq_zero ((hident n).memLp_iff.2 hX)) ?_ using 3
      · rw [(hident n).integral_eq]
      · rwa [(hident n).variance_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 Var[X 0; P].toNNReal) P'
hX : MemLp (X 0) 2 P
hindep : iIndepFun (β := fun (x : ℕ) ↦ ℝ) X P
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) P P
h : Var[X 0; P] = 0
this : ∀ᵐ (ω : Ω) ∂P, ∀ (n : ℕ), X n ω = ∫ (x : Ω), X 0 x ∂P
⊢ ∀ (n : ℕ), AEMeasurable (X n) P

Tactic:
have mX (n : ℕ) := (hident n).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 Var[X 0; P].toNNReal) P'
hX : MemLp (X 0) 2 P
hindep : iIndepFun (β := fun (x : ℕ) ↦ ℝ) X P
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) P P
h : Var[X 0; P] = 0
this : ∀ᵐ (ω : Ω) ∂P, ∀ (n : ℕ), X n ω = ∫ (x : Ω), X 0 x ∂P
mX : ∀ (n : ℕ), AEMeasurable (X n) P
⊢ TendstoInDistribution (Ω := fun (n : ℕ) ↦ Ω) (m := fun (i : ℕ) ↦ mΩ) (mE := Real.measurableSpace)
    (fun (n : ℕ) (ω : Ω) ↦
      (√(↑n : ℝ))⁻¹ * (∑ k ∈ Finset.range n, X k ω - HMul.hMul (α := ℝ) (↑n : ℝ) (∫ (x : Ω), X 0 x ∂P)))
    atTop Y (fun (x : ℕ) ↦ P) P'

Tactic:
tendstoInDistribution_of_identDistrib 0 (fun n ↦ ?_) ?_

Premises used: OfNat.ofNat, MeasureTheory.tendstoInDistribution_of_identDistrib
-- 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 Var[X 0; P].toNNReal) P'
hX : MemLp (X 0) 2 P
hindep : iIndepFun (β := fun (x : ℕ) ↦ ℝ) X P
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) P P
h : Var[X 0; P] = 0
this : ∀ᵐ (ω : Ω) ∂P, ∀ (n : ℕ), X n ω = ∫ (x : Ω), X 0 x ∂P
mX : ∀ (n : ℕ), AEMeasurable (X n) P
inl :
  ∀ (n : ℕ),
    IdentDistrib (γ := ℝ)
      (fun (ω : Ω) ↦ (√(↑0 : ℝ))⁻¹ * (∑ k ∈ Finset.range 0, X k ω - HMul.hMul (α := ℝ) (↑0 : ℝ) (∫ (x : Ω), X 0 x ∂P)))
      (fun (ω : Ω) ↦ (√(↑n : ℝ))⁻¹ * (∑ k ∈ Finset.range n, X k ω - HMul.hMul (α := ℝ) (↑n : ℝ) (∫ (x : Ω), X 0 x ∂P)))
      P P
inl₁ :
  IdentDistrib
    (fun (ω : Ω) ↦ (√(↑0 : ℝ))⁻¹ * (∑ k ∈ Finset.range 0, X k ω - HMul.hMul (α := ℝ) (↑0 : ℝ) (∫ (x : Ω), X 0 x ∂P))) Y
    P P'
⊢ TendstoInDistribution (Ω := fun (n : ℕ) ↦ Ω) (m := fun (i : ℕ) ↦ mΩ) (mE := Real.measurableSpace)
    (fun (n : ℕ) (ω : Ω) ↦
      (√(↑n : ℝ))⁻¹ * (∑ k ∈ Finset.range n, X k ω - HMul.hMul (α := ℝ) (↑n : ℝ) (∫ (x : Ω), X 0 x ∂P)))
    atTop Y (fun (x : ℕ) ↦ P) P'

Tactic:
refine tendstoInDistribution_of_identDistrib 0 (fun n ↦ ?_) ?_

Premises used: OfNat.ofNat, MeasureTheory.tendstoInDistribution_of_identDistrib
-- 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 Var[X 0; P].toNNReal) P'
hX : MemLp (X 0) 2 P
hindep : iIndepFun (β := fun (x : ℕ) ↦ ℝ) X P
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) P P
h : Var[X 0; P] = 0
this : ∀ᵐ (ω : Ω) ∂P, ∀ (n : ℕ), X n ω = ∫ (x : Ω), X 0 x ∂P
mX : ∀ (n : ℕ), AEMeasurable (X n) P
n : ℕ
⊢ AEMeasurable (β := ℝ)
    (fun (ω : Ω) ↦ (√(↑0 : ℝ))⁻¹ * (∑ k ∈ Finset.range 0, X k ω - HMul.hMul (α := ℝ) (↑0 : ℝ) (∫ (x : Ω), X 0 x ∂P))) P

Tactic:
fun_prop
-- 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 Var[X 0; P].toNNReal) P'
hX : MemLp (X 0) 2 P
hindep : iIndepFun (β := fun (x : ℕ) ↦ ℝ) X P
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) P P
h : Var[X 0; P] = 0
this : ∀ᵐ (ω : Ω) ∂P, ∀ (n : ℕ), X n ω = ∫ (x : Ω), X 0 x ∂P
mX : ∀ (n : ℕ), AEMeasurable (X n) P
n : ℕ
⊢ AEMeasurable (β := ℝ)
    (fun (ω : Ω) ↦ (√(↑n : ℝ))⁻¹ * (∑ k ∈ Finset.range n, X k ω - HMul.hMul (α := ℝ) (↑n : ℝ) (∫ (x : Ω), X 0 x ∂P))) P

Tactic:
fun_prop
-- 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 Var[X 0; P].toNNReal) P'
hX : MemLp (X 0) 2 P
hindep : iIndepFun (β := fun (x : ℕ) ↦ ℝ) X P
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) P P
h : Var[X 0; P] = 0
this : ∀ᵐ (ω : Ω) ∂P, ∀ (n : ℕ), X n ω = ∫ (x : Ω), X 0 x ∂P
mX : ∀ (n : ℕ), AEMeasurable (X n) P
n : ℕ
inl :
  (ae P).EventuallyEq (β := ℝ)
    (fun (ω : Ω) ↦ (√(↑0 : ℝ))⁻¹ * (∑ k ∈ Finset.range 0, X k ω - HMul.hMul (α := ℝ) (↑0 : ℝ) (∫ (x : Ω), X 0 x ∂P)))
    fun (ω : Ω) ↦ (√(↑n : ℝ))⁻¹ * (∑ k ∈ Finset.range n, X k ω - HMul.hMul (α := ℝ) (↑n : ℝ) (∫ (x : Ω), X 0 x ∂P))
⊢ IdentDistrib (γ := ℝ)
    (fun (ω : Ω) ↦ (√(↑0 : ℝ))⁻¹ * (∑ k ∈ Finset.range 0, X k ω - HMul.hMul (α := ℝ) (↑0 : ℝ) (∫ (x : Ω), X 0 x ∂P)))
    (fun (ω : Ω) ↦ (√(↑n : ℝ))⁻¹ * (∑ k ∈ Finset.range n, X k ω - HMul.hMul (α := ℝ) (↑n : ℝ) (∫ (x : Ω), X 0 x ∂P))) P
    P

Tactic:
refine ⟨by fun_prop, by fun_prop, Measure.map_congr ?_⟩
-- 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 Var[X 0; P].toNNReal) P'
hX : MemLp (X 0) 2 P
hindep : iIndepFun (β := fun (x : ℕ) ↦ ℝ) X P
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) P P
h : Var[X 0; P] = 0
this : ∀ᵐ (ω : Ω) ∂P, ∀ (n : ℕ), X n ω = ∫ (x : Ω), X 0 x ∂P
mX : ∀ (n : ℕ), AEMeasurable (X n) P
n : ℕ
h₁ :
  ∀ (ω : Ω) (hω : ∀ (n : ℕ), X n ω = ∫ (x : Ω), X 0 x ∂P),
    (√(↑0 : ℝ))⁻¹ * (∑ k ∈ Finset.range 0, X k ω - HMul.hMul (α := ℝ) (↑0 : ℝ) (∫ (x : Ω), X 0 x ∂P)) =
      (√(↑n : ℝ))⁻¹ * (∑ k ∈ Finset.range n, X k ω - HMul.hMul (α := ℝ) (↑n : ℝ) (∫ (x : Ω), X 0 x ∂P))
⊢ (ae P).EventuallyEq (β := ℝ)
    (fun (ω : Ω) ↦ (√(↑0 : ℝ))⁻¹ * (∑ k ∈ Finset.range 0, X k ω - HMul.hMul (α := ℝ) (↑0 : ℝ) (∫ (x : Ω), X 0 x ∂P)))
    fun (ω : Ω) ↦ (√(↑n : ℝ))⁻¹ * (∑ k ∈ Finset.range n, X k ω - HMul.hMul (α := ℝ) (↑n : ℝ) (∫ (x : Ω), X 0 x ∂P))

Tactic:
filter_upwards [this] with ω hω
-- 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 Var[X 0; P].toNNReal) P'
hX : MemLp (X 0) 2 P
hindep : iIndepFun (β := fun (x : ℕ) ↦ ℝ) X P
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) P P
h : Var[X 0; P] = 0
this : ∀ᵐ (ω : Ω) ∂P, ∀ (n : ℕ), X n ω = ∫ (x : Ω), X 0 x ∂P
mX : ∀ (n : ℕ), AEMeasurable (X n) P
n : ℕ
ω : Ω
hω : ∀ (n : ℕ), X n ω = ∫ (x : Ω), X 0 x ∂P
⊢ (√(↑0 : ℝ))⁻¹ * (∑ k ∈ Finset.range 0, X k ω - HMul.hMul (α := ℝ) (↑0 : ℝ) (∫ (x : Ω), X 0 x ∂P)) =
    (√(↑n : ℝ))⁻¹ * (∑ k ∈ Finset.range n, X k ω - HMul.hMul (α := ℝ) (↑n : ℝ) (∫ (x : Ω), X 0 x ∂P))

Tactic:
simp [hω]
-- 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 Var[X 0; P].toNNReal) P'
hX : MemLp (X 0) 2 P
hindep : iIndepFun (β := fun (x : ℕ) ↦ ℝ) X P
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) P P
h : Var[X 0; P] = 0
this : ∀ᵐ (ω : Ω) ∂P, ∀ (n : ℕ), X n ω = ∫ (x : Ω), X 0 x ∂P
mX : ∀ (n : ℕ), AEMeasurable (X n) P
⊢ AEMeasurable (β := ℝ)
    (fun (ω : Ω) ↦ (√(↑0 : ℝ))⁻¹ * (∑ k ∈ Finset.range 0, X k ω - HMul.hMul (α := ℝ) (↑0 : ℝ) (∫ (x : Ω), X 0 x ∂P))) P

Tactic:
fun_prop
-- 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 Var[X 0; P].toNNReal) P'
hX : MemLp (X 0) 2 P
hindep : iIndepFun (β := fun (x : ℕ) ↦ ℝ) X P
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) P P
h : Var[X 0; P] = 0
this : ∀ᵐ (ω : Ω) ∂P, ∀ (n : ℕ), X n ω = ∫ (x : Ω), X 0 x ∂P
mX : ∀ (n : ℕ), AEMeasurable (X n) P
funProp : AEFinStronglyMeasurable (β := ℝ) (fun (a : Ω') ↦ Y a) P'
⊢ AEMeasurable Y P'

Tactic:
fun_prop
-- 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 Var[X 0; P].toNNReal) P'
hX : MemLp (X 0) 2 P
hindep : iIndepFun (β := fun (x : ℕ) ↦ ℝ) X P
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) P P
h : Var[X 0; P] = 0
this : ∀ᵐ (ω : Ω) ∂P, ∀ (n : ℕ), X n ω = ∫ (x : Ω), X 0 x ∂P
mX : ∀ (n : ℕ), AEMeasurable (X n) P
⊢ Eq (α := Measure ℝ)
    (Measure.map
      (fun (ω : Ω) ↦ (√(↑0 : ℝ))⁻¹ * (∑ k ∈ Finset.range 0, X k ω - HMul.hMul (α := ℝ) (↑0 : ℝ) (∫ (x : Ω), X 0 x ∂P)))
      P)
    (Measure.map Y P')

Tactic:
simp [hY.map_eq, h]

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 Var[X 0; P].toNNReal) P'
hX : MemLp (X 0) 2 P
hindep : iIndepFun (β := fun (x : ℕ) ↦ ℝ) X P
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) P P
h : Var[X 0; P] = 0
this : ∀ᵐ (ω : Ω) ∂P, ∀ (n : ℕ), X n ω = ∫ (x : Ω), X 0 x ∂P
mX : ∀ (n : ℕ), AEMeasurable (X n) P
⊢ IdentDistrib
    (fun (ω : Ω) ↦ (√(↑0 : ℝ))⁻¹ * (∑ k ∈ Finset.range 0, X k ω - HMul.hMul (α := ℝ) (↑0 : ℝ) (∫ (x : Ω), X 0 x ∂P))) Y
    P P'

Tactic:
exact ⟨by fun_prop, by fun_prop, by simp [hY.map_eq, h]⟩