Documentation Verification Report

Uniform

📁 Source: Mathlib/Probability/Distributions/Uniform.lean

Statistics

Metric	Count
Definitions `IsUniform`, `uniformPDF`, `ofMultiset`, `uniformOfFinset`, `uniformOfFintype`	5
Theorems `absolutelyContinuous`, `aemeasurable`, `cond`, `hasPDF`, `integral_eq`, `isProbabilityMeasure`, `measure_preimage`, `mul_pdf_integrable`, `pdf_eq`, `pdf_eq_zero_of_measure_eq_zero_or_top`, `pdf_toReal_ae_eq`, `toMeasurable`, `toMeasurable_iff`, `uniformPDF_eq_pdf`, `uniformPDF_ite`, `mem_support_ofMultiset_iff`, `mem_support_uniformOfFinset_iff`, `mem_support_uniformOfFintype`, `ofMultiset_apply`, `ofMultiset_apply_of_notMem`, `support_ofMultiset`, `support_uniformOfFinset`, `support_uniformOfFintype`, `toMeasure_ofMultiset_apply`, `toMeasure_uniformOfFinset_apply`, `toMeasure_uniformOfFintype_apply`, `toOuterMeasure_ofMultiset_apply`, `toOuterMeasure_uniformOfFinset_apply`, `toOuterMeasure_uniformOfFintype_apply`, `uniformOfFinset_apply`, `uniformOfFinset_apply_of_mem`, `uniformOfFinset_apply_of_notMem`, `uniformOfFintype_apply`	33
Total	38

MeasureTheory.pdf

Definitions

Name	Category	Theorems
`IsUniform` 📖	MathDef	2 math math: `IsUniform.toMeasurable_iff`, `IsUniform.cond`
`uniformPDF` 📖	CompOp	2 math math: `uniformPDF_ite`, `uniformPDF_eq_pdf`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`uniformPDF_eq_pdf` 📖	mathematical	`MeasurableSet` `IsUniform`	`Filter.EventuallyEq` `ENNReal` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `uniformPDF` `MeasureTheory.pdf`	—	`MeasureTheory.Measure.instOuterMeasureClass` `Filter.EventuallyEq.trans` `Filter.EventuallyEq.symm` `IsUniform.pdf_eq` `MeasureTheory.ae_eq_refl`
`uniformPDF_ite` 📖	mathematical	—	`uniformPDF` `ENNReal` `Set` `Set.instMembership` `ENNReal.instInv` `DFunLike.coe` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `instZeroENNReal`	—	`mul_one`

