WithDensityFinite

📁 Source: Mathlib/MeasureTheory/Measure/WithDensityFinite.lean

Statistics

Metric	Count
Definitions toFinite, toFiniteAux	2
Theorems absolutelyContinuous_toFinite, ae_toFinite, ae_toFiniteAux, instIsFiniteMeasureToFinite, instIsProbabilityMeasureToFiniteOfNeZeroMeasure, isFiniteMeasure_toFiniteAux, restrict_compl_sigmaFiniteSet, sfiniteSeq_absolutelyContinuous_toFinite, toFinite_absolutelyContinuous, toFinite_apply_eq_zero_iff, toFinite_eq_self, toFinite_eq_zero_iff, toFinite_zero	13
Total	15

MeasureTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
absolutelyContinuous_toFinite 📖	mathematical	—	Measure.AbsolutelyContinuous Measure.toFinite	—	Measure.instOuterMeasureClass Measure.ae_le_iff_absolutelyContinuous Eq.ge ae_toFinite
ae_toFinite 📖	mathematical	—	ae Measure Measure.instFunLike Measure.instOuterMeasureClass Measure.toFinite	—	Measure.instOuterMeasureClass ae.congr_simp Measure.restrict_univ Measure.ae_ennreal_smul_measure_eq isFiniteMeasure_toFiniteAux ae_toFiniteAux
ae_toFiniteAux 📖	mathematical	—	ae Measure Measure.instFunLike Measure.instOuterMeasureClass Measure.toFiniteAux	—	Measure.instOuterMeasureClass exists_isFiniteMeasure_absolutelyContinuous Measure.toFiniteAux.eq_1 ae.congr_simp LE.le.antisymm Measure.AbsolutelyContinuous.ae_le
instIsFiniteMeasureToFinite 📖	mathematical	—	IsFiniteMeasure Measure.toFinite	—	Measure.toFinite.eq_1 IsZeroOrProbabilityMeasure.toIsFiniteMeasure ProbabilityTheory.instIsZeroOrProbabilityMeasureCond
instIsProbabilityMeasureToFiniteOfNeZeroMeasure 📖	mathematical	—	IsProbabilityMeasure Measure.toFinite	—	ProbabilityTheory.cond_isProbabilityMeasure isFiniteMeasure_toFiniteAux Measure.instOuterMeasureClass ae_toFiniteAux Set.compl_univ Measure.ae.neBot
isFiniteMeasure_toFiniteAux 📖	mathematical	—	IsFiniteMeasure Measure.toFiniteAux	—	exists_isFiniteMeasure_absolutelyContinuous Measure.toFiniteAux.eq_1
restrict_compl_sigmaFiniteSet 📖	mathematical	—	Measure.restrict Compl.compl Set Set.instCompl Measure.sigmaFiniteSet ENNReal Measure Measure.instSMul Algebra.toSMul ENNReal.instCommSemiring CommSemiring.toSemiring Algebra.id IsScalarTower.right Top.top instTopENNReal Measure.toFinite	—	IsScalarTower.right Measure.sigmaFiniteSet.eq_1 restrict_compl_sigmaFiniteSetWRT Measure.AbsolutelyContinuous.refl Measure.ext Measure.restrict_apply toFinite_absolutelyContinuous ENNReal.top_mul absolutelyContinuous_toFinite
sfiniteSeq_absolutelyContinuous_toFinite 📖	mathematical	—	Measure.AbsolutelyContinuous sfiniteSeq Measure.toFinite	—	Measure.AbsolutelyContinuous.trans LE.le.absolutelyContinuous sfiniteSeq_le absolutelyContinuous_toFinite
toFinite_absolutelyContinuous 📖	mathematical	—	Measure.AbsolutelyContinuous Measure.toFinite	—	Measure.instOuterMeasureClass Measure.ae_le_iff_absolutelyContinuous Eq.le ae_toFinite
toFinite_apply_eq_zero_iff 📖	mathematical	—	DFunLike.coe Measure Set ENNReal Measure.instFunLike Measure.toFinite instZeroENNReal	—	Measure.instOuterMeasureClass ae_toFinite
toFinite_eq_self 📖	mathematical	—	Measure.toFinite instSFiniteOfSigmaFinite IsFiniteMeasure.toSigmaFinite IsZeroOrProbabilityMeasure.toIsFiniteMeasure instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure	—	instSFiniteOfSigmaFinite IsFiniteMeasure.toSigmaFinite IsZeroOrProbabilityMeasure.toIsFiniteMeasure instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure Measure.toFinite.eq_1 exists_isFiniteMeasure_absolutelyContinuous Measure.toFiniteAux.eq_1 ProbabilityTheory.cond_univ
toFinite_eq_zero_iff 📖	mathematical	—	Measure.toFinite Measure Measure.instZero	—	—
toFinite_zero 📖	mathematical	—	Measure.toFinite Measure Measure.instZero instSFiniteOfNatMeasure	—	instSFiniteOfNatMeasure

MeasureTheory.Measure

Definitions

Name	Category	Theorems
toFinite 📖	CompOp	11 math math: MeasureTheory.absolutelyContinuous_toFinite, MeasureTheory.restrict_compl_sigmaFiniteSet, MeasureTheory.ae_toFinite, MeasureTheory.toFinite_eq_self, MeasureTheory.toFinite_absolutelyContinuous, MeasureTheory.toFinite_eq_zero_iff, MeasureTheory.instIsProbabilityMeasureToFiniteOfNeZeroMeasure, MeasureTheory.toFinite_apply_eq_zero_iff, MeasureTheory.instIsFiniteMeasureToFinite, MeasureTheory.sfiniteSeq_absolutelyContinuous_toFinite, MeasureTheory.toFinite_zero
toFiniteAux 📖	CompOp	2 math math: MeasureTheory.isFiniteMeasure_toFiniteAux, MeasureTheory.ae_toFiniteAux

---

← Back to Index