MeasureComp

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

Statistics

Metric	Count
Definitions	0
Theorems `comp`, `comp_left`, `comp_right`, `absolutelyContinuous_comp_of_countable`, `add_comp`, `add_comp'`, `ae_ae_of_ae_comp`, `ae_comp_iff`, `ae_comp_of_ae_ae`, `compProd_deterministic`, `compProd_eq_comp_prod`, `compProd_id_eq_copy_comp`, `comp_add`, `comp_assoc`, `comp_compProd_comm`, `comp_congr`, `comp_eq_comp_const_apply`, `comp_eq_sum_of_countable`, `comp_smul`, `copy_comp_map`, `discard_comp`, `instIsFiniteMeasureBindCoeKernelOfIsFiniteKernel`, `instIsProbabilityMeasureBindCoeKernelOfIsMarkovKernel`, `instIsZeroOrProbabilityMeasureBindCoeKernelOfIsZeroOrMarkovKernel`, `instSFiniteBindCoeKernelOfIsSFiniteKernel`, `map_comp`, `prodMkLeft_comp_compProd`, `snd_compProd`, `comp_boolKernel`, `comp_const`, `absolutelyContinuous_boolKernel_comp_left`, `absolutelyContinuous_boolKernel_comp_right`, `boolKernel_comp_measure`	33
Total	33

