Condexp

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

Statistics

Metric	Count
Definitions condExpKernel	1
Theorems comp_snd_map_prod_id, integral_condExpKernel, comp_snd_map_prod_id, condExpKernel_ae, integral_condExpKernel, integral_norm_condExpKernel, norm_integral_condExpKernel, integral_condExpKernel, integral_condExpKernel', aestronglyMeasurable_integral_condExpKernel, aestronglyMeasurable_trim_condExpKernel, compProd_trim_condExpKernel, condDistrib_apply_ae_eq_condExpKernel_map, condExpKernel_ae_eq_condExp, condExpKernel_ae_eq_condExp', condExpKernel_ae_eq_trim_condExp, condExpKernel_apply_eq_condDistrib, condExpKernel_comp_trim, condExpKernel_def, condExpKernel_eq, condExpKernel_singleton_ae_eq_cond, condExp_ae_eq_integral_condExpKernel, condExp_ae_eq_integral_condExpKernel', condExp_ae_eq_trim_integral_condExpKernel, condExp_ae_eq_trim_integral_condExpKernel_of_stronglyMeasurable, condExp_generateFrom_singleton, condExp_set_generateFrom_singleton, instIsMarkovKernelCondExpKernel, integrable_toReal_condExpKernel, measurable_condExpKernel, stronglyMeasurable_condExpKernel	31
Total	32

MeasureTheory.AEStronglyMeasurable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_snd_map_prod_id 📖	mathematical	MeasurableSpace MeasurableSpace.instLE MeasureTheory.AEStronglyMeasurable	MeasurableSpace.prod MeasureTheory.Measure.map	—	ProbabilityTheory.aestronglyMeasurable_comp_snd_map_prodMk_iff
integral_condExpKernel 📖	mathematical	MeasureTheory.AEStronglyMeasurable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	MeasureTheory.integral DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure ProbabilityTheory.Kernel.instFunLike ProbabilityTheory.condExpKernel	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim Nontrivial.to_nonempty ProbabilityTheory.condExpKernel_apply_eq_condDistrib integral_condDistrib aemeasurable_id'' inf_le_right aemeasurable_id comp_snd_map_prod_id

MeasureTheory.Integrable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_snd_map_prod_id 📖	mathematical	MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup	MeasurableSpace.prod MeasureTheory.Measure.map	—	comp_snd_map_prodMk
condExpKernel_ae 📖	mathematical	MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup	Filter.Eventually DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure ProbabilityTheory.Kernel.instFunLike ProbabilityTheory.condExpKernel MeasureTheory.ae MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim MeasureTheory.Measure.instOuterMeasureClass Finite.of_subsingleton measurableSingleton_of_standardBorel ProbabilityTheory.IsFiniteKernel.isFiniteMeasure ProbabilityTheory.IsZeroOrMarkovKernel.isFiniteKernel ProbabilityTheory.IsMarkovKernel.IsZeroOrMarkovKernel ProbabilityTheory.instIsMarkovKernelCondExpKernel Nontrivial.to_nonempty measurable_id'' inf_le_left ProbabilityTheory.condExpKernel_eq condDistrib_ae aemeasurable_id'' inf_le_right aemeasurable_id comp_snd_map_prod_id
integral_condExpKernel 📖	mathematical	MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup	MeasureTheory.integral DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure ProbabilityTheory.Kernel.instFunLike ProbabilityTheory.condExpKernel	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim Finite.of_subsingleton measurableSingleton_of_standardBorel Nontrivial.to_nonempty measurable_id'' inf_le_left ProbabilityTheory.condExpKernel_eq integral_condDistrib aemeasurable_id'' inf_le_right aemeasurable_id comp_snd_map_prod_id
integral_norm_condExpKernel 📖	mathematical	MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup	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.condExpKernel Norm.norm NormedAddCommGroup.toNorm	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim Finite.of_subsingleton measurableSingleton_of_standardBorel Nontrivial.to_nonempty measurable_id'' inf_le_left ProbabilityTheory.condExpKernel_eq integral_norm_condDistrib aemeasurable_id'' inf_le_right aemeasurable_id comp_snd_map_prod_id
norm_integral_condExpKernel 📖	mathematical	MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup	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.condExpKernel	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim Finite.of_subsingleton measurableSingleton_of_standardBorel Nontrivial.to_nonempty measurable_id'' inf_le_left ProbabilityTheory.condExpKernel_eq norm_integral_condDistrib aemeasurable_id'' inf_le_right aemeasurable_id comp_snd_map_prod_id

