CondDistrib

📁 Source: Mathlib/Probability/Kernel/CondDistrib.lean

Statistics

Metric	Count
Definitions condDistrib	1
Theorems ae_integrable_condDistrib_map_iff, comp_snd_map_prodMk, integral_condDistrib, integral_condDistrib_map, comp_snd_map_prodMk, condDistrib_ae, condDistrib_ae_map, integral_condDistrib, integral_condDistrib_map, integral_norm_condDistrib, integral_norm_condDistrib_map, norm_integral_condDistrib, norm_integral_condDistrib_map, integral_condDistrib, aestronglyMeasurable_comp_snd_map_prodMk_iff, aestronglyMeasurable_integral_condDistrib, compProd_map_condDistrib, condDistrib_ae_eq_condExp, condDistrib_ae_eq_iff_measure_eq_compProd, condDistrib_ae_eq_of_measure_eq_compProd, condDistrib_ae_eq_of_measure_eq_compProd_of_measurable, condDistrib_apply_of_ne_zero, condDistrib_comp, condDistrib_comp_map, condDistrib_comp_self, condDistrib_congr, condDistrib_congr_left, condDistrib_congr_right, condDistrib_const, condDistrib_def, condDistrib_fst_prod, condDistrib_map, condDistrib_self, condDistrib_snd_prod, condExp_ae_eq_integral_condDistrib, condExp_ae_eq_integral_condDistrib', condExp_ae_eq_integral_condDistrib_id, condExp_prod_ae_eq_integral_condDistrib, condExp_prod_ae_eq_integral_condDistrib', condExp_prod_ae_eq_integral_condDistrib₀, instIsMarkovKernelCondDistrib, integrable_comp_snd_map_prodMk_iff, integrable_toReal_condDistrib, measurable_condDistrib, setLIntegral_condDistrib_of_measurableSet, setLIntegral_preimage_condDistrib, stronglyMeasurable_integral_condDistrib	47
Total	48

MeasureTheory.AEStronglyMeasurable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ae_integrable_condDistrib_map_iff 📖	mathematical	AEMeasurable MeasureTheory.AEStronglyMeasurable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Prod.instMeasurableSpace MeasureTheory.Measure.map	Filter.Eventually MeasureTheory.Integrable SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure ProbabilityTheory.Kernel.instFunLike ProbabilityTheory.condDistrib MeasureTheory.ae MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass Real Real.pseudoMetricSpace NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing MeasureTheory.integral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal Norm.norm NormedAddCommGroup.toNorm	—	MeasureTheory.Measure.instOuterMeasureClass ProbabilityTheory.condDistrib_def MeasureTheory.Measure.isFiniteMeasure_map ae_integrable_condKernel_iff MeasureTheory.Measure.fst_map_prodMk₀
comp_snd_map_prodMk 📖	mathematical	MeasureTheory.AEStronglyMeasurable	Prod.instMeasurableSpace MeasureTheory.Measure.map	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.StronglyMeasurable.comp_measurable measurable_snd MeasureTheory.Measure.map_apply MeasureTheory.Measure.map_apply_of_aemeasurable AEMeasurable.prodMk aemeasurable_id Set.univ_prod Set.mk_preimage_prod Set.preimage_univ Set.univ_inter Set.preimage_id' MeasureTheory.Measure.map_of_not_aemeasurable Mathlib.Tactic.Contrapose.contrapose₄ Measurable.comp_aemeasurable measurable_fst MeasureTheory.Measure.QuasiMeasurePreserving.ae_eq
integral_condDistrib 📖	mathematical	AEMeasurable MeasureTheory.AEStronglyMeasurable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Prod.instMeasurableSpace MeasureTheory.Measure.map	MeasureTheory.integral DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure ProbabilityTheory.Kernel.instFunLike ProbabilityTheory.condDistrib	—	comp_aemeasurable integral_condDistrib_map
integral_condDistrib_map 📖	mathematical	AEMeasurable MeasureTheory.AEStronglyMeasurable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Prod.instMeasurableSpace MeasureTheory.Measure.map	MeasureTheory.integral DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure ProbabilityTheory.Kernel.instFunLike ProbabilityTheory.condDistrib	—	MeasureTheory.Measure.fst_map_prodMk₀ ProbabilityTheory.condDistrib_def integral_condKernel MeasureTheory.Measure.isFiniteMeasure_map

