Conditional

📁 Source: Mathlib/Probability/Independence/Conditional.lean

Statistics

Metric	Count
Definitions CondIndep, CondIndepFun, CondIndepSet, CondIndepSets, iCondIndep, iCondIndepFun, iCondIndepSet, iCondIndepSets, «term_⟂ᵢ[_,_;_]_», «term_⟂ᵢ[_,_]_»	10
Theorems condIndepSet_of_measurableSet, condIndepSets, comp, neg_left, neg_right, bInter, bUnion, biUnion, condIndep, condIndep', condIndepSet_of_mem, iInter, iUnion, inter, union, union_iff, condIndepFun_const_left, condIndepFun_const_right, condIndepFun_iff, condIndepFun_iff_compProd_map_prod_eq_compProd_prod_map_map, condIndepFun_iff_condDistrib_prod_ae_eq_prodMkLeft, condIndepFun_iff_condDistrib_prod_ae_eq_prodMkRight, condIndepFun_iff_condExp_inter_preimage_eq_mul, condIndepFun_iff_condIndep, condIndepFun_iff_condIndepSet_preimage, condIndepFun_iff_map_prod_eq_prod_comp_trim, condIndepFun_iff_map_prod_eq_prod_condDistrib_prod_condDistrib, condIndepFun_iff_map_prod_eq_prod_map_map, condIndepFun_of_measurable_left, condIndepFun_of_measurable_right, condIndepFun_self_left, condIndepFun_self_right, condIndepSet_empty_left, condIndepSet_empty_right, condIndepSet_iff, condIndepSet_iff_condIndep, condIndepSet_iff_condIndepSets_singleton, condIndepSets_iff, condIndepSets_of_condIndepSets_of_le_left, condIndepSets_of_condIndepSets_of_le_right, condIndepSets_piiUnionInter_of_disjoint, condIndepSets_singleton_iff, condIndep_bot_left, condIndep_bot_right, condIndep_iSup_of_antitone, condIndep_iSup_of_directed_le, condIndep_iSup_of_disjoint, condIndep_iSup_of_monotone, condIndep_iff, condIndep_iff_condIndepSets, condIndep_iff_forall_condIndepSet, condIndep_of_condIndep_of_le_left, condIndep_of_condIndep_of_le_right, condIndep, iCondIndepSets, condIndepFun, condIndepFun_finset, condIndepFun_finset_prod_of_notMem, condIndepFun_finset_sum_of_notMem, condIndepFun_prodMk, condIndepFun_prodMk_prodMk, condIndepFun_prod_range_succ, condIndepFun_sum_range_succ, indepFun_add_add, indepFun_add_left, indepFun_add_right, indepFun_div_div, indepFun_div_left, indepFun_div_right, indepFun_mul_left, indepFun_mul_mul, indepFun_mul_right, indepFun_sub_left, indepFun_sub_right, indepFun_sub_sub, of_subsingleton, iCondIndepFun_iff, iCondIndepFun_iff_condExp_inter_preimage_eq_mul, iCondIndepFun_iff_iCondIndep, condIndep_generateFrom_le, condIndep_generateFrom_le_nat, condIndep_generateFrom_lt, condIndep_generateFrom_of_disjoint, iCondIndepFun_indicator, iCondIndepSet_iff, iCondIndepSet_iff_iCondIndep, iCondIndepSet_iff_iCondIndepSets_singleton, condIndepSets, iCondIndep, piiUnionInter_of_notMem, iCondIndepSets_iff, iCondIndepSets_singleton_iff, iCondIndep_iff, iCondIndep_iff_iCondIndepSets	94
Total	104

ProbabilityTheory

Definitions

