Basic

📁 Source: Mathlib/Probability/Independence/Process/Basic.lean

Statistics

Metric	Count
Definitions	0
Theorems indepFun_process, indepFun_process₀, process_congr, process_congr_left, process_congr_right, process_indepFun, process_indepFun_process, process_indepFun_process₀, process_indepFun₀, indepFun_process, indepFun_process₀, process_congr, process_congr_left, process_congr_right, process_indepFun, process_indepFun_process, process_indepFun_process₀, process_indepFun₀, iIndepFun_process, iIndepFun_process₀, process_congr, iIndepFun_process, iIndepFun_process₀, process_congr	24
Total	24

ProbabilityTheory.IndepFun

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
indepFun_process 📖	mathematical	Measurable ProbabilityTheory.IndepFun MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike	ProbabilityTheory.IndepFun MeasurableSpace.pi	—	ProbabilityTheory.Kernel.IndepFun.indepFun_process ProbabilityTheory.Kernel.const.instIsZeroOrMarkovKernel
indepFun_process₀ 📖	mathematical	AEMeasurable ProbabilityTheory.IndepFun MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike	ProbabilityTheory.IndepFun MeasurableSpace.pi	—	ProbabilityTheory.Kernel.IndepFun.indepFun_process₀ IsScalarTower.right MeasureTheory.Measure.const_comp MeasureTheory.IsProbabilityMeasure.measure_univ MeasureTheory.Measure.dirac.isProbabilityMeasure one_smul ProbabilityTheory.Kernel.const.instIsZeroOrMarkovKernel
process_congr 📖	mathematical	ProbabilityTheory.IndepFun MeasurableSpace.pi Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	ProbabilityTheory.IndepFun MeasurableSpace.pi	—	MeasureTheory.Measure.instOuterMeasureClass ProbabilityTheory.Kernel.IndepFun.process_congr MeasureTheory.ae_dirac_eq instMeasurableSingletonClassOfMeasurableEq instMeasurableEqOfSecondCountableTopologyOfT2Space BorelSpace.opensMeasurable Unit.borelSpace TopologicalSpace.instSecondCountableTopologyOfLindelofSpaceOfPseudoMetrizableSpace Countable.LindelofSpace instCountablePUnit PseudoEMetricSpace.pseudoMetrizableSpace TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace
process_congr_left 📖	mathematical	ProbabilityTheory.IndepFun MeasurableSpace.pi Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	ProbabilityTheory.IndepFun MeasurableSpace.pi	—	MeasureTheory.Measure.instOuterMeasureClass ProbabilityTheory.Kernel.IndepFun.process_congr_left MeasureTheory.ae_dirac_eq instMeasurableSingletonClassOfMeasurableEq instMeasurableEqOfSecondCountableTopologyOfT2Space BorelSpace.opensMeasurable Unit.borelSpace TopologicalSpace.instSecondCountableTopologyOfLindelofSpaceOfPseudoMetrizableSpace Countable.LindelofSpace instCountablePUnit PseudoEMetricSpace.pseudoMetrizableSpace TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace
process_congr_right 📖	mathematical	ProbabilityTheory.IndepFun MeasurableSpace.pi Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	ProbabilityTheory.IndepFun MeasurableSpace.pi	—	MeasureTheory.Measure.instOuterMeasureClass ProbabilityTheory.Kernel.IndepFun.process_congr_right MeasureTheory.ae_dirac_eq instMeasurableSingletonClassOfMeasurableEq instMeasurableEqOfSecondCountableTopologyOfT2Space BorelSpace.opensMeasurable Unit.borelSpace TopologicalSpace.instSecondCountableTopologyOfLindelofSpaceOfPseudoMetrizableSpace Countable.LindelofSpace instCountablePUnit PseudoEMetricSpace.pseudoMetrizableSpace TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace
process_indepFun 📖	mathematical	Measurable ProbabilityTheory.IndepFun MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike	ProbabilityTheory.IndepFun MeasurableSpace.pi	—	ProbabilityTheory.Kernel.IndepFun.process_indepFun ProbabilityTheory.Kernel.const.instIsZeroOrMarkovKernel
process_indepFun_process 📖	mathematical	Measurable ProbabilityTheory.IndepFun MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike	ProbabilityTheory.IndepFun MeasurableSpace.pi	—	ProbabilityTheory.Kernel.IndepFun.process_indepFun_process ProbabilityTheory.Kernel.const.instIsZeroOrMarkovKernel
process_indepFun_process₀ 📖	mathematical	AEMeasurable ProbabilityTheory.IndepFun MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike	ProbabilityTheory.IndepFun MeasurableSpace.pi	—	ProbabilityTheory.Kernel.IndepFun.process_indepFun_process₀ IsScalarTower.right MeasureTheory.Measure.const_comp MeasureTheory.IsProbabilityMeasure.measure_univ MeasureTheory.Measure.dirac.isProbabilityMeasure one_smul ProbabilityTheory.Kernel.const.instIsZeroOrMarkovKernel
process_indepFun₀ 📖	mathematical	AEMeasurable ProbabilityTheory.IndepFun MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike	ProbabilityTheory.IndepFun MeasurableSpace.pi	—	ProbabilityTheory.Kernel.IndepFun.process_indepFun₀ IsScalarTower.right MeasureTheory.Measure.const_comp MeasureTheory.IsProbabilityMeasure.measure_univ MeasureTheory.Measure.dirac.isProbabilityMeasure one_smul ProbabilityTheory.Kernel.const.instIsZeroOrMarkovKernel

