CentralLimitTheorem

📁 Source: Mathlib/Probability/CentralLimitTheorem.lean

Statistics

Metric	Count
Definitions	0
Theorems charFun_inv_sqrt_mul_sum, tendstoInDistribution_inv_sqrt_mul_sum, tendstoInDistribution_inv_sqrt_mul_sum_sub, tendsto_charFun_inv_sqrt_mul_pow	4
Total	4

ProbabilityTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
charFun_inv_sqrt_mul_sum 📖	mathematical	iIndepFun Real Real.measurableSpace IdentDistrib	MeasureTheory.charFun Real Real.measurableSpace InnerProductSpace.toInner Real.instRCLike NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField RCLike.toInnerProductSpaceReal MeasureTheory.Measure.map Real.instMul Real.instInv Real.sqrt Real.instNatCast Finset.sum Real.instAddCommMonoid Finset.range Complex Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring	—	IdentDistrib.aemeasurable_fst MeasureTheory.charFun_map_mul_comp Finset.aemeasurable_fun_sum ContinuousAdd.measurableMul₂ Real.borelSpace instSecondCountableTopologyReal IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal iIndepFun.charFun_map_fun_finset_sum_eq_prod iIndepFun.restrict Finset.prod_congr IdentDistrib.map_eq Finset.prod_apply Finset.prod_const Finset.card_range
tendstoInDistribution_inv_sqrt_mul_sum 📖	mathematical	HasLaw Real Real.measurableSpace gaussianReal Real.instZero NNReal NNReal.instOne MeasureTheory.integral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Monoid.toPow Pi.monoid Real.instMonoid Real.instOne iIndepFun IdentDistrib	MeasureTheory.TendstoInDistribution Real Real.measurableSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace BorelSpace.opensMeasurable Real.borelSpace Real.instMul Real.instInv Real.sqrt Real.instNatCast Finset.sum Real.instAddCommMonoid Finset.range Filter.atTop Nat.instPreorder	—	BorelSpace.opensMeasurable Real.borelSpace AEMeasurable.const_mul ContinuousMul.measurableMul IsSemitopologicalSemiring.toSeparatelyContinuousMul IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal Finset.aemeasurable_fun_sum ContinuousAdd.measurableMul₂ instSecondCountableTopologyReal IsSemitopologicalSemiring.toContinuousAdd IdentDistrib.aemeasurable_fst HasLaw.aemeasurable MeasureTheory.Measure.isProbabilityMeasure_map MeasureTheory.ProbabilityMeasure.tendsto_iff_tendsto_charFun FiniteDimensional.rclike_to_real HasLaw.map_eq Mathlib.Tactic.DepRewrite.nddcongrArg Nat.instAtLeastTwoHAddOfNat charFun_inv_sqrt_mul_sum charFun_gaussianReal MulZeroClass.mul_zero MulZeroClass.zero_mul one_mul zero_sub neg_div tendsto_charFun_inv_sqrt_mul_pow
tendstoInDistribution_inv_sqrt_mul_sum_sub 📖	mathematical	HasLaw Real Real.measurableSpace gaussianReal Real.instZero Real.toNNReal variance MeasureTheory.MemLp ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing SeminormedAddGroup.toContinuousENorm Real.pseudoMetricSpace ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Nat.instAtLeastTwoHAddOfNat iIndepFun IdentDistrib	MeasureTheory.TendstoInDistribution Real Real.measurableSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace BorelSpace.opensMeasurable Real.borelSpace Real.instMul Real.instInv Real.sqrt Real.instNatCast Real.instSub Finset.sum Real.instAddCommMonoid Finset.range MeasureTheory.integral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Filter.atTop Nat.instPreorder	—	Nat.instAtLeastTwoHAddOfNat BorelSpace.opensMeasurable Real.borelSpace eq_or_ne MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.ae_all_iff instCountableNat IdentDistrib.integral_eq ae_eq_integral_of_variance_eq_zero MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure IdentDistrib.memLp_iff IdentDistrib.variance_eq IdentDistrib.aemeasurable_fst MeasureTheory.tendstoInDistribution_of_identDistrib AEMeasurable.const_mul ContinuousMul.measurableMul IsSemitopologicalSemiring.toSeparatelyContinuousMul IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal AEMeasurable.sub_const ContinuousSub.measurableSub IsTopologicalAddGroup.to_continuousSub instIsTopologicalAddGroupReal Finset.aemeasurable_fun_sum ContinuousAdd.measurableMul₂ instSecondCountableTopologyReal IsSemitopologicalSemiring.toContinuousAdd MeasureTheory.Measure.map_congr Filter.mp_mem Filter.univ_mem' CharP.cast_eq_zero CharP.ofCharZero RCLike.charZero_rclike Real.sqrt_zero inv_zero Finset.sum_congr Finset.sum_const zero_nsmul MulZeroClass.zero_mul sub_self MulZeroClass.mul_zero Finset.card_range nsmul_eq_mul HasLaw.aemeasurable IsScalarTower.right MeasureTheory.Measure.map_const MeasureTheory.IsProbabilityMeasure.measure_univ one_smul HasLaw.map_eq Real.toNNReal_zero gaussianReal_zero_var sq_nonneg AddGroup.existsAddOfLE IsOrderedRing.toPosMulMono Real.instIsOrderedRing IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid zero_div NNReal.eq Real.sq_sqrt sup_of_le_left div_self gaussianReal_div_const Real.sqrt_mul mul_inv_rev Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.inv_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.subst_sub Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons one_mul Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div div_one Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.eq_div_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div' Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero Mathlib.Tactic.FieldSimp.NF.cons_zero_eq_div_of_eq_div one_ne_zero NeZero.one GroupWithZero.toNontrivial Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.div_eq_eval₂ Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero MeasureTheory.TendstoInDistribution.continuous_comp Continuous.const_mul continuous_id'
tendsto_charFun_inv_sqrt_mul_pow 📖	mathematical	AEMeasurable Real Real.measurableSpace MeasureTheory.integral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Real.instZero Monoid.toPow Pi.monoid Real.instMonoid Real.instOne	Filter.Tendsto Complex Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring MeasureTheory.charFun Real Real.measurableSpace InnerProductSpace.toInner Real.instRCLike NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField RCLike.toInnerProductSpaceReal MeasureTheory.Measure.map Real.instMul Real.instInv Real.sqrt Real.instNatCast Filter.atTop Nat.instPreorder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing Complex.instNormedField Complex.exp DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.instNeg Complex.ofReal instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Complex.tendsto_pow_exp_of_isLittleO_sub_add_div Nat.instAtLeastTwoHAddOfNat MulZeroClass.zero_mul Filter.Tendsto.mul_const IsSemitopologicalSemiring.toSeparatelyContinuousMul IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal Filter.Tendsto.comp tendsto_inv_atTop_zero Real.instIsStrictOrderedRing instOrderTopologyReal Real.tendsto_sqrt_atTop tendsto_natCast_atTop_atTop Real.instIsOrderedRing Real.instArchimedean Complex.ofReal_inv Complex.ofReal_mul Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.inv_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.inv_single Mathlib.Tactic.Ring.inv_mul Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_inv_pos Complex.instCharZero Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.div_pf Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsRat.to_raw_eq Mathlib.Meta.NormNum.isRat_mul Mathlib.Meta.NormNum.IsInt.to_isRat Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNNRat.to_isRat Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.sub_pf Asymptotics.IsLittleO.comp_tendsto MeasureTheory.taylor_charFun_two one_div norm_inv RCLike.norm_natCast Asymptotics.isLittleO_norm_right Asymptotics.IsLittleO.of_const_mul_right Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul neg_div Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.pow_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ div_one Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval one_mul mul_neg Mathlib.Tactic.FieldSimp.eq_div_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div' Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_ofNat Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.inv_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.cons_ne_zero Mathlib.Meta.NormNum.isNat_eq_false RCLike.charZero_rclike Nat.cast_zero one_ne_zero NeZero.one GroupWithZero.toNontrivial Real.sq_sqrt Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one

---

← Back to Index