MeasureCompProd

📁 Source: Mathlib/Probability/Kernel/Composition/MeasureCompProd.lean

Statistics

Metric	Count
Definitions `compProd`, `«term_⊗ₘ_»`	2
Theorems `compProd`, `compProd_left`, `compProd_of_compProd`, `compProd_right`, `mutuallySingular_compProd_iff`, `compProd_of_left`, `absolutelyContinuous_compProd_iff`, `absolutelyContinuous_compProd_left_iff`, `absolutelyContinuous_compProd_of_compProd`, `absolutelyContinuous_of_compProd`, `ae_ae_of_ae_compProd`, `ae_compProd_iff`, `ae_compProd_of_ae_ae`, `compProd_add_left`, `compProd_add_right`, `compProd_apply`, `compProd_apply_prod`, `compProd_apply_univ`, `compProd_assoc`, `compProd_assoc'`, `compProd_congr`, `compProd_const`, `compProd_eq_zero_iff`, `compProd_id`, `compProd_of_not_isSFiniteKernel`, `compProd_of_not_sfinite`, `compProd_smul_left`, `compProd_sum_left`, `compProd_sum_right`, `compProd_zero_left`, `compProd_zero_right`, `dirac_compProd_apply`, `dirac_unit_compProd`, `dirac_unit_compProd_const`, `fst_compProd`, `instIsFiniteMeasureProdCompProdOfIsFiniteKernel`, `instIsProbabilityMeasureProdCompProdOfIsMarkovKernel`, `instIsZeroOrProbabilityMeasureProdCompProdOfIsZeroOrMarkovKernel`, `instSFiniteProdCompProd`, `lintegral_compProd`, `mutuallySingular_compProd_iff`, `mutuallySingular_compProd_left_iff`, `mutuallySingular_of_mutuallySingular_compProd`, `setLIntegral_compProd`, `snd_dirac_unit_compProd_const`, `compProd_apply_eq_compProd_sectR`	46
Total	48

MeasureTheory.Measure

Definitions

