OAI/NumberTheory/DukePrimeDegree/Geometry/NeutralPatchNull.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Transfer the neutral graph's full measure to the quotient patch

  1. abbrev OAI.DukePrimeDegree.neutralQuotientParam line 14
  2. lemma OAI.DukePrimeDegree.neutralQuotientParam_continuous line 18
  3. lemma OAI.DukePrimeDegree.neutralQuotientParam_injOn line 23
  4. theorem OAI.DukePrimeDegree.neutralQuotientParam_image_measure line 41
  5. theorem OAI.DukePrimeDegree.neutralQuotientParam_measurable_image line 59
  6. theorem OAI.DukePrimeDegree.neutral_patch_image_ae_graph line 76