ConditionalKernelConsistency.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Consistency of conditional component measures

A conditional probability is concentrated where its own conditional probability has the same value. Only a countable determining family of measurable sets is used to obtain one simultaneous almost-everywhere statement.

theorem OAI.PolycyclicRecognition.factorConditionalKernel_consistent line 24
Source documentation
Equality of measures, simultaneously on almost every fiber.
```
theorem factorConditionalKernel_consistent :
    ∀ᵐ y ∂μ.map f, ∀ᵐ x ∂factorConditionalKernel μ f hf y,
      factorConditionalKernel μ f hf (f x) = factorConditionalKernel μ f hf y := by
…
```
Mentions: OAI.PolycyclicRecognition.factorConditionalKernel
theorem OAI.PolycyclicRecognition.invariantConditionalMeasures_consistent line 37
Source documentation
The same consistency statement on the original action space.
```
theorem invariantConditionalMeasures_consistent :
    ∀ᵐ x ∂μ, ∀ᵐ y ∂invariantConditionalMeasures (G := G) μ x,
…
```
Mentions: OAI.PolycyclicRecognition.invariantConditionalMeasures