Documentation Verification Report

HasLaw

📁 Source: Mathlib/Probability/HasLaw.lean

Statistics

Metric	Count
Definitions `HasLaw`	1
Theorems `hasLaw`, `ae_iff`, `aemeasurable`, `comp`, `covariance_comp`, `covariance_fun_comp`, `fun_comp`, `id`, `integral_comp`, `integral_eq`, `isFiniteMeasure`, `isFiniteMeasure_iff`, `isProbabilityMeasure`, `isProbabilityMeasure_iff`, `lintegral_comp`, `map_eq`, `measurePreserving`, `variance_eq`, `hasLaw`, `hasLaw_add`, `hasLaw_fun_add`, `hasLaw_fun_mul`, `hasLaw_mul`, `hasLaw_congr`	24
Total	25

MeasureTheory.MeasurePreserving

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasLaw` 📖	mathematical	`MeasureTheory.MeasurePreserving`	`ProbabilityTheory.HasLaw`	—	`Measurable.aemeasurable` `measurable` `map_eq`

ProbabilityTheory

Definitions

Name	Category	Theorems
`HasLaw` 📖	CompData	7 math math: `MeasureTheory.MeasurePreserving.hasLaw`, `HasLaw.id`, `exists_hasLaw_indepFun`, `exists_iid`, `Measure.exists_hasLaw`, `HasPDF.hasLaw`, `hasLaw_congr`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasLaw_congr` 📖	mathematical	`Filter.EventuallyEq` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	`HasLaw`	—	`MeasureTheory.Measure.instOuterMeasureClass` `HasLaw.congr` `Filter.EventuallyEq.symm`

ProbabilityTheory.HasLaw

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ae_iff` 📖	mathematical	`ProbabilityTheory.HasLaw` `Measurable` `Prop.instMeasurableSpace`	`Filter.Eventually` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	—	`MeasureTheory.Measure.instOuterMeasureClass` `map_eq` `MeasureTheory.ae_map_iff` `aemeasurable` `measurableSet_setOf`
`aemeasurable` 📖	mathematical	`ProbabilityTheory.HasLaw`	`AEMeasurable`	—	—
`comp` 📖	—	`ProbabilityTheory.HasLaw`	—	—	`AEMeasurable.comp_aemeasurable` `aemeasurable` `map_eq` `AEMeasurable.map_map_of_aemeasurable`
`covariance_comp` 📖	mathematical	`ProbabilityTheory.HasLaw` `AEMeasurable` `Real` `Real.measurableSpace`	`ProbabilityTheory.covariance`	—	`map_eq` `ProbabilityTheory.covariance_map` `AEMeasurable.aestronglyMeasurable` `PseudoEMetricSpace.pseudoMetrizableSpace` `BorelSpace.opensMeasurable` `Real.borelSpace` `instSecondCountableTopologyReal` `aemeasurable`
`covariance_fun_comp` 📖	mathematical	`ProbabilityTheory.HasLaw` `AEMeasurable` `Real` `Real.measurableSpace`	`ProbabilityTheory.covariance`	—	`covariance_comp`
`fun_comp` 📖	—	`ProbabilityTheory.HasLaw`	—	—	`comp`
`id` 📖	mathematical	—	`ProbabilityTheory.HasLaw`	—	`aemeasurable_id` `MeasureTheory.Measure.map_id`
`integral_comp` 📖	mathematical	`ProbabilityTheory.HasLaw` `MeasureTheory.AEStronglyMeasurable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	`MeasureTheory.integral`	—	`map_eq` `MeasureTheory.integral_map` `aemeasurable`
`integral_eq` 📖	mathematical	`ProbabilityTheory.HasLaw`	`MeasureTheory.integral`	—	`integral_comp` `aestronglyMeasurable_id` `PseudoEMetricSpace.pseudoMetrizableSpace`
`isFiniteMeasure` 📖	mathematical	`ProbabilityTheory.HasLaw`	`MeasureTheory.IsFiniteMeasure`	—	`isFiniteMeasure_iff`
`isFiniteMeasure_iff` 📖	mathematical	`ProbabilityTheory.HasLaw`	`MeasureTheory.IsFiniteMeasure`	—	`map_eq` `MeasureTheory.Measure.isFiniteMeasure_map_iff` `aemeasurable`
`isProbabilityMeasure` 📖	mathematical	`ProbabilityTheory.HasLaw`	`MeasureTheory.IsProbabilityMeasure`	—	`isProbabilityMeasure_iff`
`isProbabilityMeasure_iff` 📖	mathematical	`ProbabilityTheory.HasLaw`	`MeasureTheory.IsProbabilityMeasure`	—	`map_eq` `MeasureTheory.Measure.isProbabilityMeasure_map_iff` `aemeasurable`
`lintegral_comp` 📖	mathematical	`ProbabilityTheory.HasLaw` `AEMeasurable` `ENNReal` `ENNReal.measurableSpace`	`MeasureTheory.lintegral`	—	`map_eq` `MeasureTheory.lintegral_map'` `aemeasurable`
`map_eq` 📖	mathematical	`ProbabilityTheory.HasLaw`	`MeasureTheory.Measure.map`	—	—
`measurePreserving` 📖	mathematical	`ProbabilityTheory.HasLaw` `Measurable`	`MeasureTheory.MeasurePreserving`	—	`map_eq`
`variance_eq` 📖	mathematical	`ProbabilityTheory.HasLaw` `Real` `Real.measurableSpace`	`ProbabilityTheory.variance`	—	`map_eq` `ProbabilityTheory.variance_map` `aemeasurable_id` `aemeasurable`

ProbabilityTheory.HasPDF

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasLaw` 📖	mathematical	—	`ProbabilityTheory.HasLaw` `MeasureTheory.Measure.withDensity` `MeasureTheory.pdf`	—	`MeasureTheory.HasPDF.aemeasurable` `MeasureTheory.map_eq_withDensity_pdf`

ProbabilityTheory.IndepFun

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasLaw_add` 📖	mathematical	`ProbabilityTheory.HasLaw` `ProbabilityTheory.IndepFun`	`Pi.instAdd` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `MeasureTheory.Measure.conv`	—	`AEMeasurable.add'` `ProbabilityTheory.HasLaw.aemeasurable` `map_add_eq_map_conv_map₀'` `ProbabilityTheory.HasLaw.map_eq`
`hasLaw_fun_add` 📖	mathematical	`ProbabilityTheory.HasLaw` `ProbabilityTheory.IndepFun`	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `MeasureTheory.Measure.conv`	—	`hasLaw_add`
`hasLaw_fun_mul` 📖	mathematical	`ProbabilityTheory.HasLaw` `ProbabilityTheory.IndepFun`	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MeasureTheory.Measure.mconv`	—	`hasLaw_mul`
`hasLaw_mul` 📖	mathematical	`ProbabilityTheory.HasLaw` `ProbabilityTheory.IndepFun`	`Pi.instMul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MeasureTheory.Measure.mconv`	—	`AEMeasurable.mul'` `ProbabilityTheory.HasLaw.aemeasurable` `map_mul_eq_map_mconv_map₀'` `ProbabilityTheory.HasLaw.map_eq`

---

← Back to Index