MeasureTheory.pdf.IsUniform

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`absolutelyContinuous` 📖	mathematical	`MeasureTheory.pdf.IsUniform`	`MeasureTheory.Measure.AbsolutelyContinuous` `MeasureTheory.Measure.map`	—	`ProbabilityTheory.cond_absolutelyContinuous`
`aemeasurable` 📖	mathematical	`MeasureTheory.pdf.IsUniform`	`AEMeasurable`	—	`zero_ne_one'` `NeZero.charZero_one` `ENNReal.instCharZero` `MeasureTheory.Measure.map_of_not_aemeasurable` `MeasureTheory.Measure.smul_apply` `MeasureTheory.Measure.restrict_apply` `MeasurableSet.univ` `Set.univ_inter` `smul_eq_mul` `ENNReal.inv_mul_cancel`
`cond` 📖	mathematical	—	`MeasureTheory.pdf.IsUniform` `ProbabilityTheory.cond`	—	`MeasureTheory.Measure.map_id`
`hasPDF` 📖	mathematical	`MeasureTheory.pdf.IsUniform`	`MeasureTheory.HasPDF`	—	`MeasureTheory.hasPDF_of_map_eq_withDensity` `aemeasurable` `AEMeasurable.indicator` `AEMeasurable.const_smul` `MeasurableSMul.toMeasurableConstSMul` `measurableSMul_of_mul` `MeasurableMul₂.toMeasurableMul` `ENNReal.instMeasurableMul₂` `Measurable.aemeasurable` `measurable_one` `MeasureTheory.measurableSet_toMeasurable` `MeasureTheory.withDensity_indicator` `IsScalarTower.right` `MeasureTheory.withDensity_smul` `MeasureTheory.withDensity_one` `MeasureTheory.Measure.restrict_toMeasurable` `MeasureTheory.measure_toMeasurable` `ProbabilityTheory.cond.eq_1`
`integral_eq` 📖	mathematical	`MeasureTheory.pdf.IsUniform` `Real` `Real.measurableSpace` `MeasureTheory.MeasureSpace.volume` `Real.measureSpace`	`MeasureTheory.integral` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `Real.instMul` `ENNReal.toReal` `ENNReal` `ENNReal.instInv` `DFunLike.coe` `MeasureTheory.Measure` `MeasureTheory.MeasureSpace.toMeasurableSpace` `Set` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.restrict`	—	`smul_eq_mul` `IsScalarTower.right` `MeasureTheory.integral_smul_measure` `MeasureTheory.integral_map` `aestronglyMeasurable_id` `PseudoEMetricSpace.pseudoMetrizableSpace` `BorelSpace.opensMeasurable` `Real.borelSpace` `instSecondCountableTopologyReal` `MeasureTheory.Measure.map_of_not_aemeasurable` `MeasureTheory.integral_zero_measure` `MeasureTheory.integral_non_aestronglyMeasurable` `aestronglyMeasurable_iff_aemeasurable`
`isProbabilityMeasure` 📖	mathematical	`MeasureTheory.pdf.IsUniform`	`MeasureTheory.IsProbabilityMeasure`	—	`Set.preimage_univ` `measure_preimage` `MeasurableSet.univ` `Set.inter_univ` `ENNReal.div_self`
`measure_preimage` 📖	mathematical	`MeasureTheory.pdf.IsUniform` `MeasurableSet`	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `Set.preimage` `DivInvMonoid.toDiv` `ENNReal.instDivInvMonoid` `Set.instInter`	—	`MeasureTheory.Measure.map_apply_of_aemeasurable` `aemeasurable` `ProbabilityTheory.cond_apply'` `ENNReal.div_eq_inv_mul`
`mul_pdf_integrable` 📖	mathematical	`IsCompact` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `MeasureTheory.pdf.IsUniform` `Real.measurableSpace` `MeasureTheory.MeasureSpace.volume` `Real.measureSpace`	`MeasureTheory.Integrable` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `MeasureTheory.MeasureSpace.toMeasurableSpace` `Real.instMul` `ENNReal.toReal` `MeasureTheory.pdf`	—	`MulZeroClass.mul_zero` `MeasureTheory.Integrable.congr` `Filter.mp_mem` `MeasureTheory.Measure.instOuterMeasureClass` `pdf_eq_zero_of_measure_eq_zero_or_top` `Filter.univ_mem'` `isProbabilityMeasure` `MeasureTheory.AEStronglyMeasurable.mul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `aestronglyMeasurable_id` `PseudoEMetricSpace.pseudoMetrizableSpace` `BorelSpace.opensMeasurable` `Real.borelSpace` `instSecondCountableTopologyReal` `AEMeasurable.aestronglyMeasurable` `AEMeasurable.ennreal_toReal` `Measurable.aemeasurable` `MeasureTheory.measurable_pdf` `MeasureTheory.pdf.hasFiniteIntegral_mul` `MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure` `MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure` `pdf_eq` `IsCompact.measurableSet` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `Set.indicator_mul_right` `mul_one` `MeasureTheory.lintegral_indicator` `MeasureTheory.lintegral_mul_const` `measurable_enorm` `ENNReal.mul_ne_top` `LT.lt.ne` `MeasureTheory.setLIntegral_lt_top_of_isCompact` `continuous_nnnorm` `ENNReal.inv_lt_top` `pos_iff_ne_zero` `ENNReal.instCanonicallyOrderedAdd`
`pdf_eq` 📖	mathematical	`MeasurableSet` `MeasureTheory.pdf.IsUniform`	`Filter.EventuallyEq` `ENNReal` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.pdf` `Set.indicator` `instZeroENNReal` `Function.hasSMul` `Algebra.toSMul` `ENNReal.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `ENNReal.instInv` `DFunLike.coe` `Set` `Pi.instOne` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal`	—	`MeasureTheory.Measure.instOuterMeasureClass` `ENNReal.inv_top` `zero_smul` `Set.indicator_zero'` `pdf_eq_zero_of_measure_eq_zero_or_top` `Filter.mp_mem` `MeasureTheory.measure_eq_zero_iff_ae_notMem` `Filter.univ_mem'` `ENNReal.inv_zero` `Set.indicator_of_notMem` `hasPDF` `isProbabilityMeasure` `MeasureTheory.pdf.eq_of_map_eq_withDensity` `MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure` `MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure` `AEMeasurable.indicator` `AEMeasurable.const_smul` `MeasurableSMul.toMeasurableConstSMul` `measurableSMul_of_mul` `MeasurableMul₂.toMeasurableMul` `ENNReal.instMeasurableMul₂` `Measurable.aemeasurable` `measurable_one` `MeasureTheory.withDensity_indicator` `IsScalarTower.right` `MeasureTheory.withDensity_smul` `MeasureTheory.withDensity_one` `ProbabilityTheory.cond.eq_1`
`pdf_eq_zero_of_measure_eq_zero_or_top` 📖	mathematical	`MeasureTheory.pdf.IsUniform` `DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `instZeroENNReal` `Top.top` `instTopENNReal`	`Filter.EventuallyEq` `MeasureTheory.ae` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.pdf` `Pi.instZero`	—	`MeasureTheory.Measure.instOuterMeasureClass` `ENNReal.inv_zero` `MeasureTheory.Measure.restrict_eq_zero` `smul_zero` `IsScalarTower.right` `MeasureTheory.Measure.instHaveLebesgueDecompositionZeroLeft` `ENNReal.inv_top` `zero_smul`
`pdf_toReal_ae_eq` 📖	mathematical	`MeasurableSet` `MeasureTheory.pdf.IsUniform`	`Filter.EventuallyEq` `Real` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `ENNReal.toReal` `MeasureTheory.pdf` `Set.indicator` `ENNReal` `instZeroENNReal` `Function.hasSMul` `Algebra.toSMul` `ENNReal.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `ENNReal.instInv` `DFunLike.coe` `Set` `Pi.instOne` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal`	—	`Filter.EventuallyEq.fun_comp` `MeasureTheory.Measure.instOuterMeasureClass` `pdf_eq`
`toMeasurable` 📖	mathematical	`MeasureTheory.pdf.IsUniform`	`MeasureTheory.toMeasurable`	—	`ProbabilityTheory.cond_toMeasurable_eq`
`toMeasurable_iff` 📖	mathematical	—	`MeasureTheory.pdf.IsUniform` `MeasureTheory.toMeasurable`	—	`ProbabilityTheory.cond_toMeasurable_eq`

