awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.BorelCantelli
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s μ
hs' : Eq (α := ℝ≥0∞) (∑' (n : ℕ), (μ : (a : Set Ω) → ℝ≥0∞) (s n)) ∞
this_1 : IsProbabilityMeasure μ
this :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (n : ℕ),
      Eq (α := ℝ) (μ[(s (n + 1)).indicator 1 | (↑(filtrationOfSet (s := s) hsm) : ℕ → MeasurableSpace Ω) n] ω)
        ((fun (x : Ω) ↦ μ.real (s (n + 1))) ω)
ω : Ω
hω :
  ∀ (n : ℕ),
    μ[(s (n + 1)).indicator 1 | (↑(filtrationOfSet (s := s) hsm) : ℕ → MeasurableSpace Ω) n] ω = μ.real (s (n + 1))
htends : ∀ (x : NNReal), ∀ᶠ (a : ℕ) in atTop, (↑x : ℝ≥0∞) < ∑ k ∈ Finset.range a, (μ : (a : Set Ω) → ℝ≥0∞) (s (k + 1))
B : ℝ
hB : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.range fun (n : ℕ) ↦ ∑ x ∈ Finset.range n, μ.real (s (x + 1))) x → x ≤ B
n : ℕ
⊢ Eq (α := ℝ) ((fun (n : ℕ) ↦ (∑ x ∈ Finset.range n, μ.real (s (x + 1)) : ℝ)) n)
    (∑ a ∈ Finset.range n, ENNReal.toReal ((μ : (a : Set Ω) → ℝ≥0∞) (s (a + 1))))

Tactic:
rfl
-- Module: Mathlib.Probability.BorelCantelli
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s μ
hs' : Eq (α := ℝ≥0∞) (∑' (n : ℕ), (μ : (a : Set Ω) → ℝ≥0∞) (s n)) ∞
this_1 : IsProbabilityMeasure μ
this :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (n : ℕ),
      Eq (α := ℝ) (μ[(s (n + 1)).indicator 1 | (↑(filtrationOfSet (s := s) hsm) : ℕ → MeasurableSpace Ω) n] ω)
        ((fun (x : Ω) ↦ μ.real (s (n + 1))) ω)
ω : Ω
hω :
  ∀ (n : ℕ),
    μ[(s (n + 1)).indicator 1 | (↑(filtrationOfSet (s := s) hsm) : ℕ → MeasurableSpace Ω) n] ω = μ.real (s (n + 1))
htends : ∀ (x : NNReal), ∀ᶠ (a : ℕ) in atTop, (↑x : ℝ≥0∞) < ∑ k ∈ Finset.range a, (μ : (a : Set Ω) → ℝ≥0∞) (s (k + 1))
B : ℝ
n : ℕ
hB : ENNReal.toReal (∑ k ∈ Finset.range n, (μ : (a : Set Ω) → ℝ≥0∞) (s (k + 1))) ≤ B
h : Ne (α := ℝ≥0∞) (∑ k ∈ Finset.range n, (μ : (a : Set Ω) → ℝ≥0∞) (s (k + 1))) ∞
h₁ : 0 ≤ B
⊢ ¬(↑B.toNNReal : ℝ≥0∞) < ∑ k ∈ Finset.range n, (μ : (a : Set Ω) → ℝ≥0∞) (s (k + 1))

Tactic:
rwa [not_lt, ENNReal.ofNNReal_toNNReal, ENNReal.le_ofReal_iff_toReal_le]

Premises used: ENNReal.ofNNReal_toNNReal, not_lt, ENNReal.le_ofReal_iff_toReal_le
-- Module: Mathlib.Probability.BorelCantelli
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s μ
hs' : Eq (α := ℝ≥0∞) (∑' (n : ℕ), (μ : (a : Set Ω) → ℝ≥0∞) (s n)) ∞
this_1 : IsProbabilityMeasure μ
this :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (n : ℕ),
      Eq (α := ℝ) (μ[(s (n + 1)).indicator 1 | (↑(filtrationOfSet (s := s) hsm) : ℕ → MeasurableSpace Ω) n] ω)
        ((fun (x : Ω) ↦ μ.real (s (n + 1))) ω)
