OAI/NumberTheory/DukePrimeDegree/Geometry/LeafRegularSet.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

One conull set for leaf regularity and rebasing

The measurable kernel agrees with the intrinsic leaf, is locally finite, has positive mass in every neighborhood of the origin, and satisfies the leafwise rebasing law outside a single measurable null set.

  1. theorem OAI.DukePrimeDegree.exists_rootLeaf_regular_nullset line 21