Name	Category	Theorems
CondIndep 📖	MathDef	22 math math: iCondIndepSet.condIndep_generateFrom_of_disjoint, condIndep_iff_forall_condIndepSet, condIndep_iff, condIndepSet_iff_condIndep, condIndep_bot_left, condIndep_limsup_atTop_self, iCondIndep.condIndep, iCondIndepSet.condIndep_generateFrom_lt, iCondIndepSet.condIndep_generateFrom_le_nat, CondIndepSets.condIndep, condIndep_iSup_limsup, condIndep_biSup_limsup, iCondIndepSet.condIndep_generateFrom_le, condIndep_limsup_self, condIndep_biSup_compl, condIndep_iSup_directed_limsup, condIndep_bot_right, condIndep_iSup_of_disjoint, condIndep_iff_condIndepSets, condIndep_limsup_atBot_self, CondIndepSets.condIndep', condIndepFun_iff_condIndep
CondIndepFun 📖	MathDef	36 math math: condIndepFun_iff_condExp_inter_preimage_eq_mul, iCondIndepFun.condIndepFun_prod_range_succ, iCondIndepFun.indepFun_mul_right, condIndepFun_of_measurable_left, iCondIndepFun.condIndepFun_prodMk, condIndepFun_iff_map_prod_eq_prod_comp_trim, iCondIndepFun.indepFun_mul_mul, condIndepFun_iff_map_prod_eq_prod_map_map, iCondIndepFun.indepFun_add_left, iCondIndepFun.indepFun_sub_sub, condIndepFun_iff_compProd_map_prod_eq_compProd_prod_map_map, iCondIndepFun.condIndepFun_finset, iCondIndepFun.indepFun_add_right, iCondIndepFun.indepFun_sub_left, condIndepFun_self_left, iCondIndepFun.condIndepFun_finset_sum_of_notMem, iCondIndepFun.indepFun_div_right, condIndepFun_of_measurable_right, condIndepFun_self_right, iCondIndepFun.indepFun_div_left, condIndepFun_iff_condIndepSet_preimage, iCondIndepFun.condIndepFun_prodMk_prodMk, iCondIndepFun.indepFun_div_div, iCondIndepFun.indepFun_add_add, iCondIndepFun.indepFun_sub_right, condIndepFun_const_right, iCondIndepFun.indepFun_mul_left, iCondIndepFun.condIndepFun, condIndepFun_iff_condDistrib_prod_ae_eq_prodMkRight, condIndepFun_iff_condDistrib_prod_ae_eq_prodMkLeft, iCondIndepFun.condIndepFun_finset_prod_of_notMem, condIndepFun_const_left, condIndepFun_iff, condIndepFun_iff_condIndep, iCondIndepFun.condIndepFun_sum_range_succ, condIndepFun_iff_map_prod_eq_prod_condDistrib_prod_condDistrib
CondIndepSet 📖	MathDef	9 math math: condIndep_iff_forall_condIndepSet, condIndepSet_iff_condIndep, condIndepSet_empty_left, condIndepSet_iff_condIndepSets_singleton, condIndepSet_iff, CondIndep.condIndepSet_of_measurableSet, condIndepFun_iff_condIndepSet_preimage, CondIndepSets.condIndepSet_of_mem, condIndepSet_empty_right
CondIndepSets 📖	MathDef	9 math math: iCondIndepSets.piiUnionInter_of_notMem, condIndepSets_piiUnionInter_of_disjoint, CondIndepSets.union_iff, condIndepSets_singleton_iff, condIndepSet_iff_condIndepSets_singleton, condIndepSets_iff, iCondIndepSets.condIndepSets, condIndep_iff_condIndepSets, CondIndep.condIndepSets
iCondIndep 📖	MathDef	5 math math: iCondIndepSet_iff_iCondIndep, iCondIndep_iff, iCondIndep_iff_iCondIndepSets, iCondIndepSets.iCondIndep, iCondIndepFun_iff_iCondIndep
iCondIndepFun 📖	MathDef	5 math math: iCondIndepSet.iCondIndepFun_indicator, iCondIndepFun.of_subsingleton, iCondIndepFun_iff_condExp_inter_preimage_eq_mul, iCondIndepFun_iff, iCondIndepFun_iff_iCondIndep
iCondIndepSet 📖	MathDef	3 math math: iCondIndepSet_iff_iCondIndep, iCondIndepSet_iff_iCondIndepSets_singleton, iCondIndepSet_iff
iCondIndepSets 📖	MathDef	5 math math: iCondIndepSets_singleton_iff, iCondIndepSet_iff_iCondIndepSets_singleton, iCondIndepSets_iff, iCondIndep.iCondIndepSets, iCondIndep_iff_iCondIndepSets
«term_⟂ᵢ[_,_;_]_» 📖	CompOp	—
«term_⟂ᵢ[_,_]_» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
condIndepFun_const_left 📖	mathematical	MeasurableSpace MeasurableSpace.instLE	CondIndepFun	—	Kernel.indepFun_const_left IsMarkovKernel.IsZeroOrMarkovKernel instIsMarkovKernelCondExpKernel
condIndepFun_const_right 📖	mathematical	MeasurableSpace MeasurableSpace.instLE	CondIndepFun	—	Kernel.indepFun_const_right IsMarkovKernel.IsZeroOrMarkovKernel instIsMarkovKernelCondExpKernel
condIndepFun_iff 📖	mathematical	MeasurableSpace MeasurableSpace.instLE Measurable	CondIndepFun Filter.EventuallyEq Real MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.condExp Real.normedAddCommGroup Real.instCompleteSpace InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Set.indicator Real.instZero Set Set.instInter Real.instOne Pi.instMul Real.instMul	—	MeasureTheory.Measure.instOuterMeasureClass Real.instCompleteSpace condIndepFun_iff_condIndep condIndep_iff Measurable.comap_le
condIndepFun_iff_compProd_map_prod_eq_compProd_prod_map_map 📖	mathematical	MeasurableSpace MeasurableSpace.instLE Measurable	CondIndepFun MeasureTheory.Measure.compProd Prod.instMeasurableSpace MeasureTheory.Measure.trim Kernel.map condExpKernel Kernel.prod	—	Kernel.indepFun_iff_compProd_map_prod_eq_compProd_prod_map_map MeasureTheory.isFiniteMeasure_trim IsZeroOrMarkovKernel.isFiniteKernel IsMarkovKernel.IsZeroOrMarkovKernel instIsMarkovKernelCondExpKernel
condIndepFun_iff_condDistrib_prod_ae_eq_prodMkLeft 📖	mathematical	Measurable	CondIndepFun MeasurableSpace.comap MeasurableSpace Measurable.comap_le Filter.EventuallyEq MeasureTheory.Measure MeasureTheory.ae Prod.instMeasurableSpace MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.map DFunLike.coe Kernel Kernel.instFunLike condDistrib Kernel.prodMkRight	—	condIndepFun_iff_condDistrib_prod_ae_eq_prodMkRight
condIndepFun_iff_condDistrib_prod_ae_eq_prodMkRight 📖	mathematical	Measurable	CondIndepFun MeasurableSpace.comap MeasurableSpace Measurable.comap_le Filter.EventuallyEq MeasureTheory.Measure MeasureTheory.ae Prod.instMeasurableSpace MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.map DFunLike.coe Kernel Kernel.instFunLike condDistrib Kernel.prodMkRight	—	Measurable.comap_le MeasureTheory.Measure.instOuterMeasureClass condDistrib_ae_eq_iff_measure_eq_compProd Measurable.aemeasurable Kernel.IsFiniteKernel.prodMkRight IsZeroOrMarkovKernel.isFiniteKernel IsMarkovKernel.IsZeroOrMarkovKernel instIsMarkovKernelCondDistrib condIndepFun_iff_map_prod_eq_prod_condDistrib_prod_condDistrib MeasureTheory.Measure.compProd_eq_comp_prod MeasureTheory.Measure.instSFiniteMap MeasureTheory.instSFiniteOfSigmaFinite MeasureTheory.IsFiniteMeasure.toSigmaFinite Kernel.IsSFiniteKernel.prodMkRight Kernel.IsFiniteKernel.isSFiniteKernel MeasureTheory.Measure.comp_assoc measurable_id Kernel.prod_prodMkRight_comp_deterministic_prod Kernel.isFiniteKernel_of_isFiniteKernel_snd Kernel.IsFiniteKernel.snd Kernel.isFiniteKernel_of_isFiniteKernel_fst Kernel.IsZeroOrMarkovKernel.fst Kernel.instIsMarkovKernelId Kernel.id_comp Kernel.comp_id Kernel.id.eq_1 compProd_map_condDistrib MeasureTheory.Measure.map_map MeasurableEquiv.measurable Measurable.prodMk MeasurableEquiv.symm_comp_self MeasureTheory.Measure.map_id MeasureTheory.Measure.deterministic_comp_eq_map Kernel.deterministic_comp_eq_map Kernel.prodAssoc_symm_prod
condIndepFun_iff_condExp_inter_preimage_eq_mul 📖	mathematical	MeasurableSpace MeasurableSpace.instLE Measurable	CondIndepFun Filter.EventuallyEq Real MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.condExp Real.normedAddCommGroup Real.instCompleteSpace InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Set.indicator Real.instZero Set Set.instInter Set.preimage Real.instOne Real.instMul	—	MeasureTheory.Measure.instOuterMeasureClass Real.instCompleteSpace condIndepFun_iff
condIndepFun_iff_condIndep 📖	mathematical	MeasurableSpace MeasurableSpace.instLE	CondIndepFun CondIndep MeasurableSpace.comap	—	—
condIndepFun_iff_condIndepSet_preimage 📖	mathematical	MeasurableSpace MeasurableSpace.instLE Measurable	CondIndepFun CondIndepSet Set.preimage	—	Kernel.indepFun_iff_indepSet_preimage IsMarkovKernel.IsZeroOrMarkovKernel instIsMarkovKernelCondExpKernel
condIndepFun_iff_map_prod_eq_prod_comp_trim 📖	mathematical	MeasurableSpace MeasurableSpace.instLE Measurable	CondIndepFun MeasureTheory.Measure.map MeasurableSpace.prod Prod.instMeasurableSpace MeasureTheory.Measure.bind MeasureTheory.Measure.trim DFunLike.coe Kernel MeasureTheory.Measure Kernel.instFunLike Kernel.prod Kernel.id Kernel.map condExpKernel	—	condIndepFun_iff_compProd_map_prod_eq_compProd_prod_map_map MeasureTheory.Measure.compProd_map MeasureTheory.instSFiniteOfSigmaFinite MeasureTheory.IsFiniteMeasure.toSigmaFinite MeasureTheory.isFiniteMeasure_trim Kernel.IsFiniteKernel.isSFiniteKernel IsZeroOrMarkovKernel.isFiniteKernel IsMarkovKernel.IsZeroOrMarkovKernel instIsMarkovKernelCondExpKernel Measurable.prodMk compProd_trim_condExpKernel MeasureTheory.Measure.map_map Measurable.prodMap measurable_id' Measurable.mono measurable_id le_rfl MeasureTheory.Measure.compProd_eq_comp_prod Kernel.IsSFiniteKernel.prod
condIndepFun_iff_map_prod_eq_prod_condDistrib_prod_condDistrib 📖	mathematical	Measurable	CondIndepFun MeasurableSpace.comap MeasurableSpace Measurable.comap_le MeasureTheory.Measure.map Prod.instMeasurableSpace MeasureTheory.Measure.bind DFunLike.coe Kernel MeasureTheory.Measure Kernel.instFunLike Kernel.prod Kernel.id condDistrib	—	Measurable.comap_le condIndepFun_iff_map_prod_eq_prod_comp_trim MeasureTheory.Measure.isFiniteMeasure_map MeasureTheory.Measure.map_apply Measurable.prodMk MeasurableSet.prod Measurable.mono measurable_id le_rfl MeasureTheory.Measure.bind_apply Measurable.aemeasurable Kernel.measurable MeasureTheory.lintegral_map Kernel.measurable_coe MeasureTheory.lintegral_trim MeasureTheory.lintegral_congr_ae Filter.mp_mem MeasureTheory.Measure.instOuterMeasureClass condDistrib_apply_ae_eq_condExpKernel_map Filter.univ_mem' Kernel.prod_apply_prod Kernel.IsFiniteKernel.isSFiniteKernel IsZeroOrMarkovKernel.isFiniteKernel IsMarkovKernel.IsZeroOrMarkovKernel Kernel.instIsMarkovKernelId Kernel.IsSFiniteKernel.prod Kernel.id_apply MeasureTheory.Measure.dirac_apply' instIsMarkovKernelCondDistrib Kernel.IsSFiniteKernel.map instIsMarkovKernelCondExpKernel
condIndepFun_iff_map_prod_eq_prod_map_map 📖	mathematical	MeasurableSpace MeasurableSpace.instLE Measurable	CondIndepFun Filter.EventuallyEq MeasureTheory.Measure Prod.instMeasurableSpace MeasureTheory.ae MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.trim DFunLike.coe Kernel Kernel.instFunLike Kernel.map condExpKernel Kernel.prod	—	MeasureTheory.Measure.instOuterMeasureClass condIndepFun_iff_compProd_map_prod_eq_compProd_prod_map_map Kernel.compProd_eq_iff MeasureTheory.isFiniteMeasure_trim Kernel.IsFiniteKernel.map IsZeroOrMarkovKernel.isFiniteKernel IsMarkovKernel.IsZeroOrMarkovKernel instIsMarkovKernelCondExpKernel Kernel.IsFiniteKernel.prod
condIndepFun_of_measurable_left 📖	mathematical	MeasurableSpace MeasurableSpace.instLE Measurable	CondIndepFun	—	MeasureTheory.Measure.instOuterMeasureClass Real.instCompleteSpace condIndepFun_iff Measurable.mono le_rfl Set.inter_indicator_one MeasureTheory.condExp_stronglyMeasurable_mul_of_bound MeasureTheory.StronglyMeasurable.indicator MeasureTheory.stronglyMeasurable_const MeasureTheory.integrable_indicator_iff MeasureTheory.integrableOn_const MeasureTheory.measure_ne_top enorm_ne_top MeasureTheory.ae_of_all Set.indicator.eq_1 CStarRing.norm_of_mem_unitary instCStarRingReal Real.instNontrivial SubmonoidClass.toOneMemClass Submonoid.instSubmonoidClass norm_zero Real.instZeroLEOneClass MeasureTheory.condExp_of_stronglyMeasurable MeasureTheory.IsFiniteMeasure.toSigmaFinite MeasureTheory.isFiniteMeasure_trim Measurable.le Filter.EventuallyEq.refl
condIndepFun_of_measurable_right 📖	mathematical	MeasurableSpace MeasurableSpace.instLE Measurable	CondIndepFun	—	CondIndepFun.symm condIndepFun_of_measurable_left
condIndepFun_self_left 📖	mathematical	Measurable	CondIndepFun MeasurableSpace.comap MeasurableSpace Measurable.comap_le	—	condIndepFun_of_measurable_left Measurable.comap_le comap_measurable
condIndepFun_self_right 📖	mathematical	Measurable	CondIndepFun MeasurableSpace.comap MeasurableSpace Measurable.comap_le	—	condIndepFun_of_measurable_right Measurable.comap_le comap_measurable
condIndepSet_empty_left 📖	mathematical	MeasurableSpace MeasurableSpace.instLE	CondIndepSet Set Set.instEmptyCollection	—	Kernel.indepSet_empty_left IsMarkovKernel.IsZeroOrMarkovKernel instIsMarkovKernelCondExpKernel
condIndepSet_empty_right 📖	mathematical	MeasurableSpace MeasurableSpace.instLE	CondIndepSet Set Set.instEmptyCollection	—	Kernel.indepSet_empty_right IsMarkovKernel.IsZeroOrMarkovKernel instIsMarkovKernelCondExpKernel
condIndepSet_iff 📖	mathematical	MeasurableSpace MeasurableSpace.instLE MeasurableSet	CondIndepSet Filter.EventuallyEq Real MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.condExp Real.normedAddCommGroup Real.instCompleteSpace InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Set.indicator Real.instZero Set Set.instInter Real.instOne Pi.instMul Real.instMul	—	MeasureTheory.Measure.instOuterMeasureClass Real.instCompleteSpace condIndepSet_iff_condIndepSets_singleton condIndepSets_singleton_iff
condIndepSet_iff_condIndep 📖	mathematical	MeasurableSpace MeasurableSpace.instLE	CondIndepSet CondIndep MeasurableSpace.generateFrom Set Set.instSingletonSet	—	—
condIndepSet_iff_condIndepSets_singleton 📖	mathematical	MeasurableSpace MeasurableSpace.instLE MeasurableSet	CondIndepSet CondIndepSets Set Set.instSingletonSet	—	Kernel.indepSet_iff_indepSets_singleton IsMarkovKernel.IsZeroOrMarkovKernel instIsMarkovKernelCondExpKernel
condIndepSets_iff 📖	mathematical	MeasurableSpace MeasurableSpace.instLE MeasurableSet	CondIndepSets Filter.EventuallyEq Real MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.condExp Real.normedAddCommGroup Real.instCompleteSpace InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Set.indicator Real.instZero Set Set.instInter Real.instOne Pi.instMul Real.instMul	—	MeasureTheory.Measure.instOuterMeasureClass Real.instCompleteSpace condExpKernel_ae_eq_condExp MeasurableSet.inter MeasureTheory.ae_eq_of_ae_eq_trim Filter.mp_mem Filter.univ_mem' Pi.mul_apply ENNReal.toReal_mul MeasureTheory.StronglyMeasurable.ae_eq_trim_iff ENNReal.instMetrizableSpace stronglyMeasurable_condExpKernel Measurable.stronglyMeasurable TopologicalSpace.MetrizableSpace.toPseudoMetrizableSpace ENNReal.instSecondCountableTopology BorelSpace.opensMeasurable ENNReal.borelSpace Measurable.mul ENNReal.instMeasurableMul₂ measurable_condExpKernel MeasureTheory.measure_ne_top IsFiniteKernel.isFiniteMeasure IsZeroOrMarkovKernel.isFiniteKernel IsMarkovKernel.IsZeroOrMarkovKernel instIsMarkovKernelCondExpKernel ENNReal.ofReal_toReal ENNReal.mul_ne_top
condIndepSets_of_condIndepSets_of_le_left 📖	—	MeasurableSpace MeasurableSpace.instLE CondIndepSets Set Set.instHasSubset	—	—	Kernel.indepSets_of_indepSets_of_le_left
condIndepSets_of_condIndepSets_of_le_right 📖	—	MeasurableSpace MeasurableSpace.instLE CondIndepSets Set Set.instHasSubset	—	—	Kernel.indepSets_of_indepSets_of_le_right
condIndepSets_piiUnionInter_of_disjoint 📖	mathematical	MeasurableSpace MeasurableSpace.instLE iCondIndepSets Disjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice	CondIndepSets piiUnionInter	—	Kernel.indepSets_piiUnionInter_of_disjoint
condIndepSets_singleton_iff 📖	mathematical	MeasurableSpace MeasurableSpace.instLE MeasurableSet	CondIndepSets Set Set.instSingletonSet Filter.EventuallyEq Real MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.condExp Real.normedAddCommGroup Real.instCompleteSpace InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Set.indicator Real.instZero Set.instInter Real.instOne Pi.instMul Real.instMul	—	MeasureTheory.Measure.instOuterMeasureClass Real.instCompleteSpace condIndepSets_iff Set.mem_singleton_iff
condIndep_bot_left 📖	mathematical	MeasurableSpace MeasurableSpace.instLE	CondIndep Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice MeasurableSpace.instCompleteLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder	—	Kernel.Indep.symm Kernel.indep_bot_right IsMarkovKernel.IsZeroOrMarkovKernel instIsMarkovKernelCondExpKernel
condIndep_bot_right 📖	mathematical	MeasurableSpace MeasurableSpace.instLE	CondIndep Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice MeasurableSpace.instCompleteLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder	—	Kernel.indep_bot_right IsMarkovKernel.IsZeroOrMarkovKernel instIsMarkovKernelCondExpKernel
condIndep_iSup_of_antitone 📖	mathematical	MeasurableSpace MeasurableSpace.instLE CondIndep Antitone PartialOrder.toPreorder SemilatticeInf.toPartialOrder MeasurableSpace.instPartialOrder	iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice MeasurableSpace.instCompleteLattice	—	Kernel.indep_iSup_of_antitone IsMarkovKernel.IsZeroOrMarkovKernel instIsMarkovKernelCondExpKernel
condIndep_iSup_of_directed_le 📖	mathematical	MeasurableSpace MeasurableSpace.instLE CondIndep Directed	iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice MeasurableSpace.instCompleteLattice	—	Kernel.indep_iSup_of_directed_le IsMarkovKernel.IsZeroOrMarkovKernel instIsMarkovKernelCondExpKernel
condIndep_iSup_of_disjoint 📖	mathematical	MeasurableSpace MeasurableSpace.instLE iCondIndep Disjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice	CondIndep iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice MeasurableSpace.instCompleteLattice Set.instMembership	—	Kernel.indep_iSup_of_disjoint
condIndep_iSup_of_monotone 📖	mathematical	MeasurableSpace MeasurableSpace.instLE CondIndep Monotone PartialOrder.toPreorder SemilatticeSup.toPartialOrder MeasurableSpace.instPartialOrder	iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice MeasurableSpace.instCompleteLattice	—	Kernel.indep_iSup_of_monotone IsMarkovKernel.IsZeroOrMarkovKernel instIsMarkovKernelCondExpKernel
condIndep_iff 📖	mathematical	MeasurableSpace MeasurableSpace.instLE	CondIndep Filter.EventuallyEq Real MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.condExp Real.normedAddCommGroup Real.instCompleteSpace InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Set.indicator Real.instZero Set Set.instInter Real.instOne Pi.instMul Real.instMul	—	MeasureTheory.Measure.instOuterMeasureClass Real.instCompleteSpace condIndep_iff_condIndepSets condIndepSets_iff
condIndep_iff_condIndepSets 📖	mathematical	MeasurableSpace MeasurableSpace.instLE	CondIndep CondIndepSets setOf Set MeasurableSet	—	—
condIndep_iff_forall_condIndepSet 📖	mathematical	MeasurableSpace MeasurableSpace.instLE	CondIndep CondIndepSet	—	Kernel.indep_iff_forall_indepSet
condIndep_of_condIndep_of_le_left 📖	—	MeasurableSpace MeasurableSpace.instLE CondIndep	—	—	Kernel.indep_of_indep_of_le_left
condIndep_of_condIndep_of_le_right 📖	—	MeasurableSpace MeasurableSpace.instLE CondIndep	—	—	Kernel.indep_of_indep_of_le_right
iCondIndepFun_iff 📖	mathematical	MeasurableSpace MeasurableSpace.instLE Measurable	iCondIndepFun Filter.EventuallyEq Real MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.condExp Real.normedAddCommGroup Real.instCompleteSpace InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Set.indicator Real.instZero Set.iInter Finset Finset.instMembership Real.instOne Finset.prod Pi.commMonoid Real.instCommMonoid	—	MeasureTheory.Measure.instOuterMeasureClass Real.instCompleteSpace iCondIndep_iff Measurable.comap_le
iCondIndepFun_iff_condExp_inter_preimage_eq_mul 📖	mathematical	MeasurableSpace MeasurableSpace.instLE Measurable	iCondIndepFun Filter.EventuallyEq Real MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.condExp Real.normedAddCommGroup Real.instCompleteSpace InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Set.indicator Real.instZero Set.iInter Finset Finset.instMembership Set.preimage Real.instOne Finset.prod Pi.commMonoid Real.instCommMonoid	—	MeasureTheory.Measure.instOuterMeasureClass Real.instCompleteSpace iCondIndepFun_iff Set.iInter_congr_Prop Finset.prod_congr
iCondIndepFun_iff_iCondIndep 📖	mathematical	MeasurableSpace MeasurableSpace.instLE	iCondIndepFun iCondIndep MeasurableSpace.comap	—	—
iCondIndepSet_iff 📖	mathematical	MeasurableSpace MeasurableSpace.instLE MeasurableSet	iCondIndepSet Filter.EventuallyEq Real MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.condExp Real.normedAddCommGroup Real.instCompleteSpace InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Set.indicator Real.instZero Set.iInter Finset Finset.instMembership Real.instOne Finset.prod Pi.commMonoid Real.instCommMonoid	—	MeasureTheory.Measure.instOuterMeasureClass Real.instCompleteSpace iCondIndepSet_iff_iCondIndepSets_singleton iCondIndepSets_singleton_iff
iCondIndepSet_iff_iCondIndep 📖	mathematical	MeasurableSpace MeasurableSpace.instLE	iCondIndepSet iCondIndep MeasurableSpace.generateFrom Set Set.instSingletonSet	—	—
iCondIndepSet_iff_iCondIndepSets_singleton 📖	mathematical	MeasurableSpace MeasurableSpace.instLE MeasurableSet	iCondIndepSet iCondIndepSets Set Set.instSingletonSet	—	Kernel.iIndepSet_iff_iIndepSets_singleton
iCondIndepSets_iff 📖	mathematical	MeasurableSpace MeasurableSpace.instLE MeasurableSet	iCondIndepSets Filter.EventuallyEq Real MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.condExp Real.normedAddCommGroup Real.instCompleteSpace InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Set.indicator Real.instZero Set.iInter Finset Finset.instMembership Real.instOne Finset.prod Pi.commMonoid Real.instCommMonoid	—	MeasureTheory.Measure.instOuterMeasureClass Real.instCompleteSpace condExpKernel_ae_eq_condExp MeasureTheory.ae_ball_iff Finset.countable_toSet MeasurableSet.biInter MeasureTheory.ae_eq_of_ae_eq_trim Filter.mp_mem Filter.univ_mem' ENNReal.toReal_prod Finset.prod_apply Finset.prod_congr MeasureTheory.StronglyMeasurable.ae_eq_trim_iff ENNReal.instMetrizableSpace stronglyMeasurable_condExpKernel Measurable.stronglyMeasurable TopologicalSpace.MetrizableSpace.toPseudoMetrizableSpace ENNReal.instSecondCountableTopology BorelSpace.opensMeasurable ENNReal.borelSpace Finset.measurable_fun_prod ENNReal.instMeasurableMul₂ measurable_condExpKernel MeasureTheory.measure_ne_top IsFiniteKernel.isFiniteMeasure IsZeroOrMarkovKernel.isFiniteKernel IsMarkovKernel.IsZeroOrMarkovKernel instIsMarkovKernelCondExpKernel ENNReal.prod_ne_top ENNReal.ofReal_toReal
iCondIndepSets_singleton_iff 📖	mathematical	MeasurableSpace MeasurableSpace.instLE MeasurableSet	iCondIndepSets Set Set.instSingletonSet Filter.EventuallyEq Real MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.condExp Real.normedAddCommGroup Real.instCompleteSpace InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Set.indicator Real.instZero Set.iInter Finset Finset.instMembership Real.instOne Finset.prod Pi.commMonoid Real.instCommMonoid	—	MeasureTheory.Measure.instOuterMeasureClass Real.instCompleteSpace iCondIndepSets_iff Set.iInter_congr_Prop Finset.prod_congr
iCondIndep_iff 📖	mathematical	MeasurableSpace MeasurableSpace.instLE	iCondIndep Filter.EventuallyEq Real MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.condExp Real.normedAddCommGroup Real.instCompleteSpace InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Set.indicator Real.instZero Set.iInter Finset Finset.instMembership Real.instOne Finset.prod Pi.commMonoid Real.instCommMonoid	—	MeasureTheory.Measure.instOuterMeasureClass Real.instCompleteSpace iCondIndep_iff_iCondIndepSets iCondIndepSets_iff
iCondIndep_iff_iCondIndepSets 📖	mathematical	MeasurableSpace MeasurableSpace.instLE	iCondIndep iCondIndepSets setOf Set MeasurableSet	—	—

