OAI/NumberTheory/DukePrimeDegree/Dynamics/NormalizerInvariantSigma.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A normalizer acts on the actual invariant sigma algebra

The normalizer need not fix individual ergodic components. It acts measurably on their invariant sigma algebra and preserves the trimmed base measure. These are the base-space facts needed for covariance of the component kernel.

  1. lemma OAI.DukePrimeDegree.measurable_invariantSigma_of_semiconjugacy line 20
  2. lemma OAI.DukePrimeDegree.measurePreserving_trim_of_measurable line 36
  3. lemma OAI.DukePrimeDegree.lattice_normalizer_measurable_invariantSigma line 50
  4. lemma OAI.DukePrimeDegree.lattice_normalizer_preserves_invariantSigma line 68

    Source documentation

    The actual normalizer transformation preserves the component base law whenever it preserves the ambient measure.

    lemma lattice_normalizer_preserves_invariantSigma {n : ℕ}
    (H : Subgroup (G n)) (a : G n)
    (ha : a ∈ Subgroup.normalizer (H : Set (G n)))
    (μ : Measure (X n)) (hμ : μ.map (fun x => rightAction x a) = μ) :
    @MeasurePreserving (X n) (X n)
      (actionInvariantSigma H (X n)) (actionInvariantSigma H (X n))
      (fun x => rightAction x a)
      (μ.trim (actionInvariantSigma_le H (X n)))
      (μ.trim (actionInvariantSigma_le H (X n))) := by
…