OAI/NumberTheory/DukePrimeDegree/Geometry/AtomlessDiagonalMeasure.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DukePrimeDegree.measure_singleton_eq_zero_of_continuous_orbit line 16
2. theorem OAI.DukePrimeDegree.nullSingletonClass_of_diagonal_invariant line 36

   Source documentation

   Only one nontrivial one-parameter diagonal flow is needed.

   theorem nullSingletonClass_of_diagonal_invariant (d : ℕ)
       {i j : Fin (d+1)} (hij : i ≠ j)
       (μ : Measure (X (d+1))) [IsProbabilityMeasure μ]
       (hA : ∀ u : LogCoordinates d, μ.map (fun x => rightAction x (diagonalFlow u))=μ) :
       NullSingletonClass μ := by
   …

   Mentions: OAI.DukePrimeDegree.diagonalFlow