OAI/NumberTheory/DukePrimeDegree/Geometry/ProportionalWindowMeasures.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A common unit anchor fixes proportional measures on exhausting windows

  1. theorem OAI.DukePrimeDegree.restrict_eq_of_proportional_unit_anchor line 13
  2. theorem OAI.DukePrimeDegree.eq_of_exhausting_proportional_windows line 26
  3. theorem OAI.DukePrimeDegree.map_restrict_proportional_of_normalized line 39