TODO #
Reopen https://github.com/leanprover-community/mathlib4/pull/17859 once we have more API depending on this definition.
def
MeasureTheory.Filtration.IsConsistentKernel
{X : Type u_1}
{P : Type u_2}
{mX : MeasurableSpace X}
[PartialOrder P]
(mXs : Filtration P mX)
(γ : (p : P) → ProbabilityTheory.Kernel X X)
:
A family of kernels γ on X indexed by a partial order P is consistent under conditioning
if γ p₂ ∘ₖ γ p₁ = γ p₁ whenever p₁ ≤ p₂.