BorelCantelli

📁 Source: Mathlib/Probability/BorelCantelli.lean

Statistics

Metric	Count
Definitions	0
Theorems condExp_natural_ae_eq_of_lt, indep_comap_natural_of_lt, condExp_indicator_filtrationOfSet_ae_eq, measure_limsup_eq_one	4
Total	4

ProbabilityTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
measure_limsup_eq_one 📖	mathematical	MeasurableSet iIndepSet tsum ENNReal ENNReal.instAddCommMonoid ENNReal.instTopologicalSpace DFunLike.coe MeasureTheory.Measure Set MeasureTheory.Measure.instFunLike SummationFilter.unconditional Top.top instTopENNReal	Filter.limsup CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Filter.atTop Nat.instPreorder AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	iIndepSet.isProbabilityMeasure Real.instCompleteSpace MeasureTheory.measure_congr MeasureTheory.Measure.instOuterMeasureClass Filter.eventuallyEq_set MeasureTheory.ae_mem_limsup_atTop_iff MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure MeasureTheory.measurableSet_filtrationOfSet' MeasureTheory.ae_all_iff instCountableNat iIndepSet.condExp_indicator_filtrationOfSet_ae_eq Filter.mp_mem Filter.univ_mem' Finset.sum_congr ENNReal.tsum_add_one_eq_top MeasureTheory.measure_ne_top ENNReal.tendsto_nat_tsum Filter.tendsto_atTop_atTop_of_monotone' monotone_nat_of_le_succ sub_nonneg covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Finset.sum_range_succ_sub_sum ENNReal.toReal_nonneg Filter.not_eventually Filter.Frequently.of_forall Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat not_lt ENNReal.ofNNReal_toNNReal ENNReal.le_ofReal_iff_toReal_le le_trans mem_upperBounds ENNReal.toReal_sum ENNReal.tendsto_nhds_top_iff_nnreal MeasureTheory.IsProbabilityMeasure.measure_univ

ProbabilityTheory.iIndepFun

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
condExp_natural_ae_eq_of_lt 📖	mathematical	MeasureTheory.StronglyMeasurable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ProbabilityTheory.iIndepFun Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.condExp MeasureTheory.Filtration.seq MeasureTheory.Filtration.natural EMetricSpace.metrizableSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace MeasureTheory.integral	—	isProbabilityMeasure MeasureTheory.condExp_indep_eq EMetricSpace.metrizableSpace Measurable.comap_le MeasureTheory.StronglyMeasurable.measurable PseudoEMetricSpace.pseudoMetrizableSpace MeasureTheory.Filtration.le MeasureTheory.sigmaFinite_of_sigmaFiniteFiltration MeasureTheory.IsFiniteMeasure.sigmaFiniteFiltration MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure Measurable.stronglyMeasurable BorelSpace.opensMeasurable comap_measurable indep_comap_natural_of_lt
indep_comap_natural_of_lt 📖	mathematical	MeasureTheory.StronglyMeasurable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ProbabilityTheory.iIndepFun Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	ProbabilityTheory.Indep MeasurableSpace.comap MeasureTheory.Filtration.seq MeasureTheory.Filtration.natural EMetricSpace.metrizableSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace	—	ProbabilityTheory.indep_iSup_of_disjoint Measurable.comap_le MeasureTheory.StronglyMeasurable.measurable PseudoEMetricSpace.pseudoMetrizableSpace iSup_singleton

ProbabilityTheory.iIndepSet

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
condExp_indicator_filtrationOfSet_ae_eq 📖	mathematical	MeasurableSet ProbabilityTheory.iIndepSet Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Filter.EventuallyEq Real MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.condExp MeasureTheory.Filtration.seq MeasureTheory.filtrationOfSet Real.normedAddCommGroup Real.instCompleteSpace InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Set.indicator Real.instZero Real.instOne MeasureTheory.Measure.real	—	MeasureTheory.Measure.instOuterMeasureClass Real.instCompleteSpace EMetricSpace.metrizableSpace Real.borelSpace MeasureTheory.StronglyMeasurable.indicator MeasureTheory.stronglyMeasurable_one MeasureTheory.Filtration.filtrationOfSet_eq_natural Real.instNontrivial Filter.EventuallyEq.trans ProbabilityTheory.iIndepFun.condExp_natural_ae_eq_of_lt instSecondCountableTopologyReal iIndepFun_indicator MeasureTheory.integral_indicator_const mul_one Filter.EventuallyEq.refl

---

← Back to Index