MeasureTheory.Integrable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_snd_map_prodMk 📖	mathematical	MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup	Prod.instMeasurableSpace MeasureTheory.Measure.map	—	MeasureTheory.AEStronglyMeasurable.comp_snd_map_prodMk MeasureTheory.hasFiniteIntegral_iff_enorm MeasureTheory.lintegral_map' MeasureTheory.AEStronglyMeasurable.enorm AEMeasurable.prodMk aemeasurable_id MeasureTheory.Measure.map_of_not_aemeasurable Mathlib.Tactic.Contrapose.contrapose₄ Measurable.comp_aemeasurable measurable_fst
condDistrib_ae 📖	mathematical	AEMeasurable MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup Prod.instMeasurableSpace MeasureTheory.Measure.map	Filter.Eventually DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure ProbabilityTheory.Kernel.instFunLike ProbabilityTheory.condDistrib MeasureTheory.ae MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	MeasureTheory.ae_of_ae_map condDistrib_ae_map
condDistrib_ae_map 📖	mathematical	AEMeasurable MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup Prod.instMeasurableSpace MeasureTheory.Measure.map	Filter.Eventually DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure ProbabilityTheory.Kernel.instFunLike ProbabilityTheory.condDistrib MeasureTheory.ae MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	MeasureTheory.Measure.instOuterMeasureClass ProbabilityTheory.condDistrib_def MeasureTheory.Measure.fst_map_prodMk₀ condKernel_ae MeasureTheory.Measure.isFiniteMeasure_map
integral_condDistrib 📖	mathematical	AEMeasurable MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup Prod.instMeasurableSpace MeasureTheory.Measure.map	MeasureTheory.integral DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure ProbabilityTheory.Kernel.instFunLike ProbabilityTheory.condDistrib	—	comp_aemeasurable integral_condDistrib_map
integral_condDistrib_map 📖	mathematical	AEMeasurable MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup Prod.instMeasurableSpace MeasureTheory.Measure.map	MeasureTheory.integral DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure ProbabilityTheory.Kernel.instFunLike ProbabilityTheory.condDistrib	—	MeasureTheory.integrable_norm_iff MeasureTheory.AEStronglyMeasurable.integral_condDistrib_map norm_integral_condDistrib_map
integral_norm_condDistrib 📖	mathematical	AEMeasurable MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup Prod.instMeasurableSpace MeasureTheory.Measure.map	Real Real.pseudoMetricSpace NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing MeasureTheory.integral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure ProbabilityTheory.Kernel.instFunLike ProbabilityTheory.condDistrib Norm.norm NormedAddCommGroup.toNorm	—	comp_aemeasurable integral_norm_condDistrib_map
integral_norm_condDistrib_map 📖	mathematical	AEMeasurable MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup Prod.instMeasurableSpace MeasureTheory.Measure.map	Real Real.pseudoMetricSpace NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing MeasureTheory.integral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure ProbabilityTheory.Kernel.instFunLike ProbabilityTheory.condDistrib Norm.norm NormedAddCommGroup.toNorm	—	ProbabilityTheory.condDistrib_def MeasureTheory.Measure.fst_map_prodMk₀ integral_norm_condKernel MeasureTheory.Measure.isFiniteMeasure_map
norm_integral_condDistrib 📖	mathematical	AEMeasurable MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup Prod.instMeasurableSpace MeasureTheory.Measure.map	Real Real.pseudoMetricSpace NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing Norm.norm NormedAddCommGroup.toNorm MeasureTheory.integral DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure ProbabilityTheory.Kernel.instFunLike ProbabilityTheory.condDistrib	—	comp_aemeasurable norm_integral_condDistrib_map
norm_integral_condDistrib_map 📖	mathematical	AEMeasurable MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup Prod.instMeasurableSpace MeasureTheory.Measure.map	Real Real.pseudoMetricSpace NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing Norm.norm NormedAddCommGroup.toNorm MeasureTheory.integral DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure ProbabilityTheory.Kernel.instFunLike ProbabilityTheory.condDistrib	—	ProbabilityTheory.condDistrib_def MeasureTheory.Measure.fst_map_prodMk₀ norm_integral_condKernel MeasureTheory.Measure.isFiniteMeasure_map