Name	Category	Theorems
`compProd` 📖	CompOp	74 math math: `ProbabilityTheory.Kernel.map_frestrictLe_trajMeasure_compProd_eq_map_trajMeasure`, `comp_compProd_comm`, `ProbabilityTheory.compProd_posterior_eq_map_swap`, `fst_compProd`, `snd_compProd`, `instSFiniteProdCompProd`, `MutuallySingular.compProd_of_left`, `ProbabilityTheory.condDistrib_ae_eq_iff_measure_eq_compProd`, `ProbabilityTheory.compProd_map_condDistrib`, `mutuallySingular_compProd_right_iff`, `compProd_id`, `compProd_assoc'`, `compProd_apply_univ`, `AbsolutelyContinuous.compProd_right`, `compProd_apply`, `ProbabilityTheory.Kernel.partialTraj_compProd_traj`, `compProd_map`, `AbsolutelyContinuous.compProd`, `ProbabilityTheory.condIndepFun_iff_compProd_map_prod_eq_compProd_prod_map_map`, `ProbabilityTheory.posterior_prod_id_comp`, `compProd_id_eq_copy_comp`, `compProd_withDensity`, `compProd_sum_left`, `parallelComp_comp_compProd`, `mutuallySingular_compProd_iff`, `ProbabilityTheory.condKernel_compProd`, `instIsZeroOrProbabilityMeasureProdCompProdOfIsZeroOrMarkovKernel`, `compProd_congr`, `compProd_eq_comp_prod`, `MutuallySingular.compProd_of_right'`, `dirac_unit_compProd_const`, `compProd_deterministic`, `integrable_compProd_snd_iff`, `absolutelyContinuous_compProd_left_iff`, `MutuallySingular.compProd_of_right`, `compProd_zero_left`, `instIsFiniteMeasureProdCompProdOfIsFiniteKernel`, `compProd_apply_prod`, `ProbabilityTheory.swap_compProd_posterior`, `compProd_assoc`, `IsCondKernel.disintegrate`, `ProbabilityTheory.compProd_trim_condExpKernel`, `snd_dirac_unit_compProd_const`, `compProd_add_left`, `mutuallySingular_compProd_left_iff`, `absolutelyContinuous_compProd_iff'`, `disintegrate`, `setLIntegral_compProd`, `compProd_sum_right`, `ProbabilityTheory.Kernel.indepFun_iff_compProd_map_prod_eq_compProd_prod_map_map`, `compProd_of_not_sfinite`, `instIsProbabilityMeasureProdCompProdOfIsMarkovKernel`, `dirac_compProd_apply`, `compProd_zero_right`, `compProd_of_not_isSFiniteKernel`, `ae_compProd_of_ae_ae`, `compProd_eq_zero_iff`, `ProbabilityTheory.Kernel.compProd_apply_eq_compProd_sectR`, `compProd_smul_left`, `ProbabilityTheory.Kernel.compProd_eq_iff`, `compProd_add_right`, `ae_compProd_iff`, `absolutelyContinuous_compProd_right_iff`, `dirac_unit_compProd`, `ProbabilityTheory.compProd_posterior_eq_swap_comp`, `prodMkLeft_comp_compProd`, `ProbabilityTheory.Kernel.HasSubgaussianMGF.prodMkLeft_compProd`, `AbsolutelyContinuous.compProd_left`, `compProd_eq_parallelComp_comp_copy_comp`, `ProbabilityTheory.Kernel.partialTraj_compProd_eq_map_traj`, `AbsolutelyContinuous.mutuallySingular_compProd_iff`, `lintegral_compProd`, `absolutelyContinuous_compProd_iff`, `compProd_const`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`absolutelyContinuous_compProd_iff` 📖	mathematical	`MeasureTheory.Measure` `instZero` `DFunLike.coe` `ProbabilityTheory.Kernel` `ProbabilityTheory.Kernel.instFunLike`	`AbsolutelyContinuous` `Prod.instMeasurableSpace` `compProd`	—	`absolutelyContinuous_of_compProd` `MeasureTheory.instSFiniteOfSigmaFinite` `absolutelyContinuous_compProd_of_compProd` `AbsolutelyContinuous.compProd_of_compProd`
`absolutelyContinuous_compProd_left_iff` 📖	mathematical	`MeasureTheory.Measure` `instZero` `DFunLike.coe` `ProbabilityTheory.Kernel` `ProbabilityTheory.Kernel.instFunLike`	`AbsolutelyContinuous` `Prod.instMeasurableSpace` `compProd`	—	`absolutelyContinuous_of_compProd` `AbsolutelyContinuous.compProd_left`
`absolutelyContinuous_compProd_of_compProd` 📖	—	`AbsolutelyContinuous` `Prod.instMeasurableSpace` `compProd`	—	—	`absolutelyContinuous_of_add_of_mutuallySingular` `add_comm` `compProd_add_left` `MeasureTheory.instSFiniteOfSigmaFinite` `singularPart.instSigmaFinite` `withDensity.instSFinite` `haveLebesgueDecomposition_add` `haveLebesgueDecomposition_of_sigmaFinite` `MutuallySingular.compProd_of_left` `MutuallySingular.symm` `mutuallySingular_singularPart` `AbsolutelyContinuous.trans` `AbsolutelyContinuous.compProd_left` `MeasureTheory.withDensity_absolutelyContinuous`
`absolutelyContinuous_of_compProd` 📖	—	`MeasureTheory.Measure` `instZero` `DFunLike.coe` `ProbabilityTheory.Kernel` `ProbabilityTheory.Kernel.instFunLike` `AbsolutelyContinuous` `Prod.instMeasurableSpace` `compProd`	—	—	`compProd_apply_prod` `MeasurableSet.univ` `MeasureTheory.setLIntegral_measure_zero` `compProd_of_not_isSFiniteKernel` `compProd_of_not_sfinite` `instOuterMeasureClass` `Filter.Eventually.exists` `MeasureTheory.lintegral_eq_zero_iff` `ProbabilityTheory.Kernel.measurable_coe`
`ae_ae_of_ae_compProd` 📖	mathematical	`Filter.Eventually` `MeasureTheory.ae` `MeasureTheory.Measure` `Prod.instMeasurableSpace` `instFunLike` `instOuterMeasureClass` `compProd`	`DFunLike.coe` `ProbabilityTheory.Kernel` `ProbabilityTheory.Kernel.instFunLike`	—	`instOuterMeasureClass` `ProbabilityTheory.Kernel.ae_ae_of_ae_compProd` `ProbabilityTheory.Kernel.const.instIsSFiniteKernel` `ProbabilityTheory.Kernel.IsSFiniteKernel.prodMkLeft`
`ae_compProd_iff` 📖	mathematical	`MeasurableSet` `Prod.instMeasurableSpace` `setOf`	`Filter.Eventually` `MeasureTheory.ae` `MeasureTheory.Measure` `instFunLike` `instOuterMeasureClass` `compProd` `DFunLike.coe` `ProbabilityTheory.Kernel` `ProbabilityTheory.Kernel.instFunLike`	—	`ProbabilityTheory.Kernel.ae_compProd_iff` `ProbabilityTheory.Kernel.const.instIsSFiniteKernel` `ProbabilityTheory.Kernel.IsSFiniteKernel.prodMkLeft`
`ae_compProd_of_ae_ae` 📖	mathematical	`MeasurableSet` `Prod.instMeasurableSpace` `setOf` `Filter.Eventually` `MeasureTheory.ae` `MeasureTheory.Measure` `instFunLike` `instOuterMeasureClass` `DFunLike.coe` `ProbabilityTheory.Kernel` `ProbabilityTheory.Kernel.instFunLike`	`compProd`	—	`instOuterMeasureClass` `ProbabilityTheory.Kernel.ae_compProd_of_ae_ae`
`compProd_add_left` 📖	mathematical	—	`compProd` `MeasureTheory.Measure` `instAdd` `Prod.instMeasurableSpace`	—	`ProbabilityTheory.Kernel.const_add` `ProbabilityTheory.Kernel.compProd_add_left` `ProbabilityTheory.Kernel.const.instIsSFiniteKernel` `compProd_of_not_isSFiniteKernel` `add_zero`
`compProd_add_right` 📖	mathematical	—	`compProd` `ProbabilityTheory.Kernel` `ProbabilityTheory.Kernel.instAdd` `MeasureTheory.Measure` `Prod.instMeasurableSpace` `instAdd`	—	`ProbabilityTheory.Kernel.prodMkLeft_add` `ProbabilityTheory.Kernel.compProd_add_right` `ProbabilityTheory.Kernel.IsSFiniteKernel.prodMkLeft` `compProd_of_not_sfinite` `add_zero`
`compProd_apply` 📖	mathematical	`MeasurableSet` `Prod.instMeasurableSpace`	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `instFunLike` `compProd` `MeasureTheory.lintegral` `ProbabilityTheory.Kernel` `ProbabilityTheory.Kernel.instFunLike` `Set.preimage`	—	`ProbabilityTheory.Kernel.compProd_apply` `ProbabilityTheory.Kernel.const.instIsSFiniteKernel` `ProbabilityTheory.Kernel.IsSFiniteKernel.prodMkLeft`
`compProd_apply_prod` 📖	mathematical	`MeasurableSet`	`DFunLike.coe` `MeasureTheory.Measure` `Prod.instMeasurableSpace` `Set` `ENNReal` `instFunLike` `compProd` `SProd.sprod` `Set.instSProd` `MeasureTheory.lintegral` `restrict` `ProbabilityTheory.Kernel` `ProbabilityTheory.Kernel.instFunLike`	—	`ProbabilityTheory.Kernel.compProd_apply_prod` `ProbabilityTheory.Kernel.const.instIsSFiniteKernel` `ProbabilityTheory.Kernel.IsSFiniteKernel.prodMkLeft`
`compProd_apply_univ` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.Measure` `Prod.instMeasurableSpace` `Set` `ENNReal` `instFunLike` `compProd` `Set.univ`	—	`ProbabilityTheory.Kernel.compProd_apply_univ` `ProbabilityTheory.Kernel.const.instIsSFiniteKernel` `ProbabilityTheory.Kernel.IsMarkovKernel.prodMkLeft`
`compProd_assoc` 📖	mathematical	—	`map` `Prod.instMeasurableSpace` `DFunLike.coe` `MeasurableEquiv` `EquivLike.toFunLike` `MeasurableEquiv.instEquivLike` `MeasurableEquiv.symm` `MeasurableEquiv.prodAssoc` `compProd` `ProbabilityTheory.Kernel.compProd`	—	`ext` `compProd_apply` `instSFiniteProdCompProd` `map_apply` `MeasurableEquiv.measurable` `ProbabilityTheory.Kernel.IsSFiniteKernel.compProd` `MeasurableSet.preimage` `lintegral_compProd` `ProbabilityTheory.Kernel.measurable_kernel_prodMk_left` `ProbabilityTheory.Kernel.compProd_apply` `Measurable.fun_comp` `Measurable.prodMk` `measurable_const` `measurable_id'` `ProbabilityTheory.Kernel.compProd_of_not_isSFiniteKernel_right` `compProd_zero_right` `map_zero` `compProd_of_not_isSFiniteKernel` `ProbabilityTheory.Kernel.compProd_of_not_isSFiniteKernel_left` `compProd_zero_left` `compProd_of_not_sfinite`
`compProd_assoc'` 📖	mathematical	—	`map` `Prod.instMeasurableSpace` `DFunLike.coe` `MeasurableEquiv` `EquivLike.toFunLike` `MeasurableEquiv.instEquivLike` `MeasurableEquiv.prodAssoc` `compProd` `ProbabilityTheory.Kernel.compProd`	—	`MeasurableEquiv.map_map_symm`
`compProd_congr` 📖	mathematical	`Filter.EventuallyEq` `MeasureTheory.Measure` `MeasureTheory.ae` `instFunLike` `instOuterMeasureClass` `DFunLike.coe` `ProbabilityTheory.Kernel` `ProbabilityTheory.Kernel.instFunLike`	`compProd`	—	`instOuterMeasureClass` `compProd.eq_1` `ProbabilityTheory.Kernel.compProd_congr` `ProbabilityTheory.Kernel.IsSFiniteKernel.prodMkLeft`
`compProd_const` 📖	mathematical	—	`compProd` `ProbabilityTheory.Kernel.const` `prod`	—	`ext` `compProd_apply` `ProbabilityTheory.Kernel.const.instIsSFiniteKernel` `prod_apply`
`compProd_eq_zero_iff` 📖	mathematical	—	`compProd` `MeasureTheory.Measure` `Prod.instMeasurableSpace` `instZero` `Filter.Eventually` `DFunLike.coe` `ProbabilityTheory.Kernel` `ProbabilityTheory.Kernel.instFunLike` `MeasureTheory.ae` `instFunLike` `instOuterMeasureClass`	—	`instOuterMeasureClass` `MeasureTheory.lintegral_eq_zero_iff` `ProbabilityTheory.Kernel.measurable_coe` `MeasurableSet.univ` `MeasureTheory.setLIntegral_univ` `compProd_apply_prod` `Set.univ_prod_univ` `compProd_zero_right` `compProd_congr` `ProbabilityTheory.Kernel.IsFiniteKernel.isSFiniteKernel` `ProbabilityTheory.isFiniteKernel_zero`
`compProd_id` 📖	mathematical	—	`compProd` `ProbabilityTheory.Kernel.id` `map` `Prod.instMeasurableSpace`	—	`ext` `compProd_apply` `ProbabilityTheory.Kernel.IsFiniteKernel.isSFiniteKernel` `ProbabilityTheory.IsZeroOrMarkovKernel.isFiniteKernel` `ProbabilityTheory.IsMarkovKernel.IsZeroOrMarkovKernel` `ProbabilityTheory.Kernel.instIsMarkovKernelId` `map_apply` `Measurable.prod` `measurable_id` `measurable_prodMk_left` `ProbabilityTheory.Kernel.id_apply` `dirac_apply'` `MeasureTheory.lintegral_indicator_one`
`compProd_of_not_isSFiniteKernel` 📖	mathematical	`ProbabilityTheory.IsSFiniteKernel`	`compProd` `MeasureTheory.Measure` `Prod.instMeasurableSpace` `instZero`	—	`compProd.eq_1` `ProbabilityTheory.Kernel.compProd_of_not_isSFiniteKernel_right` `ProbabilityTheory.Kernel.isSFiniteKernel_prodMkLeft_unit` `ProbabilityTheory.Kernel.zero_apply`
`compProd_of_not_sfinite` 📖	mathematical	`MeasureTheory.SFinite`	`compProd` `MeasureTheory.Measure` `Prod.instMeasurableSpace` `instZero`	—	`compProd.eq_1` `ProbabilityTheory.Kernel.compProd_of_not_isSFiniteKernel_left` `ProbabilityTheory.Kernel.isSFiniteKernel_const` `ProbabilityTheory.Kernel.zero_apply`
`compProd_smul_left` 📖	mathematical	—	`compProd` `ENNReal` `MeasureTheory.Measure` `instSMul` `Algebra.toSMul` `ENNReal.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `IsScalarTower.right` `Prod.instMeasurableSpace`	—	`ext` `IsScalarTower.right` `compProd_apply` `MeasureTheory.instSFiniteHSMulENNRealMeasure` `MeasureTheory.lintegral_smul_measure`
`compProd_sum_left` 📖	mathematical	`MeasureTheory.SFinite`	`compProd` `sum` `Prod.instMeasurableSpace`	—	`compProd.eq_1` `ProbabilityTheory.Kernel.sum_const` `ProbabilityTheory.Kernel.compProd_sum_left` `ProbabilityTheory.Kernel.const.instIsSFiniteKernel`
`compProd_sum_right` 📖	mathematical	`ProbabilityTheory.IsSFiniteKernel`	`compProd` `ProbabilityTheory.Kernel.sum` `sum` `Prod.instMeasurableSpace`	—	`compProd.eq_1` `ProbabilityTheory.Kernel.sum_prodMkLeft` `ProbabilityTheory.Kernel.compProd_sum_right` `ProbabilityTheory.Kernel.IsSFiniteKernel.prodMkLeft`
`compProd_zero_left` 📖	mathematical	—	`compProd` `MeasureTheory.Measure` `instZero` `Prod.instMeasurableSpace`	—	`ProbabilityTheory.Kernel.const_zero` `ProbabilityTheory.Kernel.compProd_zero_left`
`compProd_zero_right` 📖	mathematical	—	`compProd` `ProbabilityTheory.Kernel` `ProbabilityTheory.Kernel.instZero` `MeasureTheory.Measure` `Prod.instMeasurableSpace` `instZero`	—	`ProbabilityTheory.Kernel.prodMkLeft_zero` `ProbabilityTheory.Kernel.compProd_zero_right`
`dirac_compProd_apply` 📖	mathematical	`MeasurableSet` `Prod.instMeasurableSpace`	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `instFunLike` `compProd` `dirac` `ProbabilityTheory.Kernel` `ProbabilityTheory.Kernel.instFunLike` `Set.preimage`	—	`compProd_apply` `MeasureTheory.instSFiniteOfSigmaFinite` `dirac.instSigmaFinite` `MeasureTheory.lintegral_dirac`
`dirac_unit_compProd` 📖	mathematical	—	`compProd` `PUnit.instMeasurableSpace` `dirac` `map` `Prod.instMeasurableSpace` `DFunLike.coe` `ProbabilityTheory.Kernel` `MeasureTheory.Measure` `ProbabilityTheory.Kernel.instFunLike`	—	`ext` `dirac_compProd_apply` `instMeasurableSingletonClassOfMeasurableEq` `instMeasurableEqOfSecondCountableTopologyOfT2Space` `BorelSpace.opensMeasurable` `Unit.borelSpace` `TopologicalSpace.instSecondCountableTopologyOfLindelofSpaceOfPseudoMetrizableSpace` `Countable.LindelofSpace` `instCountablePUnit` `PseudoEMetricSpace.pseudoMetrizableSpace` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `map_apply` `measurable_prodMk_left`
`dirac_unit_compProd_const` 📖	mathematical	—	`compProd` `PUnit.instMeasurableSpace` `dirac` `ProbabilityTheory.Kernel.const` `map` `Prod.instMeasurableSpace`	—	`dirac_unit_compProd` `ProbabilityTheory.Kernel.const.instIsSFiniteKernel` `ProbabilityTheory.Kernel.const_apply`
`fst_compProd` 📖	mathematical	—	`fst` `compProd`	—	`ext` `compProd.eq_1` `fst.eq_1` `ProbabilityTheory.Kernel.fst_apply` `ProbabilityTheory.Kernel.fst_compProd` `ProbabilityTheory.Kernel.const.instIsSFiniteKernel` `ProbabilityTheory.Kernel.IsMarkovKernel.prodMkLeft` `ProbabilityTheory.Kernel.const_apply`
`instIsFiniteMeasureProdCompProdOfIsFiniteKernel` 📖	mathematical	—	`MeasureTheory.IsFiniteMeasure` `Prod.instMeasurableSpace` `compProd`	—	`compProd.eq_1` `ProbabilityTheory.IsFiniteKernel.isFiniteMeasure` `ProbabilityTheory.Kernel.IsFiniteKernel.compProd` `ProbabilityTheory.Kernel.const.instIsFiniteKernel` `ProbabilityTheory.Kernel.IsFiniteKernel.prodMkLeft`
`instIsProbabilityMeasureProdCompProdOfIsMarkovKernel` 📖	mathematical	—	`MeasureTheory.IsProbabilityMeasure` `Prod.instMeasurableSpace` `compProd`	—	`compProd.eq_1` `ProbabilityTheory.IsMarkovKernel.is_probability_measure'` `ProbabilityTheory.Kernel.IsMarkovKernel.compProd` `ProbabilityTheory.Kernel.const.instIsMarkovKernel` `ProbabilityTheory.Kernel.IsMarkovKernel.prodMkLeft`
`instIsZeroOrProbabilityMeasureProdCompProdOfIsZeroOrMarkovKernel` 📖	mathematical	—	`MeasureTheory.IsZeroOrProbabilityMeasure` `Prod.instMeasurableSpace` `compProd`	—	`compProd.eq_1` `ProbabilityTheory.IsZeroOrMarkovKernel.isZeroOrProbabilityMeasure` `ProbabilityTheory.Kernel.IsZeroOrMarkovKernel.compProd` `ProbabilityTheory.Kernel.const.instIsZeroOrMarkovKernel` `ProbabilityTheory.Kernel.IsZeroOrMarkovKernel.prodMkLeft`
`instSFiniteProdCompProd` 📖	mathematical	—	`MeasureTheory.SFinite` `Prod.instMeasurableSpace` `compProd`	—	`compProd.eq_1` `ProbabilityTheory.IsSFiniteKernel.sFinite` `ProbabilityTheory.Kernel.IsSFiniteKernel.compProd`
`lintegral_compProd` 📖	mathematical	`Measurable` `ENNReal` `Prod.instMeasurableSpace` `ENNReal.measurableSpace`	`MeasureTheory.lintegral` `compProd` `DFunLike.coe` `ProbabilityTheory.Kernel` `MeasureTheory.Measure` `ProbabilityTheory.Kernel.instFunLike`	—	`compProd.eq_1` `ProbabilityTheory.Kernel.lintegral_compProd` `ProbabilityTheory.Kernel.const.instIsSFiniteKernel` `ProbabilityTheory.Kernel.IsSFiniteKernel.prodMkLeft`
`mutuallySingular_compProd_iff` 📖	mathematical	—	`MutuallySingular` `Prod.instMeasurableSpace` `compProd`	—	`haveLebesgueDecomposition_add` `haveLebesgueDecomposition_of_sigmaFinite` `MeasureTheory.instSFiniteOfSigmaFinite` `compProd_add_left` `singularPart.instSigmaFinite` `withDensity.instSFinite` `MutuallySingular.add_left_iff` `MutuallySingular.compProd_of_left` `mutuallySingular_singularPart` `AbsolutelyContinuous.mutuallySingular_compProd_iff` `withDensity.instSigmaFinite` `MeasureTheory.withDensity_absolutelyContinuous` `MutuallySingular.mono_ac` `AbsolutelyContinuous.compProd_left` `AbsolutelyContinuous.withDensity_rnDeriv` `absolutelyContinuous_of_le` `withDensity_rnDeriv_le`
`mutuallySingular_compProd_left_iff` 📖	mathematical	`MeasureTheory.Measure` `instZero` `DFunLike.coe` `ProbabilityTheory.Kernel` `ProbabilityTheory.Kernel.instFunLike`	`MutuallySingular` `Prod.instMeasurableSpace` `compProd`	—	`withDensity_rnDeriv_eq_zero` `haveLebesgueDecomposition_of_sigmaFinite` `instOuterMeasureClass` `mutuallySingular_of_mutuallySingular_compProd` `MeasureTheory.instSFiniteOfSigmaFinite` `absolutelyContinuous_of_le` `withDensity_rnDeriv_le` `MeasureTheory.withDensity_absolutelyContinuous` `MeasureTheory.ae_eq_bot` `Filter.eventually_false_iff_eq_bot` `MutuallySingular.compProd_of_left`
`mutuallySingular_of_mutuallySingular_compProd` 📖	mathematical	`MutuallySingular` `Prod.instMeasurableSpace` `compProd` `AbsolutelyContinuous`	`Filter.Eventually` `DFunLike.coe` `ProbabilityTheory.Kernel` `MeasureTheory.Measure` `ProbabilityTheory.Kernel.instFunLike` `MeasureTheory.ae` `instFunLike` `instOuterMeasureClass`	—	`MutuallySingular.measurableSet_nullSet` `MutuallySingular.measure_nullSet` `MutuallySingular.measure_compl_nullSet` `Filter.mp_mem` `instOuterMeasureClass` `MeasureTheory.lintegral_eq_zero_iff'` `Measurable.aemeasurable` `ProbabilityTheory.Kernel.measurable_kernel_prodMk_left` `MeasurableSet.compl` `compProd_apply` `Filter.univ_mem'` `measurable_prodMk_left`
`setLIntegral_compProd` 📖	mathematical	`Measurable` `ENNReal` `Prod.instMeasurableSpace` `ENNReal.measurableSpace` `MeasurableSet`	`MeasureTheory.lintegral` `restrict` `compProd` `SProd.sprod` `Set` `Set.instSProd` `DFunLike.coe` `ProbabilityTheory.Kernel` `MeasureTheory.Measure` `ProbabilityTheory.Kernel.instFunLike`	—	`compProd.eq_1` `ProbabilityTheory.Kernel.setLIntegral_compProd` `ProbabilityTheory.Kernel.const.instIsSFiniteKernel` `ProbabilityTheory.Kernel.IsSFiniteKernel.prodMkLeft`
`snd_dirac_unit_compProd_const` 📖	mathematical	—	`snd` `PUnit.instMeasurableSpace` `compProd` `dirac` `ProbabilityTheory.Kernel.const`	—	`compProd_const` `MeasureTheory.instSFiniteOfCountable` `instCountablePUnit` `snd_prod` `dirac.isProbabilityMeasure`

