OAI/NumberTheory/DukePrimeDegree/Geometry/TemperedChartRadius.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Subexponential chart radii along almost every diagonal orbit

Bounded height increments and finite invariant mass give sublinear height growth by the maximal occupation inequality. Applied to the actual local injectivity height, this proves the chart control needed in entropy comparisons without assuming an integrable logarithmic cusp height.

  1. theorem OAI.DukePrimeDegree.ae_height_div_tendsto_zero line 19
  2. theorem OAI.DukePrimeDegree.exists_tempered_local_injectivity_height line 40
  3. lemma OAI.DukePrimeDegree.radius_eventually_ge_exp_of_sublinear line 57
  4. theorem OAI.DukePrimeDegree.ae_local_injectivity_subexponential line 80

    Source documentation

    Local quotient charts shrink more slowly than every fixed exponential along almost every diagonal orbit.

    theorem ae_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,
      LocalInjectivityAt (Real.exp (-ε*(n:ℝ)))
        ((fun y => rightAction y (diagonalOneParameter ell hell (-1)))^[n] x) := by
…

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