OAI/NumberTheory/DukePrimeDegree/Geometry/CompactNeutralFibers.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Uniform finite covers of neutral itinerary fibers

The small displacement bound puts every bilateral fiber in one fixed compact subset of the diagonal centralizer. Thus the number of reference orbits needed for a given accuracy is independent of the base point and the length of the observed orbit.

  1. def OAI.DukePrimeDegree.compactNeutralDisplacements line 24
  2. theorem OAI.DukePrimeDegree.isCompact_compactNeutralDisplacements line 29
  3. theorem OAI.DukePrimeDegree.mem_compactNeutralDisplacements_of_small line 48
  4. theorem OAI.DukePrimeDegree.finite_neutral_itinerary_cover line 66

    Source documentation

    A bilateral fiber with a small neutral lift admits a fixed finite list of reference orbits; its geometric coding cost does not grow in time.

    theorem finite_neutral_itinerary_cover {n : ℕ}
    (ell : Fin n → ℝ) (hell : ∑ i, ell i=0)
    (Q : X n → ℕ)
    (hQ : ∀ x y,
      (∀ k : ℕ,
        Q ((fun z => rightAction z (diagonalOneParameter ell hell (-1)))^[k] y) =
        Q ((fun z => rightAction z (diagonalOneParameter ell hell (-1)))^[k] x)) →
      (∀ k : ℕ,
        Q ((fun z => rightAction z (diagonalOneParameter ell hell 1))^[k] y) =
        Q ((fun z => rightAction z (diagonalOneParameter ell hell 1))^[k] x)) →
      ∃ g ∈ matrixBall n 1, rightAction x g=y ∧
        ∀ t : ℝ, Commute g (diagonalOneParameter ell hell t))
…