MeasureTheory.Measure.AbsolutelyContinuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`compProd` 📖	mathematical	`MeasureTheory.Measure.AbsolutelyContinuous` `Filter.Eventually` `DFunLike.coe` `ProbabilityTheory.Kernel` `MeasureTheory.Measure` `ProbabilityTheory.Kernel.instFunLike` `MeasureTheory.ae` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	`Prod.instMeasurableSpace` `MeasureTheory.Measure.compProd`	—	`MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.sFinite_of_absolutelyContinuous` `trans` `compProd_right` `compProd_left`
`compProd_left` 📖	mathematical	`MeasureTheory.Measure.AbsolutelyContinuous`	`Prod.instMeasurableSpace` `MeasureTheory.Measure.compProd`	—	`MeasureTheory.sFinite_of_absolutelyContinuous` `MeasureTheory.Measure.compProd_apply` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.lintegral_eq_zero_iff` `ProbabilityTheory.Kernel.measurable_kernel_prodMk_left` `ae_eq` `MeasureTheory.Measure.compProd_of_not_isSFiniteKernel`
`compProd_of_compProd` 📖	—	`MeasureTheory.Measure.AbsolutelyContinuous` `Prod.instMeasurableSpace` `MeasureTheory.Measure.compProd`	—	—	`MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.measure_eq_zero_iff_ae_notMem` `MeasureTheory.Measure.ae_compProd_iff` `MeasurableSet.compl` `ae_le` `MeasureTheory.Measure.compProd_of_not_sfinite`
`compProd_right` 📖	mathematical	`Filter.Eventually` `MeasureTheory.Measure.AbsolutelyContinuous` `DFunLike.coe` `ProbabilityTheory.Kernel` `MeasureTheory.Measure` `ProbabilityTheory.Kernel.instFunLike` `MeasureTheory.ae` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	`Prod.instMeasurableSpace` `MeasureTheory.Measure.compProd`	—	`MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.Measure.compProd_apply` `MeasureTheory.lintegral_eq_zero_iff` `ProbabilityTheory.Kernel.measurable_kernel_prodMk_left` `Filter.mp_mem` `Filter.univ_mem'` `MeasureTheory.Measure.compProd_of_not_isSFiniteKernel`
`mutuallySingular_compProd_iff` 📖	mathematical	`MeasureTheory.Measure.AbsolutelyContinuous`	`MeasureTheory.Measure.MutuallySingular` `Prod.instMeasurableSpace` `MeasureTheory.Measure.compProd`	—	`MeasureTheory.Measure.haveLebesgueDecomposition_add` `MeasureTheory.Measure.haveLebesgueDecomposition_of_sigmaFinite` `MeasureTheory.instSFiniteOfSigmaFinite` `MeasureTheory.Measure.compProd_add_left` `MeasureTheory.Measure.singularPart.instSigmaFinite` `MeasureTheory.Measure.withDensity.instSFinite` `MeasureTheory.Measure.MutuallySingular.add_right_iff` `MeasureTheory.Measure.MutuallySingular.compProd_of_left` `MeasureTheory.Measure.MutuallySingular.symm` `MeasureTheory.Measure.mutuallySingular_singularPart` `MeasureTheory.Measure.MutuallySingular.mono_ac` `rfl` `compProd_left` `MeasureTheory.Measure.absolutelyContinuous_withDensity_rnDeriv` `MeasureTheory.withDensity_absolutelyContinuous`

