OAI/NumberTheory/DukePrimeDegree/Geometry/CountableWeakKernel.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

A probability kernel is measurable for the weak topology

A countable family of finite-basis-union evaluations defines a stronger second-countable topology on probabilities. Kernel evaluations are measurable for that topology, and the countable Portmanteau criterion makes the map to the usual weak topology continuous. No global measurable-space instance on probabilities is changed.

  1. structure OAI.DukePrimeDegree.BasisProbability line 27

    Source documentation

    A separate wrapper retains both probability topologies without overriding the existing weak topology.

    structure BasisProbability where
…
  2. def OAI.DukePrimeDegree.basisProbabilityTests line 30
  3. instance OAI.DukePrimeDegree.(instance at line 34) line 34
  4. lemma OAI.DukePrimeDegree.basisProbabilityTests_isInducing line 38
  5. instance OAI.DukePrimeDegree.(instance at line 41) line 41
  6. instance OAI.DukePrimeDegree.(instance at line 44) line 44
  7. instance OAI.DukePrimeDegree.(instance at line 46) line 46
  8. theorem OAI.DukePrimeDegree.continuous_basisProbability_toProbability line 48
  9. theorem OAI.DukePrimeDegree.measurable_kernel_basisProbability line 58
  10. theorem OAI.DukePrimeDegree.measurable_kernel_probability_weak line 76

    Source documentation

    The codomain carries the Borel sigma algebra of weak convergence.

    theorem measurable_kernel_probability_weak
    {Z : Type*} [mZ : MeasurableSpace Z] (κ : Kernel Z Y) [IsMarkovKernel κ] :
    @Measurable Z (ProbabilityMeasure Y) mZ (borel (ProbabilityMeasure Y))
      (fun z => ⟨κ z, inferInstance⟩) := by
…