OAI/GroupTheory/PolycyclicRecognition/Analysis/PairErgodic.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Ergodic probabilities on compact normalized sections

Second countability of the model group gives a Polish topology on the compact normalized section. Ergodic decomposition therefore applies to its invariant probabilities.

  1. instance OAI.PolycyclicRecognition.normalizedPair_polishSpace line 25
  2. theorem OAI.PolycyclicRecognition.exists_normalizedPair_ergodic_probability line 35

    Source documentation

    All the measurable-space hypotheses of the published decomposition theorem are discharged on the actual normalized pair space.

    theorem exists_normalizedPair_ergodic_probability
    [Nonempty (NormalizedPair G Λ)]
    (M : ThompsonNonamenability.InvariantMean G)
    (hdec : ErgodicDecompositionInput G (NormalizedPair G Λ)) :
    ∃ μ : Measure (NormalizedPair G Λ),
      IsProbabilityMeasure μ ∧ ErgodicSMul G (NormalizedPair G Λ) μ :=
…

    Mentions: OAI.PolycyclicRecognition.NormalizedPair, OAI.ThompsonNonamenability.InvariantMean, OAI.PolycyclicRecognition.ErgodicDecompositionInput