ExponentialCoarseMetric.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform coarse metric bounds for exponential lines

theorem OAI.PolycyclicRecognition.continuous_radial_exponential_metric_bound line 18

Source documentation

Continuity on one fixed unit ball and the one-parameter identity give one uniform coarse metric bound for all exponential directions.

theorem continuous_radial_exponential_metric_bound
    (Exp : V → G) (hcont : Continuous Exp) (hzero : Exp 0 = 1)
    (hmul : ∀ v : V, ∀ s t : ℝ, Exp ((s + t) • v) = Exp (s • v) * Exp (t • v)) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ v : V, dist 1 (Exp v) ≤ C * (1 + ‖v‖) := by
…

theorem OAI.PolycyclicRecognition.continuous_radial_exponential_coarse_dist line 61

Source documentation

The same constant controls distances on every exponential line.

theorem continuous_radial_exponential_coarse_dist
    (Exp : V → G) (hcont : Continuous Exp) (hzero : Exp 0 = 1)
    (hmul : ∀ v : V, ∀ s t : ℝ, Exp ((s + t) • v) = Exp (s • v) * Exp (t • v)) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ (v : V) (s t : ℝ),
      dist (Exp (s • v)) (Exp (t • v)) ≤ C * ‖v‖ * |t - s| + C := by
…