awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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]
⊢ Eq (α := ℝ) (∫ (x : Ω), (X 0 x - ∫ (x : Ω), X 0 x ∂P) / √Var[X 0; P] ∂P) 0
have convert_6 : HSub.hSub (α := ℝ) (∫ (a : Ω), X 0 a ∂P) (∫ (a : Ω), ∫ (x : Ω), X 0 x ∂P ∂P) / √Var[X 0; P] = 0
Tactic: rw [integral_div, integral_sub intX0 (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
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]
⊢ Eq (α := ℝ)
    (∫ (x : Ω), HPow.hPow (α := Ω → ℝ) (β := ℕ) (fun (ω : Ω) ↦ (X 0 ω - ∫ (x : Ω), X 0 x ∂P) / √Var[X 0; P]) 2 x ∂P) 1
have convert_7 : Eq (α := ℝ) (∫ (x : Ω), HPow.hPow (β := ℕ) (X 0 x - ∫ (x : Ω), X 0 x ∂P) 2 / HPow.hPow (β := ℕ) (√Var[X 0; P]) 2 ∂P) 1
Tactic: simp only [Pi.pow_apply, div_pow]
-- 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]
⊢ Eq (α := ℝ) (∫ (x : Ω), HPow.hPow (β := ℕ) (X 0 x - ∫ (x : Ω), X 0 x ∂P) 2 / HPow.hPow (β := ℕ) (√Var[X 0; P]) 2 ∂P) 1
have convert_7 : (∫ (a : Ω), HPow.hPow (β := ℕ) (X 0 a - ∫ (x : Ω), X 0 x ∂P) 2 ∂P) / HPow.hPow (β := ℕ) (√Var[X 0; P]) 2 = 1
Tactic: rw [integral_div, ← variance_eq_integral mX0, Real.sq_sqrt (variance_nonneg _ _), div_self hX]
-- 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_7 : (∫ (a : Ω), HPow.hPow (β := ℕ) (X 0 a - ∫ (x : Ω), X 0 x ∂P) 2 ∂P) / HPow.hPow (β := ℕ) (√Var[X 0; P]) 2 = 1
⊢ Eq (α := ℝ) (∫ (x : Ω), HPow.hPow (β := ℕ) (X 0 x - ∫ (x : Ω), X 0 x ∂P) 2 / HPow.hPow (β := ℕ) (√Var[X 0; P]) 2 ∂P) 1
have convert_7₁ : Var[X 0; P] / HPow.hPow (β := ℕ) (√Var[X 0; P]) 2 = 1
Tactic: rw [integral_div, ← variance_eq_integral mX0, Real.sq_sqrt (variance_nonneg _ _), div_self hX]
-- 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_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
⊢ Eq (α := ℝ) (∫ (x : Ω), HPow.hPow (β := ℕ) (X 0 x - ∫ (x : Ω), X 0 x ∂P) 2 / HPow.hPow (β := ℕ) (√Var[X 0; P]) 2 ∂P) 1
have convert_7₂ : Var[X 0; P] / Var[X 0; P] = 1
Tactic: rw [integral_div, ← variance_eq_integral mX0, Real.sq_sqrt (variance_nonneg _ _), div_self hX]
-- 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_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
⊢ Eq (α := ℝ) (∫ (x : Ω), HPow.hPow (β := ℕ) (X 0 x - ∫ (x : Ω), X 0 x ∂P) 2 / HPow.hPow (β := ℕ) (√Var[X 0; P]) 2 ∂P) 1
have convert_7₃ : Eq (α := ℝ) 1 1
Tactic: rw [integral_div, ← variance_eq_integral mX0, Real.sq_sqrt (variance_nonneg _ _), div_self hX]
-- 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 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
⊢ 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'
have 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'
Tactic: obtain h | h := eq_or_ne Var[X 0; P] 0
-- 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 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'
⊢ 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'
have 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'
Tactic: obtain h | h := eq_or_ne Var[X 0; P] 0
-- 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 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
have refine : ∀ (n : ℕ), ∀ᵐ (a : Ω) ∂P, X n a = ∫ (x : Ω), X 0 x ∂P
Tactic: refine ae_all_iff.2 fun n ↦ ?_
-- 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 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 : ℕ
⊢ ∀ᵐ (a : Ω) ∂P, X n a = ∫ (x : Ω), X 0 x ∂P
have h₁ : ∀ (x : Ω), Eq (α := ℝ) (∫ (x : Ω), X 0 x ∂P) (∫ (x : Ω), X n x ∂P)
Tactic: convert! (ae_eq_integral_of_variance_eq_zero ((hident n).memLp_iff.2 hX)) ?_ using 3
-- 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 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)
⊢ ∀ᵐ (a : Ω) ∂P, X n a = ∫ (x : Ω), X 0 x ∂P
have convert! : Var[X n; P] = 0
Tactic: convert! (ae_eq_integral_of_variance_eq_zero ((hident n).memLp_iff.2 hX)) ?_ using 3
-- 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 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 : Ω
⊢ Eq (α := ℝ) (∫ (x : Ω), X 0 x ∂P) (∫ (x : Ω), X n x ∂P)
have h₁ : Eq (α := ℝ) (∫ (x : Ω), X 0 x ∂P) (∫ (x : Ω), X 0 x ∂P)
Tactic: rw [(hident n).integral_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 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
⊢ 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'
have this : ∀ᵐ (ω : Ω) ∂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]
-- 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 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
⊢ 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'
have mX : ∀ (n : ℕ), AEMeasurable (X n) P
Tactic: have mX (n : ℕ) := (hident n).aemeasurable_fst
-- 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 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'
have 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
Tactic: refine tendstoInDistribution_of_identDistrib 0 (fun n ↦ ?_) ?_
-- 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 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
⊢ 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'
have inl₁ : IdentDistrib
  (fun (ω : Ω) ↦ (√(↑0 : ℝ))⁻¹ * (∑ k ∈ Finset.range 0, X k ω - HMul.hMul (α := ℝ) (↑0 : ℝ) (∫ (x : Ω), X 0 x ∂P))) Y P
  P'
