OAI/NumberTheory/DukePrimeDegree/Geometry/RootTranslateBox.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Translation covariance of root boxes

A measure-preserving root translation transports the actual coordinate measure and its disintegration. This is the local input for identifying invariant root conditionals with Lebesgue measure.

  1. def OAI.DukePrimeDegree.RootBox.translate line 23
  2. lemma OAI.DukePrimeDegree.RootBox.translate_domain line 46
  3. theorem OAI.DukePrimeDegree.RootBox.translate_coordinateMeasure line 55
  4. theorem OAI.DukePrimeDegree.RootBox.translate_marginal line 81
  5. theorem OAI.DukePrimeDegree.RootBox.translate_conditionalKernel line 92