OAI/NumberTheory/DukePrimeDegree/Geometry/QuotientLiftMeasure.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Lifting an arbitrary finite measure through the arithmetic covering

The countable sum over deck transformations restricts on every injective chart to the original quotient measure. In particular this construction applies also to singular invariant measures.

  1. lemma OAI.DukePrimeDegree.quotient_left_integral line 19
  2. lemma OAI.DukePrimeDegree.quotient_fiber_representative line 28
  3. def OAI.DukePrimeDegree.quotientLiftMeasure line 43
  4. theorem OAI.DukePrimeDegree.quotientLiftMeasure_injective_chart line 46
  5. theorem OAI.DukePrimeDegree.quotient_measure_ext_on_injective_charts line 85
  6. theorem OAI.DukePrimeDegree.quotientLiftMeasure_section_independent line 108
  7. theorem OAI.DukePrimeDegree.quotientLiftMeasure_locallyFinite line 118