OAI/NumberTheory/DukePrimeDegree/Geometry/RootFactorHolonomy.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Full holonomy in extremal-root product coordinates

The real quotient of a positive-root group records the displacement of the selected intrinsic leaf even when both remaining and selected coordinates change. This permits comparison at different good centers in the disintegration step of EK2003, Proposition 8.3.

  1. theorem OAI.DukePrimeDegree.exists_nullset_positiveRootGroup_holonomy line 20
  2. theorem OAI.DukePrimeDegree.exists_nullset_rootFactor_holonomy line 56