CountableWeakTests.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Countably many measure evaluations determine weak convergence

Finite unions from a countable open basis suffice for the Portmanteau lower bound on every open set. This is used to connect the measurable kernel evaluations to the weak topology, without assuming a measurable selection of tangent frames.

def OAI.DukePrimeDegree.finiteBasisUnion line 25
lemma OAI.DukePrimeDegree.isOpen_finiteBasisUnion line 29
theorem OAI.DukePrimeDegree.tendsto_probability_of_finiteBasisUnion line 33
theorem OAI.DukePrimeDegree.measurable_kernel_finiteBasisUnion line 87
Source documentation
The coordinate map into the countable family of open-set tests is measurable for every actual probability kernel.
```
theorem measurable_kernel_finiteBasisUnion
    {Z : Type*} [MeasurableSpace Z] (κ : ProbabilityTheory.Kernel Z Y)
    (F : Finset (countableBasis Y)) :
    Measurable (fun z => κ z (finiteBasisUnion F)) :=
…
```
Mentions: OAI.DukePrimeDegree.finiteBasisUnion