OAI/NumberTheory/DukePrimeDegree/Dynamics/RootInvariantNonatomic.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Invariant roots have nonatomic conditional measures

The pointwise atomic transversal is incompatible with any fixed nonzero measure-preserving root translation. Diagonal ergodicity then selects the nonatomic branch of the intrinsic leaf alternative.

  1. theorem OAI.DukePrimeDegree.not_ae_dirac_of_root_invariant line 19
  2. theorem OAI.DukePrimeDegree.ae_nonatomic_of_root_invariant line 41