MeasureTheory.StronglyMeasurable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
integral_condExpKernel 📖	mathematical	MeasureTheory.StronglyMeasurable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	MeasureTheory.integral DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure ProbabilityTheory.Kernel.instFunLike ProbabilityTheory.condExpKernel	—	mono integral_condExpKernel' inf_le_left
integral_condExpKernel' 📖	mathematical	MeasureTheory.StronglyMeasurable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	MeasurableSpace SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice MeasurableSpace.instCompleteLattice MeasureTheory.integral DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure ProbabilityTheory.Kernel.instFunLike ProbabilityTheory.condExpKernel	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim Nontrivial.to_nonempty ProbabilityTheory.condExpKernel_apply_eq_condDistrib integral_condDistrib comp_measurable measurable_snd

ProbabilityTheory

Definitions

Name	Category	Theorems
condExpKernel 📖	CompOp	30 math math: MeasureTheory.Integrable.norm_integral_condExpKernel, integrable_toReal_condExpKernel, condIndepFun_iff_map_prod_eq_prod_comp_trim, condExpKernel_comp_trim, MeasureTheory.AEStronglyMeasurable.integral_condExpKernel, stronglyMeasurable_condExpKernel, condExpKernel_ae_eq_condExp', condIndepFun_iff_map_prod_eq_prod_map_map, condExp_ae_eq_trim_integral_condExpKernel_of_stronglyMeasurable, condExp_ae_eq_trim_integral_condExpKernel, condDistrib_apply_ae_eq_condExpKernel_map, MeasureTheory.Integrable.integral_norm_condExpKernel, MeasureTheory.StronglyMeasurable.integral_condExpKernel, condIndepFun_iff_compProd_map_prod_eq_compProd_prod_map_map, MeasureTheory.Integrable.integral_condExpKernel, condExp_ae_eq_integral_condExpKernel, condExpKernel_singleton_ae_eq_cond, MeasureTheory.StronglyMeasurable.integral_condExpKernel', condExp_ae_eq_integral_condExpKernel', condExpKernel_def, condExpKernel_ae_eq_condExp, aestronglyMeasurable_trim_condExpKernel, condExpKernel_ae_eq_trim_condExp, instIsMarkovKernelCondExpKernel, measurable_condExpKernel, compProd_trim_condExpKernel, condExpKernel_eq, MeasureTheory.Integrable.condExpKernel_ae, aestronglyMeasurable_integral_condExpKernel, condExpKernel_apply_eq_condDistrib

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
aestronglyMeasurable_integral_condExpKernel 📖	mathematical	MeasureTheory.AEStronglyMeasurable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	MeasureTheory.integral DFunLike.coe Kernel MeasureTheory.Measure Kernel.instFunLike condExpKernel	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim Nontrivial.to_nonempty measurable_id'' inf_le_left condExpKernel_eq aestronglyMeasurable_integral_condDistrib aemeasurable_id'' inf_le_right aemeasurable_id MeasureTheory.AEStronglyMeasurable.comp_snd_map_prod_id MeasureTheory.AEStronglyMeasurable.mono MeasurableSpace.comap_id
aestronglyMeasurable_trim_condExpKernel 📖	mathematical	MeasurableSpace MeasurableSpace.instLE MeasureTheory.AEStronglyMeasurable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	Filter.Eventually Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass DFunLike.coe Kernel Kernel.instFunLike condExpKernel MeasureTheory.Measure.trim	—	MeasureTheory.Measure.ae_ae_of_ae_comp MeasureTheory.Measure.instOuterMeasureClass condExpKernel_comp_trim
compProd_trim_condExpKernel 📖	mathematical	MeasurableSpace MeasurableSpace.instLE	MeasureTheory.Measure.compProd MeasureTheory.Measure.trim condExpKernel MeasureTheory.Measure.map MeasurableSpace.prod	—	isEmpty_or_nonempty MeasureTheory.Measure.eq_zero_of_isEmpty MeasureTheory.Measure.trim.congr_simp MeasureTheory.zero_trim condExpKernel.congr_simp MeasureTheory.Measure.compProd_zero_left MeasureTheory.Measure.map_zero measurable_id'' inf_le_left condExpKernel_eq inf_of_le_left compProd_map_condDistrib Measurable.aemeasurable measurable_id MeasureTheory.trim_eq_map Kernel.ext MeasureTheory.Measure.ext
condDistrib_apply_ae_eq_condExpKernel_map 📖	mathematical	Measurable MeasurableSet	Filter.EventuallyEq ENNReal MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass DFunLike.coe Set Kernel Kernel.instFunLike condDistrib MeasurableSpace.comap Kernel.map condExpKernel	—	MeasureTheory.Measure.instOuterMeasureClass Kernel.map_apply' Filter.mp_mem Real.instCompleteSpace condExpKernel_ae_eq_condExp Measurable.comap_le condDistrib_ae_eq_condExp Filter.univ_mem' MeasureTheory.measureReal_eq_measureReal_iff MeasureTheory.measure_ne_top IsFiniteKernel.isFiniteMeasure IsZeroOrMarkovKernel.isFiniteKernel IsMarkovKernel.IsZeroOrMarkovKernel instIsMarkovKernelCondDistrib instIsMarkovKernelCondExpKernel
condExpKernel_ae_eq_condExp 📖	mathematical	MeasurableSpace MeasurableSpace.instLE MeasurableSet	Filter.EventuallyEq Real MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.real DFunLike.coe Kernel Kernel.instFunLike condExpKernel MeasureTheory.condExp Real.normedAddCommGroup Real.instCompleteSpace InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Set.indicator Real.instZero Real.instOne	—	Filter.EventuallyEq.trans MeasureTheory.Measure.instOuterMeasureClass Real.instCompleteSpace condExpKernel_ae_eq_condExp' inf_of_le_left Filter.EventuallyEq.refl
condExpKernel_ae_eq_condExp' 📖	mathematical	MeasurableSet	Filter.EventuallyEq Real MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.real DFunLike.coe Kernel Kernel.instFunLike condExpKernel MeasureTheory.condExp MeasurableSpace SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice MeasurableSpace.instCompleteLattice Real.normedAddCommGroup Real.instCompleteSpace InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Set.indicator Real.instZero Real.instOne	—	MeasureTheory.Measure.instOuterMeasureClass Real.instCompleteSpace isEmpty_or_nonempty MeasureTheory.Measure.eq_zero_of_isEmpty MeasureTheory.ae.congr_simp MeasureTheory.ae_zero condExpKernel.congr_simp condDistrib_ae_eq_condExp measurable_id'' inf_le_right measurable_id condExpKernel_apply_eq_condDistrib MeasurableSpace.comap_id
condExpKernel_ae_eq_trim_condExp 📖	mathematical	MeasurableSpace MeasurableSpace.instLE MeasurableSet	Filter.EventuallyEq Real MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.trim MeasureTheory.Measure.real DFunLike.coe Kernel Kernel.instFunLike condExpKernel MeasureTheory.condExp Real.normedAddCommGroup Real.instCompleteSpace InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Set.indicator Real.instZero Real.instOne	—	MeasureTheory.Measure.instOuterMeasureClass Real.instCompleteSpace MeasureTheory.StronglyMeasurable.ae_eq_trim_iff EMetricSpace.metrizableSpace Measurable.stronglyMeasurable PseudoEMetricSpace.pseudoMetrizableSpace instSecondCountableTopologyReal BorelSpace.opensMeasurable Real.borelSpace Measurable.ennreal_toReal measurable_condExpKernel MeasureTheory.stronglyMeasurable_condExp condExpKernel_ae_eq_condExp
condExpKernel_apply_eq_condDistrib 📖	mathematical	—	DFunLike.coe Kernel MeasureTheory.Measure Kernel.instFunLike condExpKernel MeasurableSpace SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice MeasurableSpace.instCompleteLattice condDistrib	—	measurable_id'' inf_le_left condExpKernel_eq
condExpKernel_comp_trim 📖	mathematical	MeasurableSpace MeasurableSpace.instLE	MeasureTheory.Measure.bind MeasureTheory.Measure.trim DFunLike.coe Kernel MeasureTheory.Measure Kernel.instFunLike condExpKernel	—	MeasureTheory.Measure.snd_compProd MeasureTheory.instSFiniteOfSigmaFinite MeasureTheory.IsFiniteMeasure.toSigmaFinite MeasureTheory.isFiniteMeasure_trim Kernel.IsFiniteKernel.isSFiniteKernel IsZeroOrMarkovKernel.isFiniteKernel IsMarkovKernel.IsZeroOrMarkovKernel instIsMarkovKernelCondExpKernel compProd_trim_condExpKernel MeasureTheory.Measure.snd_map_prodMk measurable_id'' MeasureTheory.Measure.map_id
condExpKernel_def 📖	mathematical	—	condExpKernel Kernel Kernel.comap MeasurableSpace SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice MeasurableSpace.instCompleteLattice condDistrib Kernel.instZero	—	—
condExpKernel_eq 📖	mathematical	—	condExpKernel Kernel.comap MeasurableSpace SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice MeasurableSpace.instCompleteLattice condDistrib measurable_id'' inf_le_left	—	measurable_id'' inf_le_left condExpKernel_def
condExpKernel_singleton_ae_eq_cond 📖	mathematical	MeasurableSet	Filter.Eventually ENNReal DFunLike.coe MeasureTheory.Measure Set MeasureTheory.Measure.instFunLike Kernel MeasurableSpace.generateFrom Set.instSingletonSet Kernel.instFunLike condExpKernel cond MeasureTheory.ae MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.restrict	—	MeasureTheory.Measure.instOuterMeasureClass Real.instCompleteSpace MeasureTheory.ae_restrict_le condExpKernel_ae_eq_condExp MeasurableSpace.generateFrom_singleton_le Filter.mp_mem condExp_set_generateFrom_singleton Filter.univ_mem' ENNReal.toReal_eq_toReal_iff' MeasureTheory.measure_ne_top IsFiniteKernel.isFiniteMeasure IsZeroOrMarkovKernel.isFiniteKernel IsMarkovKernel.IsZeroOrMarkovKernel instIsMarkovKernelCondExpKernel MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure instIsZeroOrProbabilityMeasureCond MeasureTheory.measureReal_def
condExp_ae_eq_integral_condExpKernel 📖	mathematical	MeasurableSpace MeasurableSpace.instLE 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 MeasureTheory.integral DFunLike.coe Kernel Kernel.instFunLike condExpKernel	—	Filter.EventuallyEq.symm MeasureTheory.Measure.instOuterMeasureClass Filter.EventuallyEq.trans condExp_ae_eq_integral_condExpKernel' inf_of_le_left Filter.EventuallyEq.refl
condExp_ae_eq_integral_condExpKernel' 📖	mathematical	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 SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice MeasurableSpace.instCompleteLattice MeasureTheory.integral DFunLike.coe Kernel Kernel.instFunLike condExpKernel	—	MeasureTheory.Measure.instOuterMeasureClass isEmpty_or_nonempty MeasureTheory.Measure.eq_zero_of_isEmpty MeasureTheory.ae.congr_simp MeasureTheory.ae_zero condExpKernel.congr_simp Measurable.mono measurable_id le_rfl inf_le_right condExpKernel_apply_eq_condDistrib condExp_ae_eq_integral_condDistrib_id MeasurableSpace.comap_id
condExp_ae_eq_trim_integral_condExpKernel 📖	mathematical	MeasurableSpace MeasurableSpace.instLE 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.Measure.trim MeasureTheory.condExp MeasureTheory.integral DFunLike.coe Kernel Kernel.instFunLike condExpKernel	—	Filter.EventuallyEq.trans MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.condExp_congr_ae_trim condExp_ae_eq_trim_integral_condExpKernel_of_stronglyMeasurable MeasureTheory.integrable_congr Filter.EventuallyEq.symm Filter.mp_mem aestronglyMeasurable_trim_condExpKernel Filter.univ_mem' MeasureTheory.integral_congr_ae
condExp_ae_eq_trim_integral_condExpKernel_of_stronglyMeasurable 📖	mathematical	MeasurableSpace MeasurableSpace.instLE 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.Measure.trim MeasureTheory.condExp MeasureTheory.integral DFunLike.coe Kernel Kernel.instFunLike condExpKernel	—	MeasureTheory.StronglyMeasurable.ae_eq_trim_of_stronglyMeasurable EMetricSpace.metrizableSpace MeasureTheory.stronglyMeasurable_condExp MeasureTheory.StronglyMeasurable.integral_condExpKernel condExp_ae_eq_integral_condExpKernel
condExp_generateFrom_singleton 📖	mathematical	MeasurableSet 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.Measure.restrict MeasureTheory.condExp MeasurableSpace.generateFrom Set Set.instSingletonSet MeasureTheory.integral cond	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.restrict_eq_zero MeasureTheory.ae_eq_trans Filter.EventuallyEq.symm MeasureTheory.condExp_restrict_ae_eq_restrict MeasurableSpace.generateFrom_singleton_le MeasureTheory.IsFiniteMeasure.toSigmaFinite MeasureTheory.isFiniteMeasure_trim MeasurableSpace.measurableSet_generateFrom MeasureTheory.ae_eq_condExp_of_forall_setIntegral_eq MeasureTheory.isFiniteMeasureRestrict MeasureTheory.Integrable.restrict MeasureTheory.integrableOn_const_iff enorm_ne_top MeasureTheory.measure_lt_top MeasureTheory.measurableSet_generateFrom_singleton_iff MeasureTheory.Measure.restrict_empty MeasureTheory.integral_const zero_smul MeasureTheory.integral_zero_measure IsScalarTower.right MeasureTheory.integral_smul_measure ENNReal.toReal_inv MeasureTheory.measureReal_restrict_apply Set.univ_inter MeasureTheory.measureReal_restrict_apply_self smul_inv_smul₀ ENNReal.toReal_ne_zero MeasureTheory.measure_ne_top MeasureTheory.Measure.restrict_restrict Set.inter_self MeasurableSet.compl Set.compl_inter_self MeasureTheory.measureReal_empty MeasureTheory.setIntegral_measure_zero MeasureTheory.Measure.restrict_apply_eq_zero MeasureTheory.measure_empty MeasureTheory.Measure.restrict_univ MeasureTheory.measureReal_ne_zero_iff MeasureTheory.StronglyMeasurable.aestronglyMeasurable MeasureTheory.stronglyMeasurable_const
condExp_set_generateFrom_singleton 📖	mathematical	MeasurableSet	Filter.EventuallyEq Real MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.restrict MeasureTheory.condExp MeasurableSpace.generateFrom Set Set.instSingletonSet Real.normedAddCommGroup Real.instCompleteSpace InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Set.indicator Real.instZero Real.instOne MeasureTheory.Measure.real cond	—	MeasureTheory.Measure.instOuterMeasureClass Real.instCompleteSpace MeasureTheory.integral_indicator_one condExp_generateFrom_singleton MeasureTheory.Integrable.indicator MeasureTheory.integrable_const
instIsMarkovKernelCondExpKernel 📖	mathematical	—	IsMarkovKernel condExpKernel	—	isEmpty_or_nonempty IsEmpty.false condExpKernel_def Kernel.IsMarkovKernel.comap instIsMarkovKernelCondDistrib
integrable_toReal_condExpKernel 📖	mathematical	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 condExpKernel	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim Finite.of_subsingleton measurableSingleton_of_standardBorel Nontrivial.to_nonempty measurable_id'' inf_le_left condExpKernel_eq integrable_toReal_condDistrib aemeasurable_id'' inf_le_right
measurable_condExpKernel 📖	mathematical	MeasurableSet	Measurable ENNReal ENNReal.measurableSpace DFunLike.coe MeasureTheory.Measure Set MeasureTheory.Measure.instFunLike Kernel Kernel.instFunLike condExpKernel	—	Kernel.measurable_coe
stronglyMeasurable_condExpKernel 📖	mathematical	MeasurableSet	MeasureTheory.StronglyMeasurable ENNReal ENNReal.instTopologicalSpace DFunLike.coe MeasureTheory.Measure Set MeasureTheory.Measure.instFunLike Kernel Kernel.instFunLike condExpKernel	—	Measurable.stronglyMeasurable TopologicalSpace.MetrizableSpace.toPseudoMetrizableSpace ENNReal.instMetrizableSpace ENNReal.instSecondCountableTopology BorelSpace.opensMeasurable ENNReal.borelSpace measurable_condExpKernel

---

← Back to Index