ω : Ω
hω :
  ∀ (n : ℕ),
    μ[(s (n + 1)).indicator 1 | (↑(filtrationOfSet (s := s) hsm) : ℕ → MeasurableSpace Ω) n] ω = μ.real (s (n + 1))
htends : ∀ (x : NNReal), ∀ᶠ (a : ℕ) in atTop, (↑x : ℝ≥0∞) < ∑ k ∈ Finset.range a, (μ : (a : Set Ω) → ℝ≥0∞) (s (k + 1))
B : ℝ
n : ℕ
hB : ENNReal.toReal (∑ k ∈ Finset.range n, (μ : (a : Set Ω) → ℝ≥0∞) (s (k + 1))) ≤ B
⊢ Ne (α := ℝ≥0∞) (∑ k ∈ Finset.range n, (μ : (a : Set Ω) → ℝ≥0∞) (s (k + 1))) ∞

Tactic:
simp
-- Module: Mathlib.Probability.BorelCantelli
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s μ
hs' : Eq (α := ℝ≥0∞) (∑' (n : ℕ), (μ : (a : Set Ω) → ℝ≥0∞) (s n)) ∞
this_1 : IsProbabilityMeasure μ
this :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (n : ℕ),
      Eq (α := ℝ) (μ[(s (n + 1)).indicator 1 | (↑(filtrationOfSet (s := s) hsm) : ℕ → MeasurableSpace Ω) n] ω)
        ((fun (x : Ω) ↦ μ.real (s (n + 1))) ω)
ω : Ω
hω :
  ∀ (n : ℕ),
    μ[(s (n + 1)).indicator 1 | (↑(filtrationOfSet (s := s) hsm) : ℕ → MeasurableSpace Ω) n] ω = μ.real (s (n + 1))
htends : ∀ (x : NNReal), ∀ᶠ (a : ℕ) in atTop, (↑x : ℝ≥0∞) < ∑ k ∈ Finset.range a, (μ : (a : Set Ω) → ℝ≥0∞) (s (k + 1))
B : ℝ
n : ℕ
hB : ENNReal.toReal (∑ k ∈ Finset.range n, (μ : (a : Set Ω) → ℝ≥0∞) (s (k + 1))) ≤ B
⊢ 0 ≤ ENNReal.toReal (∑ k ∈ Finset.range n, (μ : (a : Set Ω) → ℝ≥0∞) (s (k + 1)))

Tactic:
positivity
-- Module: Mathlib.Probability.BorelCantelli
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s μ
hs' : Eq (α := ℝ≥0∞) (∑' (n : ℕ), (μ : (a : Set Ω) → ℝ≥0∞) (s n)) ∞
this_1 : IsProbabilityMeasure μ
this :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (n : ℕ),
      Eq (α := ℝ) (μ[(s (n + 1)).indicator 1 | (↑(filtrationOfSet (s := s) hsm) : ℕ → MeasurableSpace Ω) n] ω)
        ((fun (x : Ω) ↦ μ.real (s (n + 1))) ω)
ω : Ω
hω :
  ∀ (n : ℕ),
    μ[(s (n + 1)).indicator 1 | (↑(filtrationOfSet (s := s) hsm) : ℕ → MeasurableSpace Ω) n] ω = μ.real (s (n + 1))
htends : ∀ (x : NNReal), ∀ᶠ (a : ℕ) in atTop, (↑x : ℝ≥0∞) < ∑ k ∈ Finset.range a, (μ : (a : Set Ω) → ℝ≥0∞) (s (k + 1))
B : ℝ
n : ℕ
hB : ENNReal.toReal (∑ k ∈ Finset.range n, (μ : (a : Set Ω) → ℝ≥0∞) (s (k + 1))) ≤ B
⊢ 0 ≤ B

Tactic:
exact le_trans (by positivity) hB

Premises used: le_trans
-- Module: Mathlib.Probability.CDF
Goal:
μ : Measure ℝ
x : ℝ
⊢ 0 ≤ (↑(cdf μ) : ℝ → ℝ) x

Tactic:
condCDF_nonneg _ _ _