ProbabilityTheory.Kernel.IndepFun

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
indepFun_process 📖	mathematical	Measurable ProbabilityTheory.Kernel.IndepFun MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike	ProbabilityTheory.Kernel.IndepFun MeasurableSpace.pi	—	symm process_indepFun
indepFun_process₀ 📖	mathematical	AEMeasurable MeasureTheory.Measure.bind DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure ProbabilityTheory.Kernel.instFunLike ProbabilityTheory.Kernel.IndepFun MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike	ProbabilityTheory.Kernel.IndepFun MeasurableSpace.pi	—	symm process_indepFun₀
process_congr 📖	mathematical	ProbabilityTheory.Kernel.IndepFun MeasurableSpace.pi Filter.Eventually Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass DFunLike.coe ProbabilityTheory.Kernel ProbabilityTheory.Kernel.instFunLike	ProbabilityTheory.Kernel.IndepFun MeasurableSpace.pi	—	MeasureTheory.Measure.instOuterMeasureClass process_congr_left process_congr_right
process_congr_left 📖	mathematical	ProbabilityTheory.Kernel.IndepFun MeasurableSpace.pi Filter.Eventually Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass DFunLike.coe ProbabilityTheory.Kernel ProbabilityTheory.Kernel.instFunLike	ProbabilityTheory.Kernel.IndepFun MeasurableSpace.pi	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.MeasurableSet.eq_preimage_restrict_countable Set.Countable.to_subtype Filter.mp_mem MeasureTheory.ae_all_iff Filter.univ_mem' MeasureTheory.measure_congr MeasureTheory.ae_eq_set_inter Filter.EventuallyEq.preimage Filter.EventuallyEq.symm Filter.EventuallyEq.rfl
process_congr_right 📖	mathematical	ProbabilityTheory.Kernel.IndepFun MeasurableSpace.pi Filter.Eventually Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass DFunLike.coe ProbabilityTheory.Kernel ProbabilityTheory.Kernel.instFunLike	ProbabilityTheory.Kernel.IndepFun MeasurableSpace.pi	—	MeasureTheory.Measure.instOuterMeasureClass symm process_congr_left
process_indepFun 📖	mathematical	Measurable ProbabilityTheory.Kernel.IndepFun MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike	ProbabilityTheory.Kernel.IndepFun MeasurableSpace.pi	—	IsPiSystem.comap MeasureTheory.isPiSystem_squareCylinders MeasurableSpace.isPiSystem_measurableSet MeasureTheory.generateFrom_squareCylinders MeasurableSpace.comap_generateFrom ProbabilityTheory.Kernel.IndepSets.indep Measurable.comap_le measurable_pi_iff MeasurableSpace.generateFrom_measurableSet MeasureTheory.Measure.instOuterMeasureClass Set.ext Finset.coe_attach MeasurableSet.pi Finset.countable_toSet Filter.mp_mem measure_inter_preimage_eq_mul Filter.univ_mem'
process_indepFun_process 📖	mathematical	Measurable ProbabilityTheory.Kernel.IndepFun MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike	ProbabilityTheory.Kernel.IndepFun MeasurableSpace.pi	—	process_indepFun measurable_pi_lambda indepFun_process
process_indepFun_process₀ 📖	mathematical	AEMeasurable MeasureTheory.Measure.bind DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure ProbabilityTheory.Kernel.instFunLike ProbabilityTheory.Kernel.IndepFun MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike	ProbabilityTheory.Kernel.IndepFun MeasurableSpace.pi	—	process_congr process_indepFun_process MeasureTheory.Measure.ae_ae_of_ae_comp Filter.EventuallyEq.symm MeasureTheory.Measure.instOuterMeasureClass
process_indepFun₀ 📖	mathematical	AEMeasurable MeasureTheory.Measure.bind DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure ProbabilityTheory.Kernel.instFunLike ProbabilityTheory.Kernel.IndepFun MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike	ProbabilityTheory.Kernel.IndepFun MeasurableSpace.pi	—	congr' process_congr_left process_indepFun MeasureTheory.ae_of_all MeasureTheory.Measure.instOuterMeasureClass Filter.EventuallyEq.rfl MeasureTheory.Measure.ae_ae_of_ae_comp Filter.EventuallyEq.symm

