OAI/NumberTheory/DukePrimeDegree/Dynamics/TemperedOrbitWindows.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Uniform subexponential chart control on finite orbit windows

The maximal height on the first N iterates is still sublinear. This retains the local chart radius simultaneously along the whole word, without an integrability assumption on the cusp height.

  1. def OAI.DukePrimeDegree.windowHeight line 18
  2. lemma OAI.DukePrimeDegree.height_le_windowHeight line 21
  3. theorem OAI.DukePrimeDegree.ae_windowHeight_affine_bound line 25
  4. theorem OAI.DukePrimeDegree.ae_windowHeight_div_tendsto_zero line 42
  5. theorem OAI.DukePrimeDegree.ae_window_local_injectivity_subexponential line 65

    Source documentation

    One radius works at every time in an N-letter orbit window.

    theorem ae_window_local_injectivity_subexponential (d : ℕ)
    (μ : Measure (X (d+1))) [IsFiniteMeasure μ]
    (hA : ∀ u : LogCoordinates d, μ.map (fun x => rightAction x (diagonalFlow u))=μ)
    (ell : Fin (d+1) → ℝ) (hell : ∑ i, ell i=0) :
    ∀ᵐ x ∂μ, ∀ ε : ℝ, 0 < ε → ∀ᶠ N : ℕ in atTop, ∀ k ≤ N,
      LocalInjectivityAt (Real.exp (-ε*(N:ℝ)))
        ((fun y => rightAction y (diagonalOneParameter ell hell (-1)))^[k] x) := by
…

    Mentions: OAI.DukePrimeDegree.diagonalFlow, OAI.DukePrimeDegree.LocalInjectivityAt