OAI/NumberTheory/DukePrimeDegree/Dynamics/PositiveOrbitRestriction.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A positive-mass orbit supplies the finite homogeneous measure

No homogeneous decomposition is needed once a single orbit of the actual measure stabilizer has positive mass: restriction to that orbit is a nonzero finite invariant measure. The resulting orbit obstruction identifies Haar probability from the stated positive-orbit hypothesis.

  1. theorem OAI.DukePrimeDegree.isHaar_of_positive_invariantSubgroup_orbit line 27

    Source documentation

    The existing invariant subgroup itself can be used as the orbit group. Thus one positive-mass orbit is enough for the arithmetic prime-degree obstruction, with no decomposition or orbit measure added as another premise.

    theorem isHaar_of_positive_invariantSubgroup_orbit
    (d : ℕ) (hprime : (d + 1).Prime)
    (μ : Measure (X (d + 1))) [IsProbabilityMeasure μ]
    (hA : ∀ u : LogCoordinates d, μ.map (fun x => rightAction x (diagonalFlow u)) = μ)
    (r : Setoid (Fin (d + 1)))
    (hr : ∀ i j, r i j ↔ rootInvarianceRelation μ i j)
    (hnontrivial : ∃ i j, i ≠ j ∧ r i j)
    (g : G (d + 1))
    (hpos : μ (range (latticeOrbitPoint g (invariantRightSubgroup μ))) ≠ 0) :
    IsHaarProbability μ := by
…

    Mentions: OAI.DukePrimeDegree.diagonalFlow, OAI.DukePrimeDegree.latticeOrbitPoint