CountableMeasureTests.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

A countable determining family for finite measures

Finite intersections of a countable measurable generator form a countable pi system. Equality on this family and equality of total mass determine a finite measure. This permits simultaneous statements about conditional kernels.

def OAI.PolycyclicRecognition.finiteMeasureTest line 23
Source documentation
Finite intersections, including the empty intersection.
```
def finiteMeasureTest (I : Finset ℕ) : Set X :=
…
```
theorem OAI.PolycyclicRecognition.measurableSet_finiteMeasureTest line 26
theorem OAI.PolycyclicRecognition.finiteMeasureTest_union line 31
theorem OAI.PolycyclicRecognition.isPiSystem_finiteMeasureTest line 42
theorem OAI.PolycyclicRecognition.generateFrom_finiteMeasureTest line 46
theorem OAI.PolycyclicRecognition.measure_eq_of_finiteMeasureTests line 56
Source documentation
A countable determining test suitable for probability kernels.
```
theorem measure_eq_of_finiteMeasureTests (μ ν : Measure X) [IsFiniteMeasure μ]
    (h : ∀ I, μ (finiteMeasureTest X I) = ν (finiteMeasureTest X I)) : μ = ν := by
…
```
Mentions: OAI.PolycyclicRecognition.finiteMeasureTest