OAI/NumberTheory/DukePrimeDegree/Entropy/NeutralFiberNames.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DukePrimeDegree.measurable_choice_fin_on line 15
2. def OAI.DukePrimeDegree.bilateralNameFiber line 32
3. theorem OAI.DukePrimeDegree.measurableSet_bilateralNameFiber line 41
4. theorem OAI.DukePrimeDegree.measurable_neutral_fiber_names line 56

   Source documentation

   Every finite time segment has a measurable reference label on the fiber, using a list whose size is independent of the time segment.

   theorem measurable_neutral_fiber_names {n : ℕ}
       (ell : Fin n → ℝ) (hell : ∑ i, ell i=0)
       (Q : X n → ℕ) (hQ : Measurable Q)
       (hlift : ∀ x y, y ∈ bilateralNameFiber ell hell Q x →
         ∃ g ∈ matrixBall n 1, rightAction x g=y ∧
           ∀ t : ℝ, Commute g (diagonalOneParameter ell hell t))
       {ε : ℝ} (hε : 0 < ε) :
       ∃ (M : ℕ) (v : Fin M → G n), ∀ (N : ℕ) (x : X n),
         ∃ r : X n → Fin M, Measurable r ∧
           ∀ y ∈ bilateralNameFiber ell hell Q x, ∀ j : Fin N,
             quotientLogDistance
               (rightAction (rightAction x (v (r y)))
   …

   Mentions: OAI.DukePrimeDegree.bilateralNameFiber, OAI.DukePrimeDegree.quotientLogDistance