Unique

📁 Source: Mathlib/Probability/Kernel/Disintegration/Unique.lean

Statistics

Metric	Count
Definitions Unique	1
Theorems apply_eq_measure_condKernel_of_compProd_eq, condKernel_apply_eq_condKernel, condKernel_compProd, condKernel_const, eq_condKernel_of_kernel_eq_compProd, eq_condKernel_of_measure_eq_compProd, eq_condKernel_of_measure_eq_compProd', eq_condKernel_of_measure_eq_compProd_real	8
Total	9

ProbabilityTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
condKernel_compProd 📖	mathematical	—	Filter.EventuallyEq MeasureTheory.Measure MeasureTheory.ae MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass DFunLike.coe Kernel Kernel.instFunLike MeasureTheory.Measure.condKernel MeasureTheory.Measure.compProd MeasureTheory.Measure.instIsFiniteMeasureProdCompProdOfIsFiniteKernel IsZeroOrMarkovKernel.isFiniteKernel IsMarkovKernel.IsZeroOrMarkovKernel	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.instIsFiniteMeasureProdCompProdOfIsFiniteKernel IsZeroOrMarkovKernel.isFiniteKernel IsMarkovKernel.IsZeroOrMarkovKernel eq_condKernel_of_measure_eq_compProd MeasureTheory.Measure.fst_compProd MeasureTheory.instSFiniteOfSigmaFinite MeasureTheory.IsFiniteMeasure.toSigmaFinite Filter.EventuallyEq.symm
condKernel_const 📖	mathematical	—	Filter.EventuallyEq MeasureTheory.Measure MeasureTheory.ae MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.fst DFunLike.coe Kernel Prod.instMeasurableSpace Kernel.instFunLike Kernel.condKernel Kernel.const Kernel.const.instIsFiniteKernel MeasureTheory.Measure.condKernel	—	MeasureTheory.Measure.instOuterMeasureClass Kernel.const.instIsFiniteKernel IsFiniteKernel.isFiniteMeasure Kernel.condKernel_apply_eq_condKernel Filter.mp_mem Filter.univ_mem'
eq_condKernel_of_kernel_eq_compProd 📖	mathematical	Kernel.compProd Kernel.fst	Filter.Eventually MeasureTheory.Measure DFunLike.coe Kernel Prod.instMeasurableSpace Kernel.instFunLike Kernel.condKernel MeasureTheory.ae MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	Filter.mp_mem MeasureTheory.Measure.instOuterMeasureClass IsFiniteKernel.isFiniteMeasure Kernel.apply_eq_measure_condKernel_of_compProd_eq Kernel.condKernel_apply_eq_condKernel Filter.univ_mem'
eq_condKernel_of_measure_eq_compProd 📖	mathematical	MeasureTheory.Measure.compProd MeasureTheory.Measure.fst	Filter.Eventually MeasureTheory.Measure DFunLike.coe Kernel Kernel.instFunLike MeasureTheory.Measure.condKernel MeasureTheory.ae MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	MeasureTheory.measurableEmbedding_embeddingReal MeasureTheory.Measure.ext MeasureTheory.Measure.fst_apply MeasureTheory.Measure.map_apply Measurable.prod measurable_fst Measurable.comp MeasurableEmbedding.measurable measurable_snd standardBorel_of_polish Real.borelSpace instPolishSpaceOfSeparableSpaceOfIsCompletelyMetrizableSpace TopologicalSpace.SecondCountableTopology.to_separableSpace instSecondCountableTopologyReal TopologicalSpace.IsCompletelyMetrizableSpace.of_completeSpace_metrizable Real.instCompleteSpace EMetric.instIsCountablyGeneratedUniformity T6Space.toT0Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace MeasureTheory.Measure.isFiniteMeasure_map MeasureTheory.Measure.instOuterMeasureClass eq_condKernel_of_measure_eq_compProd_real Kernel.IsFiniteKernel.map Measurable.prodMap measurable_id MeasureTheory.Measure.compProd_apply MeasureTheory.Measure.instSFiniteFstOfProd MeasureTheory.instSFiniteOfSigmaFinite MeasureTheory.IsFiniteMeasure.toSigmaFinite Kernel.IsSFiniteKernel.map Kernel.IsFiniteKernel.isSFiniteKernel Kernel.map_apply' measurable_prodMk_left MeasureTheory.Measure.disintegrate MeasureTheory.Measure.condKernel.instIsCondKernel IsZeroOrMarkovKernel.isFiniteKernel IsMarkovKernel.IsZeroOrMarkovKernel MeasureTheory.Measure.instIsMarkovKernelCondKernel Filter.mp_mem Filter.univ_mem' Kernel.map_apply Set.preimage_image_eq MeasurableEmbedding.injective MeasurableEmbedding.measurableSet_image
eq_condKernel_of_measure_eq_compProd' 📖	mathematical	MeasureTheory.Measure.compProd MeasureTheory.Measure.fst MeasurableSet	Filter.Eventually ENNReal DFunLike.coe MeasureTheory.Measure Set MeasureTheory.Measure.instFunLike Kernel Kernel.instFunLike MeasureTheory.Measure.condKernel MeasureTheory.ae MeasureTheory.Measure.instOuterMeasureClass	—	MeasureTheory.ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite MeasureTheory.IsFiniteMeasure.toSigmaFinite MeasureTheory.Measure.fst.instIsFiniteMeasure Kernel.measurable_coe MeasureTheory.Measure.setLIntegral_condKernel_eq_measure_prod MeasureTheory.lintegral_indicator MeasureTheory.Measure.compProd_apply MeasurableSet.prod MeasureTheory.Measure.instSFiniteFstOfProd MeasureTheory.instSFiniteOfSigmaFinite Set.indicator_of_mem Set.mk_preimage_prod_right Set.indicator_of_notMem Set.mk_preimage_prod_right_eq_empty MeasureTheory.measure_empty MeasureTheory.Measure.instOuterMeasureClass
eq_condKernel_of_measure_eq_compProd_real 📖	mathematical	MeasureTheory.Measure.compProd Real Real.measurableSpace MeasureTheory.Measure.fst	Filter.Eventually MeasureTheory.Measure DFunLike.coe Kernel Kernel.instFunLike MeasureTheory.Measure.condKernel standardBorel_of_polish UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.borelSpace instPolishSpaceOfSeparableSpaceOfIsCompletelyMetrizableSpace TopologicalSpace.SecondCountableTopology.to_separableSpace instSecondCountableTopologyReal TopologicalSpace.IsCompletelyMetrizableSpace.of_completeSpace_metrizable Real.instCompleteSpace EMetric.instIsCountablyGeneratedUniformity EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace Real.metricSpace T6Space.toT0Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace Real.instInhabited MeasureTheory.ae MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	standardBorel_of_polish Real.borelSpace instPolishSpaceOfSeparableSpaceOfIsCompletelyMetrizableSpace TopologicalSpace.SecondCountableTopology.to_separableSpace instSecondCountableTopologyReal TopologicalSpace.IsCompletelyMetrizableSpace.of_completeSpace_metrizable Real.instCompleteSpace EMetric.instIsCountablyGeneratedUniformity T6Space.toT0Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace MeasureTheory.Measure.instOuterMeasureClass eq_condKernel_of_measure_eq_compProd' Kernel.IsFiniteKernel.isSFiniteKernel MeasurableSet.univ MeasurableSpace.ae_induction_on_inter Real.borel_eq_generateFrom_Iic_rat Real.isPiSystem_Iic_rat MeasureTheory.measure_empty Set.iUnion_singleton_eq_range MeasureTheory.ae_all_iff Encodable.countable measurableSet_Iic BorelSpace.opensMeasurable instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid Filter.mp_mem Filter.univ_mem' MeasureTheory.measure_compl MeasureTheory.measure_ne_top IsFiniteKernel.isFiniteMeasure IsZeroOrMarkovKernel.isFiniteKernel IsMarkovKernel.IsZeroOrMarkovKernel MeasureTheory.Measure.instIsMarkovKernelCondKernel MeasureTheory.ae_of_all MeasureTheory.measure_iUnion instCountableNat tsum_congr MeasureTheory.Measure.ext

