noncomputable def CentralLimitTheorem.expTaylorRemainder (x : ℝ) : ℂ

theorem CentralLimitTheorem.norm_ofReal_mul_I (x : ℝ) : ‖↑x * Complex.I‖ = |x|

theorem CentralLimitTheorem.expTaylorRemainder_le_cube {x : ℝ} (hx : |x| ≤ 1) : ‖expTaylorRemainder x‖ ≤ |x| ^ 3

theorem CentralLimitTheorem.expTaylorRemainder_le_sq {x : ℝ} (hx : 1 ≤ |x|) : ‖expTaylorRemainder x‖ ≤ 4 * |x| ^ 2

theorem CentralLimitTheorem.expTaylorRemainder_le_min (x : ℝ) : ‖expTaylorRemainder x‖ ≤ 4 * min (|x| ^ 2) (|x| ^ 3)

theorem CentralLimitTheorem.min_pow_le_rpow (x α : ℝ) (hα1 : 0 < α) (hα2 : α < 1) : min (|x| ^ 2) (|x| ^ 3) ≤ |x| ^ (2 + α)

theorem CentralLimitTheorem.expTaylorRemainder_le_rpow (x α : ℝ) (hα1 : 0 < α) (hα2 : α < 1) : ‖expTaylorRemainder x‖ ≤ 4 * |x| ^ (2 + α)

theorem CentralLimitTheorem.memLp_two_of_higher_moment {Ω : Type u_1} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {X : Ω → ℝ} {α : ℝ} (hα : 0 < α) (hLp : MeasureTheory.MemLp X (ENNReal.ofReal (2 + α)) P) : MeasureTheory.MemLp X 2 P

theorem CentralLimitTheorem.central_limit_theorem {Ω : Type u_1} {Ω' : Type u_2} [MeasurableSpace Ω] [MeasurableSpace Ω'] {P : MeasureTheory.Measure Ω} {P' : MeasureTheory.Measure Ω'} [MeasureTheory.IsProbabilityMeasure P] [MeasureTheory.IsProbabilityMeasure P'] {X : ℕ → Ω → ℝ} {Y : Ω' → ℝ} {α : ℝ} (hα : 0 < α) (hLp : MeasureTheory.MemLp (X 0) (ENNReal.ofReal (2 + α)) P) (hindep : ProbabilityTheory.iIndepFun X P) (hident : ∀ (i : ℕ), ProbabilityTheory.IdentDistrib (X i) (X 0) P P) (hY : ProbabilityTheory.HasLaw Y (ProbabilityTheory.gaussianReal 0 (ProbabilityTheory.variance (X 0) P).toNNReal) P') : MeasureTheory.TendstoInDistribution (fun (n : ℕ) (ω : Ω) => (√↑n)⁻¹ * (∑ k ∈ Finset.range n, X k ω - ↑n * ∫ (x : Ω), X 0 x ∂P)) Filter.atTop Y (fun (x : ℕ) => P) P'