Premises used: ProbabilityTheory.condCDF_nonneg
-- Module: Mathlib.Probability.CDF
Goal:
μ : Measure ℝ
x : ℝ
⊢ (↑(cdf μ) : ℝ → ℝ) x ≤ 1

Tactic:
condCDF_le_one _ _ _

Premises used: ProbabilityTheory.condCDF_le_one
-- Module: Mathlib.Probability.CDF
Goal:
μ : Measure ℝ
⊢ Monotone (↑(cdf μ) : ℝ → ℝ)

Tactic:
(condCDF _ _).mono

Premises used: StieltjesFunction.mono, ProbabilityTheory.condCDF
-- Module: Mathlib.Probability.CDF
Goal:
μ : Measure ℝ
⊢ Tendsto (↑(cdf μ) : ℝ → ℝ) atBot (𝓝 0)

Tactic:
tendsto_condCDF_atBot _ _

Premises used: ProbabilityTheory.tendsto_condCDF_atBot
-- Module: Mathlib.Probability.CDF
Goal:
μ : Measure ℝ
⊢ Tendsto (↑(cdf μ) : ℝ → ℝ) atTop (𝓝 1)

Tactic:
tendsto_condCDF_atTop _ _

Premises used: ProbabilityTheory.tendsto_condCDF_atTop
-- Module: Mathlib.Probability.CDF
Goal:
μ : Measure ℝ
inst : IsProbabilityMeasure μ
x : ℝ
⊢ ∫⁻ (a : Unit),
      ENNReal.ofReal
        ((↑(condCDF (mα := PUnit.instMeasurableSpace) (Measure.prod (dirac ()) μ) a) : ℝ → ℝ)
          x) ∂fst (Measure.prod (dirac ()) μ) =
    (Measure.prod (dirac ()) μ : (a : Set (Unit × ℝ)) → ENNReal) (SProd.sprod (α := Set Unit) univ (Iic x))

Tactic:
have h := lintegral_condCDF ((dirac Unit.unit).prod μ) x
-- Module: Mathlib.Probability.CDF
Goal:
μ : Measure ℝ
inst : IsProbabilityMeasure μ
x : ℝ
h :
  ∫⁻ (a : Unit),
      ENNReal.ofReal
        ((↑(condCDF (mα := PUnit.instMeasurableSpace) (Measure.prod (dirac ()) μ) a) : ℝ → ℝ)
          x) ∂fst (Measure.prod (dirac ()) μ) =
    (Measure.prod (dirac ()) μ : (a : Set (Unit × ℝ)) → ENNReal) (SProd.sprod (α := Set Unit) univ (Iic x))
⊢ ENNReal.ofReal ((↑(cdf μ) : ℝ → ℝ) x) = (μ : (a : Set ℝ) → ENNReal) (Iic x)

Tactic:
simpa only [fst_prod, prod_prod, measure_univ, one_mul, lintegral_dirac] using h

Premises used: MeasureTheory.Measure.fst_prod, MeasureTheory.lintegral_dirac, MeasureTheory.IsProbabilityMeasure.measure_univ, MeasureTheory.Measure.prod_prod, one_mul
-- Module: Mathlib.Probability.CDF
Goal:
μ : Measure ℝ
inst : IsProbabilityMeasure μ
x : ℝ
rw : (↑(cdf μ) : ℝ → ℝ) x = ENNReal.toReal ((μ : (a : Set ℝ) → ENNReal) (Iic x))
rw₁ : (↑(cdf μ) : ℝ → ℝ) x = (ENNReal.ofReal ((↑(cdf μ) : ℝ → ℝ) x)).toReal
rw₂ rw₃ : (↑(cdf μ) : ℝ → ℝ) x = (↑(cdf μ) : ℝ → ℝ) x
⊢ (↑(cdf μ) : ℝ → ℝ) x = μ.real (Iic x)

Tactic:
rw [measureReal_def, ← ofReal_cdf μ x, ENNReal.toReal_ofReal (cdf_nonneg μ x)]