ProbabilityTheory.Kernel.iIndepFun

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
iIndepFun_process 📖	mathematical	Measurable ProbabilityTheory.Kernel.iIndepFun Finset SetLike.instMembership Finset.instSetLike MeasurableSpace.pi	ProbabilityTheory.Kernel.iIndepFun MeasurableSpace.pi	—	eq_or_ne MeasureTheory.Measure.instOuterMeasureClass ProbabilityTheory.Kernel.exists_ae_eq_isMarkovKernel ae_isProbabilityMeasure congr Filter.EventuallyEq.symm IsPiSystem.comap MeasureTheory.isPiSystem_squareCylinders MeasurableSpace.isPiSystem_measurableSet MeasureTheory.generateFrom_squareCylinders MeasurableSpace.comap_generateFrom ProbabilityTheory.Kernel.iIndepSets.iIndep Measurable.comap_le measurable_pi_iff Set.iInter₂_congr Finset.prod_congr Set.ext Set.iInter_congr_Prop Finset.coe_attach Set.iInter_true MeasurableSet.pi Finset.countable_toSet Filter.mp_mem measure_inter_preimage_eq_mul Filter.univ_mem' Finset.prod_coe_sort Function.sometimes_spec
iIndepFun_process₀ 📖	mathematical	AEMeasurable MeasureTheory.Measure.bind DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure ProbabilityTheory.Kernel.instFunLike ProbabilityTheory.Kernel.iIndepFun Finset SetLike.instMembership Finset.instSetLike MeasurableSpace.pi	ProbabilityTheory.Kernel.iIndepFun MeasurableSpace.pi	—	process_congr iIndepFun_process MeasureTheory.Measure.ae_ae_of_ae_comp Filter.EventuallyEq.symm MeasureTheory.Measure.instOuterMeasureClass
process_congr 📖	mathematical	ProbabilityTheory.Kernel.iIndepFun MeasurableSpace.pi Filter.Eventually Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass DFunLike.coe ProbabilityTheory.Kernel ProbabilityTheory.Kernel.instFunLike	ProbabilityTheory.Kernel.iIndepFun MeasurableSpace.pi	—	MeasureTheory.Measure.instOuterMeasureClass biInf_congr Finset.prod_congr Set.iInter_congr_Prop MeasureTheory.ae_ball_iff Finset.countable_toSet Set.Countable.to_subtype Filter.mp_mem MeasureTheory.ae_all_iff Filter.univ_mem' MeasureTheory.measure_congr MeasureTheory.ae_eq_set_biInter Filter.EventuallyEq.symm Filter.EventuallyEq.preimage Function.sometimes_spec MeasureTheory.MeasurableSet.eq_preimage_restrict_countable

ProbabilityTheory.iIndepFun

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
iIndepFun_process 📖	mathematical	Measurable ProbabilityTheory.iIndepFun Finset SetLike.instMembership Finset.instSetLike MeasurableSpace.pi	ProbabilityTheory.iIndepFun MeasurableSpace.pi	—	ProbabilityTheory.Kernel.iIndepFun.iIndepFun_process
iIndepFun_process₀ 📖	mathematical	AEMeasurable ProbabilityTheory.iIndepFun Finset SetLike.instMembership Finset.instSetLike MeasurableSpace.pi	ProbabilityTheory.iIndepFun MeasurableSpace.pi	—	ProbabilityTheory.Kernel.iIndepFun.iIndepFun_process₀ IsScalarTower.right MeasureTheory.Measure.const_comp MeasureTheory.IsProbabilityMeasure.measure_univ MeasureTheory.Measure.dirac.isProbabilityMeasure one_smul
process_congr 📖	mathematical	ProbabilityTheory.iIndepFun MeasurableSpace.pi Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	ProbabilityTheory.iIndepFun MeasurableSpace.pi	—	MeasureTheory.Measure.instOuterMeasureClass ProbabilityTheory.Kernel.iIndepFun.process_congr MeasureTheory.ae_dirac_eq instMeasurableSingletonClassOfMeasurableEq instMeasurableEqOfSecondCountableTopologyOfT2Space BorelSpace.opensMeasurable Unit.borelSpace TopologicalSpace.instSecondCountableTopologyOfLindelofSpaceOfPseudoMetrizableSpace Countable.LindelofSpace instCountablePUnit PseudoEMetricSpace.pseudoMetrizableSpace TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace

---

← Back to Index