OAI/NumberTheory/DukePrimeDegree/Geometry/WeylRootBoxes.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Reindexing actual root boxes without changing the root parameter

A coordinate permutation carries the pivot, transverse slice, and quotient root box to their permuted versions. The real root coordinate is unchanged, so disintegration transports the conditional measure without a rescaling.

  1. def OAI.DukePrimeDegree.rootSliceReindexHomeomorph line 20
  2. def OAI.DukePrimeDegree.rootReindexCoordinates line 46
  3. lemma OAI.DukePrimeDegree.rootReindexCoordinates_param line 50
  4. def OAI.DukePrimeDegree.RootBox.reindex line 64
  5. lemma OAI.DukePrimeDegree.RootBox.reindex_domain line 86
  6. theorem OAI.DukePrimeDegree.RootBox.reindex_coordinateMeasure line 96
  7. theorem OAI.DukePrimeDegree.RootBox.reindex_marginal line 121
  8. theorem OAI.DukePrimeDegree.RootBox.reindex_conditionalKernel line 130