MeasureTheory.Measure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`absolutelyContinuous_comp_of_countable` 📖	mathematical	—	`Filter.Eventually` `AbsolutelyContinuous` `DFunLike.coe` `ProbabilityTheory.Kernel` `MeasureTheory.Measure` `ProbabilityTheory.Kernel.instFunLike` `bind` `MeasureTheory.ae` `instFunLike` `instOuterMeasureClass`	—	`instOuterMeasureClass` `IsScalarTower.right` `comp_eq_sum_of_countable` `MeasureTheory.ae_iff_of_countable` `absolutelyContinuous_sum_right` `absolutelyContinuous_smul`
`add_comp` 📖	mathematical	—	`bind` `DFunLike.coe` `ProbabilityTheory.Kernel` `MeasureTheory.Measure` `ProbabilityTheory.Kernel.instFunLike` `ProbabilityTheory.Kernel.instAdd` `instAdd`	—	`comp_eq_comp_const_apply` `ProbabilityTheory.Kernel.comp_add_left`
`add_comp'` 📖	mathematical	—	`bind` `Pi.instAdd` `MeasureTheory.Measure` `instAdd` `DFunLike.coe` `ProbabilityTheory.Kernel` `ProbabilityTheory.Kernel.instFunLike`	—	`ProbabilityTheory.Kernel.coe_add` `add_comp`
`ae_ae_of_ae_comp` 📖	—	`Filter.Eventually` `MeasureTheory.ae` `MeasureTheory.Measure` `instFunLike` `instOuterMeasureClass` `bind` `DFunLike.coe` `ProbabilityTheory.Kernel` `ProbabilityTheory.Kernel.instFunLike`	—	—	`instOuterMeasureClass` `ProbabilityTheory.Kernel.ae_ae_of_ae_comp` `comp_eq_comp_const_apply`
`ae_comp_iff` 📖	mathematical	`MeasurableSet` `setOf`	`Filter.Eventually` `MeasureTheory.ae` `MeasureTheory.Measure` `instFunLike` `instOuterMeasureClass` `bind` `DFunLike.coe` `ProbabilityTheory.Kernel` `ProbabilityTheory.Kernel.instFunLike`	—	`instOuterMeasureClass` `ae_ae_of_ae_comp` `ae_comp_of_ae_ae`
`ae_comp_of_ae_ae` 📖	mathematical	`MeasurableSet` `setOf` `Filter.Eventually` `MeasureTheory.ae` `MeasureTheory.Measure` `instFunLike` `instOuterMeasureClass` `DFunLike.coe` `ProbabilityTheory.Kernel` `ProbabilityTheory.Kernel.instFunLike`	`bind`	—	`instOuterMeasureClass` `comp_eq_comp_const_apply` `ProbabilityTheory.Kernel.ae_comp_of_ae_ae`
`compProd_deterministic` 📖	mathematical	`Measurable`	`compProd` `ProbabilityTheory.Kernel.deterministic` `map` `Prod.instMeasurableSpace`	—	`compProd_eq_comp_prod` `ProbabilityTheory.Kernel.IsFiniteKernel.isSFiniteKernel` `ProbabilityTheory.IsZeroOrMarkovKernel.isFiniteKernel` `ProbabilityTheory.IsMarkovKernel.IsZeroOrMarkovKernel` `ProbabilityTheory.Kernel.isMarkovKernel_deterministic` `measurable_id` `ProbabilityTheory.Kernel.id.eq_1` `Measurable.prodMk` `ProbabilityTheory.Kernel.deterministic_prod_deterministic` `deterministic_comp_eq_map`
`compProd_eq_comp_prod` 📖	mathematical	—	`compProd` `bind` `Prod.instMeasurableSpace` `DFunLike.coe` `ProbabilityTheory.Kernel` `MeasureTheory.Measure` `ProbabilityTheory.Kernel.instFunLike` `ProbabilityTheory.Kernel.prod` `ProbabilityTheory.Kernel.id`	—	`compProd.eq_1` `ProbabilityTheory.Kernel.compProd_prodMkLeft_eq_comp` `ProbabilityTheory.Kernel.const.instIsSFiniteKernel`
`compProd_id_eq_copy_comp` 📖	mathematical	—	`compProd` `ProbabilityTheory.Kernel.id` `bind` `Prod.instMeasurableSpace` `DFunLike.coe` `ProbabilityTheory.Kernel` `MeasureTheory.Measure` `ProbabilityTheory.Kernel.instFunLike` `ProbabilityTheory.Kernel.copy`	—	`compProd_id` `ProbabilityTheory.Kernel.copy.eq_1` `deterministic_comp_eq_map`
`comp_add` 📖	mathematical	—	`bind` `MeasureTheory.Measure` `instAdd` `DFunLike.coe` `ProbabilityTheory.Kernel` `ProbabilityTheory.Kernel.instFunLike`	—	`comp_eq_comp_const_apply` `ProbabilityTheory.Kernel.const_add` `ProbabilityTheory.Kernel.comp_add_right`
`comp_assoc` 📖	mathematical	—	`bind` `DFunLike.coe` `ProbabilityTheory.Kernel` `MeasureTheory.Measure` `ProbabilityTheory.Kernel.instFunLike` `ProbabilityTheory.Kernel.comp`	—	`bind_bind` `ProbabilityTheory.Kernel.aemeasurable`
`comp_compProd_comm` 📖	mathematical	—	`bind` `Prod.instMeasurableSpace` `compProd` `DFunLike.coe` `ProbabilityTheory.Kernel` `MeasureTheory.Measure` `ProbabilityTheory.Kernel.instFunLike` `snd` `ProbabilityTheory.Kernel.compProd`	—	`ext` `bind_apply` `ProbabilityTheory.Kernel.aemeasurable` `snd_apply` `measurable_snd` `lintegral_compProd` `ProbabilityTheory.Kernel.measurable_coe` `ProbabilityTheory.Kernel.compProd_apply` `compProd_of_not_isSFiniteKernel` `bind_zero_left` `ProbabilityTheory.Kernel.compProd_of_not_isSFiniteKernel_left` `bind_zero_right` `snd_zero`
`comp_congr` 📖	mathematical	`Filter.Eventually` `MeasureTheory.Measure` `DFunLike.coe` `ProbabilityTheory.Kernel` `ProbabilityTheory.Kernel.instFunLike` `MeasureTheory.ae` `instFunLike` `instOuterMeasureClass`	`bind`	—	`instOuterMeasureClass` `bind_congr_right`
`comp_eq_comp_const_apply` 📖	mathematical	—	`bind` `DFunLike.coe` `ProbabilityTheory.Kernel` `MeasureTheory.Measure` `ProbabilityTheory.Kernel.instFunLike` `PUnit.instMeasurableSpace` `ProbabilityTheory.Kernel.comp` `ProbabilityTheory.Kernel.const`	—	`ProbabilityTheory.Kernel.comp_apply` `ProbabilityTheory.Kernel.const_apply`
`comp_eq_sum_of_countable` 📖	mathematical	—	`bind` `DFunLike.coe` `ProbabilityTheory.Kernel` `MeasureTheory.Measure` `ProbabilityTheory.Kernel.instFunLike` `sum` `ENNReal` `instSMul` `Algebra.toSMul` `ENNReal.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `IsScalarTower.right` `Set` `instFunLike` `Set.instSingletonSet`	—	`ext` `IsScalarTower.right` `sum_apply` `bind_apply` `Measurable.aemeasurable` `ProbabilityTheory.Kernel.measurable` `MeasureTheory.lintegral_countable'` `mul_comm`
`comp_smul` 📖	mathematical	—	`bind` `ENNReal` `MeasureTheory.Measure` `instSMul` `Algebra.toSMul` `ENNReal.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `IsScalarTower.right` `DFunLike.coe` `ProbabilityTheory.Kernel` `ProbabilityTheory.Kernel.instFunLike`	—	`ext` `IsScalarTower.right` `bind_apply` `ProbabilityTheory.Kernel.aemeasurable` `MeasureTheory.lintegral_smul_measure`
`copy_comp_map` 📖	mathematical	`AEMeasurable`	`bind` `Prod.instMeasurableSpace` `map` `DFunLike.coe` `ProbabilityTheory.Kernel` `MeasureTheory.Measure` `ProbabilityTheory.Kernel.instFunLike` `ProbabilityTheory.Kernel.copy`	—	`ProbabilityTheory.Kernel.copy.eq_1` `deterministic_comp_eq_map` `AEMeasurable.map_map_of_aemeasurable` `AEMeasurable.prodMk` `aemeasurable_id`
`discard_comp` 📖	mathematical	—	`bind` `PUnit.instMeasurableSpace` `DFunLike.coe` `ProbabilityTheory.Kernel` `MeasureTheory.Measure` `ProbabilityTheory.Kernel.instFunLike` `ProbabilityTheory.Kernel.discard` `ENNReal` `instSMul` `Algebra.toSMul` `ENNReal.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `IsScalarTower.right` `Set` `instFunLike` `Set.univ` `dirac`	—	`ext` `IsScalarTower.right` `bind_apply` `ProbabilityTheory.Kernel.aemeasurable` `ProbabilityTheory.Kernel.discard_apply` `dirac_apply'` `MeasureTheory.lintegral_const` `mul_comm`
`instIsFiniteMeasureBindCoeKernelOfIsFiniteKernel` 📖	mathematical	—	`MeasureTheory.IsFiniteMeasure` `bind` `DFunLike.coe` `ProbabilityTheory.Kernel` `MeasureTheory.Measure` `ProbabilityTheory.Kernel.instFunLike`	—	`snd_compProd` `MeasureTheory.instSFiniteOfSigmaFinite` `MeasureTheory.IsFiniteMeasure.toSigmaFinite` `ProbabilityTheory.Kernel.IsFiniteKernel.isSFiniteKernel` `snd.instIsFiniteMeasure` `instIsFiniteMeasureProdCompProdOfIsFiniteKernel`
`instIsProbabilityMeasureBindCoeKernelOfIsMarkovKernel` 📖	mathematical	—	`MeasureTheory.IsProbabilityMeasure` `bind` `DFunLike.coe` `ProbabilityTheory.Kernel` `MeasureTheory.Measure` `ProbabilityTheory.Kernel.instFunLike`	—	`snd_compProd` `MeasureTheory.instSFiniteOfSigmaFinite` `MeasureTheory.IsFiniteMeasure.toSigmaFinite` `MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure` `MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure` `ProbabilityTheory.Kernel.IsFiniteKernel.isSFiniteKernel` `ProbabilityTheory.IsZeroOrMarkovKernel.isFiniteKernel` `ProbabilityTheory.IsMarkovKernel.IsZeroOrMarkovKernel` `snd.instIsProbabilityMeasure` `instIsProbabilityMeasureProdCompProdOfIsMarkovKernel`
`instIsZeroOrProbabilityMeasureBindCoeKernelOfIsZeroOrMarkovKernel` 📖	mathematical	—	`MeasureTheory.IsZeroOrProbabilityMeasure` `bind` `DFunLike.coe` `ProbabilityTheory.Kernel` `MeasureTheory.Measure` `ProbabilityTheory.Kernel.instFunLike`	—	`snd_compProd` `MeasureTheory.instSFiniteOfSigmaFinite` `MeasureTheory.IsFiniteMeasure.toSigmaFinite` `MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure` `ProbabilityTheory.Kernel.IsFiniteKernel.isSFiniteKernel` `ProbabilityTheory.IsZeroOrMarkovKernel.isFiniteKernel` `snd.instIsZeroOrProbabilityMeasure` `instIsZeroOrProbabilityMeasureProdCompProdOfIsZeroOrMarkovKernel`
`instSFiniteBindCoeKernelOfIsSFiniteKernel` 📖	mathematical	—	`MeasureTheory.SFinite` `bind` `DFunLike.coe` `ProbabilityTheory.Kernel` `MeasureTheory.Measure` `ProbabilityTheory.Kernel.instFunLike`	—	`snd_compProd` `instSFiniteSndOfProd` `instSFiniteProdCompProd`
`map_comp` 📖	mathematical	`Measurable`	`map` `bind` `DFunLike.coe` `ProbabilityTheory.Kernel` `MeasureTheory.Measure` `ProbabilityTheory.Kernel.instFunLike` `ProbabilityTheory.Kernel.map`	—	`ext` `map_apply` `bind_apply` `ProbabilityTheory.Kernel.aemeasurable` `ProbabilityTheory.Kernel.map_apply'`
`prodMkLeft_comp_compProd` 📖	mathematical	—	`bind` `Prod.instMeasurableSpace` `compProd` `DFunLike.coe` `ProbabilityTheory.Kernel` `MeasureTheory.Measure` `ProbabilityTheory.Kernel.instFunLike` `ProbabilityTheory.Kernel.prodMkLeft`	—	`snd_compProd` `measurable_snd` `ProbabilityTheory.Kernel.prodMkLeft.eq_1` `snd.eq_1` `deterministic_comp_eq_map` `comp_assoc` `ProbabilityTheory.Kernel.comp_deterministic_eq_comap`
`snd_compProd` 📖	mathematical	—	`snd` `compProd` `bind` `DFunLike.coe` `ProbabilityTheory.Kernel` `MeasureTheory.Measure` `ProbabilityTheory.Kernel.instFunLike`	—	`ext` `bind_apply` `ProbabilityTheory.Kernel.aemeasurable` `snd_apply` `compProd_apply` `measurable_snd`