Premises used: ProbabilityTheory.cdf_nonneg, ENNReal.toReal_ofReal, MeasureTheory.measureReal_def, ProbabilityTheory.ofReal_cdf
-- Module: Mathlib.Probability.CDF
Goal:
μ : Measure ℝ
measure_univ : Eq (α := ENNReal) (((cdf μ).measure : (a : Set ℝ) → ENNReal) univ : ENNReal) (1 : ENNReal)
⊢ IsProbabilityMeasure (m0 := Real.measurableSpace) (cdf μ).measure

Tactic:
constructor
-- Module: Mathlib.Probability.CDF
Goal:
μ : Measure ℝ
⊢ Eq (α := ENNReal) (((cdf μ).measure : (a : Set ℝ) → ENNReal) univ : ENNReal) (1 : ENNReal)

Tactic:
simp only [StieltjesFunction.measure_univ _ (tendsto_cdf_atBot μ) (tendsto_cdf_atTop μ), sub_zero,
    ENNReal.ofReal_one]

Premises used: sub_zero, StieltjesFunction.measure_univ, ENNReal.ofReal_one, ProbabilityTheory.tendsto_cdf_atTop, ProbabilityTheory.tendsto_cdf_atBot
-- Module: Mathlib.Probability.CDF
Goal:
μ : Measure ℝ
inst : IsProbabilityMeasure μ
⊢ (cdf μ).measure = μ

Tactic:
ext_of_Iic (cdf μ).measure μ (fun a ↦ ?_)

Premises used: StieltjesFunction.measure, MeasureTheory.Measure.ext_of_Iic, ProbabilityTheory.cdf
-- Module: Mathlib.Probability.CDF
Goal:
μ : Measure ℝ
inst : IsProbabilityMeasure μ
refine :
  ∀ (a : ℝ),
    Eq (α := ENNReal) (((cdf μ).measure : (a : Set ℝ) → ENNReal) (Iic a) : ENNReal)
      ((μ : (a : Set ℝ) → ENNReal) (Iic a) : ENNReal)
⊢ (cdf μ).measure = μ

Tactic:
refine ext_of_Iic (cdf μ).measure μ (fun a ↦ ?_)

Premises used: StieltjesFunction.measure, MeasureTheory.Measure.ext_of_Iic, ProbabilityTheory.cdf
-- Module: Mathlib.Probability.CDF
Goal:
μ : Measure ℝ
inst : IsProbabilityMeasure μ
a : ℝ
rw : ENNReal.ofReal ((↑(cdf μ) : ℝ → ℝ) a - 0) = (μ : (a : Set ℝ) → ENNReal) (Iic a)
rw₁ : ENNReal.ofReal ((↑(cdf μ) : ℝ → ℝ) a) = (μ : (a : Set ℝ) → ENNReal) (Iic a)
rw₂ rw₃ :
  Eq (α := ENNReal) ((μ : (a : Set ℝ) → ENNReal) (Iic a) : ENNReal) ((μ : (a : Set ℝ) → ENNReal) (Iic a) : ENNReal)
⊢ Eq (α := ENNReal) (((cdf μ).measure : (a : Set ℝ) → ENNReal) (Iic a) : ENNReal)
    ((μ : (a : Set ℝ) → ENNReal) (Iic a) : ENNReal)

Tactic:
rw [StieltjesFunction.measure_Iic _ (tendsto_cdf_atBot μ), sub_zero, ofReal_cdf]

Premises used: sub_zero, StieltjesFunction.measure_Iic, ProbabilityTheory.tendsto_cdf_atBot, ProbabilityTheory.ofReal_cdf
-- Module: Mathlib.Probability.CDF
Goal:
f : StieltjesFunction ℝ
hf0 : Tendsto (↑f : ℝ → ℝ) atBot (𝓝 0)
hf1 : Tendsto (↑f : ℝ → ℝ) atTop (𝓝 1)
⊢ cdf f.measure = f

Tactic:
(cdf f.measure).eq_of_measure_of_tendsto_atBot f ?_ (tendsto_cdf_atBot _) hf0

