OAI/NumberTheory/DukePrimeDegree/Entropy/RowConditionalCompatibility.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Nested row conditionals agree with one-root conditionals

The explicit row/root coordinate change transports the real conditional in a row disintegration to the conditional in the existing one-root chart. This is the chart compatibility needed to apply the root-leaf holonomy theorem inside the row-product argument.

  1. def OAI.DukePrimeDegree.rowSplitMeasure line 21
  2. instance OAI.DukePrimeDegree.rowSplitMeasure_finite line 26
  3. def OAI.DukePrimeDegree.rowSingleMeasure line 30
  4. instance OAI.DukePrimeDegree.rowSingleMeasure_finite line 35
  5. theorem OAI.DukePrimeDegree.row_conditional_compatibility line 39