RootInductionStep.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The extremal-root step of the product argument

For a nonempty closed collection of positive roots, one root can be removed while preserving closure. Its actual intrinsic leaf measure is constant along the closed group generated by the remaining roots, off one common null set. This is the holonomy step in Einsiedler--Katok (2003), Proposition 8.3.

lemma OAI.DukePrimeDegree.erase_neutral_root_closed line 23
lemma OAI.DukePrimeDegree.positiveRootPattern_mono line 40

theorem OAI.DukePrimeDegree.exists_extremal_root_leaf_constancy line 49

Source documentation

The remaining closed root group acts trivially on the selected root's normalized intrinsic leaf data. No product-structure hypothesis is used here.

theorem exists_extremal_root_leaf_constancy
    (d : ℕ) (S : Finset (Fin (d + 1) × Fin (d + 1))) (hS : S.Nonempty)
    (hpos : ∀ p ∈ S, p.1 < p.2)
    (hcomp : ∀ a b c : Fin (d + 1), (a, b) ∈ S → (b, c) ∈ S → (a, c) ∈ S)
    (μ : Measure (X (d + 1))) [IsFiniteMeasure μ]
    (hA : ∀ u : LogCoordinates d, μ.map (fun x => rightAction x (diagonalFlow u)) = μ) :
    ∃ p ∈ S, ∃ hp : p.1 ≠ p.2,
      (∀ a b c : Fin (d + 1), (a, b) ∈ S.erase p → (b, c) ∈ S.erase p →
        (a, c) ∈ S.erase p) ∧
      ∃ N : Set (X (d + 1)), MeasurableSet N ∧ μ N = 0 ∧
        ∀ x ∉ N, ∀ g ∈ (positiveRootGeneratedGroup (S.erase p)).topologicalClosure,
          rightAction x g ∉ N →
…

Mentions: OAI.DukePrimeDegree.diagonalFlow, OAI.DukePrimeDegree.positiveRootGeneratedGroup