OAI/NumberTheory/DukePrimeDegree/Geometry/DenseDiagonalGenerators.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

A finite dense generating family for diagonal parameters

In each real logarithmic coordinate, shifts by one and by square root of two generate a dense additive subgroup. Thus the diagonal action has a concrete finite topologically generating family; no one of its elements is asserted to be ergodic.

  1. def OAI.DukePrimeDegree.diagonalParameterGenerators line 26
  2. def OAI.DukePrimeDegree.singleCoordinateAddHom line 29
  3. lemma OAI.DukePrimeDegree.continuous_singleCoordinateAddHom line 35
  4. theorem OAI.DukePrimeDegree.dense_diagonalParameterGenerators line 50
  5. def OAI.DukePrimeDegree.multiplicativeParameterGenerators line 83
  6. lemma OAI.DukePrimeDegree.dense_multiplicativeParameterGenerators line 86
  7. def OAI.DukePrimeDegree.parameterDomainHom line 98

    Source documentation

    On an abelian group the domain-action type tag is also a group homomorphism, so dense generators transfer to the Koopman action.

    def parameterDomainHom : Multiplicative (I → ℝ) →*
    (Multiplicative (I → ℝ))ᵈᵐᵃ where
…
  8. def OAI.DukePrimeDegree.domainParameterGenerators line 104
  9. theorem OAI.DukePrimeDegree.dense_domainParameterGenerators line 107