OAI/NumberTheory/DukePrimeDegree/Geometry/NeutralLeafVersion.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A pointwise neutral-invariant version of the intrinsic leaf data

Neutral diagonal translations have root scaling factor one, so their actual leaf kernels agree almost everywhere. Haar orbit constants give a version of the countable determining data invariant under every neutral translation at every point.

  1. theorem OAI.DukePrimeDegree.ae_neutralSpace_rootKernel_eq line 22
  2. theorem OAI.DukePrimeDegree.exists_strictly_neutral_invariant_leafData line 56