ProbabilityTheory.CondIndep

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
condIndepSet_of_measurableSet 📖	mathematical	MeasurableSpace MeasurableSpace.instLE ProbabilityTheory.CondIndep MeasurableSet	ProbabilityTheory.CondIndepSet	—	ProbabilityTheory.Kernel.Indep.indepSet_of_measurableSet
condIndepSets 📖	mathematical	MeasurableSpace MeasurableSpace.instLE ProbabilityTheory.CondIndep MeasurableSpace.generateFrom	ProbabilityTheory.CondIndepSets	—	ProbabilityTheory.Kernel.Indep.indepSets

ProbabilityTheory.CondIndepFun

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp 📖	—	MeasurableSpace MeasurableSpace.instLE ProbabilityTheory.CondIndepFun Measurable	—	—	ProbabilityTheory.Kernel.IndepFun.comp
neg_left 📖	mathematical	MeasurableSpace MeasurableSpace.instLE ProbabilityTheory.CondIndepFun	Pi.instNeg	—	comp MeasurableNeg.measurable_neg measurable_id
neg_right 📖	mathematical	MeasurableSpace MeasurableSpace.instLE ProbabilityTheory.CondIndepFun	Pi.instNeg	—	comp measurable_id MeasurableNeg.measurable_neg

ProbabilityTheory.CondIndepSets

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bInter 📖	mathematical	MeasurableSpace MeasurableSpace.instLE Set Set.instMembership ProbabilityTheory.CondIndepSets	Set.iInter	—	ProbabilityTheory.Kernel.IndepSets.bInter
bUnion 📖	mathematical	MeasurableSpace MeasurableSpace.instLE ProbabilityTheory.CondIndepSets	Set.iUnion Set Set.instMembership	—	biUnion
biUnion 📖	mathematical	MeasurableSpace MeasurableSpace.instLE ProbabilityTheory.CondIndepSets	Set.iUnion Set Set.instMembership	—	ProbabilityTheory.Kernel.IndepSets.biUnion
condIndep 📖	mathematical	MeasurableSpace MeasurableSpace.instLE IsPiSystem MeasurableSpace.generateFrom ProbabilityTheory.CondIndepSets	ProbabilityTheory.CondIndep	—	ProbabilityTheory.Kernel.IndepSets.indep ProbabilityTheory.IsMarkovKernel.IsZeroOrMarkovKernel ProbabilityTheory.instIsMarkovKernelCondExpKernel
condIndep' 📖	mathematical	MeasurableSpace MeasurableSpace.instLE MeasurableSet IsPiSystem ProbabilityTheory.CondIndepSets	ProbabilityTheory.CondIndep MeasurableSpace.generateFrom	—	ProbabilityTheory.Kernel.IndepSets.indep' ProbabilityTheory.IsMarkovKernel.IsZeroOrMarkovKernel ProbabilityTheory.instIsMarkovKernelCondExpKernel
condIndepSet_of_mem 📖	mathematical	MeasurableSpace MeasurableSpace.instLE Set Set.instMembership MeasurableSet ProbabilityTheory.CondIndepSets	ProbabilityTheory.CondIndepSet	—	ProbabilityTheory.Kernel.IndepSets.indepSet_of_mem ProbabilityTheory.IsMarkovKernel.IsZeroOrMarkovKernel ProbabilityTheory.instIsMarkovKernelCondExpKernel
iInter 📖	mathematical	MeasurableSpace MeasurableSpace.instLE ProbabilityTheory.CondIndepSets	Set.iInter Set	—	ProbabilityTheory.Kernel.IndepSets.iInter
iUnion 📖	mathematical	MeasurableSpace MeasurableSpace.instLE ProbabilityTheory.CondIndepSets	Set.iUnion Set	—	ProbabilityTheory.Kernel.IndepSets.iUnion
inter 📖	mathematical	MeasurableSpace MeasurableSpace.instLE ProbabilityTheory.CondIndepSets	Set Set.instInter	—	ProbabilityTheory.Kernel.IndepSets.inter
union 📖	mathematical	MeasurableSpace MeasurableSpace.instLE ProbabilityTheory.CondIndepSets	Set Set.instUnion	—	ProbabilityTheory.Kernel.IndepSets.union
union_iff 📖	mathematical	MeasurableSpace MeasurableSpace.instLE	ProbabilityTheory.CondIndepSets Set Set.instUnion	—	ProbabilityTheory.Kernel.IndepSets.union_iff

