OAI/Analysis/SphereIsometry/ReturnMapBounds.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Tingley.radius_ratio_le_factor line 12
2. theorem OAI.Tingley.return_coefficient_le line 21
3. theorem OAI.Tingley.return_pair_error_le line 35
4. theorem OAI.Tingley.return_pair_uniform_bound line 58
5. theorem OAI.Tingley.return_factor_mem_Ico line 81

   Source documentation

   The exact square factor, with its strict upper bound.

   theorem return_factor_mem_Ico {t M : ℝ} (ht0 : 0 < t)
       (hM : 0 < M) (hMU : M < 1 + t) :
       (1 - M / (1 + t)) ^ 2 ∈ Set.Ico (0 : ℝ) 1 := by
   …

6. theorem OAI.Tingley.return_contraction_factor_mem_Ico line 94

   Source documentation

   Nonemptiness is used only to bound M by one actual positive radius.

   theorem return_contraction_factor_mem_Ico {X : Type*}
       {C : Set X} {p s : X → ℝ} {t M : ℝ}
       (ht0 : 0 < t) (ht1 : t < 1) (hM : 0 < M) (hCne : C.Nonempty)
       (hp : ∀ v ∈ C, 1 - t ≤ p v)
       (hsU : ∀ v ∈ C, s v ≤ 1 + t)
       (hsm : ∀ v ∈ C, s v = p v + M) :
       (1 - M / (1 + t)) ^ 2 ∈ Set.Ico (0 : ℝ) 1 := by
   …