OAI/Geometry/EinsteinFour/JacobiInverse.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PositiveEinsteinFour.Jacobi.inverse_perturbation_bound line 12
2. theorem OAI.PositiveEinsteinFour.Jacobi.uniform_inverse_neighborhood line 73

   Source documentation

   The inverse bounds can be chosen once on a compact preconjugate interval, including the continuously normalized initial endpoint.

   theorem uniform_inverse_neighborhood
       {R : Type*} [NormedRing R] [HasSummableGeomSeries R] [Nontrivial R]
       {B : ℝ → R} {t : ℝ}
       (hB : ContinuousOn B (Set.Icc 0 t)) (hunit : ∀ s ∈ Set.Icc 0 t, IsUnit (B s)) :
       ∃ K : ℝ, 0 < K ∧ ∀ s ∈ Set.Icc 0 t, ∀ A : R,
         ‖A - B s‖ ≤ 1 / (2 * K) →
         IsUnit A ∧ ‖Ring.inverse A‖ ≤ 2 * K ∧
           ‖Ring.inverse A - Ring.inverse (B s)‖ ≤ 2 * K ^ 2 * ‖A - B s‖ := by
   …