PositiveWidthSmallLog.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Short metric factors fit inside every positive-width ordinary box

theorem OAI.PolycyclicRecognition.exists_small_distance_exponential_box line 19

Source documentation

A sufficiently small exponential-in-distance logarithmic bound fits inside the unit box at the ambient scale. The permitted distance fraction is fixed uniformly over all large scales and all logarithms.

theorem exists_small_distance_exponential_box
    {L N J : Type*} [LieRing L] [LieAlgebra ℝ L] [Fintype J]
    (b : Basis J ℝ L) (cost : J → ℝ) (Exp : L → N)
    {lo C A : ℝ} (hlo : 0 < lo) (hcost : ∀ j, lo ≤ cost j)
    (hC : 0 ≤ C) (hA : 0 ≤ A) (q : ℕ) :
    ∃ η S : ℝ, 0 < η ∧ η ≤ 1 ∧ 1 ≤ S ∧
      ∀ r : ℝ, S ≤ r → ∀ a : ℝ, 0 ≤ a → a ≤ η * r → ∀ v : L,
      ‖b.equivFun v‖ ≤ C * (3 + a) ^ q * Real.exp (A * (a + 1)) →
      Exp v ∈ exponentialCoordinateBox Exp (exponentialRescaleBasis b cost r) 1 := by
…

Mentions: OAI.PolycyclicRecognition.exponentialCoordinateBox, OAI.PolycyclicRecognition.exponentialRescaleBasis