Premises used: StieltjesFunction.measure, StieltjesFunction.eq_of_measure_of_tendsto_atBot, ProbabilityTheory.tendsto_cdf_atBot, ProbabilityTheory.cdf
-- Module: Mathlib.Probability.CDF
Goal:
f : StieltjesFunction ℝ
hf0 : Tendsto (↑f : ℝ → ℝ) atBot (𝓝 0)
hf1 : Tendsto (↑f : ℝ → ℝ) atTop (𝓝 1)
refine : Eq (α := Measure ℝ) (cdf f.measure).measure f.measure
⊢ cdf f.measure = f

Tactic:
refine (cdf f.measure).eq_of_measure_of_tendsto_atBot f ?_ (tendsto_cdf_atBot _) hf0

Premises used: StieltjesFunction.measure, StieltjesFunction.eq_of_measure_of_tendsto_atBot, ProbabilityTheory.tendsto_cdf_atBot, ProbabilityTheory.cdf
-- Module: Mathlib.Probability.CDF
Goal:
f : StieltjesFunction ℝ
hf0 : Tendsto (↑f : ℝ → ℝ) atBot (𝓝 0)
hf1 : Tendsto (↑f : ℝ → ℝ) atTop (𝓝 1)
rw : ENNReal.ofReal (HSub.hSub (α := ℝ) 1 0) = 1
rw₁ : ENNReal.ofReal 1 = 1
rw₂ rw₃ : Eq (α := ENNReal) 1 1
⊢ Eq (α := ENNReal) ((f.measure : (a : Set ℝ) → ENNReal) univ : ENNReal) (1 : ENNReal)

Tactic:
rw [f.measure_univ hf0 hf1, sub_zero, ENNReal.ofReal_one]

Premises used: sub_zero, StieltjesFunction.measure_univ, ENNReal.ofReal_one
-- Module: Mathlib.Probability.CDF
Goal:
f : StieltjesFunction ℝ
hf0 : Tendsto (↑f : ℝ → ℝ) atBot (𝓝 0)
hf1 : Tendsto (↑f : ℝ → ℝ) atTop (𝓝 1)
⊢ IsProbabilityMeasure (m0 := Real.measurableSpace) f.measure

Tactic:
have h_prob : IsProbabilityMeasure f.measure :=
    ⟨by rw [f.measure_univ hf0 hf1, sub_zero, ENNReal.ofReal_one]⟩
-- Module: Mathlib.Probability.CDF
Goal:
f : StieltjesFunction ℝ
hf0 : Tendsto (↑f : ℝ → ℝ) atBot (𝓝 0)
hf1 : Tendsto (↑f : ℝ → ℝ) atTop (𝓝 1)
h_prob : IsProbabilityMeasure (m0 := Real.measurableSpace) f.measure
⊢ Eq (α := Measure ℝ) (cdf f.measure).measure f.measure

Tactic:
measure_cdf f.measure

Premises used: StieltjesFunction.measure, ProbabilityTheory.measure_cdf
-- Module: Mathlib.Probability.CDF
Goal:
f : StieltjesFunction ℝ
hf0 : Tendsto (↑f : ℝ → ℝ) atBot (𝓝 0)
hf1 : Tendsto (↑f : ℝ → ℝ) atTop (𝓝 1)
h_prob : IsProbabilityMeasure (m0 := Real.measurableSpace) f.measure
⊢ Eq (α := Measure ℝ) (cdf f.measure).measure f.measure

Tactic:
exact measure_cdf f.measure

Premises used: StieltjesFunction.measure, ProbabilityTheory.measure_cdf
-- Module: Mathlib.Probability.CDF
Goal:
μ : Measure (↑I : Type)
inst : IsProbabilityMeasure μ
x : (↑I : Type)
⊢ AEMeasurable (Subtype.val (p := fun (x : ℝ) ↦ x ∈ I)) μ

Tactic:
fun_prop
-- Module: Mathlib.Probability.CDF
Goal:
μ : Measure (↑I : Type)
inst : IsProbabilityMeasure μ
x : (↑I : Type)
⊢ IsProbabilityMeasure (m0 := Real.measurableSpace) (Measure.map (Subtype.val (p := fun (x : ℝ) ↦ x ∈ I)) μ)

