SwitchBounds.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Short switches at supporting heights

Logarithmic distortion turns a polynomial times a subexponential coordinate bound into a sublinear metric displacement. The estimate is uniform in the points before and after a switch.

theorem OAI.PolycyclicRecognition.log_polynomial_exp_le line 18

Source documentation

The polynomial correction contributes only a logarithmic error.

theorem log_polynomial_exp_le {C r δ : ℝ} (hC : 0 ≤ C) (hr : 0 ≤ r)
    (hδ : 0 ≤ δ) (b : ℕ) :
    Real.log (2 + C * (1 + r) ^ b * Real.exp (r * δ)) ≤
      Real.log (2 + C) + (b : ℝ) * Real.log (1 + r) + r * δ := by
…

theorem OAI.PolycyclicRecognition.switch_length_le line 33

Source documentation

Uniform coordinate bounds give the quantitative switch-length bound.

theorem switch_length_le
    {G V : Type*} [PseudoMetricSpace G] [One G] [NormedAddCommGroup V]
    (Exp : V → G) {D C r δ : ℝ} (hD : 0 ≤ D) (hC : 0 ≤ C)
    (hr : 0 ≤ r) (hδ : 0 ≤ δ) (b : ℕ)
    (hdist : ∀ v, dist 1 (Exp v) ≤ D * Real.log (2 + ‖v‖))
    {v : V} (hv : ‖v‖ ≤ C * (1 + r) ^ b * Real.exp (r * δ)) :
    dist 1 (Exp v) ≤
      D * (Real.log (2 + C) + (b : ℝ) * Real.log (1 + r) + r * δ) := by
…

theorem OAI.PolycyclicRecognition.switch_length_sublinear line 48

Source documentation

Coordinate size polynomial times exp(o(r)) gives a switch of length o(r). This is an individual-displacement estimate, uniform over every family sharing the displayed coordinate bound.

theorem switch_length_sublinear
    {G V : Type*} [PseudoMetricSpace G] [One G] [NormedAddCommGroup V]
    (Exp : V → G) {D C : ℝ} (hD : 0 ≤ D) (hC : 0 ≤ C) (b : ℕ)
    (hdist : ∀ v, dist 1 (Exp v) ≤ D * Real.log (2 + ‖v‖))
    (v : ℝ → V) (δ : ℝ → ℝ) (hδ : ∀ᶠ r in atTop, 0 ≤ δ r)
    (hδlim : Tendsto δ atTop (𝓝 0))
    (hv : ∀ᶠ r in atTop, ‖v r‖ ≤ C * (1 + r) ^ b * Real.exp (r * δ r)) :
    Tendsto (fun r => dist 1 (Exp (v r)) / r) atTop (𝓝 0) := by
…