OAI/NumberTheory/DukePrimeDegree/Geometry/RootAtomicTransversal.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DukePrimeDegree.intrinsicRootLeaf_dirac_of_nullset_transversal line 12
2. theorem OAI.DukePrimeDegree.intrinsicRootLeaf_dirac_iff_transversal line 50

   Source documentation

   For diagonal-invariant finite measures, atomicity is exactly the existence of a measurable conull set meeting each root orbit once.

   theorem intrinsicRootLeaf_dirac_iff_transversal (d : ℕ)
       {i j : Fin (d+1)} (hij : i ≠ j)
       (μ : Measure (X (d+1))) [IsFiniteMeasure μ]
       (hA : ∀ u : LogCoordinates d, μ.map (fun x => rightAction x (diagonalFlow u))=μ) :
       (∀ᵐ x ∂μ, intrinsicRootLeaf hij μ x=Measure.dirac 0) ↔
         ∃ N : Set (X (d+1)), MeasurableSet N ∧ μ N=0 ∧
           ∀ x ∉ N, ∀ t : ℝ,
             rightAction x (Matrix.SpecialLinearGroup.transvection hij t) ∉ N → t=0 := by
   …

   Mentions: OAI.DukePrimeDegree.diagonalFlow