Tactic:
haveI : IsProbabilityMeasure (μ.map Subtype.val) := isProbabilityMeasure_map (by fun_prop)
-- Module: Mathlib.Probability.CDF
Goal:
μ : Measure (↑I : Type)
inst : IsProbabilityMeasure μ
x : (↑I : Type)
this : IsProbabilityMeasure (m0 := Real.measurableSpace) (Measure.map (Subtype.val (p := fun (x : ℝ) ↦ x ∈ I)) μ)
rw :
  Measure.real (m := Real.measurableSpace) (Measure.map (Subtype.val (p := fun (x : ℝ) ↦ x ∈ I)) μ) (Iic (↑x : ℝ)) =
    μ.real (Icc 0 x)
rw₁ : μ.real (Subtype.val (p := fun (x : ℝ) ↦ x ∈ I) ⁻¹' Iic (↑x : ℝ)) = μ.real (Icc 0 x)
rw₂ rw₃ : μ.real (Icc 0 x) = μ.real (Icc 0 x)
⊢ (↑(cdf (Measure.map (Subtype.val (p := fun (x : ℝ) ↦ x ∈ I)) μ)) : ℝ → ℝ) (↑x : ℝ) = μ.real (Icc 0 x)

Tactic:
rw [ProbabilityTheory.cdf_eq_real,
    map_measureReal_apply measurable_subtype_coe measurableSet_Iic, subtype_Iic_eq_Icc]

Premises used: measurable_subtype_coe, ProbabilityTheory.cdf_eq_real, measurableSet_Iic, MeasureTheory.map_measureReal_apply, unitInterval.subtype_Iic_eq_Icc
-- Module: Mathlib.Probability.CDF
Goal:
μ ν : Measure ℝ
inst : IsProbabilityMeasure μ
inst_1 : IsProbabilityMeasure ν
h : cdf μ = cdf ν
rw : (cdf μ).measure = ν
rw₁ : Eq (α := Measure ℝ) (cdf μ).measure (cdf ν).measure
rw₂ rw₃ : Eq (α := Measure ℝ) (cdf ν).measure (cdf ν).measure
⊢ μ = ν

Tactic:
rw [← measure_cdf μ, ← measure_cdf ν, h]

Premises used: ProbabilityTheory.measure_cdf
-- Module: Mathlib.Probability.CDF
Goal:
μ ν : Measure ℝ
inst : IsProbabilityMeasure μ
inst_1 : IsProbabilityMeasure ν
h : μ = ν
rw rw₁ : cdf ν = cdf ν
⊢ cdf μ = cdf ν

Tactic:
rw [h]
-- Module: Mathlib.Probability.CentralLimitTheorem
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
X : ℕ → Ω → ℝ
hindep : iIndepFun (β := fun (x : ℕ) ↦ ℝ) X P
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) P P
n : ℕ
t : ℝ
⊢ ∀ (n : ℕ), AEMeasurable (X n) P

Tactic:
have mX n := (hident n).aemeasurable_fst
-- Module: Mathlib.Probability.CentralLimitTheorem
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
X : ℕ → Ω → ℝ
hindep : iIndepFun (β := fun (x : ℕ) ↦ ℝ) X P
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) P P
n : ℕ
t : ℝ
mX : ∀ (n : ℕ), AEMeasurable (X n) P
rw :
  (∏ i ∈ Finset.range n, charFun (mE := Real.measurableSpace) (Measure.map (X i) P)) ((√(↑n : ℝ))⁻¹ * t) =
    charFun (mE := Real.measurableSpace) (Measure.map (X 0) P) ((√(↑n : ℝ))⁻¹ * t) ^ n
hf : AEMeasurable (β := ℝ) (fun (ω : Ω) ↦ ∑ k ∈ Finset.range n, X k ω) P
⊢ charFun (mE := Real.measurableSpace) (Measure.map (fun (ω : Ω) ↦ (√(↑n : ℝ))⁻¹ * ∑ k ∈ Finset.range n, X k ω) P) t =
    charFun (mE := Real.measurableSpace) (Measure.map (X 0) P) ((√(↑n : ℝ))⁻¹ * t) ^ n

Tactic:
rw [charFun_map_mul_comp, (hindep.restrict _).charFun_map_fun_finsetSum_eq_prod (fun _ _ ↦ mX _)]

