ConditionalKernelFiber.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Every measurable observable of the conditioning factor is almost surely constant under almost every component, at its value on that component.

theorem OAI.PolycyclicRecognition.factorConditionalKernel_fiber line 26
Source documentation
A factor observable retains its value under the conditional probability.
```
theorem factorConditionalKernel_fiber :
    ∀ᵐ y ∂μ.map f, ∀ᵐ x ∂factorConditionalKernel μ f hf y, h (f x) = h y := by
…
```
Mentions: OAI.PolycyclicRecognition.factorConditionalKernel