OAI/NumberTheory/DukePrimeDegree/Dynamics/RootOrbitRebase.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Rebasing at every pair outside a single null set

Countably many long root boxes turn coordinate disintegration into a pointwise rebasing law along all root orbits. In particular, if a root conditional is Dirac almost everywhere, one conull set meets each root orbit at most once. This is the atomic case needed by the support argument.

  1. lemma OAI.DukePrimeDegree.rootBox_rebase_outside_nullset line 21
  2. theorem OAI.DukePrimeDegree.exists_nullset_root_orbit_rebase line 57
  3. lemma OAI.DukePrimeDegree.based_dirac_eq_self_only_at_zero line 117
  4. theorem OAI.DukePrimeDegree.exists_nullset_atomic_root_transversal line 126