OAI/NumberTheory/DukePrimeDegree/Geometry/QuotientMeasurableSection.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A measurable section of the actual arithmetic quotient

Local inverse charts and a countable disjoint cover give the section. It is used to lift an arbitrary quotient measure before taking neutral leaf coordinates; no absolute continuity with respect to Haar is required.

  1. theorem OAI.DukePrimeDegree.exists_measurable_quotient_section line 20