OAI/NumberTheory/DukePrimeDegree/Entropy/FirstRootConditionalProduct.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Product conditionals in the first Gaussian root factor

Pulling an actual root-box coordinate measure back through the open remaining-root chart supplies the coordinate transport required by the neutral-holonomy product argument. Thus no product hypothesis is imposed on the ambient measure.

  1. abbrev OAI.DukePrimeDegree.rootFactorCoordinateMap line 24
  2. def OAI.DukePrimeDegree.rootFactorPullback line 28
  3. lemma OAI.DukePrimeDegree.rootFactorCoordinateMap_embedding line 33
  4. lemma OAI.DukePrimeDegree.rootFactorPullback_finite line 38
  5. lemma OAI.DukePrimeDegree.rootFactorPullback_map line 49
  6. theorem OAI.DukePrimeDegree.firstRootChart_conditional_product line 72