Invariance

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

Statistics

Metric	Count
Definitions IsReversible	1
Theorems comp, comp_const, def, invariant	4
Total	5

ProbabilityTheory.Kernel

Definitions

Name	Category	Theorems
IsReversible 📖	MathDef	—

ProbabilityTheory.Kernel.Invariant

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp 📖	mathematical	ProbabilityTheory.Kernel.Invariant	ProbabilityTheory.Kernel.comp	—	isEmpty_or_nonempty MeasureTheory.Measure.instSubsingleton eq_1 MeasureTheory.Measure.comp_assoc
comp_const 📖	mathematical	ProbabilityTheory.Kernel.Invariant	ProbabilityTheory.Kernel.comp ProbabilityTheory.Kernel.const	—	ProbabilityTheory.Kernel.comp_const def
def 📖	mathematical	ProbabilityTheory.Kernel.Invariant	MeasureTheory.Measure.bind DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure ProbabilityTheory.Kernel.instFunLike	—	—

ProbabilityTheory.Kernel.IsReversible

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
invariant 📖	mathematical	ProbabilityTheory.Kernel.IsReversible	ProbabilityTheory.Kernel.Invariant	—	MeasureTheory.Measure.ext MeasureTheory.Measure.bind_apply ProbabilityTheory.Kernel.aemeasurable MeasureTheory.IsProbabilityMeasure.measure_univ ProbabilityTheory.IsMarkovKernel.is_probability_measure' MeasureTheory.lintegral_const MeasureTheory.Measure.restrict_apply Set.univ_inter one_mul MeasureTheory.Measure.restrict_univ MeasurableSet.univ

---

← Back to Index