Kolmogorov

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

Statistics

Metric	Count
Definitions IsAEKolmogorovProcess, mk, IsKolmogorovProcess	3
Theorems IsKolmogorovProcess_mk, ae_eq_mk, aemeasurable, aemeasurable_edist, aestronglyMeasurable_edist, edist_eq_zero, edist_eq_zero_of_const_eq_zero, kolmogorovCondition, p_pos, q_pos, IsAEKolmogorovProcess, edist_eq_zero, edist_eq_zero_of_const_eq_zero, kolmogorovCondition, measurable, measurablePair, measurable_edist, mk_of_secondCountableTopology, p_pos, q_pos, stronglyMeasurable_edist	21
Total	24

ProbabilityTheory

Definitions

Name	Category	Theorems
IsAEKolmogorovProcess 📖	MathDef	1 math math: IsKolmogorovProcess.IsAEKolmogorovProcess
IsKolmogorovProcess 📖	CompData	2 math math: IsAEKolmogorovProcess.IsKolmogorovProcess_mk, IsKolmogorovProcess.mk_of_secondCountableTopology

ProbabilityTheory.IsAEKolmogorovProcess

Definitions

Name	Category	Theorems
mk 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
IsKolmogorovProcess_mk 📖	mathematical	ProbabilityTheory.IsAEKolmogorovProcess	ProbabilityTheory.IsKolmogorovProcess	—	MeasureTheory.Measure.instOuterMeasureClass
ae_eq_mk 📖	mathematical	ProbabilityTheory.IsAEKolmogorovProcess	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	MeasureTheory.Measure.instOuterMeasureClass
aemeasurable 📖	mathematical	ProbabilityTheory.IsAEKolmogorovProcess	AEMeasurable	—	MeasureTheory.Measure.instOuterMeasureClass ProbabilityTheory.IsKolmogorovProcess.measurable Filter.mp_mem Filter.univ_mem'
aemeasurable_edist 📖	mathematical	ProbabilityTheory.IsAEKolmogorovProcess	AEMeasurable ENNReal ENNReal.measurableSpace EDist.edist PseudoEMetricSpace.toEDist	—	MeasureTheory.AEStronglyMeasurable.aemeasurable TopologicalSpace.MetrizableSpace.toPseudoMetrizableSpace ENNReal.instMetrizableSpace ENNReal.borelSpace aestronglyMeasurable_edist
aestronglyMeasurable_edist 📖	mathematical	ProbabilityTheory.IsAEKolmogorovProcess	MeasureTheory.AEStronglyMeasurable ENNReal ENNReal.instTopologicalSpace EDist.edist PseudoEMetricSpace.toEDist	—	MeasureTheory.Measure.instOuterMeasureClass ProbabilityTheory.IsKolmogorovProcess.stronglyMeasurable_edist Filter.mp_mem Filter.univ_mem'
edist_eq_zero 📖	mathematical	ProbabilityTheory.IsAEKolmogorovProcess EDist.edist PseudoEMetricSpace.toEDist ENNReal instZeroENNReal	Filter.Eventually MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.lintegral_eq_zero_iff' AEMeasurable.pow_const ENNReal.hasMeasurablePow aemeasurable_edist nonpos_iff_eq_zero ENNReal.instCanonicallyOrderedAdd kolmogorovCondition ENNReal.zero_rpow_of_pos q_pos MulZeroClass.mul_zero Filter.mp_mem Filter.univ_mem' p_pos not_lt_of_gt
edist_eq_zero_of_const_eq_zero 📖	mathematical	ProbabilityTheory.IsAEKolmogorovProcess NNReal instZeroNNReal	Filter.Eventually ENNReal EDist.edist PseudoEMetricSpace.toEDist instZeroENNReal MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.lintegral_eq_zero_iff' AEMeasurable.pow_const ENNReal.hasMeasurablePow aemeasurable_edist nonpos_iff_eq_zero ENNReal.instCanonicallyOrderedAdd kolmogorovCondition MulZeroClass.zero_mul Filter.mp_mem Filter.univ_mem' p_pos not_lt_of_gt
kolmogorovCondition 📖	mathematical	ProbabilityTheory.IsAEKolmogorovProcess	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder MeasureTheory.lintegral Real ENNReal.instPowReal EDist.edist PseudoEMetricSpace.toEDist Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.ofNNReal	—	MeasureTheory.lintegral_congr_ae Filter.mp_mem MeasureTheory.Measure.instOuterMeasureClass Filter.univ_mem' ProbabilityTheory.IsKolmogorovProcess.kolmogorovCondition
p_pos 📖	mathematical	ProbabilityTheory.IsAEKolmogorovProcess	Real Real.instLT Real.instZero	—	ProbabilityTheory.IsKolmogorovProcess.p_pos
q_pos 📖	mathematical	ProbabilityTheory.IsAEKolmogorovProcess	Real Real.instLT Real.instZero	—	ProbabilityTheory.IsKolmogorovProcess.q_pos

