OAI/NumberTheory/DukePrimeDegree/Dynamics/InvariantMeasureGroup.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The closed group preserving a finite measure

The ambient measure stabilizer is closed. Consequently the topological closure of the invariant root-generated group still preserves the measure.

  1. lemma OAI.PrimeDegreePackets.continuous_integral_rightAction line 18
  2. lemma OAI.PrimeDegreePackets.invariantRightSubgroup_eq_tests line 34
  3. theorem OAI.PrimeDegreePackets.isClosed_invariantRightSubgroup line 58

    Source documentation

    The stabilizer of a finite measure is a closed subgroup of the real special linear group.

    theorem isClosed_invariantRightSubgroup {n : ℕ} (μ : Measure (X n)) [IsFiniteMeasure μ] :
    IsClosed (invariantRightSubgroup μ : Set (G n)) := by
…

    Mentions: OAI.PrimeDegreePackets.X, OAI.PrimeDegreePackets.invariantRightSubgroup, OAI.PrimeDegreePackets.G

  4. theorem OAI.PrimeDegreePackets.rootGenerated_topologicalClosure_le line 65

    Source documentation

    Closing the actual root-generated group introduces no new failure of measure invariance.

    theorem rootGenerated_topologicalClosure_le {n : ℕ} (μ : Measure (X n)) [IsFiniteMeasure μ] :
    (invariantRootGeneratedGroup μ).topologicalClosure ≤ invariantRightSubgroup μ := by
…

    Mentions: OAI.PrimeDegreePackets.X, OAI.PrimeDegreePackets.invariantRootGeneratedGroup, OAI.PrimeDegreePackets.invariantRightSubgroup