MeasureTheory.Measure.AbsolutelyContinuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp` 📖	mathematical	`MeasureTheory.Measure.AbsolutelyContinuous` `Filter.Eventually` `DFunLike.coe` `ProbabilityTheory.Kernel` `MeasureTheory.Measure` `ProbabilityTheory.Kernel.instFunLike` `MeasureTheory.ae` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	`MeasureTheory.Measure.bind`	—	`MeasureTheory.Measure.instOuterMeasureClass` `trans` `comp_left` `comp_right`
`comp_left` 📖	mathematical	`Filter.Eventually` `MeasureTheory.Measure.AbsolutelyContinuous` `DFunLike.coe` `ProbabilityTheory.Kernel` `MeasureTheory.Measure` `ProbabilityTheory.Kernel.instFunLike` `MeasureTheory.ae` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	`MeasureTheory.Measure.bind`	—	`MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.Measure.bind_apply` `ProbabilityTheory.Kernel.aemeasurable` `MeasureTheory.lintegral_eq_zero_iff` `ProbabilityTheory.Kernel.measurable_coe` `Filter.mp_mem` `Filter.univ_mem'`
`comp_right` 📖	mathematical	`MeasureTheory.Measure.AbsolutelyContinuous`	`MeasureTheory.Measure.bind` `DFunLike.coe` `ProbabilityTheory.Kernel` `MeasureTheory.Measure` `ProbabilityTheory.Kernel.instFunLike`	—	`MeasureTheory.Measure.bind_apply` `ProbabilityTheory.Kernel.aemeasurable` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.lintegral_eq_zero_iff` `ProbabilityTheory.Kernel.measurable_coe` `ae_eq`

ProbabilityTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`absolutelyContinuous_boolKernel_comp_left` 📖	mathematical	—	`MeasureTheory.Measure.AbsolutelyContinuous` `MeasureTheory.Measure.bind` `Bool.instMeasurableSpace` `DFunLike.coe` `Kernel` `MeasureTheory.Measure` `Kernel.instFunLike` `Kernel.boolKernel`	—	`IsScalarTower.right` `MeasureTheory.Measure.AbsolutelyContinuous.add_right` `MeasureTheory.Measure.absolutelyContinuous_smul` `add_comm` `boolKernel_comp_measure`
`absolutelyContinuous_boolKernel_comp_right` 📖	mathematical	—	`MeasureTheory.Measure.AbsolutelyContinuous` `MeasureTheory.Measure.bind` `Bool.instMeasurableSpace` `DFunLike.coe` `Kernel` `MeasureTheory.Measure` `Kernel.instFunLike` `Kernel.boolKernel`	—	`IsScalarTower.right` `MeasureTheory.Measure.AbsolutelyContinuous.add_right` `MeasureTheory.Measure.absolutelyContinuous_smul` `boolKernel_comp_measure`
`boolKernel_comp_measure` 📖	mathematical	—	`MeasureTheory.Measure.bind` `Bool.instMeasurableSpace` `DFunLike.coe` `Kernel` `MeasureTheory.Measure` `Kernel.instFunLike` `Kernel.boolKernel` `MeasureTheory.Measure.instAdd` `ENNReal` `MeasureTheory.Measure.instSMul` `Algebra.toSMul` `ENNReal.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `IsScalarTower.right` `Set` `MeasureTheory.Measure.instFunLike` `Set.instSingletonSet`	—	`MeasureTheory.Measure.ext` `IsScalarTower.right` `MeasureTheory.Measure.bind_apply` `Kernel.aemeasurable` `MeasureTheory.lintegral_fintype` `Bool.instMeasurableSingletonClass` `Finset.sum_insert` `Finset.sum_singleton` `mul_comm`

ProbabilityTheory.Kernel

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_boolKernel` 📖	mathematical	—	`comp` `Bool.instMeasurableSpace` `boolKernel` `MeasureTheory.Measure.bind` `DFunLike.coe` `ProbabilityTheory.Kernel` `MeasureTheory.Measure` `instFunLike`	—	`ext` `comp_apply`
`comp_const` 📖	mathematical	—	`comp` `const` `MeasureTheory.Measure.bind` `DFunLike.coe` `ProbabilityTheory.Kernel` `MeasureTheory.Measure` `instFunLike`	—	—

---

← Back to Index