StrongLaw

📁 Source: Mathlib/Probability/StrongLaw.lean

Statistics

Metric	Count
Definitions truncation	1
Theorems integrable_truncation, memLp_truncation, truncation, truncation, abs_truncation_le_abs_self, abs_truncation_le_bound, integral_truncation_eq_intervalIntegral, integral_truncation_eq_intervalIntegral_of_nonneg, integral_truncation_le_integral_of_nonneg, moment_truncation_eq_intervalIntegral, moment_truncation_eq_intervalIntegral_of_nonneg, strong_law_Lp, strong_law_ae, strong_law_ae_of_measurable, strong_law_ae_real, strong_law_ae_simpleFunc_comp, strong_law_aux1, strong_law_aux2, strong_law_aux3, strong_law_aux4, strong_law_aux5, strong_law_aux6, strong_law_aux7, sum_prob_mem_Ioc_le, sum_variance_truncation_le, tendsto_integral_truncation, truncation_eq_of_nonneg, truncation_eq_self, truncation_nonneg, truncation_zero, tsum_prob_mem_Ioi_lt_top	31
Total	32

MeasureTheory.AEStronglyMeasurable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
integrable_truncation 📖	mathematical	MeasureTheory.AEStronglyMeasurable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace	MeasureTheory.Integrable SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing ProbabilityTheory.truncation	—	MeasureTheory.memLp_one_iff_integrable memLp_truncation
memLp_truncation 📖	mathematical	MeasureTheory.AEStronglyMeasurable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace	MeasureTheory.MemLp ContinuousENorm.toENorm SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing SeminormedAddGroup.toContinuousENorm ProbabilityTheory.truncation	—	MeasureTheory.MemLp.of_bound truncation Filter.Eventually.of_forall MeasureTheory.Measure.instOuterMeasureClass ProbabilityTheory.abs_truncation_le_bound
truncation 📖	mathematical	MeasureTheory.AEStronglyMeasurable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace	ProbabilityTheory.truncation	—	comp_aemeasurable MeasureTheory.StronglyMeasurable.aestronglyMeasurable MeasureTheory.StronglyMeasurable.indicator stronglyMeasurable_id PseudoEMetricSpace.pseudoMetrizableSpace BorelSpace.opensMeasurable Real.borelSpace instSecondCountableTopologyReal measurableSet_Ioc instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid aemeasurable

ProbabilityTheory

Definitions