ProbabilityTheory.iCondIndep

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
condIndep 📖	mathematical	MeasurableSpace MeasurableSpace.instLE ProbabilityTheory.iCondIndep	ProbabilityTheory.CondIndep	—	ProbabilityTheory.Kernel.iIndep.indep
iCondIndepSets 📖	mathematical	MeasurableSpace MeasurableSpace.instLE MeasurableSpace.generateFrom ProbabilityTheory.iCondIndep	ProbabilityTheory.iCondIndepSets	—	ProbabilityTheory.Kernel.iIndep.iIndepSets

ProbabilityTheory.iCondIndepFun

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
condIndepFun 📖	mathematical	MeasurableSpace MeasurableSpace.instLE ProbabilityTheory.iCondIndepFun	ProbabilityTheory.CondIndepFun	—	ProbabilityTheory.Kernel.iIndepFun.indepFun
condIndepFun_finset 📖	mathematical	MeasurableSpace MeasurableSpace.instLE Disjoint Finset Finset.partialOrder Finset.instOrderBot ProbabilityTheory.iCondIndepFun Measurable	ProbabilityTheory.CondIndepFun MeasurableSpace.pi SetLike.instMembership Finset.instSetLike	—	ProbabilityTheory.Kernel.iIndepFun.indepFun_finset
condIndepFun_finset_prod_of_notMem 📖	mathematical	MeasurableSpace MeasurableSpace.instLE ProbabilityTheory.iCondIndepFun Measurable Finset Finset.instMembership	ProbabilityTheory.CondIndepFun Finset.prod Pi.commMonoid	—	ProbabilityTheory.Kernel.iIndepFun.indepFun_finset_prod_of_notMem
condIndepFun_finset_sum_of_notMem 📖	mathematical	MeasurableSpace MeasurableSpace.instLE ProbabilityTheory.iCondIndepFun Measurable Finset Finset.instMembership	ProbabilityTheory.CondIndepFun Finset.sum Pi.addCommMonoid	—	ProbabilityTheory.Kernel.iIndepFun.indepFun_finset_sum_of_notMem
condIndepFun_prodMk 📖	mathematical	MeasurableSpace MeasurableSpace.instLE ProbabilityTheory.iCondIndepFun Measurable	ProbabilityTheory.CondIndepFun Prod.instMeasurableSpace	—	ProbabilityTheory.Kernel.iIndepFun.indepFun_prodMk
condIndepFun_prodMk_prodMk 📖	mathematical	MeasurableSpace MeasurableSpace.instLE ProbabilityTheory.iCondIndepFun Measurable	ProbabilityTheory.CondIndepFun Prod.instMeasurableSpace	—	Finset.mem_insert_self Finset.mem_insert_of_mem Finset.mem_singleton_self Measurable.prodMk measurable_pi_apply ProbabilityTheory.Kernel.IndepFun.comp ProbabilityTheory.Kernel.iIndepFun.indepFun_finset
condIndepFun_prod_range_succ 📖	mathematical	MeasurableSpace MeasurableSpace.instLE ProbabilityTheory.iCondIndepFun Measurable	ProbabilityTheory.CondIndepFun Finset.prod Pi.commMonoid Finset.range	—	ProbabilityTheory.Kernel.iIndepFun.indepFun_prod_range_succ
condIndepFun_sum_range_succ 📖	mathematical	MeasurableSpace MeasurableSpace.instLE ProbabilityTheory.iCondIndepFun Measurable	ProbabilityTheory.CondIndepFun Finset.sum Pi.addCommMonoid Finset.range	—	ProbabilityTheory.Kernel.iIndepFun.indepFun_sum_range_succ
indepFun_add_add 📖	mathematical	MeasurableSpace MeasurableSpace.instLE ProbabilityTheory.iCondIndepFun Measurable	ProbabilityTheory.CondIndepFun Pi.instAdd	—	ProbabilityTheory.Kernel.iIndepFun.indepFun_add_add
indepFun_add_left 📖	mathematical	MeasurableSpace MeasurableSpace.instLE ProbabilityTheory.iCondIndepFun Measurable	ProbabilityTheory.CondIndepFun Pi.instAdd	—	ProbabilityTheory.Kernel.iIndepFun.indepFun_add_left
indepFun_add_right 📖	mathematical	MeasurableSpace MeasurableSpace.instLE ProbabilityTheory.iCondIndepFun Measurable	ProbabilityTheory.CondIndepFun Pi.instAdd	—	ProbabilityTheory.Kernel.iIndepFun.indepFun_add_right
indepFun_div_div 📖	mathematical	MeasurableSpace MeasurableSpace.instLE ProbabilityTheory.iCondIndepFun Measurable	ProbabilityTheory.CondIndepFun Pi.instDiv	—	ProbabilityTheory.Kernel.iIndepFun.indepFun_div_div
indepFun_div_left 📖	mathematical	MeasurableSpace MeasurableSpace.instLE ProbabilityTheory.iCondIndepFun Measurable	ProbabilityTheory.CondIndepFun Pi.instDiv	—	ProbabilityTheory.Kernel.iIndepFun.indepFun_div_left
indepFun_div_right 📖	mathematical	MeasurableSpace MeasurableSpace.instLE ProbabilityTheory.iCondIndepFun Measurable	ProbabilityTheory.CondIndepFun Pi.instDiv	—	ProbabilityTheory.Kernel.iIndepFun.indepFun_div_right
indepFun_mul_left 📖	mathematical	MeasurableSpace MeasurableSpace.instLE ProbabilityTheory.iCondIndepFun Measurable	ProbabilityTheory.CondIndepFun Pi.instMul	—	ProbabilityTheory.Kernel.iIndepFun.indepFun_mul_left
indepFun_mul_mul 📖	mathematical	MeasurableSpace MeasurableSpace.instLE ProbabilityTheory.iCondIndepFun Measurable	ProbabilityTheory.CondIndepFun Pi.instMul	—	ProbabilityTheory.Kernel.iIndepFun.indepFun_mul_mul
indepFun_mul_right 📖	mathematical	MeasurableSpace MeasurableSpace.instLE ProbabilityTheory.iCondIndepFun Measurable	ProbabilityTheory.CondIndepFun Pi.instMul	—	ProbabilityTheory.Kernel.iIndepFun.indepFun_mul_right
indepFun_sub_left 📖	mathematical	MeasurableSpace MeasurableSpace.instLE ProbabilityTheory.iCondIndepFun Measurable	ProbabilityTheory.CondIndepFun Pi.instSub	—	ProbabilityTheory.Kernel.iIndepFun.indepFun_sub_left
indepFun_sub_right 📖	mathematical	MeasurableSpace MeasurableSpace.instLE ProbabilityTheory.iCondIndepFun Measurable	ProbabilityTheory.CondIndepFun Pi.instSub	—	ProbabilityTheory.Kernel.iIndepFun.indepFun_sub_right
indepFun_sub_sub 📖	mathematical	MeasurableSpace MeasurableSpace.instLE ProbabilityTheory.iCondIndepFun Measurable	ProbabilityTheory.CondIndepFun Pi.instSub	—	ProbabilityTheory.Kernel.iIndepFun.indepFun_sub_sub
of_subsingleton 📖	mathematical	MeasurableSpace MeasurableSpace.instLE	ProbabilityTheory.iCondIndepFun	—	ProbabilityTheory.Kernel.iIndepFun.of_subsingleton ProbabilityTheory.instIsMarkovKernelCondExpKernel

