Proper

📁 Source: Mathlib/Probability/Kernel/Proper.lean

Statistics

Metric	Count
Definitions IsProper	1
Theorems inter_eq_indicator_mul, lintegral_mul, of_inter_eq_indicator_mul, of_restrict_eq_indicator_smul, restrict_eq_indicator_smul, restrict_eq_indicator_smul', setLIntegral_eq_comp, setLIntegral_eq_indicator_mul_lintegral, setLIntegral_inter_eq_indicator_mul_setLIntegral, isProper_iff_inter_eq_indicator_mul, isProper_iff_restrict_eq_indicator_smul	11
Total	12

ProbabilityTheory.Kernel

Definitions

Name	Category	Theorems
IsProper 📖	CompData	4 math math: IsProper.of_restrict_eq_indicator_smul, isProper_iff_restrict_eq_indicator_smul, IsProper.of_inter_eq_indicator_mul, isProper_iff_inter_eq_indicator_mul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isProper_iff_inter_eq_indicator_mul 📖	mathematical	MeasurableSpace MeasurableSpace.instLE	IsProper DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike ProbabilityTheory.Kernel instFunLike Set.instInter Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring Set.indicator instZeroENNReal Pi.instOne AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	IsScalarTower.right isProper_iff_restrict_eq_indicator_smul restrict_apply MeasureTheory.Measure.restrict_apply
isProper_iff_restrict_eq_indicator_smul 📖	mathematical	MeasurableSpace MeasurableSpace.instLE	IsProper DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike restrict ENNReal MeasureTheory.Measure.instSMul Algebra.toSMul ENNReal.instCommSemiring CommSemiring.toSemiring Algebra.id IsScalarTower.right Set.indicator instZeroENNReal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	IsScalarTower.right inf_le_right inf_eq_left

ProbabilityTheory.Kernel.IsProper

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inter_eq_indicator_mul 📖	mathematical	MeasurableSpace MeasurableSpace.instLE ProbabilityTheory.Kernel.IsProper MeasurableSet	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike ProbabilityTheory.Kernel ProbabilityTheory.Kernel.instFunLike Set.instInter Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring Set.indicator instZeroENNReal Pi.instOne AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	ProbabilityTheory.Kernel.isProper_iff_inter_eq_indicator_mul
lintegral_mul 📖	mathematical	ProbabilityTheory.Kernel.IsProper MeasurableSpace MeasurableSpace.instLE Measurable ENNReal ENNReal.measurableSpace	MeasureTheory.lintegral DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure ProbabilityTheory.Kernel.instFunLike Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring	—	Measurable.ennreal_induction smul_mul_assoc IsScalarTower.right MeasureTheory.lintegral_const_mul Measurable.mul ENNReal.instMeasurableMul₂ Measurable.indicator measurable_one add_mul Distrib.rightDistribClass MeasureTheory.lintegral_add_right Measurable.mono le_rfl ENNReal.iSup_mul MeasureTheory.lintegral_iSup Monotone.mul_const IsOrderedRing.toMulPosMono Pi.isOrderedRing ENNReal.instIsOrderedRing zero_le Pi.instCanonicallyOrderedAddForall ENNReal.instCanonicallyOrderedAdd
of_inter_eq_indicator_mul 📖	mathematical	MeasurableSpace MeasurableSpace.instLE DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike ProbabilityTheory.Kernel ProbabilityTheory.Kernel.instFunLike Set.instInter Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring Set.indicator instZeroENNReal Pi.instOne AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	ProbabilityTheory.Kernel.IsProper	—	ProbabilityTheory.Kernel.isProper_iff_inter_eq_indicator_mul
of_restrict_eq_indicator_smul 📖	mathematical	MeasurableSpace MeasurableSpace.instLE DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure ProbabilityTheory.Kernel.instFunLike ProbabilityTheory.Kernel.restrict ENNReal MeasureTheory.Measure.instSMul Algebra.toSMul ENNReal.instCommSemiring CommSemiring.toSemiring Algebra.id IsScalarTower.right Set.indicator instZeroENNReal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	ProbabilityTheory.Kernel.IsProper	—	IsScalarTower.right ProbabilityTheory.Kernel.isProper_iff_restrict_eq_indicator_smul
restrict_eq_indicator_smul 📖	mathematical	MeasurableSpace MeasurableSpace.instLE ProbabilityTheory.Kernel.IsProper MeasurableSet	DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure ProbabilityTheory.Kernel.instFunLike ProbabilityTheory.Kernel.restrict ENNReal MeasureTheory.Measure.instSMul Algebra.toSMul ENNReal.instCommSemiring CommSemiring.toSemiring Algebra.id IsScalarTower.right Set.indicator instZeroENNReal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	IsScalarTower.right ProbabilityTheory.Kernel.isProper_iff_restrict_eq_indicator_smul
restrict_eq_indicator_smul' 📖	mathematical	ProbabilityTheory.Kernel.IsProper MeasurableSet MeasurableSpace SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice MeasurableSpace.instCompleteLattice	DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure ProbabilityTheory.Kernel.instFunLike ProbabilityTheory.Kernel.restrict inf_le_right ENNReal MeasureTheory.Measure.instSMul Algebra.toSMul ENNReal.instCommSemiring CommSemiring.toSemiring Algebra.id IsScalarTower.right Set.indicator instZeroENNReal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	—
setLIntegral_eq_comp 📖	mathematical	ProbabilityTheory.Kernel.IsProper MeasurableSpace MeasurableSpace.instLE MeasurableSet	MeasureTheory.lintegral MeasureTheory.Measure.restrict DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike ProbabilityTheory.Kernel ProbabilityTheory.Kernel.instFunLike MeasureTheory.Measure.bind Set.instInter	—	MeasureTheory.Measure.bind_apply MeasurableSet.inter Measurable.aemeasurable Measurable.mono ProbabilityTheory.Kernel.measurable le_rfl inter_eq_indicator_mul one_mul MeasureTheory.lintegral_indicator
setLIntegral_eq_indicator_mul_lintegral 📖	mathematical	ProbabilityTheory.Kernel.IsProper MeasurableSpace MeasurableSpace.instLE Measurable ENNReal ENNReal.measurableSpace MeasurableSet	MeasureTheory.lintegral MeasureTheory.Measure.restrict DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure ProbabilityTheory.Kernel.instFunLike Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring Set.indicator instZeroENNReal Pi.instOne AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	one_mul MeasureTheory.lintegral_indicator
setLIntegral_inter_eq_indicator_mul_setLIntegral 📖	mathematical	ProbabilityTheory.Kernel.IsProper MeasurableSpace MeasurableSpace.instLE Measurable ENNReal ENNReal.measurableSpace MeasurableSet	MeasureTheory.lintegral MeasureTheory.Measure.restrict DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure ProbabilityTheory.Kernel.instFunLike Set Set.instInter Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring Set.indicator instZeroENNReal Pi.instOne AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	MeasureTheory.lintegral_indicator setLIntegral_eq_indicator_mul_lintegral Measurable.indicator MeasureTheory.setLIntegral_indicator

---

← Back to Index