NeutralNameCovers.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Measurable selection of neutral orbit approximations

A finite cover by neutral displacements admits a measurable choice of reference displacement. The same finite list works for every orbit length.

theorem OAI.DukePrimeDegree.measurable_choice_fin_cover line 22

theorem OAI.DukePrimeDegree.compact_neutral_measurable_selector line 55

Source documentation

A compact collection of neutral displacements can be encoded by one measurable finite label, uniformly for all real times.

theorem compact_neutral_measurable_selector {n : ℕ}
    (ell : Fin n → ℝ) (hell : ∑ i, ell i=0)
    (K : Set (G n)) (hK : IsCompact K)
    (hcomm : ∀ g ∈ K, ∀ t : ℝ, Commute g (diagonalOneParameter ell hell t))
    {ε : ℝ} (hε : 0 < ε) :
    ∃ (N : ℕ) (g : Fin N → G n) (r : K → Fin N),
      (∀ i, g i ∈ K) ∧ Measurable r ∧
      ∀ (k : K) (x : X n) (t : ℝ),
        quotientLogDistance
          (rightAction (rightAction x k.val) (diagonalOneParameter ell hell t))
          (rightAction (rightAction x (g (r k))) (diagonalOneParameter ell hell t)) < ε := by
…

Mentions: OAI.DukePrimeDegree.quotientLogDistance