Posterior

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

Statistics

Metric	Count
Definitions posterior, «term_†_»	2
Theorems absolutelyContinuous_comp_of_absolutelyContinuous, absolutelyContinuous_of_posterior, absolutelyContinuous_posterior, absolutelyContinuous_posterior_iff, ae_eq_posterior_of_compProd_eq, ae_eq_posterior_of_compProd_eq_swap_comp, compProd_posterior_eq_map_swap, compProd_posterior_eq_swap_comp, deterministic_comp_posterior, instIsMarkovKernelPosterior, parallelProd_posterior_comp_copy_comp, posterior_boolKernel_apply_false, posterior_boolKernel_apply_true, posterior_comp, posterior_comp_self, posterior_eq_withDensity, posterior_eq_withDensity_of_countable, posterior_id, posterior_posterior, posterior_prod_id_comp, rnDeriv_posterior, rnDeriv_posterior_ae_prod, rnDeriv_posterior_symm, swap_compProd_posterior	24
Total	26

ProbabilityTheory

Definitions

Name	Category	Theorems
posterior 📖	CompOp	22 math math: absolutelyContinuous_posterior_iff, posterior_eq_withDensity, compProd_posterior_eq_map_swap, posterior_boolKernel_apply_true, ae_eq_posterior_of_compProd_eq_swap_comp, rnDeriv_posterior_symm, posterior_prod_id_comp, instIsMarkovKernelPosterior, parallelProd_posterior_comp_copy_comp, posterior_boolKernel_apply_false, swap_compProd_posterior, posterior_id, rnDeriv_posterior, posterior_posterior, posterior_comp_self, posterior_eq_withDensity_of_countable, absolutelyContinuous_posterior, compProd_posterior_eq_swap_comp, rnDeriv_posterior_ae_prod, ae_eq_posterior_of_compProd_eq, deterministic_comp_posterior, posterior_comp
«term_†_» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
absolutelyContinuous_of_posterior 📖	—	Filter.Eventually MeasureTheory.Measure.AbsolutelyContinuous DFunLike.coe Kernel MeasureTheory.Measure Kernel.instFunLike posterior MeasureTheory.ae MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.bind	—	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.compProd_const MeasureTheory.Measure.instSFiniteBindCoeKernelOfIsSFiniteKernel MeasureTheory.instSFiniteOfSigmaFinite MeasureTheory.IsFiniteMeasure.toSigmaFinite Kernel.IsFiniteKernel.isSFiniteKernel MeasureTheory.Measure.AbsolutelyContinuous.compProd_right Kernel.const.instIsSFiniteKernel swap_compProd_posterior MeasureTheory.Measure.prod_swap MeasureTheory.Measure.swap_comp MeasureTheory.Measure.AbsolutelyContinuous.map measurable_swap MeasureTheory.Measure.AbsolutelyContinuous.kernel_of_compProd Kernel.const.instIsFiniteKernel MeasureTheory.Measure.instIsFiniteMeasureBindCoeKernelOfIsFiniteKernel
absolutelyContinuous_posterior 📖	mathematical	Filter.Eventually MeasureTheory.Measure.AbsolutelyContinuous DFunLike.coe Kernel MeasureTheory.Measure Kernel.instFunLike MeasureTheory.ae MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	posterior MeasureTheory.Measure.bind	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.compProd_const MeasureTheory.instSFiniteOfSigmaFinite MeasureTheory.IsFiniteMeasure.toSigmaFinite MeasureTheory.Measure.AbsolutelyContinuous.compProd_right Kernel.const.instIsSFiniteKernel compProd_posterior_eq_map_swap MeasureTheory.Measure.prod_swap MeasureTheory.Measure.AbsolutelyContinuous.map measurable_swap MeasureTheory.Measure.AbsolutelyContinuous.kernel_of_compProd IsZeroOrMarkovKernel.isFiniteKernel IsMarkovKernel.IsZeroOrMarkovKernel instIsMarkovKernelPosterior Kernel.const.instIsFiniteKernel MeasurableSpace.instCountableOrCountablyGeneratedOfCountablyGenerated countablyGenerated_of_standardBorel MeasureTheory.Measure.instSFiniteBindCoeKernelOfIsSFiniteKernel Kernel.IsFiniteKernel.isSFiniteKernel
absolutelyContinuous_posterior_iff 📖	mathematical	—	Filter.Eventually MeasureTheory.Measure.AbsolutelyContinuous DFunLike.coe Kernel MeasureTheory.Measure Kernel.instFunLike posterior MeasureTheory.ae MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.bind	—	MeasureTheory.Measure.instOuterMeasureClass absolutelyContinuous_of_posterior absolutelyContinuous_posterior MeasureTheory.Measure.instSFiniteBindCoeKernelOfIsSFiniteKernel MeasureTheory.instSFiniteOfSigmaFinite MeasureTheory.IsFiniteMeasure.toSigmaFinite Kernel.IsFiniteKernel.isSFiniteKernel
ae_eq_posterior_of_compProd_eq 📖	mathematical	MeasureTheory.Measure.compProd MeasureTheory.Measure.bind DFunLike.coe Kernel MeasureTheory.Measure Kernel.instFunLike MeasureTheory.Measure.map Prod.instMeasurableSpace	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass posterior	—	Filter.EventuallyEq.symm MeasureTheory.Measure.instOuterMeasureClass Kernel.ae_eq_of_compProd_eq MeasurableSpace.instCountableOrCountablyGeneratedOfCountablyGenerated countablyGenerated_of_standardBorel MeasureTheory.Measure.instIsFiniteMeasureBindCoeKernelOfIsFiniteKernel IsZeroOrMarkovKernel.isFiniteKernel IsMarkovKernel.IsZeroOrMarkovKernel instIsMarkovKernelPosterior compProd_posterior_eq_map_swap
ae_eq_posterior_of_compProd_eq_swap_comp 📖	mathematical	MeasureTheory.Measure.compProd MeasureTheory.Measure.bind DFunLike.coe Kernel MeasureTheory.Measure Kernel.instFunLike Prod.instMeasurableSpace Kernel.swap	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass posterior	—	ae_eq_posterior_of_compProd_eq MeasureTheory.Measure.swap_comp
compProd_posterior_eq_map_swap 📖	mathematical	—	MeasureTheory.Measure.compProd MeasureTheory.Measure.bind DFunLike.coe Kernel MeasureTheory.Measure Kernel.instFunLike posterior MeasureTheory.Measure.map Prod.instMeasurableSpace	—	MeasureTheory.Measure.isFiniteMeasure_map MeasureTheory.Measure.instIsFiniteMeasureProdCompProdOfIsFiniteKernel MeasureTheory.Measure.fst_map_swap MeasureTheory.Measure.snd_compProd MeasureTheory.instSFiniteOfSigmaFinite MeasureTheory.IsFiniteMeasure.toSigmaFinite Kernel.IsFiniteKernel.isSFiniteKernel MeasureTheory.Measure.disintegrate MeasureTheory.Measure.condKernel.instIsCondKernel
compProd_posterior_eq_swap_comp 📖	mathematical	—	MeasureTheory.Measure.compProd MeasureTheory.Measure.bind DFunLike.coe Kernel MeasureTheory.Measure Kernel.instFunLike posterior Prod.instMeasurableSpace Kernel.swap	—	compProd_posterior_eq_map_swap MeasureTheory.Measure.swap_comp
deterministic_comp_posterior 📖	mathematical	Measurable	Filter.EventuallyEq MeasureTheory.Measure MeasureTheory.ae MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.map DFunLike.coe Kernel Kernel.instFunLike Kernel.comp Kernel.deterministic posterior IsZeroOrMarkovKernel.isFiniteKernel IsMarkovKernel.IsZeroOrMarkovKernel Kernel.isMarkovKernel_deterministic Kernel.id	—	Kernel.ae_eq_of_compProd_eq IsZeroOrMarkovKernel.isFiniteKernel IsMarkovKernel.IsZeroOrMarkovKernel Kernel.isMarkovKernel_deterministic MeasurableSpace.instCountableOrCountablyGeneratedOfCountablyGenerated MeasureTheory.Measure.isFiniteMeasure_map Kernel.IsFiniteKernel.comp instIsMarkovKernelPosterior Kernel.instIsMarkovKernelId MeasureTheory.Measure.deterministic_comp_eq_map MeasureTheory.Measure.compProd_eq_parallelComp_comp_copy_comp MeasureTheory.Measure.instSFiniteBindCoeKernelOfIsSFiniteKernel MeasureTheory.instSFiniteOfSigmaFinite MeasureTheory.IsFiniteMeasure.toSigmaFinite Kernel.IsFiniteKernel.isSFiniteKernel Kernel.parallelComp_id_left_comp_parallelComp MeasureTheory.Measure.comp_assoc parallelProd_posterior_comp_copy_comp Kernel.parallelComp_comp_parallelComp Kernel.id_comp Kernel.comp_id Kernel.deterministic_comp_copy MeasureTheory.Measure.compProd_id_eq_copy_comp MeasureTheory.Measure.instSFiniteMap
instIsMarkovKernelPosterior 📖	mathematical	—	IsMarkovKernel posterior	—	posterior.eq_1 MeasureTheory.Measure.instIsMarkovKernelCondKernel
parallelProd_posterior_comp_copy_comp 📖	mathematical	—	MeasureTheory.Measure.bind Prod.instMeasurableSpace DFunLike.coe Kernel MeasureTheory.Measure Kernel.instFunLike Kernel.copy Kernel.parallelComp Kernel.id posterior	—	MeasureTheory.Measure.compProd_eq_parallelComp_comp_copy_comp MeasureTheory.Measure.instSFiniteBindCoeKernelOfIsSFiniteKernel MeasureTheory.instSFiniteOfSigmaFinite MeasureTheory.IsFiniteMeasure.toSigmaFinite Kernel.IsFiniteKernel.isSFiniteKernel compProd_posterior_eq_swap_comp MeasureTheory.Measure.comp_assoc Kernel.swap_parallelComp Kernel.comp_assoc Kernel.swap_copy
posterior_boolKernel_apply_false 📖	mathematical	—	Filter.Eventually ENNReal DFunLike.coe MeasureTheory.Measure Bool.instMeasurableSpace Set MeasureTheory.Measure.instFunLike Kernel Kernel.instFunLike posterior standardBorelSpace_of_discreteMeasurableSpace instDiscreteMeasurableSpace Bool.countable Kernel.boolKernel Kernel.instIsFiniteKernelBoolBoolKernelOfIsFiniteMeasure Set.instSingletonSet Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring MeasureTheory.Measure.rnDeriv MeasureTheory.Measure.bind MeasureTheory.ae MeasureTheory.Measure.instOuterMeasureClass	—	Filter.mp_mem MeasureTheory.Measure.instOuterMeasureClass standardBorelSpace_of_discreteMeasurableSpace instDiscreteMeasurableSpace Bool.countable Kernel.instIsFiniteKernelBoolBoolKernelOfIsFiniteMeasure posterior_eq_withDensity_of_countable Filter.univ_mem' MeasureTheory.withDensity_apply IsScalarTower.right MeasureTheory.Measure.restrict_singleton MeasureTheory.lintegral_smul_measure MeasureTheory.lintegral_dirac Bool.instMeasurableSingletonClass
posterior_boolKernel_apply_true 📖	mathematical	—	Filter.Eventually ENNReal DFunLike.coe MeasureTheory.Measure Bool.instMeasurableSpace Set MeasureTheory.Measure.instFunLike Kernel Kernel.instFunLike posterior standardBorelSpace_of_discreteMeasurableSpace instDiscreteMeasurableSpace Bool.countable Kernel.boolKernel Kernel.instIsFiniteKernelBoolBoolKernelOfIsFiniteMeasure Set.instSingletonSet Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring MeasureTheory.Measure.rnDeriv MeasureTheory.Measure.bind MeasureTheory.ae MeasureTheory.Measure.instOuterMeasureClass	—	Filter.mp_mem MeasureTheory.Measure.instOuterMeasureClass standardBorelSpace_of_discreteMeasurableSpace instDiscreteMeasurableSpace Bool.countable Kernel.instIsFiniteKernelBoolBoolKernelOfIsFiniteMeasure posterior_eq_withDensity_of_countable Filter.univ_mem' MeasureTheory.withDensity_apply IsScalarTower.right MeasureTheory.Measure.restrict_singleton MeasureTheory.lintegral_smul_measure MeasureTheory.lintegral_dirac Bool.instMeasurableSingletonClass
posterior_comp 📖	mathematical	—	Filter.EventuallyEq MeasureTheory.Measure MeasureTheory.ae MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.bind DFunLike.coe Kernel Kernel.instFunLike posterior Kernel.comp Kernel.IsFiniteKernel.comp MeasureTheory.Measure.instIsFiniteMeasureBindCoeKernelOfIsFiniteKernel	—	MeasureTheory.Measure.instOuterMeasureClass Kernel.IsFiniteKernel.comp MeasureTheory.Measure.instIsFiniteMeasureBindCoeKernelOfIsFiniteKernel MeasureTheory.Measure.comp_assoc Filter.EventuallyEq.symm ae_eq_posterior_of_compProd_eq_swap_comp IsZeroOrMarkovKernel.isFiniteKernel IsMarkovKernel.IsZeroOrMarkovKernel instIsMarkovKernelPosterior MeasureTheory.Measure.compProd_eq_comp_prod MeasureTheory.Measure.instSFiniteBindCoeKernelOfIsSFiniteKernel MeasureTheory.instSFiniteOfSigmaFinite MeasureTheory.IsFiniteMeasure.toSigmaFinite Kernel.IsSFiniteKernel.comp Kernel.IsFiniteKernel.isSFiniteKernel parallelProd_posterior_comp_copy_comp Kernel.parallelComp_comm Kernel.comp_assoc Kernel.swap_parallelComp Kernel.swap_copy
posterior_comp_self 📖	mathematical	—	MeasureTheory.Measure.bind DFunLike.coe Kernel MeasureTheory.Measure Kernel.instFunLike posterior	—	MeasureTheory.Measure.snd_compProd MeasureTheory.Measure.instSFiniteBindCoeKernelOfIsSFiniteKernel MeasureTheory.instSFiniteOfSigmaFinite MeasureTheory.IsFiniteMeasure.toSigmaFinite Kernel.IsFiniteKernel.isSFiniteKernel IsZeroOrMarkovKernel.isFiniteKernel IsMarkovKernel.IsZeroOrMarkovKernel instIsMarkovKernelPosterior compProd_posterior_eq_map_swap MeasureTheory.Measure.snd_map_swap MeasureTheory.Measure.fst_compProd
posterior_eq_withDensity 📖	mathematical	Filter.Eventually MeasureTheory.Measure.AbsolutelyContinuous DFunLike.coe Kernel MeasureTheory.Measure Kernel.instFunLike MeasureTheory.Measure.bind MeasureTheory.ae MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	posterior MeasureTheory.Measure.withDensity Kernel.rnDeriv Kernel.const	—	MeasureTheory.Measure.instOuterMeasureClass Filter.mp_mem absolutelyContinuous_posterior MeasureTheory.Measure.instSFiniteBindCoeKernelOfIsSFiniteKernel MeasureTheory.instSFiniteOfSigmaFinite MeasureTheory.IsFiniteMeasure.toSigmaFinite Kernel.IsFiniteKernel.isSFiniteKernel MeasurableSpace.instCountableOrCountablyGeneratedOfCountablyGenerated countablyGenerated_of_standardBorel rnDeriv_posterior_symm Filter.univ_mem' MeasureTheory.Measure.ext MeasureTheory.Measure.setLIntegral_rnDeriv MeasureTheory.Measure.haveLebesgueDecomposition_of_sigmaFinite IsSFiniteKernel.sFinite IsZeroOrMarkovKernel.isFiniteKernel IsMarkovKernel.IsZeroOrMarkovKernel instIsMarkovKernelPosterior MeasureTheory.withDensity_apply MeasureTheory.setLIntegral_congr_fun_ae Kernel.rnDeriv_eq_rnDeriv_measure Kernel.const.instIsFiniteKernel Kernel.const_apply
posterior_eq_withDensity_of_countable 📖	mathematical	—	Filter.Eventually MeasureTheory.Measure DFunLike.coe Kernel Kernel.instFunLike posterior MeasureTheory.Measure.withDensity MeasureTheory.Measure.rnDeriv MeasureTheory.Measure.bind MeasureTheory.ae MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	MeasureTheory.Measure.instOuterMeasureClass MeasurableSpace.instCountableOrCountablyGeneratedOfCountable Kernel.rnDeriv_eq_rnDeriv_measure Kernel.const.instIsFiniteKernel MeasureTheory.Measure.instIsFiniteMeasureBindCoeKernelOfIsFiniteKernel Filter.mp_mem MeasureTheory.ae_all_iff posterior_eq_withDensity MeasureTheory.Measure.absolutelyContinuous_comp_of_countable measurableSingleton_of_standardBorel Filter.univ_mem'
posterior_id 📖	mathematical	—	Filter.EventuallyEq MeasureTheory.Measure MeasureTheory.ae MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass DFunLike.coe Kernel Kernel.instFunLike posterior Kernel.id IsZeroOrMarkovKernel.isFiniteKernel IsMarkovKernel.IsZeroOrMarkovKernel Kernel.instIsMarkovKernelId	—	MeasureTheory.Measure.instOuterMeasureClass IsZeroOrMarkovKernel.isFiniteKernel IsMarkovKernel.IsZeroOrMarkovKernel Kernel.instIsMarkovKernelId ae_eq_posterior_of_compProd_eq_swap_comp MeasureTheory.Measure.id_comp MeasureTheory.Measure.compProd_id_eq_copy_comp MeasureTheory.instSFiniteOfSigmaFinite MeasureTheory.IsFiniteMeasure.toSigmaFinite MeasureTheory.Measure.comp_assoc Kernel.swap_copy Filter.mp_mem Filter.univ_mem'
posterior_posterior 📖	mathematical	—	Filter.EventuallyEq MeasureTheory.Measure MeasureTheory.ae MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass DFunLike.coe Kernel Kernel.instFunLike posterior MeasureTheory.Measure.bind MeasureTheory.Measure.instIsFiniteMeasureBindCoeKernelOfIsFiniteKernel IsZeroOrMarkovKernel.isFiniteKernel IsMarkovKernel.IsZeroOrMarkovKernel instIsMarkovKernelPosterior	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.instIsFiniteMeasureBindCoeKernelOfIsFiniteKernel IsZeroOrMarkovKernel.isFiniteKernel IsMarkovKernel.IsZeroOrMarkovKernel instIsMarkovKernelPosterior ae_eq_posterior_of_compProd_eq_swap_comp posterior_comp_self compProd_posterior_eq_swap_comp MeasureTheory.Measure.comp_assoc Kernel.swap_swap MeasureTheory.Measure.id_comp Filter.mp_mem Filter.univ_mem'
posterior_prod_id_comp 📖	mathematical	—	MeasureTheory.Measure.bind Prod.instMeasurableSpace DFunLike.coe Kernel MeasureTheory.Measure Kernel.instFunLike Kernel.prod posterior Kernel.id MeasureTheory.Measure.compProd	—	Kernel.swap_prod Kernel.IsFiniteKernel.isSFiniteKernel IsZeroOrMarkovKernel.isFiniteKernel IsMarkovKernel.IsZeroOrMarkovKernel Kernel.instIsMarkovKernelId instIsMarkovKernelPosterior MeasureTheory.Measure.comp_assoc MeasureTheory.Measure.compProd_eq_comp_prod MeasureTheory.Measure.instSFiniteBindCoeKernelOfIsSFiniteKernel MeasureTheory.instSFiniteOfSigmaFinite MeasureTheory.IsFiniteMeasure.toSigmaFinite compProd_posterior_eq_swap_comp Kernel.swap_swap MeasureTheory.Measure.id_comp
rnDeriv_posterior 📖	mathematical	Filter.Eventually MeasureTheory.Measure.AbsolutelyContinuous DFunLike.coe Kernel MeasureTheory.Measure Kernel.instFunLike MeasureTheory.Measure.bind MeasureTheory.ae MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	ENNReal Kernel.rnDeriv MeasurableSpace.instCountableOrCountablyGeneratedOfCountablyGenerated countablyGenerated_of_standardBorel posterior Kernel.const	—	MeasureTheory.Measure.instOuterMeasureClass MeasurableSpace.instCountableOrCountablyGeneratedOfCountablyGenerated countablyGenerated_of_standardBorel MeasureTheory.Measure.ae_ae_of_ae_prod MeasureTheory.Measure.instSFiniteBindCoeKernelOfIsSFiniteKernel MeasureTheory.instSFiniteOfSigmaFinite MeasureTheory.IsFiniteMeasure.toSigmaFinite Kernel.IsFiniteKernel.isSFiniteKernel rnDeriv_posterior_ae_prod
rnDeriv_posterior_ae_prod 📖	mathematical	Filter.Eventually MeasureTheory.Measure.AbsolutelyContinuous DFunLike.coe Kernel MeasureTheory.Measure Kernel.instFunLike MeasureTheory.Measure.bind MeasureTheory.ae MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	ENNReal Kernel.rnDeriv MeasurableSpace.instCountableOrCountablyGeneratedOfCountablyGenerated countablyGenerated_of_standardBorel posterior Kernel.const Prod.instMeasurableSpace MeasureTheory.Measure.prod	—	MeasureTheory.Measure.instOuterMeasureClass MeasurableSpace.instCountableOrCountablyGeneratedOfCountablyGenerated countablyGenerated_of_standardBorel MeasureTheory.setLIntegral_prod_symm MeasureTheory.Measure.instSFiniteBindCoeKernelOfIsSFiniteKernel MeasureTheory.instSFiniteOfSigmaFinite MeasureTheory.IsFiniteMeasure.toSigmaFinite Kernel.IsFiniteKernel.isSFiniteKernel Measurable.comp_aemeasurable' Kernel.measurable_rnDeriv AEMeasurable.prodMk AEMeasurable.snd aemeasurable_id AEMeasurable.fst swap_compProd_posterior MeasureTheory.Measure.swap_comp MeasureTheory.Measure.map_apply measurable_swap MeasurableSet.prod Set.preimage_swap_prod MeasureTheory.Measure.compProd_apply_prod IsZeroOrMarkovKernel.isFiniteKernel IsMarkovKernel.IsZeroOrMarkovKernel instIsMarkovKernelPosterior MeasureTheory.lintegral_congr_ae MeasureTheory.ae_restrict_of_ae Filter.mp_mem absolutelyContinuous_posterior Filter.univ_mem' Kernel.setLIntegral_rnDeriv Kernel.const.instIsFiniteKernel MeasureTheory.setLIntegral_prod Measurable.aemeasurable MeasureTheory.Measure.instIsFiniteMeasureBindCoeKernelOfIsFiniteKernel MeasureTheory.ae_eq_of_setLIntegral_prod_eq ne_of_lt MeasureTheory.setLIntegral_univ Set.univ_prod_univ MeasurableSet.univ MeasureTheory.measure_lt_top MeasureTheory.Measure.instIsFiniteMeasureProdCompProdOfIsFiniteKernel
rnDeriv_posterior_symm 📖	mathematical	Filter.Eventually MeasureTheory.Measure.AbsolutelyContinuous DFunLike.coe Kernel MeasureTheory.Measure Kernel.instFunLike MeasureTheory.Measure.bind MeasureTheory.ae MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	ENNReal Kernel.rnDeriv MeasurableSpace.instCountableOrCountablyGeneratedOfCountablyGenerated countablyGenerated_of_standardBorel posterior Kernel.const	—	MeasureTheory.Measure.instOuterMeasureClass MeasurableSpace.instCountableOrCountablyGeneratedOfCountablyGenerated countablyGenerated_of_standardBorel MeasureTheory.Measure.ae_ae_comm MeasureTheory.instSFiniteOfSigmaFinite MeasureTheory.IsFiniteMeasure.toSigmaFinite MeasureTheory.Measure.instSFiniteBindCoeKernelOfIsSFiniteKernel Kernel.IsFiniteKernel.isSFiniteKernel Measurable.eq instMeasurableEqOfSecondCountableTopologyOfT2Space BorelSpace.opensMeasurable ENNReal.borelSpace ENNReal.instSecondCountableTopology ENNReal.instT2Space Kernel.measurable_rnDeriv Measurable.fun_comp Measurable.prodMk Measurable.snd measurable_id' Measurable.fst rnDeriv_posterior
swap_compProd_posterior 📖	mathematical	—	MeasureTheory.Measure.bind Prod.instMeasurableSpace MeasureTheory.Measure.compProd DFunLike.coe Kernel MeasureTheory.Measure Kernel.instFunLike posterior Kernel.swap	—	compProd_posterior_eq_swap_comp MeasureTheory.Measure.comp_assoc Kernel.swap_swap MeasureTheory.Measure.id_comp

ProbabilityTheory.Kernel

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
absolutelyContinuous_comp_of_absolutelyContinuous 📖	mathematical	Filter.Eventually MeasureTheory.Measure.AbsolutelyContinuous DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike MeasureTheory.ae MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	MeasureTheory.Measure.bind	—	MeasureTheory.Measure.instOuterMeasureClass ProbabilityTheory.absolutelyContinuous_posterior_iff ProbabilityTheory.absolutelyContinuous_posterior

---

← Back to Index