OAI/NumberTheory/DukePrimeDegree/Geometry/StationaryRestrictions.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Gluing stationary restrictions over a countable cover

For a Markov kernel, stationary restrictions of one finite measure are closed under intersections and unions. Thus local stationarity on a countable almost-everywhere cover implies global stationarity.

  1. lemma OAI.DukePrimeDegree.bind_kernel_mono line 25
  2. lemma OAI.DukePrimeDegree.bind_kernel_add line 33
  3. lemma OAI.DukePrimeDegree.bind_kernel_univ line 39
  4. theorem OAI.DukePrimeDegree.bind_kernel_real line 44
  5. theorem OAI.DukePrimeDegree.bind_eq_of_real_integrals line 51
  6. theorem OAI.DukePrimeDegree.stationary_restrict_inter line 63
  7. theorem OAI.DukePrimeDegree.stationary_restrict_union line 86
  8. theorem OAI.DukePrimeDegree.stationary_restrict_iUnion_of_monotone line 102
  9. theorem OAI.DukePrimeDegree.stationary_of_countable_restrictions line 133

    Source documentation

    The local restrictions must use the same actual Markov kernel. No global stationarity hypothesis is used.

    theorem stationary_of_countable_restrictions (κ : Kernel Y Y) [IsMarkovKernel κ]
    (μ : Measure Y) [IsFiniteMeasure μ]
    (E : ℕ → Set Y) (hE : ∀ n, MeasurableSet (E n))
    (hcover : ∀ᵐ y ∂μ, y ∈ ⋃ n, E n)
    (hs : ∀ n, (μ.restrict (E n)).bind κ = μ.restrict (E n)) :
    μ.bind κ = μ := by
…
  10. theorem OAI.DukePrimeDegree.stationary_of_countable_indexed_restrictions line 155

    Source documentation

    The cover may use any countable index type, including a countable family of quotient charts with different coordinate domains.

    theorem stationary_of_countable_indexed_restrictions {ι : Type*} [Countable ι]
    (κ : Kernel Y Y) [IsMarkovKernel κ] (μ : Measure Y) [IsFiniteMeasure μ]
    (E : ι → Set Y) (hE : ∀ i, MeasurableSet (E i))
    (hcover : ∀ᵐ y ∂μ, y ∈ ⋃ i, E i)
    (hs : ∀ i, (μ.restrict (E i)).bind κ = μ.restrict (E i)) :
    μ.bind κ = μ := by
…