ProbabilityTheory.Kernel

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply_eq_measure_condKernel_of_compProd_eq 📖	mathematical	compProd fst	Filter.EventuallyEq MeasureTheory.Measure MeasureTheory.ae MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass DFunLike.coe ProbabilityTheory.Kernel instFunLike Prod.instMeasurableSpace MeasureTheory.Measure.condKernel ProbabilityTheory.IsFiniteKernel.isFiniteMeasure	—	measurable_prodMk_left MeasureTheory.Measure.ext MeasureTheory.Measure.compProd_apply MeasureTheory.Measure.instSFiniteFstOfProd ProbabilityTheory.IsSFiniteKernel.sFinite IsFiniteKernel.isSFiniteKernel IsSFiniteKernel.comap compProd_apply IsSFiniteKernel.fst ProbabilityTheory.IsFiniteKernel.isFiniteMeasure MeasureTheory.Measure.instOuterMeasureClass ProbabilityTheory.eq_condKernel_of_measure_eq_compProd IsFiniteKernel.comap fst_apply Filter.mp_mem Filter.univ_mem' comap_apply
condKernel_apply_eq_condKernel 📖	mathematical	—	Filter.EventuallyEq MeasureTheory.Measure MeasureTheory.ae MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass DFunLike.coe ProbabilityTheory.Kernel instFunLike fst Prod.instMeasurableSpace condKernel MeasureTheory.Measure.condKernel ProbabilityTheory.IsFiniteKernel.isFiniteMeasure	—	apply_eq_measure_condKernel_of_compProd_eq ProbabilityTheory.IsZeroOrMarkovKernel.isFiniteKernel ProbabilityTheory.IsMarkovKernel.IsZeroOrMarkovKernel instIsMarkovKernelCondKernel disintegrate condKernel.instIsCondKernel

(root)

Definitions

Name	Category	Theorems
Unique 📖	CompData	17 math math: CategoryTheory.Limits.IsZero.unique_to, Submodule.unique_quotient_iff_eq_top, AddAction.pretransitive_iff_unique_quotient_of_nonempty, Fintype.card_eq_one_iff_nonempty_unique, OrderType.type_eq_one, simply_connected_iff_unique_homotopic, Ordinal.type_eq_one_iff_unique, unique_iff_existsUnique, CategoryTheory.Limits.IsZero.unique_from, Module.Basis.nonempty_unique_index_of_finrank_eq_one, unique_iff_subsingleton_and_nonempty, unique_subtype_iff_existsUnique, nonempty_unique, ENat.card_eq_one_iff_unique, MulAction.pretransitive_iff_unique_quotient_of_nonempty, Unique.subsingleton_unique, CategoryTheory.equiv_punit_iff_unique

---

← Back to Index