ProbabilityTheory.IsKolmogorovProcess

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
IsAEKolmogorovProcess 📖	mathematical	ProbabilityTheory.IsKolmogorovProcess	ProbabilityTheory.IsAEKolmogorovProcess	—	MeasureTheory.Measure.instOuterMeasureClass
edist_eq_zero 📖	mathematical	ProbabilityTheory.IsKolmogorovProcess EDist.edist PseudoEMetricSpace.toEDist ENNReal instZeroENNReal	Filter.Eventually MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	ProbabilityTheory.IsAEKolmogorovProcess.edist_eq_zero IsAEKolmogorovProcess
edist_eq_zero_of_const_eq_zero 📖	mathematical	ProbabilityTheory.IsKolmogorovProcess NNReal instZeroNNReal	Filter.Eventually ENNReal EDist.edist PseudoEMetricSpace.toEDist instZeroENNReal MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	ProbabilityTheory.IsAEKolmogorovProcess.edist_eq_zero_of_const_eq_zero IsAEKolmogorovProcess
kolmogorovCondition 📖	mathematical	ProbabilityTheory.IsKolmogorovProcess	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder MeasureTheory.lintegral Real ENNReal.instPowReal EDist.edist PseudoEMetricSpace.toEDist Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.ofNNReal	—	—
measurable 📖	mathematical	ProbabilityTheory.IsKolmogorovProcess	Measurable	—	Measurable.comp Measurable.mono measurable_fst prod_le_borel_prod le_rfl measurablePair
measurablePair 📖	mathematical	ProbabilityTheory.IsKolmogorovProcess	Measurable borel instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace	—	—
measurable_edist 📖	mathematical	ProbabilityTheory.IsKolmogorovProcess	Measurable ENNReal ENNReal.measurableSpace EDist.edist PseudoEMetricSpace.toEDist	—	MeasureTheory.StronglyMeasurable.measurable TopologicalSpace.MetrizableSpace.toPseudoMetrizableSpace ENNReal.instMetrizableSpace ENNReal.borelSpace stronglyMeasurable_edist
mk_of_secondCountableTopology 📖	mathematical	Measurable ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder MeasureTheory.lintegral Real ENNReal.instPowReal EDist.edist PseudoEMetricSpace.toEDist Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.ofNNReal Real.instLT Real.instZero	ProbabilityTheory.IsKolmogorovProcess	—	Measurable.prodMk BorelSpace.measurable_eq Prod.borelSpace secondCountableTopologyEither_of_right
p_pos 📖	mathematical	ProbabilityTheory.IsKolmogorovProcess	Real Real.instLT Real.instZero	—	—
q_pos 📖	mathematical	ProbabilityTheory.IsKolmogorovProcess	Real Real.instLT Real.instZero	—	—
stronglyMeasurable_edist 📖	mathematical	ProbabilityTheory.IsKolmogorovProcess	MeasureTheory.StronglyMeasurable ENNReal ENNReal.instTopologicalSpace EDist.edist PseudoEMetricSpace.toEDist	—	MeasureTheory.StronglyMeasurable.comp_measurable Continuous.stronglyMeasurable BorelSpace.opensMeasurable TopologicalSpace.MetrizableSpace.toPseudoMetrizableSpace ENNReal.instMetrizableSpace secondCountableTopologyEither_of_right ENNReal.instSecondCountableTopology continuous_edist measurablePair

---

← Back to Index