MeasureTheory.Measure.MutuallySingular

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`compProd_of_left` 📖	mathematical	`MeasureTheory.Measure.MutuallySingular`	`Prod.instMeasurableSpace` `MeasureTheory.Measure.compProd`	—	`MeasurableSet.prod` `measurableSet_nullSet` `MeasurableSet.univ` `MeasureTheory.Measure.compProd_apply_prod` `Set.compl_prod_eq_union` `restrict_nullSet` `MeasureTheory.lintegral_zero_measure` `Set.compl_univ` `Set.prod_empty` `Set.union_empty` `MeasurableSet.compl` `restrict_compl_nullSet` `MeasureTheory.Measure.compProd_of_not_isSFiniteKernel` `MeasureTheory.Measure.compProd_of_not_sfinite`

ProbabilityTheory

Definitions

Name	Category	Theorems
`«term_⊗ₘ_»` 📖	CompOp	—

ProbabilityTheory.Kernel

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`compProd_apply_eq_compProd_sectR` 📖	mathematical	—	`DFunLike.coe` `ProbabilityTheory.Kernel` `Prod.instMeasurableSpace` `MeasureTheory.Measure` `instFunLike` `compProd` `MeasureTheory.Measure.compProd` `sectR`	—	`MeasureTheory.Measure.ext` `compProd_apply` `MeasureTheory.Measure.compProd_apply` `ProbabilityTheory.IsSFiniteKernel.sFinite` `instIsSFiniteKernelSectROfProd`

---

← Back to Index