OAI/NumberTheory/DukePrimeDegree/Dynamics/OrbitBasepoint.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Changing the basepoint of a lattice orbit

Left translation on the orbit group induces the expected homeomorphism between the two actual stabilizer quotients. It intertwines their right actions and transports finite invariant measures without new hypotheses.

  1. def OAI.DukePrimeDegree.latticeOrbitBasepointHomeomorph line 20
  2. lemma OAI.DukePrimeDegree.latticeOrbitBasepointHomeomorph_rightAction line 59
  3. lemma OAI.DukePrimeDegree.latticeOrbitBasepointHomeomorph_symm_rightAction line 69
  4. theorem OAI.DukePrimeDegree.latticeOrbitBasepoint_measure_invariant line 79

    Source documentation

    The transported measure has exactly the same right invariances.

    theorem latticeOrbitBasepoint_measure_invariant {n : ℕ}
    (g : G n) (H : Subgroup (G n)) (h : H)
    (μ : Measure (LatticeOrbitQuotient g H))
    (hinv : ∀ k : H, μ.map (fun x => latticeOrbitRightAction g H x k) = μ) (k : H) :
    (μ.map (latticeOrbitBasepointHomeomorph g H h).symm).map
      (fun x => latticeOrbitRightAction (g * h.val) H x k) =
        μ.map (latticeOrbitBasepointHomeomorph g H h).symm := by
…

    Mentions: OAI.DukePrimeDegree.LatticeOrbitQuotient, OAI.DukePrimeDegree.latticeOrbitRightAction, OAI.DukePrimeDegree.latticeOrbitBasepointHomeomorph