Premises used: ProbabilityTheory.iIndepFun.charFun_map_fun_finsetSum_eq_prod, MeasureTheory.charFun_map_mul_comp, ProbabilityTheory.iIndepFun.restrict
-- Module: Mathlib.Probability.CentralLimitTheorem
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
X : ℕ → Ω → ℝ
hindep : iIndepFun (β := fun (x : ℕ) ↦ ℝ) X P
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) P P
n : ℕ
t : ℝ
mX : ∀ (n : ℕ), AEMeasurable (X n) P
⊢ (∏ i ∈ Finset.range n, charFun (mE := Real.measurableSpace) (Measure.map (X i) P)) ((√(↑n : ℝ))⁻¹ * t) =
    charFun (mE := Real.measurableSpace) (Measure.map (X 0) P) ((√(↑n : ℝ))⁻¹ * t) ^ n

Tactic:
simp [fun i ↦ (hident i).map_eq]

Premises used: ProbabilityTheory.IdentDistrib.map_eq
-- Module: Mathlib.Probability.CentralLimitTheorem
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
X : ℕ → Ω → ℝ
hindep : iIndepFun (β := fun (x : ℕ) ↦ ℝ) X P
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) P P
n : ℕ
t : ℝ
mX : ∀ (n : ℕ), AEMeasurable (X n) P
⊢ AEMeasurable (β := ℝ) (fun (ω : Ω) ↦ ∑ k ∈ Finset.range n, X k ω) P

Tactic:
Finset.aemeasurable_fun_sum _ fun _ _ ↦ mX _

Premises used: Finset.aemeasurable_fun_sum
-- Module: Mathlib.Probability.CentralLimitTheorem
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
X : ℕ → Ω → ℝ
hindep : iIndepFun (β := fun (x : ℕ) ↦ ℝ) X P
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) P P
n : ℕ
t : ℝ
mX : ∀ (n : ℕ), AEMeasurable (X n) P
⊢ AEMeasurable (β := ℝ) (fun (ω : Ω) ↦ ∑ k ∈ Finset.range n, X k ω) P

Tactic:
exact Finset.aemeasurable_fun_sum _ fun _ _ ↦ mX _

Premises used: Finset.aemeasurable_fun_sum
-- 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 (β := ℕ) (↑t : ℂ) 2 / 2 / (↑n : ℂ)))
    fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) 1 (↑n : ℂ)
⊢ Tendsto (fun (n : ℕ) ↦ charFun (mE := Real.measurableSpace) (Measure.map X P) ((√(↑n : ℝ))⁻¹ * t) ^ n) atTop
    (𝓝 (cexp (-HPow.hPow (β := ℕ) (↑t : ℂ) 2 / 2)))

Tactic:
apply tendsto_pow_exp_of_isLittleO_sub_add_div

Premises used: Complex.tendsto_pow_exp_of_isLittleO_sub_add_div
-- 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
⊢ Eq (α := (n : ℕ) → ℝ) (fun (n : ℕ) ↦ ‖HDiv.hDiv (α := ℂ) 1 (↑n : ℂ)‖) fun (n : ℕ) ↦ ‖HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)‖

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 :
  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
⊢ Eq (α := (n : ℕ) → ℝ) (fun (n : ℕ) ↦ ‖HDiv.hDiv (α := ℂ) 1 (↑n : ℂ)‖) fun (n : ℕ) ↦ ‖HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)‖

Tactic:
have aux : (fun (n : ℕ) ↦ ‖(1 / n : ℂ)‖) = fun (n : ℕ) ↦ ‖(1 / n : ℝ)‖ := by 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 :
  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 : ℝ)‖
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 : ℝ)
⊢ 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]

Premises used: Asymptotics.isLittleO_norm_right
-- 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 : ℝ)‖
⊢ 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:
.of_const_mul_right (c := t ^ 2) ?_

Premises used: Asymptotics.IsLittleO.of_const_mul_right
-- 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 : ℝ)‖
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 : ℝ)
⊢ 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:
refine .of_const_mul_right (c := t ^ 2) ?_
-- 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 : ℝ)‖
⊢ 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:
this