OAI/NumberTheory/DukePrimeDegree/Geometry/PositiveRootHolonomy.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Holonomy across a positive-root pattern

A flow neutral on one root and contracting every other allowed matrix entry sends every element of the pattern to its selected root entry. The proved neutral holonomy theorem then identifies the actual leaves.

  1. theorem OAI.DukePrimeDegree.rootPattern_isolated_limit line 21
  2. theorem OAI.DukePrimeDegree.positiveRootPattern_isolated_limit line 73
  3. theorem OAI.DukePrimeDegree.exists_nullset_positiveRootPattern_holonomy line 87

    Source documentation

    One common null set controls all positive-pattern orbit pairs. This is the leaf-constancy input for the root-product induction.

    theorem exists_nullset_positiveRootPattern_holonomy
    (d : ℕ) (S : Finset (Fin (d + 1) × Fin (d + 1)))
    (hpos : ∀ p ∈ S, p.1 < p.2) {a b : Fin (d + 1)} (hab : a ≠ b)
    (ell : Fin (d + 1) → ℝ) (hell : ∑ r, ell r = 0) (hneut : ell a = ell b)
    (hdecay : ∀ p ∈ S, p ≠ (a, b) → ell p.1 < ell p.2)
    (μ : Measure (X (d + 1))) [IsFiniteMeasure μ]
    (hA : ∀ u : LogCoordinates d, μ.map (fun x => rightAction x (diagonalFlow u)) = μ) :
    ∃ N : Set (X (d + 1)), MeasurableSet N ∧ μ N = 0 ∧
      ∀ x ∉ N, ∀ y ∉ N, ∀ g : G (d + 1), PositiveRootPattern S g →
        rightAction x g = y → intrinsicRootLeaf hab μ y =
          basedRealMeasure (intrinsicRootLeaf hab μ x) (g.val a b) := by
…

    Mentions: OAI.DukePrimeDegree.diagonalFlow, OAI.DukePrimeDegree.PositiveRootPattern