Process

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

Statistics

Metric	Count
Definitions	0
Theorems indepFun_process, process_indepFun, process_indepFun_process, indepFun_process, process_indepFun, process_indepFun_process, iIndepFun_process, iIndepFun_process	8
Total	8

ProbabilityTheory.IndepFun

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
indepFun_process 📖	—	AEMeasurable Measurable ProbabilityTheory.IndepFun MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike	—	—	ProbabilityTheory.Kernel.IndepFun.indepFun_process congr Filter.EventuallyEq.rfl MeasureTheory.Measure.instOuterMeasureClass ProbabilityTheory.Kernel.const.instIsZeroOrMarkovKernel Filter.EventuallyEq.symm
process_indepFun 📖	—	Measurable AEMeasurable ProbabilityTheory.IndepFun MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike	—	—	ProbabilityTheory.Kernel.IndepFun.process_indepFun congr Filter.EventuallyEq.rfl MeasureTheory.Measure.instOuterMeasureClass ProbabilityTheory.Kernel.const.instIsZeroOrMarkovKernel Filter.EventuallyEq.symm
process_indepFun_process 📖	—	Measurable ProbabilityTheory.IndepFun MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike	—	—	ProbabilityTheory.Kernel.IndepFun.process_indepFun_process ProbabilityTheory.Kernel.const.instIsZeroOrMarkovKernel

ProbabilityTheory.Kernel.IndepFun

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
indepFun_process 📖	—	Measurable ProbabilityTheory.Kernel.IndepFun MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike	—	—	symm process_indepFun
process_indepFun 📖	—	Measurable ProbabilityTheory.Kernel.IndepFun MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike	—	—	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 📖	—	Measurable ProbabilityTheory.Kernel.IndepFun MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike	—	—	process_indepFun measurable_pi_lambda indepFun_process

ProbabilityTheory.Kernel.iIndepFun

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
iIndepFun_process 📖	—	Measurable ProbabilityTheory.Kernel.iIndepFun Finset SetLike.instMembership Finset.instSetLike 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

ProbabilityTheory.iIndepFun

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
iIndepFun_process 📖	—	Measurable ProbabilityTheory.iIndepFun Finset SetLike.instMembership Finset.instSetLike MeasurableSpace.pi	—	—	ProbabilityTheory.Kernel.iIndepFun.iIndepFun_process

---

← Back to Index