ProbabilityTheory.iCondIndepSet

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
condIndep_generateFrom_le 📖	mathematical	MeasurableSpace MeasurableSpace.instLE MeasurableSet ProbabilityTheory.iCondIndepSet Preorder.toLT	ProbabilityTheory.CondIndep MeasurableSpace.generateFrom Set Set.instSingletonSet setOf Preorder.toLE	—	ProbabilityTheory.Kernel.iIndepSet.indep_generateFrom_le
condIndep_generateFrom_le_nat 📖	mathematical	MeasurableSpace MeasurableSpace.instLE MeasurableSet ProbabilityTheory.iCondIndepSet	ProbabilityTheory.CondIndep MeasurableSpace.generateFrom Set Set.instSingletonSet setOf	—	ProbabilityTheory.Kernel.iIndepSet.indep_generateFrom_le_nat
condIndep_generateFrom_lt 📖	mathematical	MeasurableSpace MeasurableSpace.instLE MeasurableSet ProbabilityTheory.iCondIndepSet	ProbabilityTheory.CondIndep MeasurableSpace.generateFrom Set Set.instSingletonSet setOf Preorder.toLT	—	ProbabilityTheory.Kernel.iIndepSet.indep_generateFrom_lt
condIndep_generateFrom_of_disjoint 📖	mathematical	MeasurableSpace MeasurableSpace.instLE MeasurableSet ProbabilityTheory.iCondIndepSet Disjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice	ProbabilityTheory.CondIndep MeasurableSpace.generateFrom setOf Set.instMembership	—	ProbabilityTheory.Kernel.iIndepSet.indep_generateFrom_of_disjoint
iCondIndepFun_indicator 📖	mathematical	MeasurableSpace MeasurableSpace.instLE ProbabilityTheory.iCondIndepSet	ProbabilityTheory.iCondIndepFun Set.indicator	—	ProbabilityTheory.Kernel.iIndepSet.iIndepFun_indicator

ProbabilityTheory.iCondIndepSets

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
condIndepSets 📖	mathematical	MeasurableSpace MeasurableSpace.instLE ProbabilityTheory.iCondIndepSets	ProbabilityTheory.CondIndepSets	—	ProbabilityTheory.Kernel.iIndepSets.indepSets
iCondIndep 📖	mathematical	MeasurableSpace MeasurableSpace.instLE IsPiSystem MeasurableSpace.generateFrom ProbabilityTheory.iCondIndepSets	ProbabilityTheory.iCondIndep	—	ProbabilityTheory.Kernel.iIndepSets.iIndep
piiUnionInter_of_notMem 📖	mathematical	MeasurableSpace MeasurableSpace.instLE ProbabilityTheory.iCondIndepSets Finset Finset.instMembership	ProbabilityTheory.CondIndepSets piiUnionInter SetLike.coe Finset.instSetLike	—	ProbabilityTheory.Kernel.iIndepSets.piiUnionInter_of_notMem

---

← Back to Index