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₂.