MeasureTheory.StronglyMeasurable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
integral_condDistrib 📖	mathematical	MeasureTheory.StronglyMeasurable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Prod.instMeasurableSpace	MeasureTheory.integral DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure ProbabilityTheory.Kernel.instFunLike ProbabilityTheory.condDistrib	—	ProbabilityTheory.condDistrib_def integral_kernel_prod_right' ProbabilityTheory.Kernel.IsFiniteKernel.isSFiniteKernel ProbabilityTheory.IsZeroOrMarkovKernel.isFiniteKernel ProbabilityTheory.IsMarkovKernel.IsZeroOrMarkovKernel MeasureTheory.Measure.instIsMarkovKernelCondKernel

ProbabilityTheory

Definitions

Name	Category	Theorems
condDistrib 📖	CompOp	51 math math: condDistrib_apply_of_ne_zero, condDistrib_ae_eq_condExp, MeasureTheory.AEStronglyMeasurable.integral_condDistrib_map, condExp_ae_eq_integral_condDistrib_id, condExp_ae_eq_integral_condDistrib, stronglyMeasurable_integral_condDistrib, measurable_condDistrib, MeasureTheory.Integrable.integral_norm_condDistrib_map, MeasureTheory.Integrable.norm_integral_condDistrib, condDistrib_ae_eq_iff_measure_eq_compProd, compProd_map_condDistrib, condDistrib_ae_eq_of_measure_eq_compProd, condDistrib_comp_map, aestronglyMeasurable_integral_condDistrib, condDistrib_apply_ae_eq_condExpKernel_map, Kernel.condDistrib_trajMeasure, condDistrib_congr_left, condDistrib_comp, MeasureTheory.Integrable.integral_condDistrib_map, MeasureTheory.Integrable.condDistrib_ae, condDistrib_snd_prod, condExp_prod_ae_eq_integral_condDistrib, MeasureTheory.StronglyMeasurable.integral_condDistrib, condDistrib_ae_eq_of_measure_eq_compProd_of_measurable, condExpKernel_def, MeasureTheory.Integrable.norm_integral_condDistrib_map, MeasureTheory.Integrable.integral_norm_condDistrib, condExp_prod_ae_eq_integral_condDistrib₀, condDistrib_def, MeasureTheory.AEStronglyMeasurable.ae_integrable_condDistrib_map_iff, MeasureTheory.Integrable.integral_condDistrib, condDistrib_self, condExp_ae_eq_integral_condDistrib', condDistrib_comp_self, condDistrib_congr_right, condExpKernel_eq, condIndepFun_iff_condDistrib_prod_ae_eq_prodMkRight, condDistrib_const, MeasureTheory.AEStronglyMeasurable.integral_condDistrib, condDistrib_fst_prod, condDistrib_congr, integrable_toReal_condDistrib, condIndepFun_iff_condDistrib_prod_ae_eq_prodMkLeft, condDistrib_map, setLIntegral_condDistrib_of_measurableSet, setLIntegral_preimage_condDistrib, instIsMarkovKernelCondDistrib, MeasureTheory.Integrable.condDistrib_ae_map, condExp_prod_ae_eq_integral_condDistrib', condExpKernel_apply_eq_condDistrib, condIndepFun_iff_map_prod_eq_prod_condDistrib_prod_condDistrib

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
aestronglyMeasurable_comp_snd_map_prodMk_iff 📖	mathematical	Measurable	MeasureTheory.AEStronglyMeasurable Prod.instMeasurableSpace MeasureTheory.Measure.map	—	MeasureTheory.AEStronglyMeasurable.comp_measurable Measurable.prodMk measurable_id MeasureTheory.AEStronglyMeasurable.comp_snd_map_prodMk
aestronglyMeasurable_integral_condDistrib 📖	mathematical	AEMeasurable MeasureTheory.AEStronglyMeasurable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Prod.instMeasurableSpace MeasureTheory.Measure.map	MeasurableSpace.comap MeasureTheory.integral DFunLike.coe Kernel MeasureTheory.Measure Kernel.instFunLike condDistrib	—	MeasureTheory.AEStronglyMeasurable.comp_ae_measurable' MeasureTheory.AEStronglyMeasurable.integral_condDistrib_map
compProd_map_condDistrib 📖	mathematical	AEMeasurable	MeasureTheory.Measure.compProd MeasureTheory.Measure.map condDistrib Prod.instMeasurableSpace	—	condDistrib_def MeasureTheory.Measure.fst_map_prodMk₀ MeasureTheory.Measure.disintegrate MeasureTheory.Measure.condKernel.instIsCondKernel
condDistrib_ae_eq_condExp 📖	mathematical	Measurable MeasurableSet	Filter.EventuallyEq Real MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.real DFunLike.coe Kernel Kernel.instFunLike condDistrib MeasureTheory.condExp MeasurableSpace.comap Real.normedAddCommGroup Real.instCompleteSpace InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Set.indicator Real.instZero Set.preimage Real.instOne	—	MeasureTheory.ae_eq_condExp_of_forall_setIntegral_eq Real.instCompleteSpace Measurable.comap_le MeasureTheory.IsFiniteMeasure.toSigmaFinite MeasureTheory.isFiniteMeasure_trim MeasureTheory.Integrable.indicator MeasureTheory.integrable_const MeasureTheory.Integrable.integrableOn integrable_toReal_condDistrib Measurable.aemeasurable MeasureTheory.integral_toReal Measurable.mono measurable_condDistrib le_rfl Filter.Eventually.of_forall MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.measure_lt_top IsFiniteKernel.isFiniteMeasure IsZeroOrMarkovKernel.isFiniteKernel IsMarkovKernel.IsZeroOrMarkovKernel instIsMarkovKernelCondDistrib MeasureTheory.integral_indicator_const MeasureTheory.measureReal_restrict_apply smul_eq_mul mul_one Set.inter_comm setLIntegral_condDistrib_of_measurableSet MeasureTheory.measureReal_def Measurable.aestronglyMeasurable PseudoEMetricSpace.pseudoMetrizableSpace instSecondCountableTopologyReal BorelSpace.opensMeasurable Real.borelSpace Measurable.ennreal_toReal
condDistrib_ae_eq_iff_measure_eq_compProd 📖	mathematical	AEMeasurable	Filter.EventuallyEq MeasureTheory.Measure MeasureTheory.ae MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.map DFunLike.coe Kernel Kernel.instFunLike condDistrib Prod.instMeasurableSpace MeasureTheory.Measure.compProd	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.compProd_congr Kernel.IsFiniteKernel.isSFiniteKernel IsZeroOrMarkovKernel.isFiniteKernel IsMarkovKernel.IsZeroOrMarkovKernel instIsMarkovKernelCondDistrib Filter.EventuallyEq.symm compProd_map_condDistrib condDistrib_ae_eq_of_measure_eq_compProd
condDistrib_ae_eq_of_measure_eq_compProd 📖	mathematical	AEMeasurable MeasureTheory.Measure.map Prod.instMeasurableSpace MeasureTheory.Measure.compProd	Filter.EventuallyEq MeasureTheory.Measure MeasureTheory.ae MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass DFunLike.coe Kernel Kernel.instFunLike condDistrib	—	MeasureTheory.Measure.instOuterMeasureClass condDistrib_ae_eq_of_measure_eq_compProd_of_measurable MeasureTheory.Measure.map_congr Filter.mp_mem Filter.univ_mem' condDistrib_congr MeasureTheory.ae.congr_simp MeasureTheory.Measure.map_of_not_aemeasurable MeasureTheory.ae_zero
condDistrib_ae_eq_of_measure_eq_compProd_of_measurable 📖	mathematical	Measurable MeasureTheory.Measure.map Prod.instMeasurableSpace MeasureTheory.Measure.compProd	Filter.EventuallyEq MeasureTheory.Measure MeasureTheory.ae MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass DFunLike.coe Kernel Kernel.instFunLike condDistrib	—	MeasureTheory.Measure.ext MeasureTheory.Measure.map_apply MeasureTheory.Measure.fst_apply Measurable.prod measurable_fst MeasureTheory.Measure.instOuterMeasureClass condDistrib_def Filter.EventuallyEq.symm eq_condKernel_of_measure_eq_compProd
condDistrib_apply_of_ne_zero 📖	mathematical	Measurable	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike Kernel Kernel.instFunLike condDistrib Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.instInv MeasureTheory.Measure.map Set.instSingletonSet Prod.instMeasurableSpace SProd.sprod Set.instSProd	—	condDistrib_def MeasureTheory.Measure.condKernel_apply_of_ne_zero MeasureTheory.Measure.fst_map_prodMk
condDistrib_comp 📖	mathematical	AEMeasurable Measurable	Filter.EventuallyEq MeasureTheory.Measure MeasureTheory.ae MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.map DFunLike.coe Kernel Kernel.instFunLike condDistrib Kernel.map	—	MeasureTheory.Measure.instOuterMeasureClass condDistrib_ae_eq_of_measure_eq_compProd Measurable.comp_aemeasurable' Kernel.IsFiniteKernel.map IsZeroOrMarkovKernel.isFiniteKernel IsMarkovKernel.IsZeroOrMarkovKernel instIsMarkovKernelCondDistrib AEMeasurable.map_map_of_aemeasurable Measurable.aemeasurable Measurable.prodMap measurable_id' AEMeasurable.prodMk compProd_map_condDistrib MeasureTheory.Measure.compProd_map MeasureTheory.Measure.instSFiniteMap MeasureTheory.instSFiniteOfSigmaFinite MeasureTheory.IsFiniteMeasure.toSigmaFinite Kernel.IsFiniteKernel.isSFiniteKernel MeasureTheory.ae.congr_simp MeasureTheory.Measure.map_of_not_aemeasurable MeasureTheory.ae_zero
condDistrib_comp_map 📖	mathematical	AEMeasurable	MeasureTheory.Measure.bind MeasureTheory.Measure.map DFunLike.coe Kernel MeasureTheory.Measure Kernel.instFunLike condDistrib	—	MeasureTheory.Measure.snd_compProd MeasureTheory.Measure.instSFiniteMap MeasureTheory.instSFiniteOfSigmaFinite MeasureTheory.IsFiniteMeasure.toSigmaFinite Kernel.IsFiniteKernel.isSFiniteKernel IsZeroOrMarkovKernel.isFiniteKernel IsMarkovKernel.IsZeroOrMarkovKernel instIsMarkovKernelCondDistrib compProd_map_condDistrib MeasureTheory.Measure.snd_map_prodMk₀
condDistrib_comp_self 📖	mathematical	Measurable	Filter.EventuallyEq MeasureTheory.Measure MeasureTheory.ae MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.map DFunLike.coe Kernel Kernel.instFunLike condDistrib Kernel.deterministic	—	MeasureTheory.Measure.instOuterMeasureClass condDistrib_ae_eq_of_measure_eq_compProd Measurable.comp_aemeasurable' IsZeroOrMarkovKernel.isFiniteKernel IsMarkovKernel.IsZeroOrMarkovKernel Kernel.isMarkovKernel_deterministic MeasureTheory.Measure.compProd_deterministic MeasureTheory.Measure.instSFiniteMap MeasureTheory.instSFiniteOfSigmaFinite MeasureTheory.IsFiniteMeasure.toSigmaFinite AEMeasurable.map_map_of_aemeasurable AEMeasurable.prodMk aemeasurable_id Measurable.aemeasurable MeasureTheory.ae.congr_simp MeasureTheory.Measure.map_of_not_aemeasurable MeasureTheory.ae_zero
condDistrib_congr 📖	mathematical	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	condDistrib	—	MeasureTheory.Measure.instOuterMeasureClass condDistrib_def MeasureTheory.Measure.map_congr Filter.mp_mem Filter.univ_mem'
condDistrib_congr_left 📖	mathematical	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	condDistrib	—	MeasureTheory.Measure.instOuterMeasureClass condDistrib_congr Filter.EventuallyEq.refl
condDistrib_congr_right 📖	mathematical	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	condDistrib	—	MeasureTheory.Measure.instOuterMeasureClass condDistrib_congr Filter.EventuallyEq.refl
condDistrib_const 📖	mathematical	—	Filter.EventuallyEq MeasureTheory.Measure MeasureTheory.ae MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.map DFunLike.coe Kernel Kernel.instFunLike condDistrib Kernel.deterministic measurable_const	—	MeasureTheory.Measure.instOuterMeasureClass measurable_const Filter.mp_mem condDistrib_comp_self Filter.univ_mem'
condDistrib_def 📖	mathematical	—	condDistrib MeasureTheory.Measure.condKernel MeasureTheory.Measure.map Prod.instMeasurableSpace	—	—
condDistrib_fst_prod 📖	mathematical	AEMeasurable	Filter.EventuallyEq MeasureTheory.Measure MeasureTheory.ae MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.map DFunLike.coe Kernel Kernel.instFunLike condDistrib Prod.instMeasurableSpace MeasureTheory.Measure.prod MeasureTheory.Measure.prod.instIsFiniteMeasure MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.prod.instIsFiniteMeasure MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure MeasureTheory.Measure.isFiniteMeasure_map condDistrib_map IsScalarTower.right MeasureTheory.Measure.map_fst_prod MeasureTheory.instSFiniteOfSigmaFinite MeasureTheory.IsFiniteMeasure.toSigmaFinite MeasureTheory.IsProbabilityMeasure.measure_univ one_smul AEMeasurable.fst aemeasurable_id Filter.EventuallyEq.symm MeasureTheory.ae.congr_simp condDistrib.congr_simp AEMeasurable.map_map_of_aemeasurable MeasureTheory.Measure.map_of_not_aemeasurable MeasureTheory.ae_zero
condDistrib_map 📖	mathematical	AEMeasurable MeasureTheory.Measure.map	Filter.EventuallyEq MeasureTheory.Measure MeasureTheory.ae MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass DFunLike.coe Kernel Kernel.instFunLike condDistrib MeasureTheory.Measure.isFiniteMeasure_map	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.isFiniteMeasure_map AEMeasurable.map_map_of_aemeasurable condDistrib_ae_eq_of_measure_eq_compProd IsZeroOrMarkovKernel.isFiniteKernel IsMarkovKernel.IsZeroOrMarkovKernel instIsMarkovKernelCondDistrib compProd_map_condDistrib AEMeasurable.comp_aemeasurable' AEMeasurable.prodMk
condDistrib_self 📖	mathematical	—	Filter.EventuallyEq MeasureTheory.Measure MeasureTheory.ae MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.map DFunLike.coe Kernel Kernel.instFunLike condDistrib Kernel.id	—	MeasureTheory.Measure.instOuterMeasureClass measurable_id condDistrib.congr_simp CompTriple.comp_eq CompTriple.instId_comp CompTriple.instIsIdId condDistrib_comp_self
condDistrib_snd_prod 📖	mathematical	AEMeasurable	Filter.EventuallyEq MeasureTheory.Measure MeasureTheory.ae MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.map DFunLike.coe Kernel Kernel.instFunLike condDistrib Prod.instMeasurableSpace MeasureTheory.Measure.prod MeasureTheory.Measure.prod.instIsFiniteMeasure MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.prod.instIsFiniteMeasure MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure MeasureTheory.Measure.isFiniteMeasure_map condDistrib_map IsScalarTower.right MeasureTheory.Measure.map_snd_prod MeasureTheory.instSFiniteOfSigmaFinite MeasureTheory.IsFiniteMeasure.toSigmaFinite MeasureTheory.IsProbabilityMeasure.measure_univ one_smul AEMeasurable.snd aemeasurable_id Filter.EventuallyEq.symm MeasureTheory.ae.congr_simp condDistrib.congr_simp AEMeasurable.map_map_of_aemeasurable MeasureTheory.Measure.map_of_not_aemeasurable MeasureTheory.ae_zero
condExp_ae_eq_integral_condDistrib 📖	mathematical	Measurable AEMeasurable MeasureTheory.StronglyMeasurable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup MeasureTheory.Integrable SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.condExp MeasurableSpace.comap MeasureTheory.integral DFunLike.coe Kernel Kernel.instFunLike condDistrib	—	condExp_prod_ae_eq_integral_condDistrib MeasureTheory.StronglyMeasurable.comp_measurable measurable_snd
condExp_ae_eq_integral_condDistrib' 📖	mathematical	Measurable MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.condExp MeasurableSpace.comap MeasureTheory.integral DFunLike.coe Kernel Kernel.instFunLike condDistrib standardBorel_of_polish instPolishSpaceOfSeparableSpaceOfIsCompletelyMetrizableSpace TopologicalSpace.SecondCountableTopology.to_separableSpace TopologicalSpace.IsCompletelyMetrizableSpace.of_completeSpace_metrizable EMetric.instIsCountablyGeneratedUniformity EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace T6Space.toT0Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace AddTorsor.nonempty SeminormedAddGroup.toAddGroup NormedAddTorsor.toAddTorsor SeminormedAddCommGroup.toNormedAddTorsor	—	condExp_ae_eq_integral_condDistrib standardBorel_of_polish instPolishSpaceOfSeparableSpaceOfIsCompletelyMetrizableSpace TopologicalSpace.SecondCountableTopology.to_separableSpace TopologicalSpace.IsCompletelyMetrizableSpace.of_completeSpace_metrizable EMetric.instIsCountablyGeneratedUniformity T6Space.toT0Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace AddTorsor.nonempty MeasureTheory.AEStronglyMeasurable.aemeasurable PseudoEMetricSpace.pseudoMetrizableSpace stronglyMeasurable_id BorelSpace.opensMeasurable
condExp_ae_eq_integral_condDistrib_id 📖	mathematical	Measurable MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.condExp MeasurableSpace.comap MeasureTheory.integral DFunLike.coe Kernel Kernel.instFunLike condDistrib	—	condExp_prod_ae_eq_integral_condDistrib' aemeasurable_id MeasureTheory.Integrable.comp_snd_map_prodMk
condExp_prod_ae_eq_integral_condDistrib 📖	mathematical	Measurable AEMeasurable MeasureTheory.StronglyMeasurable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Prod.instMeasurableSpace MeasureTheory.Integrable SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.condExp MeasurableSpace.comap MeasureTheory.integral DFunLike.coe Kernel Kernel.instFunLike condDistrib	—	MeasureTheory.integrable_map_measure MeasureTheory.StronglyMeasurable.aestronglyMeasurable AEMeasurable.prodMk Measurable.aemeasurable condExp_prod_ae_eq_integral_condDistrib'
condExp_prod_ae_eq_integral_condDistrib' 📖	mathematical	Measurable AEMeasurable MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup Prod.instMeasurableSpace MeasureTheory.Measure.map	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.condExp MeasurableSpace.comap MeasureTheory.integral DFunLike.coe Kernel Kernel.instFunLike condDistrib	—	MeasureTheory.integrable_map_measure AEMeasurable.prodMk Measurable.aemeasurable Filter.EventuallyEq.symm MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.ae_eq_condExp_of_forall_setIntegral_eq Measurable.comap_le MeasureTheory.IsFiniteMeasure.toSigmaFinite MeasureTheory.isFiniteMeasure_trim MeasureTheory.Integrable.integrableOn MeasureTheory.Integrable.integral_condDistrib MeasureTheory.integral_map MeasureTheory.Measure.restrict_map MeasureTheory.AEStronglyMeasurable.restrict MeasureTheory.AEStronglyMeasurable.integral_condDistrib_map MeasureTheory.Measure.fst_map_prodMk₀ condDistrib_def MeasureTheory.Measure.isFiniteMeasure_map MeasureTheory.Measure.setIntegral_condKernel_univ_right MeasureTheory.setIntegral_map MeasurableSet.prod MeasurableSet.univ Set.mk_preimage_prod Set.preimage_univ Set.inter_univ aestronglyMeasurable_integral_condDistrib
condExp_prod_ae_eq_integral_condDistrib₀ 📖	mathematical	Measurable AEMeasurable MeasureTheory.AEStronglyMeasurable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Prod.instMeasurableSpace MeasureTheory.Measure.map MeasureTheory.Integrable SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.condExp MeasurableSpace.comap MeasureTheory.integral DFunLike.coe Kernel Kernel.instFunLike condDistrib	—	MeasureTheory.integrable_map_measure AEMeasurable.prodMk Measurable.aemeasurable condExp_prod_ae_eq_integral_condDistrib'
instIsMarkovKernelCondDistrib 📖	mathematical	—	IsMarkovKernel condDistrib	—	condDistrib_def MeasureTheory.Measure.instIsMarkovKernelCondKernel
integrable_comp_snd_map_prodMk_iff 📖	mathematical	Measurable	MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup Prod.instMeasurableSpace MeasureTheory.Measure.map	—	MeasureTheory.Integrable.comp_measurable Measurable.prodMk measurable_id MeasureTheory.Integrable.comp_snd_map_prodMk
integrable_toReal_condDistrib 📖	mathematical	AEMeasurable MeasurableSet	MeasureTheory.Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing MeasureTheory.Measure.real DFunLike.coe Kernel MeasureTheory.Measure Kernel.instFunLike condDistrib	—	MeasureTheory.integrable_toReal_of_lintegral_ne_top Measurable.comp_aemeasurable Kernel.measurable_coe ne_of_lt MeasureTheory.lintegral_mono MeasureTheory.prob_le_one IsZeroOrMarkovKernel.isZeroOrProbabilityMeasure IsMarkovKernel.IsZeroOrMarkovKernel instIsMarkovKernelCondDistrib MeasureTheory.lintegral_one MeasureTheory.measure_lt_top
measurable_condDistrib 📖	mathematical	MeasurableSet	Measurable ENNReal MeasurableSpace.comap ENNReal.measurableSpace DFunLike.coe MeasureTheory.Measure Set MeasureTheory.Measure.instFunLike Kernel Kernel.instFunLike condDistrib	—	Measurable.comp Kernel.measurable_coe Measurable.of_comap_le le_rfl
setLIntegral_condDistrib_of_measurableSet 📖	mathematical	Measurable AEMeasurable MeasurableSet MeasurableSpace.comap	MeasureTheory.lintegral MeasureTheory.Measure.restrict DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike Kernel Kernel.instFunLike condDistrib Set.instInter Set.preimage	—	setLIntegral_preimage_condDistrib
setLIntegral_preimage_condDistrib 📖	mathematical	Measurable AEMeasurable MeasurableSet	MeasureTheory.lintegral MeasureTheory.Measure.restrict Set.preimage DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike Kernel Kernel.instFunLike condDistrib Set.instInter	—	MeasureTheory.lintegral_map Kernel.measurable_coe condDistrib_def MeasureTheory.Measure.restrict_map MeasureTheory.Measure.fst_map_prodMk₀ MeasureTheory.Measure.setLIntegral_condKernel_eq_measure_prod MeasureTheory.Measure.map_apply_of_aemeasurable AEMeasurable.prodMk Measurable.aemeasurable MeasurableSet.prod Set.mk_preimage_prod
stronglyMeasurable_integral_condDistrib 📖	mathematical	MeasureTheory.StronglyMeasurable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Prod.instMeasurableSpace	MeasurableSpace.comap MeasureTheory.integral DFunLike.coe Kernel MeasureTheory.Measure Kernel.instFunLike condDistrib	—	MeasureTheory.StronglyMeasurable.comp_measurable MeasureTheory.StronglyMeasurable.integral_condDistrib Measurable.of_comap_le le_rfl

---

← Back to Index