Documentation Verification Report

MeasurableSpace

📁 Source: Mathlib/Analysis/Normed/Lp/MeasurableSpace.lean

Statistics

Metric	Count
Definitions `toLp`, `MeasurableSpace`, `measurableSpace`	3
Theorems `coe_toLp`, `coe_toLp_symm`, `toLp_apply`, `toLp_symm_apply`, `borelSpace`, `borelSpace`, `measurable_ofLp`, `measurable_toLp`	8
Total	11

MeasurableEquiv

Definitions

Name	Category	Theorems
`toLp` 📖	CompOp	6 math math: `toLp_symm_apply`, `coe_toLp`, `EuclideanSpace.volume_preserving_symm_measurableEquiv_toLp`, `WithLp.volume_preserving_symm_measurableEquiv_toLp_prod`, `toLp_apply`, `coe_toLp_symm`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_toLp` 📖	mathematical	—	`DFunLike.coe` `MeasurableEquiv` `WithLp` `WithLp.measurableSpace` `EquivLike.toFunLike` `instEquivLike` `toLp` `WithLp.toLp`	—	—
`coe_toLp_symm` 📖	mathematical	—	`DFunLike.coe` `MeasurableEquiv` `WithLp` `WithLp.measurableSpace` `EquivLike.toFunLike` `instEquivLike` `symm` `toLp` `WithLp.ofLp`	—	—
`toLp_apply` 📖	mathematical	—	`DFunLike.coe` `MeasurableEquiv` `WithLp` `WithLp.measurableSpace` `EquivLike.toFunLike` `instEquivLike` `toLp` `WithLp.toLp`	—	—
`toLp_symm_apply` 📖	mathematical	—	`DFunLike.coe` `MeasurableEquiv` `WithLp` `WithLp.measurableSpace` `EquivLike.toFunLike` `instEquivLike` `symm` `toLp` `WithLp.ofLp`	—	—

PiLp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`borelSpace` 📖	mathematical	`BorelSpace` `SecondCountableTopology`	`BorelSpace` `PiLp` `topologicalSpace` `WithLp.measurableSpace` `MeasurableSpace.pi`	—	`topologicalSpace.eq_1` `borel_comap` `WithLp.measurableSpace.eq_1` `BorelSpace.measurable_eq` `Pi.borelSpace`

WithLp

Definitions

Name	Category	Theorems
`measurableSpace` 📖	CompOp	63 math math: `measurable_ofLp`, `ProbabilityTheory.isGaussian_multivariateGaussian`, `ProbabilityTheory.covarianceBilin_multivariateGaussian`, `GaussianFourier.integral_cexp_neg_mul_sq_norm_add_of_euclideanSpace`, `ProbabilityTheory.measurePreserving_restrict₂_multivariateGaussian`, `ProbabilityTheory.HasGaussianLaw.toLp_pi`, `OrthonormalBasis.measurePreserving_repr`, `instIsAddHaarMeasureEuclideanSpaceRealFinHausdorffMeasureCast`, `ProbabilityTheory.charFun_multivariateGaussian`, `MeasureTheory.charFunDual_pi'`, `ProbabilityTheory.covarianceBilin_apply_basisFun_self`, `MeasurableEquiv.toLp_symm_apply`, `GaussianFourier.integrable_cexp_neg_mul_sq_norm_add_of_euclideanSpace`, `borelSpace`, `EuclideanSpace.volume_closedBall_fin_three`, `measurable_toLp`, `PiLp.volume_preserving_toLp`, `MeasureTheory.charFun_eq_prod_iff`, `ProbabilityTheory.multivariateGaussian_of_not_posSemidef`, `EuclideanSpace.volume_closedBall_fin_two`, `ProbabilityTheory.map_pi_eq_stdGaussian`, `ProbabilityTheory.integral_id_multivariateGaussian`, `MeasurableEquiv.coe_toLp`, `MeasureTheory.charFun_pi`, `NumberField.mixedEmbedding.euclidean.volumePreserving_toMixed`, `ProbabilityTheory.variance_eval_multivariateGaussian`, `volume_preserving_toLp`, `PiLp.volume_preserving_ofLp`, `ProbabilityTheory.indepFun_iff_charFunDual_prod'`, `PiLp.borelSpace`, `ProbabilityTheory.indepFun_iff_charFun_prod`, `ProbabilityTheory.covarianceBilin_apply_pi`, `EuclideanSpace.volume_ball_fin_three`, `ProbabilityTheory.covarianceBilin_apply_basisFun`, `OrthonormalBasis.measurePreserving_repr_symm`, `EuclideanSpace.volume_preserving_symm_measurableEquiv_toLp`, `volume_preserving_symm_measurableEquiv_toLp_prod`, `EuclideanSpace.volume_ball_fin_two`, `EuclideanSpace.volume_ball`, `ProbabilityTheory.iIndepFun_iff_charFunDual_pi'`, `MeasureTheory.charFunDual_prod'`, `ProbabilityTheory.measurePreserving_eval_multivariateGaussian`, `ProbabilityTheory.iIndepFun_iff_charFun_pi`, `volume_preserving_ofLp`, `MeasureTheory.charFunDual_eq_pi_iff'`, `volume_euclideanSpace_eq_dirac`, `ProbabilityTheory.integral_id_multivariateGaussian'`, `EuclideanSpace.coe_measurableEquiv`, `ProbabilityTheory.multivariateGaussian_zero_one`, `ProbabilityTheory.HasGaussianLaw.toLp_prodMk`, `NumberField.mixedEmbedding.euclidean.volumePreserving_toMixed_symm`, `EuclideanSpace.measurableEquiv_toEquiv`, `EuclideanSpace.euclideanHausdorffMeasure_eq_volume`, `OrthonormalBasis.measurePreserving_measurableEquiv`, `MeasureTheory.charFun_eq_pi_iff`, `MeasurableEquiv.toLp_apply`, `MeasureTheory.charFun_prod`, `ProbabilityTheory.covariance_eval_multivariateGaussian`, `MeasureTheory.charFunDual_eq_prod_iff'`, `EuclideanSpace.volume_closedBall`, `EuclideanSpace.coe_measurableEquiv_symm`, `MeasureTheory.Measure.euclideanHausdorffMeasure_def`, `MeasurableEquiv.coe_toLp_symm`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`borelSpace` 📖	mathematical	—	`BorelSpace` `WithLp` `instProdTopologicalSpace` `measurableSpace` `Prod.instMeasurableSpace`	—	`instProdTopologicalSpace.eq_1` `borel_comap` `measurableSpace.eq_1` `BorelSpace.measurable_eq` `Prod.borelSpace`
`measurable_ofLp` 📖	mathematical	—	`Measurable` `WithLp` `measurableSpace` `ofLp`	—	`comap_measurable`
`measurable_toLp` 📖	mathematical	—	`Measurable` `WithLp` `measurableSpace` `toLp`	—	`Set.preimage_preimage`