Name	Category	Theorems
truncation 📖	CompOp	22 math math: MeasureTheory.AEStronglyMeasurable.memLp_truncation, tendsto_integral_truncation, abs_truncation_le_bound, integral_truncation_eq_intervalIntegral, integral_truncation_eq_intervalIntegral_of_nonneg, sum_variance_truncation_le, moment_truncation_eq_intervalIntegral_of_nonneg, truncation_eq_self, MeasureTheory.AEStronglyMeasurable.truncation, moment_truncation_eq_intervalIntegral, IdentDistrib.truncation, integral_truncation_le_integral_of_nonneg, truncation_eq_of_nonneg, MeasureTheory.AEStronglyMeasurable.integrable_truncation, strong_law_aux4, abs_truncation_le_abs_self, strong_law_aux1, strong_law_aux2, strong_law_aux3, strong_law_aux5, truncation_nonneg, truncation_zero

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
abs_truncation_le_abs_self 📖	mathematical	—	Real Real.instLE abs Real.lattice Real.instAddGroup truncation	—	le_rfl abs_zero IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add
abs_truncation_le_bound 📖	mathematical	—	Real Real.instLE abs Real.lattice Real.instAddGroup truncation	—	abs_le_abs neg_le IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add LT.lt.le abs_zero
integral_truncation_eq_intervalIntegral 📖	mathematical	MeasureTheory.AEStronglyMeasurable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instLE Real.instZero	MeasureTheory.integral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal truncation intervalIntegral Real.instNeg MeasureTheory.Measure.map Real.measurableSpace	—	pow_one moment_truncation_eq_intervalIntegral one_ne_zero
integral_truncation_eq_intervalIntegral_of_nonneg 📖	mathematical	MeasureTheory.AEStronglyMeasurable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Pi.hasLe Real.instLE Pi.instZero Real.instZero	MeasureTheory.integral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal truncation intervalIntegral MeasureTheory.Measure.map Real.measurableSpace	—	pow_one moment_truncation_eq_intervalIntegral_of_nonneg one_ne_zero
integral_truncation_le_integral_of_nonneg 📖	mathematical	MeasureTheory.Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing Pi.hasLe Real.instLE Pi.instZero Real.instZero	MeasureTheory.integral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal truncation	—	MeasureTheory.integral_mono_of_nonneg Real.instIsOrderedAddMonoid IsStrictOrderedModule.toIsOrderedModule IsStrictOrderedRing.toIsStrictOrderedModule Real.instIsStrictOrderedRing instClosedIciTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Filter.Eventually.of_forall MeasureTheory.Measure.instOuterMeasureClass truncation_nonneg le_abs_self abs_truncation_le_abs_self abs_of_nonneg IsOrderedAddMonoid.toAddLeftMono
moment_truncation_eq_intervalIntegral 📖	mathematical	MeasureTheory.AEStronglyMeasurable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instLE Real.instZero	MeasureTheory.integral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Monoid.toNatPow Real.instMonoid truncation intervalIntegral Real.instNeg MeasureTheory.Measure.map Real.measurableSpace	—	measurableSet_Ioc BorelSpace.opensMeasurable Real.borelSpace instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid MeasureTheory.integral_map MeasureTheory.AEStronglyMeasurable.aemeasurable PseudoEMetricSpace.pseudoMetrizableSpace Measurable.aestronglyMeasurable instSecondCountableTopologyReal Measurable.pow_const Monoid.measurablePow ContinuousMul.measurableMul₂ IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Measurable.indicator measurable_id intervalIntegral.integral_of_le le_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Nat.instAtLeastTwoHAddOfNat Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.neg_congr Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Linarith.add_lt_of_le_of_neg Real.instIsStrictOrderedRing Mathlib.Tactic.Linarith.mul_nonpos Real.instIsOrderedRing Mathlib.Tactic.Linarith.sub_nonpos_of_le Mathlib.Meta.NormNum.isNat_lt_true RCLike.charZero_rclike Mathlib.Tactic.Linarith.sub_neg_of_lt MeasureTheory.integral_indicator ite_pow zero_pow
moment_truncation_eq_intervalIntegral_of_nonneg 📖	mathematical	MeasureTheory.AEStronglyMeasurable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Pi.hasLe Real.instLE Pi.instZero Real.instZero	MeasureTheory.integral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Monoid.toNatPow Real.instMonoid truncation intervalIntegral MeasureTheory.Measure.map Real.measurableSpace	—	measurableSet_Ioc BorelSpace.opensMeasurable Real.borelSpace instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid truncation_eq_of_nonneg le_or_gt MeasureTheory.integral_map MeasureTheory.AEStronglyMeasurable.aemeasurable PseudoEMetricSpace.pseudoMetrizableSpace Measurable.aestronglyMeasurable instSecondCountableTopologyReal Measurable.pow_const Monoid.measurablePow ContinuousMul.measurableMul₂ IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Measurable.indicator measurable_id intervalIntegral.integral_of_le MeasureTheory.integral_indicator ite_pow zero_pow intervalIntegral.integral_of_ge LT.lt.le Set.Ioc_eq_empty_of_le Set.indicator_empty MeasureTheory.integral_zero MeasureTheory.integral_eq_zero_of_ae MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.ae_map_iff measurableSet_Ici instClosedIciTopology Filter.Eventually.of_forall Filter.mp_mem Filter.univ_mem' Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.cast_zero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Linarith.add_lt_of_le_of_neg Real.instIsStrictOrderedRing Mathlib.Tactic.Linarith.sub_nonpos_of_le Real.instIsOrderedRing Mathlib.Tactic.Linarith.sub_neg_of_lt
strong_law_Lp 📖	mathematical	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal MeasureTheory.MemLp ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toPseudoMetricSpace Pairwise Function.onFun IndepFun IdentDistrib	Filter.Tendsto MeasureTheory.eLpNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Real SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField Real.instInv Real.instNatCast Finset.sum Finset.range MeasureTheory.integral Filter.atTop Nat.instPreorder nhds ENNReal.instTopologicalSpace instZeroENNReal	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.ae_all_iff instCountableNat IdentDistrib.ae_snd IdentDistrib.symm measurableSet_eq OpensMeasurableSpace.toMeasurableSingletonClass BorelSpace.opensMeasurable T5Space.toT1Space T6Space.toT5Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace MeasureTheory.integral_eq_zero_of_ae sub_zero MeasureTheory.eLpNorm_eq_zero_of_ae_zero Filter.mp_mem Filter.univ_mem' Finset.sum_congr Finset.sum_const_zero smul_zero ENNReal.instT5Space Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat MeasureTheory.MemLp.isProbabilityMeasure_of_indepFun LT.lt.ne' LT.lt.trans_le zero_lt_one IsOrderedRing.toZeroLEOneClass ENNReal.instIsOrderedRing NeZero.charZero_one ENNReal.instCharZero zero_ne_one IdentDistrib.aestronglyMeasurable_iff PseudoEMetricSpace.pseudoMetrizableSpace MeasureTheory.MemLp.integrable MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure MeasureTheory.AEStronglyMeasurable.const_smul UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul Finset.aestronglyMeasurable_fun_sum IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup MeasureTheory.tendsto_Lp_finite_of_tendstoInMeasure MeasureTheory.memLp_const Finset.sum_apply MeasureTheory.UniformIntegrable.unifIntegrable MeasureTheory.uniformIntegrable_average MemLp.uniformIntegrable_of_identDistrib MeasureTheory.tendstoInMeasure_of_tendsto_ae strong_law_ae
strong_law_ae 📖	mathematical	MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup Pairwise Function.onFun IndepFun IdentDistrib	Filter.Eventually Filter.Tendsto Real SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField Real.instInv Real.instNatCast Finset.sum Finset.range Filter.atTop Nat.instPreorder nhds MeasureTheory.integral MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.ae_all_iff instCountableNat IdentDistrib.ae_snd IdentDistrib.symm measurableSet_eq OpensMeasurableSpace.toMeasurableSingletonClass BorelSpace.opensMeasurable T5Space.toT1Space T6Space.toT5Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace Filter.mp_mem Filter.univ_mem' Finset.sum_congr Finset.sum_const_zero smul_zero Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat MeasureTheory.integral_eq_zero_of_ae MeasureTheory.Integrable.isProbabilityMeasure_of_indepFun zero_ne_one IdentDistrib.integrable_iff MeasureTheory.Integrable.congr strong_law_ae_of_measurable IndepFun.congr IdentDistrib.trans PseudoEMetricSpace.pseudoMetrizableSpace MeasureTheory.integral_congr_ae Filter.Tendsto.congr
strong_law_ae_of_measurable 📖	mathematical	MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup MeasureTheory.StronglyMeasurable Pairwise Function.onFun IndepFun IdentDistrib	Filter.Eventually Filter.Tendsto Real SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField Real.instInv Real.instNatCast Finset.sum Finset.range Filter.atTop Nat.instPreorder nhds MeasureTheory.integral MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	Set.union_singleton MeasureTheory.StronglyMeasurable.separableSpace_range_union_singleton PseudoEMetricSpace.pseudoMetrizableSpace BorelSpace.opensMeasurable MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.ae_all_iff instCountableNat strong_law_ae_simpleFunc_comp MeasureTheory.StronglyMeasurable.measurable Measurable.norm Measurable.sub_stronglyMeasurable IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalAddGroup.toContinuousNeg measurable_id MeasureTheory.SimpleFunc.stronglyMeasurable strong_law_ae_real MeasureTheory.Integrable.norm MeasureTheory.Integrable.sub MeasureTheory.SimpleFunc.integrable_of_isFiniteMeasure MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure IndepFun.comp IdentDistrib.comp Filter.mp_mem Filter.univ_mem' tendsto_iff_norm_sub_tendsto_zero tendsto_order instOrderTopologyReal Filter.Eventually.of_forall LT.lt.trans_le norm_nonneg Nat.instAtLeastTwoHAddOfNat div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo lt_of_not_ge Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Nat.cast_one Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Mathlib.Tactic.Linarith.sub_neg_of_lt CancelDenoms.sub_subst CancelDenoms.add_subst CancelDenoms.div_subst Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike Mathlib.Meta.NormNum.isNat_mul Mathlib.Tactic.Linarith.mul_nonpos Mathlib.Tactic.Linarith.sub_nonpos_of_le Mathlib.Meta.NormNum.isNat_lt_true norm_sub_rev Filter.Eventually.exists Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat MeasureTheory.tendsto_integral_norm_approxOn_sub MeasureTheory.integral_sub LE.le.trans_lt MeasureTheory.norm_integral_le_integral_norm Finset.sum_sub_distrib smul_sub Mathlib.Tactic.Abel.unfold_sub Mathlib.Tactic.Abel.subst_into_addg Mathlib.Tactic.Abel.term_atomg Mathlib.Tactic.Abel.subst_into_negg Mathlib.Tactic.Abel.term_neg neg_zero Mathlib.Tactic.Abel.term_add_constg zero_add Mathlib.Tactic.Abel.term_add_termg Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.isInt_neg Mathlib.Tactic.Abel.zero_termg Mathlib.Tactic.Abel.const_add_termg add_zero norm_add₃_le add_le_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add norm_smul NormedSpace.toNormSMulClass norm_inv RCLike.norm_natCast div_eq_inv_mul mul_le_mul_of_nonneg_left IsOrderedRing.toPosMulMono norm_sum_le inv_nonneg_of_nonneg Nat.cast_nonneg' Real.instZeroLEOneClass le_of_lt add_le_add_left LT.lt.le
strong_law_ae_real 📖	mathematical	MeasureTheory.Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing Pairwise Function.onFun IndepFun Real.measurableSpace IdentDistrib	Filter.Eventually Filter.Tendsto DivInvMonoid.toDiv Real.instDivInvMonoid Finset.sum Real.instAddCommMonoid Finset.range Real.instNatCast Filter.atTop Nat.instPreorder nhds MeasureTheory.integral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.ae_all_iff instCountableNat IdentDistrib.ae_snd IdentDistrib.symm measurableSet_eq instMeasurableSingletonClassOfMeasurableEq instMeasurableEqOfSecondCountableTopologyOfT2Space BorelSpace.opensMeasurable Real.borelSpace instSecondCountableTopologyReal TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace Filter.mp_mem Filter.univ_mem' Finset.sum_congr Finset.sum_const_zero zero_div T5Space.toT1Space T6Space.toT5Space instT6SpaceOfMetrizableSpace Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat MeasureTheory.integral_eq_zero_of_ae MeasureTheory.Integrable.isProbabilityMeasure_of_indepFun zero_ne_one Measurable.max HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid measurable_id' measurable_const Measurable.neg ContinuousNeg.measurableNeg IsTopologicalRing.toContinuousNeg instIsTopologicalRingReal strong_law_aux7 MeasureTheory.Integrable.pos_part IndepFun.comp IdentDistrib.comp le_max_right MeasureTheory.Integrable.neg_part max_zero_sub_max_neg_zero_eq_self IsOrderedAddMonoid.toAddLeftMono MeasureTheory.integral_sub Filter.Tendsto.sub IsTopologicalAddGroup.to_continuousSub instIsTopologicalAddGroupReal
strong_law_ae_simpleFunc_comp 📖	mathematical	Measurable Pairwise Function.onFun IndepFun IdentDistrib	Filter.Eventually Filter.Tendsto Real SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField Real.instInv Real.instNatCast Finset.sum Finset.range DFunLike.coe MeasureTheory.SimpleFunc MeasureTheory.SimpleFunc.instFunLike Filter.atTop Nat.instPreorder nhds MeasureTheory.integral MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	MeasureTheory.SimpleFunc.induction MeasureTheory.Measure.instOuterMeasureClass Finset.sum_congr Set.piecewise_eq_indicator measurable_indicator_const_iff instMeasurableSingletonClassOfMeasurableEq instMeasurableEqOfSecondCountableTopologyOfT2Space BorelSpace.opensMeasurable Real.borelSpace instSecondCountableTopologyReal TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace NeZero.charZero_one RCLike.charZero_rclike strong_law_ae_real MeasureTheory.SimpleFunc.integrable_of_isFiniteMeasure MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure IndepFun.comp IdentDistrib.comp Filter.mp_mem Filter.univ_mem' Set.indicator_smul_const_apply one_smul integral_smul_const smul_smul Filter.Tendsto.smul_const IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul Finset.sum_add_distrib smul_add MeasureTheory.integral_add Filter.Tendsto.add IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup
strong_law_aux1 📖	mathematical	MeasureTheory.Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing MeasureTheory.MeasureSpace.toMeasurableSpace MeasureTheory.MeasureSpace.volume Pairwise Function.onFun IndepFun Real.measurableSpace IdentDistrib Real.instLE Real.instZero Real.instLT Real.instOne	Filter.Eventually abs Real.lattice Real.instAddGroup Real.instSub Finset.sum Real.instAddCommMonoid Finset.range Nat.floor Real.semiring Real.partialOrder FloorRing.toFloorSemiring Real.instRing Real.linearOrder Real.instIsStrictOrderedRing Real.instFloorRing Monoid.toNatPow Real.instMonoid truncation Real.instNatCast MeasureTheory.integral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Pi.addCommMonoid Real.instMul Filter.atTop Nat.instPreorder MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	LT.lt.trans zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike IdentDistrib.aestronglyMeasurable_snd PseudoEMetricSpace.pseudoMetrizableSpace Real.borelSpace IdentDistrib.symm MeasureTheory.StronglyMeasurable.indicator stronglyMeasurable_id BorelSpace.opensMeasurable instSecondCountableTopologyReal measurableSet_Ioc instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid Real.instIsStrictOrderedRing MeasureTheory.Measure.instOuterMeasureClass Nat.floor_mono pow_right_mono₀ IsOrderedRing.toPosMulMono Real.instIsOrderedRing LT.lt.le Nat.instAtLeastTwoHAddOfNat Finset.sum_le_sum IsOrderedAddMonoid.toAddLeftMono mul_le_mul_of_nonneg_left IdentDistrib.variance_eq IdentDistrib.truncation variance_le_expectation_sq MeasureTheory.AEStronglyMeasurable.truncation inv_nonneg_of_nonneg PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Even.pow_nonneg IsStrictOrderedRing.toIsOrderedRing AddGroup.existsAddOfLE even_two_mul sum_variance_truncation_le IndepFun.variance_sum MeasureTheory.AEStronglyMeasurable.memLp_truncation MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure IdentDistrib.aestronglyMeasurable_fst IndepFun.comp MeasureTheory.StronglyMeasurable.measurable Finset.sum_congr Finset.mul_sum Finset.sum_mul Finset.sum_sigma' Finset.sum_nbij' LT.lt.trans_le Sigma.eta eq_zero_or_pos Nat.instCanonicallyOrderedAdd Nat.cast_zero truncation_zero variance_zero MulZeroClass.mul_zero mul_le_mul_of_nonneg_right IsOrderedRing.toMulPosMono Finset.filter.congr_simp one_div sum_div_nat_floor_pow_sq_le_div_sq Nat.cast_pos Real.instNontrivial variance_nonneg div_eq_mul_inv mul_assoc mul_nonneg pow_nonneg inv_nonneg sub_nonneg covariant_swap_add_of_covariant_add ENNReal.instIsOrderedAddMonoid meas_ge_le_variance_div_sq MeasureTheory.memLp_finset_sum' IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal mul_pos Nat.instZeroLEOneClass Nat.le_floor Nat.cast_one one_le_pow₀ ENNReal.ofReal_sum_of_nonneg div_nonneg sq_nonneg ENNReal.ofReal_le_ofReal div_eq_inv_mul mul_inv mul_comm mul_pow inv_pow le_of_lt pow_pos IsStrictOrderedRing.toZeroLEOneClass inv_pos_of_pos LE.le.trans_lt le_of_tendsto_of_tendsto' OrderTopology.to_orderClosedTopology ENNReal.instOrderTopology Filter.atTop_neBot instIsDirectedOrder Nat.instIsStrictOrderedRing instArchimedeanNat ENNReal.tendsto_nat_tsum tendsto_const_nhds ENNReal.ofReal_lt_top Filter.mp_mem MeasureTheory.ae_eventually_notMem LT.lt.ne Filter.univ_mem' Finset.sum_apply
strong_law_aux2 📖	mathematical	MeasureTheory.Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing MeasureTheory.MeasureSpace.toMeasurableSpace MeasureTheory.MeasureSpace.volume Pairwise Function.onFun IndepFun Real.measurableSpace IdentDistrib Real.instLE Real.instZero Real.instLT Real.instOne	Filter.Eventually Asymptotics.IsLittleO Real.norm Filter.atTop Nat.instPreorder Real.instSub Finset.sum Real.instAddCommMonoid Finset.range Nat.floor Real.semiring Real.partialOrder FloorRing.toFloorSemiring Real.instRing Real.linearOrder Real.instIsStrictOrderedRing Real.instFloorRing Monoid.toNatPow Real.instMonoid truncation Real.instNatCast MeasureTheory.integral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Pi.addCommMonoid MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	Real.instIsStrictOrderedRing MeasureTheory.Measure.instOuterMeasureClass exists_seq_strictAnti_tendsto instOrderTopologyReal LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instNoMaxOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial TopologicalSpace.PseudoMetrizableSpace.firstCountableTopology PseudoEMetricSpace.pseudoMetrizableSpace strong_law_aux1 Filter.mp_mem MeasureTheory.ae_all_iff instCountableNat Filter.univ_mem' Asymptotics.isLittleO_iff Filter.Eventually.exists Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat tendsto_order Nat.abs_cast LE.le.trans LT.lt.le mul_le_mul_of_nonneg_right IsOrderedRing.toMulPosMono Nat.cast_nonneg
strong_law_aux3 📖	mathematical	MeasureTheory.Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing MeasureTheory.MeasureSpace.toMeasurableSpace MeasureTheory.MeasureSpace.volume IdentDistrib Real.measurableSpace	Asymptotics.IsLittleO Real.norm Filter.atTop Nat.instPreorder Real.instSub MeasureTheory.integral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Finset.sum Pi.addCommMonoid Real.instAddCommMonoid Finset.range truncation Real.instNatCast Real.instMul	—	IdentDistrib.integral_eq Real.borelSpace IdentDistrib.truncation Filter.Tendsto.comp tendsto_integral_truncation tendsto_natCast_atTop_atTop Real.instIsOrderedRing Real.instArchimedean Finset.sum_apply Finset.sum_sub_distrib Finset.sum_const Finset.card_range nsmul_eq_mul MeasureTheory.integral_finset_sum MeasureTheory.AEStronglyMeasurable.integrable_truncation MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure IdentDistrib.integrable_snd IdentDistrib.symm Asymptotics.isLittleO_sum_range_of_tendsto_zero tendsto_sub_nhds_zero_iff instIsTopologicalAddGroupReal
strong_law_aux4 📖	mathematical	MeasureTheory.Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing MeasureTheory.MeasureSpace.toMeasurableSpace MeasureTheory.MeasureSpace.volume Pairwise Function.onFun IndepFun Real.measurableSpace IdentDistrib Real.instLE Real.instZero Real.instLT Real.instOne	Filter.Eventually Asymptotics.IsLittleO Real.norm Filter.atTop Nat.instPreorder Real.instSub Finset.sum Real.instAddCommMonoid Finset.range Nat.floor Real.semiring Real.partialOrder FloorRing.toFloorSemiring Real.instRing Real.linearOrder Real.instIsStrictOrderedRing Real.instFloorRing Monoid.toNatPow Real.instMonoid truncation Real.instNatCast Real.instMul MeasureTheory.integral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	Filter.mp_mem MeasureTheory.Measure.instOuterMeasureClass Real.instIsStrictOrderedRing strong_law_aux2 Filter.univ_mem' Filter.Tendsto.comp tendsto_nat_floor_atTop tendsto_pow_atTop_atTop_of_one_lt AddGroup.existsAddOfLE Real.instArchimedean Finset.sum_apply sub_add_sub_cancel Asymptotics.IsLittleO.add Asymptotics.IsLittleO.comp_tendsto strong_law_aux3
strong_law_aux5 📖	mathematical	MeasureTheory.Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing MeasureTheory.MeasureSpace.toMeasurableSpace MeasureTheory.MeasureSpace.volume IdentDistrib Real.measurableSpace Real.instLE Real.instZero	Filter.Eventually Asymptotics.IsLittleO Real.norm Filter.atTop Nat.instPreorder Real.instSub Finset.sum Real.instAddCommMonoid Finset.range truncation Real.instNatCast MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	IdentDistrib.measure_mem_eq measurableSet_Ioi BorelSpace.opensMeasurable Real.borelSpace instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid tsum_prob_mem_Ioi_lt_top MeasureTheory.Measure.instOuterMeasureClass Filter.mp_mem MeasureTheory.ae_eventually_notMem LT.lt.ne Filter.univ_mem' Filter.Tendsto.congr' Filter.Ioi_mem_atTop instNoTopOrderOfNoMaxOrder Nat.instNoMaxOrder sub_self lt_of_lt_of_le IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedRing Real.instNontrivial tendsto_const_nhds Finset.sum_sub_distrib Asymptotics.isLittleO_sum_range_of_tendsto_zero
strong_law_aux6 📖	mathematical	MeasureTheory.Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing MeasureTheory.MeasureSpace.toMeasurableSpace MeasureTheory.MeasureSpace.volume Pairwise Function.onFun IndepFun Real.measurableSpace IdentDistrib Real.instLE Real.instZero Real.instLT Real.instOne	Filter.Eventually Filter.Tendsto DivInvMonoid.toDiv Real.instDivInvMonoid Finset.sum Real.instAddCommMonoid Finset.range Nat.floor Real.semiring Real.partialOrder FloorRing.toFloorSemiring Real.instRing Real.linearOrder Real.instIsStrictOrderedRing Real.instFloorRing Monoid.toNatPow Real.instMonoid Real.instNatCast Filter.atTop Nat.instPreorder nhds MeasureTheory.integral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	Real.instIsStrictOrderedRing LT.lt.trans_le zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid one_le_pow₀ IsOrderedRing.toPosMulMono Real.instIsOrderedRing LT.lt.le Filter.mp_mem MeasureTheory.Measure.instOuterMeasureClass strong_law_aux5 strong_law_aux4 Filter.univ_mem' tendsto_sub_nhds_zero_iff instIsTopologicalAddGroupReal Asymptotics.isLittleO_one_iff NormedDivisionRing.to_normOneClass Filter.Tendsto.comp tendsto_nat_floor_atTop tendsto_pow_atTop_atTop_of_one_lt AddGroup.existsAddOfLE Real.instArchimedean sub_sub_sub_cancel_left Asymptotics.IsLittleO.sub Asymptotics.IsLittleO.comp_tendsto Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.subst_sub Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ div_one Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval 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 Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg LT.lt.ne' Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_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.cons_ne_zero one_ne_zero NeZero.one GroupWithZero.toNontrivial Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.FieldSimp.NF.one_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Asymptotics.IsLittleO.mul_isBigO NormedDivisionRing.toNormMulClass Asymptotics.isBigO_refl
strong_law_aux7 📖	mathematical	MeasureTheory.Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing MeasureTheory.MeasureSpace.toMeasurableSpace MeasureTheory.MeasureSpace.volume Pairwise Function.onFun IndepFun Real.measurableSpace IdentDistrib Real.instLE Real.instZero	Filter.Eventually Filter.Tendsto DivInvMonoid.toDiv Real.instDivInvMonoid Finset.sum Real.instAddCommMonoid Finset.range Real.instNatCast Filter.atTop Nat.instPreorder nhds MeasureTheory.integral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	MeasureTheory.Measure.instOuterMeasureClass exists_seq_strictAnti_tendsto instOrderTopologyReal LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing instNoMaxOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial TopologicalSpace.PseudoMetrizableSpace.firstCountableTopology PseudoEMetricSpace.pseudoMetrizableSpace strong_law_aux6 Filter.mp_mem MeasureTheory.ae_all_iff instCountableNat Filter.univ_mem' tendsto_div_of_monotone_of_tendsto_div_floor_pow Finset.sum_le_sum_of_subset_of_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Finset.range_mono
sum_prob_mem_Ioc_le 📖	mathematical	MeasureTheory.Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing MeasureTheory.MeasureSpace.toMeasurableSpace MeasureTheory.MeasureSpace.volume Pi.hasLe Real.instLE Pi.instZero Real.instZero	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder Finset.sum ENNReal.instAddCommMonoid Finset.range DFunLike.coe MeasureTheory.Measure Set MeasureTheory.Measure.instFunLike setOf Set.instMembership Set.Ioc Real.instPreorder Real.instNatCast ENNReal.ofReal Real.instAdd MeasureTheory.integral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Real.instOne	—	Finset.sum_congr intervalIntegral.sum_integral_adjacent_intervals_Ico LE.le.trans LT.lt.le Finset.mem_range Continuous.intervalIntegrable MeasureTheory.isLocallyFiniteMeasure_of_isFiniteMeasureOnCompacts instWeaklyLocallyCompactSpaceOfLocallyCompactSpace locallyCompact_of_proper instProperSpaceReal MeasureTheory.Measure.Regular.toIsFiniteMeasureOnCompacts MeasureTheory.Measure.InnerRegularCompactLTTop.instRegularOfBorelSpaceOfR1SpaceOfIsFiniteMeasure Real.borelSpace instR1Space TopologicalSpace.PseudoMetrizableSpace.regularSpace PseudoEMetricSpace.pseudoMetrizableSpace MeasureTheory.Measure.InnerRegular.instInnerRegularCompactLTTop MeasureTheory.Measure.instInnerRegularOfPseudoMetrizableSpaceOfSigmaCompactSpaceOfBorelSpaceOfSigmaFinite SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace instIsTopologicalAddGroupReal TopologicalSpace.SecondCountableTopology.to_separableSpace instSecondCountableTopologyReal MeasureTheory.IsFiniteMeasure.toSigmaFinite MeasureTheory.Measure.isFiniteMeasure_map MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure continuous_const Finset.sum_sigma' Finset.sum_nbij' Nat.instNoMaxOrder Sigma.eta Nat.cast_add Nat.cast_one Finset.sum_le_sum IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Finset.sum_const Finset.card_range nsmul_eq_mul Nat.cast_min Real.instIsStrictOrderedRing mul_le_mul_of_nonneg_right IsOrderedRing.toMulPosMono Real.instIsOrderedRing min_le_left intervalIntegral.integral_nonneg IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le Real.instZeroLEOneClass intervalIntegral.integral_of_le MeasureTheory.setIntegral_mono_on IsStrictOrderedModule.toIsOrderedModule IsStrictOrderedRing.toIsStrictOrderedModule instClosedIciTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Continuous.integrableOn_Ioc BorelSpace.opensMeasurable MeasureTheory.Measure.Regular.of_sigmaCompactSpace_of_isLocallyFiniteMeasure MeasureTheory.IsFiniteMeasure.toIsLocallyFiniteMeasure ConditionallyCompleteLinearOrder.toCompactIccSpace instOrderTopologyReal TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace Continuous.add IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal continuous_id measurableSet_Ioc instClosedIicTopology mul_one covariant_swap_add_of_covariant_add IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT AddRightCancelSemigroup.toIsRightCancelAdd contravariant_swap_add_of_contravariant_add intervalIntegral.sum_integral_adjacent_intervals Nat.cast_zero intervalIntegral.integral_add integral_truncation_eq_intervalIntegral_of_nonneg le_imp_le_of_le_of_le add_le_add_left integral_truncation_le_integral_of_nonneg le_refl add_le_add_right Nat.cast_nonneg MeasureTheory.integral_const Real.instCompleteSpace MeasureTheory.measureReal_restrict_apply' Set.univ_inter ENNReal.toReal_one ENNReal.toReal_mono ENNReal.one_ne_top MeasureTheory.prob_le_one MeasureTheory.instIsZeroOrProbabilityMeasureMap MeasureTheory.ofReal_setIntegral_one MeasureTheory.Measure.map_apply_of_aemeasurable MeasureTheory.Integrable.aemeasurable MeasureTheory.measureReal_restrict_apply MeasureTheory.ofReal_measureReal ENNReal.ofReal_sum_of_nonneg Nat.cast_le RCLike.charZero_rclike ENNReal.ofReal_le_ofReal
sum_variance_truncation_le 📖	mathematical	MeasureTheory.Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing MeasureTheory.MeasureSpace.toMeasurableSpace MeasureTheory.MeasureSpace.volume Pi.hasLe Real.instLE Pi.instZero Real.instZero	Finset.sum Real.instAddCommMonoid Finset.range Real.instMul Real.instInv Monoid.toNatPow Real.instMonoid Real.instNatCast MeasureTheory.integral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Pi.monoid truncation instOfNatAtLeastTwo Nat.instAtLeastTwoHAddOfNat	—	moment_truncation_eq_intervalIntegral_of_nonneg two_ne_zero Nat.instAtLeastTwoHAddOfNat Finset.sum_congr intervalIntegral.sum_integral_adjacent_intervals Continuous.intervalIntegrable MeasureTheory.isLocallyFiniteMeasure_of_isFiniteMeasureOnCompacts instWeaklyLocallyCompactSpaceOfLocallyCompactSpace locallyCompact_of_proper instProperSpaceReal MeasureTheory.Measure.Regular.toIsFiniteMeasureOnCompacts MeasureTheory.Measure.InnerRegularCompactLTTop.instRegularOfBorelSpaceOfR1SpaceOfIsFiniteMeasure Real.borelSpace instR1Space TopologicalSpace.PseudoMetrizableSpace.regularSpace PseudoEMetricSpace.pseudoMetrizableSpace MeasureTheory.Measure.InnerRegular.instInnerRegularCompactLTTop MeasureTheory.Measure.instInnerRegularOfPseudoMetrizableSpaceOfSigmaCompactSpaceOfBorelSpaceOfSigmaFinite SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace instIsTopologicalAddGroupReal TopologicalSpace.SecondCountableTopology.to_separableSpace instSecondCountableTopologyReal MeasureTheory.IsFiniteMeasure.toSigmaFinite MeasureTheory.Measure.isFiniteMeasure_map MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure Continuous.pow IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal continuous_id Nat.cast_zero Finset.mul_sum Finset.sum_mul Finset.sum_sigma' Finset.sum_nbij' lt_trans Sigma.eta Nat.cast_add Nat.cast_one Finset.sum_le_sum IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid mul_le_mul_of_nonneg_right IsOrderedRing.toMulPosMono Real.instIsOrderedRing sum_Ioo_inv_sq_le Real.instIsStrictOrderedRing intervalIntegral.integral_nonneg_of_forall IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le Real.instZeroLEOneClass sq_nonneg AddGroup.existsAddOfLE IsOrderedRing.toPosMulMono intervalIntegral.integral_const_mul intervalIntegral.integral_of_le MeasureTheory.setIntegral_mono_on IsStrictOrderedModule.toIsOrderedModule IsStrictOrderedRing.toIsStrictOrderedModule instClosedIciTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Continuous.integrableOn_Ioc BorelSpace.opensMeasurable MeasureTheory.Measure.Regular.of_sigmaCompactSpace_of_isLocallyFiniteMeasure MeasureTheory.IsFiniteMeasure.toIsLocallyFiniteMeasure ConditionallyCompleteLinearOrder.toCompactIccSpace instOrderTopologyReal TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace Continuous.comp' Continuous.fun_mul continuous_const continuous_id' measurableSet_Ioc instClosedIicTopology Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.atom_pf' Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw LE.le.trans_lt Nat.cast_nonneg div_le_one PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Right.add_pos_of_nonneg_of_pos covariant_swap_add_of_covariant_add Nat.cast_nonneg' Mathlib.Meta.Positivity.pos_of_isNat Real.instNontrivial le_of_lt mul_pos one_mul Continuous.mul mul_le_mul_of_nonneg_left integral_truncation_eq_intervalIntegral_of_nonneg integral_truncation_le_integral_of_nonneg zero_le_two
tendsto_integral_truncation 📖	mathematical	MeasureTheory.Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing	Filter.Tendsto MeasureTheory.integral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal truncation Filter.atTop Real.instPreorder nhds	—	MeasureTheory.tendsto_integral_filter_of_dominated_convergence instIsCountablyGenerated_atTop instOrderTopologyReal TopologicalSpace.SecondCountableTopology.to_separableSpace instSecondCountableTopologyReal Filter.Eventually.of_forall MeasureTheory.AEStronglyMeasurable.truncation MeasureTheory.Integrable.aestronglyMeasurable Filter.univ_mem' MeasureTheory.Measure.instOuterMeasureClass Real.norm_eq_abs abs_truncation_le_abs_self MeasureTheory.Integrable.abs instHasSolidNormReal Real.instIsOrderedAddMonoid Filter.Tendsto.congr' Filter.mp_mem Filter.Ioi_mem_atTop instNoTopOrderOfNoMaxOrder instNoMaxOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial truncation_eq_self tendsto_const_nhds
truncation_eq_of_nonneg 📖	mathematical	Real Real.instLE Real.instZero	truncation Set.indicator Set.Ioc Real.instPreorder	—	LE.le.lt_or_eq lt_of_not_ge Mathlib.Tactic.Linarith.lt_irrefl Nat.instAtLeastTwoHAddOfNat Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.neg_congr Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Real.instIsStrictOrderedRing Mathlib.Tactic.Linarith.mul_neg Mathlib.Tactic.Linarith.sub_neg_of_lt Real.instIsOrderedRing Mathlib.Meta.NormNum.isNat_lt_true RCLike.charZero_rclike Mathlib.Tactic.Linarith.sub_nonpos_of_le
truncation_eq_self 📖	mathematical	Real Real.instLT abs Real.lattice Real.instAddGroup	truncation	—	abs_lt IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add LT.lt.le
truncation_nonneg 📖	mathematical	Real Real.instLE Real.instZero	truncation	—	Set.indicator_apply_nonneg
truncation_zero 📖	mathematical	—	truncation Real Real.instZero Pi.instZero	—	neg_zero Set.Ioc_eq_empty Set.indicator_empty
tsum_prob_mem_Ioi_lt_top 📖	mathematical	MeasureTheory.Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing MeasureTheory.MeasureSpace.toMeasurableSpace MeasureTheory.MeasureSpace.volume Pi.hasLe Real.instLE Pi.instZero Real.instZero	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder tsum ENNReal.instAddCommMonoid ENNReal.instTopologicalSpace DFunLike.coe MeasureTheory.Measure Set MeasureTheory.Measure.instFunLike setOf Set.instMembership Set.Ioi Real.instPreorder Real.instNatCast SummationFilter.unconditional Top.top instTopENNReal	—	tendsto_finset_sum ENNReal.instContinuousAdd Set.Subset.antisymm exists_nat_ge Real.instIsOrderedRing Real.instArchimedean Set.mem_iUnion MeasureTheory.tendsto_measure_iUnion_atTop instIsCountablyGenerated_atTop OrderTopology.of_linearLocallyFinite instDiscreteTopologyNat TopologicalSpace.SecondCountableTopology.to_separableSpace TopologicalSpace.instSecondCountableTopologyOfLindelofSpaceOfPseudoMetrizableSpace Countable.LindelofSpace instCountableNat PseudoEMetricSpace.pseudoMetrizableSpace LE.le.trans Nat.cast_le IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass RCLike.charZero_rclike le_of_tendsto_of_tendsto OrderTopology.to_orderClosedTopology ENNReal.instOrderTopology Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat tendsto_const_nhds Filter.mp_mem Filter.Ici_mem_atTop Filter.univ_mem' sum_prob_mem_Ioc_le LE.le.trans_lt ENNReal.tendsto_nat_tsum Filter.Eventually.of_forall ENNReal.ofReal_lt_top

ProbabilityTheory.IdentDistrib

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
truncation 📖	mathematical	ProbabilityTheory.IdentDistrib Real Real.measurableSpace	ProbabilityTheory.truncation	—	comp Measurable.indicator measurable_id measurableSet_Ioc BorelSpace.opensMeasurable Real.borelSpace instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid

---

← Back to Index