PMF

Definitions

Name	Category	Theorems
`ofMultiset` 📖	CompOp	6 math math: `toMeasure_ofMultiset_apply`, `mem_support_ofMultiset_iff`, `toOuterMeasure_ofMultiset_apply`, `support_ofMultiset`, `ofMultiset_apply_of_notMem`, `ofMultiset_apply`
`uniformOfFinset` 📖	CompOp	7 math math: `uniformOfFinset_apply_of_mem`, `toOuterMeasure_uniformOfFinset_apply`, `support_uniformOfFinset`, `uniformOfFinset_apply_of_notMem`, `uniformOfFinset_apply`, `mem_support_uniformOfFinset_iff`, `toMeasure_uniformOfFinset_apply`
`uniformOfFintype` 📖	CompOp	5 math math: `uniformOfFintype_apply`, `toMeasure_uniformOfFintype_apply`, `mem_support_uniformOfFintype`, `toOuterMeasure_uniformOfFintype_apply`, `support_uniformOfFintype`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mem_support_ofMultiset_iff` 📖	mathematical	—	`Set` `Set.instMembership` `support` `ofMultiset` `Finset` `Finset.instMembership` `Multiset.toFinset`	—	`support_ofMultiset`
`mem_support_uniformOfFinset_iff` 📖	mathematical	`Finset.Nonempty`	`Set` `Set.instMembership` `support` `uniformOfFinset` `Finset` `Finset.instMembership`	—	`support_uniformOfFinset`
`mem_support_uniformOfFintype` 📖	mathematical	—	`Set` `Set.instMembership` `support` `uniformOfFintype`	—	`support_uniformOfFintype`
`ofMultiset_apply` 📖	mathematical	—	`DFunLike.coe` `PMF` `ENNReal` `instFunLike` `ofMultiset` `DivInvMonoid.toDiv` `ENNReal.instDivInvMonoid` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Multiset.count` `Multiset.card`	—	—
`ofMultiset_apply_of_notMem` 📖	mathematical	`Multiset` `Multiset.instMembership`	`DFunLike.coe` `PMF` `ENNReal` `instFunLike` `ofMultiset` `instZeroENNReal`	—	`ENNReal.instCharZero`
`support_ofMultiset` 📖	mathematical	—	`support` `ofMultiset` `SetLike.coe` `Finset` `Finset.instSetLike` `Multiset.toFinset`	—	`Set.ext` `ENNReal.instCharZero`
`support_uniformOfFinset` 📖	mathematical	`Finset.Nonempty`	`support` `uniformOfFinset` `SetLike.coe` `Finset` `Finset.instSetLike`	—	`Set.ext`
`support_uniformOfFintype` 📖	mathematical	—	`support` `uniformOfFintype` `Top.top` `Set` `BooleanAlgebra.toTop` `Set.instBooleanAlgebra`	—	`Set.ext` `uniformOfFintype_apply`
`toMeasure_ofMultiset_apply` 📖	mathematical	`MeasurableSet`	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `toMeasure` `ofMultiset` `DivInvMonoid.toDiv` `ENNReal.instDivInvMonoid` `tsum` `ENNReal.instAddCommMonoid` `ENNReal.instTopologicalSpace` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Multiset.count` `Multiset.filter` `Set.instMembership` `SummationFilter.unconditional` `Multiset.card`	—	`toMeasure_apply_eq_toOuterMeasure_apply` `toOuterMeasure_ofMultiset_apply`
`toMeasure_uniformOfFinset_apply` 📖	mathematical	`Finset.Nonempty` `MeasurableSet`	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `toMeasure` `uniformOfFinset` `DivInvMonoid.toDiv` `ENNReal.instDivInvMonoid` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Finset.card` `Finset.filter` `Set.instMembership`	—	`toMeasure_apply_eq_toOuterMeasure_apply` `toOuterMeasure_uniformOfFinset_apply`
`toMeasure_uniformOfFintype_apply` 📖	mathematical	`MeasurableSet`	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `toMeasure` `uniformOfFintype` `DivInvMonoid.toDiv` `ENNReal.instDivInvMonoid` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Fintype.card` `Set.Elem`	—	`toMeasure_uniformOfFinset_apply` `Finset.univ_nonempty` `Fintype.card_subtype`
`toOuterMeasure_ofMultiset_apply` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.OuterMeasure` `Set` `ENNReal` `MeasureTheory.OuterMeasure.instFunLikeSetENNReal` `toOuterMeasure` `ofMultiset` `DivInvMonoid.toDiv` `ENNReal.instDivInvMonoid` `tsum` `ENNReal.instAddCommMonoid` `ENNReal.instTopologicalSpace` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Multiset.count` `Multiset.filter` `Set.instMembership` `SummationFilter.unconditional` `Multiset.card`	—	`div_eq_mul_inv` `toOuterMeasure_apply` `tsum_congr` `Multiset.count_filter_of_pos` `Multiset.count_eq_zero_of_notMem` `CharP.cast_eq_zero` `CharP.ofCharZero` `ENNReal.instCharZero` `MulZeroClass.zero_mul`
`toOuterMeasure_uniformOfFinset_apply` 📖	mathematical	`Finset.Nonempty`	`DFunLike.coe` `MeasureTheory.OuterMeasure` `Set` `ENNReal` `MeasureTheory.OuterMeasure.instFunLikeSetENNReal` `toOuterMeasure` `uniformOfFinset` `DivInvMonoid.toDiv` `ENNReal.instDivInvMonoid` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Finset.card` `Finset.filter` `Set.instMembership`	—	`toOuterMeasure_apply` `tsum_congr` `tsum_eq_sum` `SummationFilter.instLeAtTopUnconditional` `Finset.mem_filter` `Finset.sum_congr` `Finset.sum_const` `nsmul_eq_mul` `div_eq_mul_inv`
`toOuterMeasure_uniformOfFintype_apply` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.OuterMeasure` `Set` `ENNReal` `MeasureTheory.OuterMeasure.instFunLikeSetENNReal` `toOuterMeasure` `uniformOfFintype` `DivInvMonoid.toDiv` `ENNReal.instDivInvMonoid` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Fintype.card` `Set.Elem`	—	`Finset.univ_nonempty` `uniformOfFintype.eq_1` `toOuterMeasure_uniformOfFinset_apply` `Fintype.card_subtype` `Finset.card_univ`
`uniformOfFinset_apply` 📖	mathematical	`Finset.Nonempty`	`DFunLike.coe` `PMF` `ENNReal` `instFunLike` `uniformOfFinset` `Finset` `Finset.instMembership` `Finset.decidableMem` `ENNReal.instInv` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Finset.card` `instZeroENNReal`	—	—
`uniformOfFinset_apply_of_mem` 📖	mathematical	`Finset.Nonempty` `Finset` `Finset.instMembership`	`DFunLike.coe` `PMF` `ENNReal` `instFunLike` `uniformOfFinset` `ENNReal.instInv` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Finset.card`	—	—
`uniformOfFinset_apply_of_notMem` 📖	mathematical	`Finset.Nonempty` `Finset` `Finset.instMembership`	`DFunLike.coe` `PMF` `ENNReal` `instFunLike` `uniformOfFinset` `instZeroENNReal`	—	—
`uniformOfFintype_apply` 📖	mathematical	—	`DFunLike.coe` `PMF` `ENNReal` `instFunLike` `uniformOfFintype` `ENNReal.instInv` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Fintype.card`	—	—

---

← Back to Index