(root)

Definitions

Name	Category	Theorems
`MeasurableSpace` 📖	CompData	204 math math: `MeasureTheory.OuterMeasure.IsMetric.borel_le_caratheodory`, `measurable_from_top`, `MeasureTheory.OuterMeasure.IsMetric.le_caratheodory`, `MeasurableSpace.comap_mono`, `MeasurableSpace.comap_const`, `MeasurableSpace.comap_bot`, `ProbabilityTheory.condIndep_iSup_of_antitone`, `ProbabilityTheory.Kernel.indep_iSup_directed_limsup`, `ProbabilityTheory.indep_iSup_of_monotone`, `ProbabilityTheory.indep_limsup_atTop_self`, `MeasurableSpace.generateFrom_empty`, `MeasureTheory.condLExp_bot'`, `MeasureTheory.AddContent.measure_eq`, `Measurable.sup_of_right`, `MeasureTheory.VectorMeasure.trim_eq_self`, `ProbabilityTheory.condIndep_bot_left`, `MeasurableSpace.map_mono`, `ProbabilityTheory.condIndep_iSup_of_monotone`, `MeasurableSpace.exists_countablyGenerated_le_of_countablySeparated`, `OpensMeasurableSpace.borel_le`, `MeasurableSpace.measurableSet_iInf`, `MeasurableSpace.measurableSet_sSup`, `ProbabilityTheory.Kernel.indep_limsup_atBot_self`, `ProbabilityTheory.exists_hasLaw_indepFun`, `MeasurableSpace.map_const`, `le_eventuallyMeasurableSpace`, `ProbabilityTheory.indep_biSup_limsup`, `MeasureTheory.OuterMeasure.le_sum_caratheodory`, `MeasureTheory.IsStoppingTime.measurableSpace_le_of_le_const`, `MeasurableSpace.generateFrom_iUnion_measurableSet`, `ProbabilityTheory.Kernel.indep_iSup_limsup`, `generateFrom_Icc_mem_le_borel`, `PMF.toOuterMeasure_caratheodory`, `ProbabilityTheory.indep_iSup_of_directed_le`, `MeasurableSpace.invariants_le`, `MeasureTheory.condLExp_bot`, `MeasurableSpace.generateFrom_sup_generateFrom`, `Measurable.comap_le`, `ProbabilityTheory.condIndep_limsup_atTop_self`, `ProbabilityTheory.iIndep_precomp_of_bijective`, `MeasurableSpace.generateFrom_memPartition_le`, `indep_comap_of_bcf`, `ProbabilityTheory.Kernel.indep_limsup_self`, `generateFrom_Ico_mem_le_borel`, `MeasurableSpace.map_inf`, `MeasurableSpace.comap_compl`, `ProbabilityTheory.condExpKernel_ae_eq_condExp'`, `ProbabilityTheory.exists_iid`, `Measurable.le_map`, `borel_eq_top_of_discrete`, `MeasureTheory.IsStoppingTime.measurableSpace_mono`, `indepSets_comap_of_bcf`, `ProbabilityTheory.iIndep_comap_mem_iff`, `MeasureTheory.cylinderEvents_mono`, `StieltjesFunction.borel_le_measurable`, `MeasureTheory.OuterMeasure.le_add_caratheodory`, `ProbabilityTheory.indep_iSup_limsup`, `MeasurableSpace.measurableSet_bot_iff`, `MeasureTheory.Filtration.rightCont_apply`, `MeasureTheory.OuterMeasure.zero_caratheodory`, `le_generateFrom_piiUnionInter`, `MeasurableSpace.comap_prodMk`, `MeasureTheory.OuterMeasure.top_caratheodory`, `MeasurableSpace.measurableSpace_iSup_eq`, `MeasureTheory.IsStoppingTime.measurableSpace_le`, `MeasureTheory.Measure.pi_caratheodory`, `ProbabilityTheory.iIndepSet.iIndep_comap_mem`, `MeasureTheory.trim_eq_self`, `ProbabilityTheory.Kernel.IsProper.restrict_eq_indicator_smul'`, `MeasureTheory.condExp_bot`, `ProbabilityTheory.condIndepFun_self_left`, `MeasurableSpace.generateFrom_singleton_univ`, `MeasureTheory.Filtration.rightCont_def`, `MeasureTheory.condExp_def`, `measurable_iff_comap_le`, `generateFrom_piiUnionInter_measurableSet`, `ProbabilityTheory.condIndep_iSup_limsup`, `ProbabilityTheory.Kernel.iIndep_comap_mem_iff`, `MeasureTheory.StronglyMeasurable.integral_condExpKernel'`, `ProbabilityTheory.Kernel.indep_iSup_of_directed_le`, `MeasureTheory.Filtration.le'`, `ProbabilityTheory.condExp_ae_eq_integral_condExpKernel'`, `MeasurableSpace.CountablyGenerated.sup`, `ProbabilityTheory.Kernel.indep_iSup_of_monotone`, `MeasureTheory.IsStoppingTime.measurableSpace_min`, `MeasurableSpace.generateFrom_mono`, `MeasureTheory.Filtration.rightCont_eq_of_not_isMax`, `MeasureTheory.tendsto_ae_condExp`, `ProbabilityTheory.indep_iSup_directed_limsup`, `ProbabilityTheory.iSup_partitionFiltration_eq_generateFrom_range`, `ProbabilityTheory.condIndep_biSup_limsup`, `ProbabilityTheory.condIndep_limsup_self`, `ProbabilityTheory.condExpKernel_def`, `MeasureTheory.SimpleFunc.simpleFunc_bot'`, `ProbabilityTheory.Kernel.iIndep_precomp_of_bijective`, `ProbabilityTheory.condIndepFun_self_right`, `MeasurableSpace.comap_iSup`, `MeasureTheory.IsStoppingTime.measurableSpace_min_const`, `ProbabilityTheory.Kernel.indep_biSup_limsup`, `MeasureTheory.OuterMeasure.le_smul_caratheodory`, `MeasureTheory.sigmaFinite_bot_iff`, `generateFrom_piiUnionInter_le`, `MeasurableSpace.generateFrom_memPartition_le_range`, `MeasurableSpace.inf_le_invariants_comp`, `ProbabilityTheory.indep_limsup_atBot_self`, `Measurable.iSup'`, `MeasureTheory.tendsto_eLpNorm_condExp`, `MeasurableSpace.gc_comap_map`, `MeasureTheory.condLExp_bot_ae_eq`, `ProbabilityTheory.iSup_countableFiltration`, `ProbabilityTheory.indep_iSup_of_antitone`, `MeasurableSpace.generateFrom_countablePartition_le`, `pi_le_borel_pi`, `MeasureTheory.Filtration.rightCont_eq`, `ProbabilityTheory.condIndep_biSup_compl`, `MeasurableSpace.le_def`, `MeasurableSpace.map_iInf`, `ProbabilityTheory.condIndep_iSup_directed_limsup`, `MeasureTheory.cylinderEvents_le_pi`, `MeasureTheory.Filtration.coeFn_sup`, `ProbabilityTheory.condVar_bot'`, `ProbabilityTheory.Kernel.indep_limsup_atTop_self`, `MeasurableSpace.comap_sup`, `ProbabilityTheory.Kernel.indep_iSup_of_antitone`, `Measurable.sup_of_left`, `MeasurableSpace.measurableSet_sInf`, `ProbabilityTheory.condIndep_bot_right`, `MeasureTheory.Content.borel_le_caratheodory`, `MeasureTheory.measurableSpace_le_predictable_of_measurableSet`, `MeasurableSpace.generateFrom_singleton`, `MeasureTheory.trim_trim`, `ProbabilityTheory.indep_bot_right`, `ProbabilityTheory.condVar_bot_ae_eq`, `MeasureTheory.Filtration.mono`, `ProbabilityTheory.indep_bot_left`, `MeasureTheory.Filtration.sSup_def`, `MeasureTheory.Filtration.le`, `instDiscreteMeasurableSpace`, `MeasurableSpace.comap_le_iff_le_map`, `MeasureTheory.SimpleFunc.simpleFunc_bot`, `ProbabilityTheory.condVar_bot`, `MeasurableSpace.le_invariants_iterate`, `measurable_iff_le_map`, `ProbabilityTheory.indep_biSup_compl`, `MeasureTheory.comap_eval_le_generateFrom_squareCylinders_singleton`, `MeasurableSpace.measurableSet_injective`, `ProbabilityTheory.condExpKernel_eq`, `MeasurableSpace.comap_map_le`, `stronglyMeasurable_bot_iff`, `MeasurableSpace.map_top`, `MeasurableSpace.generateFrom_memPartition_le_succ`, `ProbabilityTheory.condIndepFun_iff_condDistrib_prod_ae_eq_prodMkRight`, `MeasurableSpace.generateFrom_countablePartition_le_succ`, `MeasurableSpace.generateFrom_singleton_le`, `MeasurableSpace.iSup_generateFrom`, `MeasureTheory.condLExp_def`, `ProbabilityTheory.condIndep_iSup_of_disjoint`, `borel_eq_top_of_countable`, `ProbabilityTheory.iIndep.precomp`, `prod_le_borel_prod`, `ProbabilityTheory.iSup_partitionFiltration`, `MeasurableSpace.measurableSet_top`, `ProbabilityTheory.Kernel.indep_bot_left`, `MeasureTheory.sigmaFinite_trim_bot_iff`, `MeasureTheory.le_toOuterMeasure_caratheodory`, `ProbabilityTheory.condIndepFun_iff_condDistrib_prod_ae_eq_prodMkLeft`, `ProbabilityTheory.condIndep_limsup_atBot_self`, `MeasurableSpace.generateFrom_iUnion_memPartition_le`, `ProbabilityTheory.Kernel.iIndep.precomp`, `borel_anti`, `MeasurableSpace.le_map_comap`, `MeasureTheory.condExp_bot'`, `ProbabilityTheory.Kernel.indep_bot_right`, `MeasurableSpace.comap_le_comap_pi`, `MeasureTheory.OuterMeasure.dirac_caratheodory`, `MeasureTheory.Submartingale.exists_ae_trim_tendsto_of_bdd`, `MeasureTheory.Filtration.rightCont_eq_of_neBot_nhdsGT`, `ProbabilityTheory.condIndep_iSup_of_directed_le`, `MeasureTheory.Filtration.coeFn_inf`, `Measure.exists_hasLaw`, `ProbabilityTheory.Kernel.id_prod_eq`, `ProbabilityTheory.Kernel.indep_biSup_compl`, `MeasurableSpace.generateFrom_le_iff`, `MeasurableSpace.measurableSet_inf`, `MeasurableSpace.measurableSet_sup`, `MeasureTheory.Filtration.mono'`, `ProbabilityTheory.indep_iSup_of_disjoint`, `MeasureTheory.IsStoppingTime.le_measurableSpace_of_const_le`, `MeasurableSpace.DynkinSystem.ofMeasurableSpace_le_ofMeasurableSpace_iff`, `ProbabilityTheory.Kernel.indep_iSup_of_disjoint`, `MeasurableSpace.generateFrom_le`, `measurableSet_iSup_of_mem_piiUnionInter`, `MeasurableSpace.monotone_map`, `MeasurableSpace.generateFrom_singleton_empty`, `MeasureTheory.condExp_bot_ae_eq`, `ProbabilityTheory.indep_limsup_self`, `MeasureTheory.Filtration.stronglyMeasurable_limitProcess`, `MeasureTheory.IsStoppingTime.measurableSpace_le_of_le`, `MeasurableSpace.comap_not`, `MeasurableSpace.monotone_comap`, `MeasurableSpace.measurableSet_iSup`, `MeasureTheory.Filtration.sInf_def`, `ProbabilityTheory.condExpKernel_apply_eq_condDistrib`, `ProbabilityTheory.condIndepFun_iff_map_prod_eq_prod_condDistrib_prod_condDistrib`

---

← Back to Index