Tactic: refine tendstoInDistribution_of_identDistrib 0 (fun n ↦ ?_) ?_
-- 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 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 : ℕ
⊢ 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
have 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))
Tactic: refine ⟨by fun_prop, by fun_prop, Measure.map_congr ?_⟩
-- 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 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 : ℕ
⊢ (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))
have 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))
Tactic: filter_upwards [this] with ω hω
-- 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 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 Y P'
have funProp : AEFinStronglyMeasurable (β := ℝ) (fun (a : Ω') ↦ Y a) P'
Tactic: fun_prop
-- 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 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
⊢ HasLaw (fun (ω : Ω') ↦ Y ω / √Var[X 0; P]) (gaussianReal 0 1) P'
have h₁ : 0 = 0 / √Var[X 0; P]
Tactic: convert! gaussianReal_div_const 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 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
h₁ : 0 = 0 / √Var[X 0; P]
⊢ HasLaw (fun (ω : Ω') ↦ Y ω / √Var[X 0; P]) (gaussianReal 0 1) P'
have h₂ : 1 = Var[X 0; P].toNNReal / NNReal.mk (HPow.hPow (β := ℕ) (√Var[X 0; P]) 2) sorry
Tactic: convert! gaussianReal_div_const 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 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
⊢ 1 = Var[X 0; P].toNNReal / NNReal.mk (HPow.hPow (β := ℕ) (√Var[X 0; P]) 2) ⋯
have h₁ : (↑1 : ℝ) = (↑(Var[X 0; P].toNNReal / NNReal.mk (HPow.hPow (β := ℕ) (√Var[X 0; P]) 2) sorry) : ℝ)
Tactic: ext
-- 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 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
⊢ 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'
have this : HasLaw (fun (ω : Ω') ↦ Y ω / √Var[X 0; P]) (gaussianReal 0 1) P'
Tactic: have : HasLaw (fun ω ↦ Y ω / √Var[X 0; P]) (gaussianReal 0 1) P' := by
    convert! gaussianReal_div_const hY _
    · simp
    · ext; simp [h]
-- 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 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 : HasLaw (fun (ω : Ω') ↦ Y ω / √Var[X 0; P]) (gaussianReal 0 1) 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'
have h₁ : ∀ (x : ℕ) (x_1 : Ω),
  (√(↑x : ℝ))⁻¹ * (∑ k ∈ Finset.range x, X k x_1 - HMul.hMul (α := ℝ) (↑x : ℝ) (∫ (x : Ω), X 0 x ∂P)) =
    ((fun (x : ℝ) ↦ √Var[X 0; P] * x) ∘ fun (ω : Ω) ↦
        (√((↑x : ℝ) * Var[X 0; P]))⁻¹ *
          (∑ k ∈ Finset.range x, X k ω - HMul.hMul (α := ℝ) (↑x : ℝ) (∫ (x : Ω), X 0 x ∂P)))
      x_1
Tactic: convert!
    (tendstoInDistribution_inv_sqrt_mul_var_mul_sum_sub this h hindep hident).continuous_comp (g :=
      (√Var[X 0; P] * ·)) (by fun_prop)