OAI/Geometry/RCD/Coordinates/PatchBudget.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.exists_uniform_patch_budget line 11

   Source documentation

   A common positive budget controls every coefficient below a fixed bound, both absolutely and relative to the desired iteration tolerance.

   theorem exists_uniform_patch_budget {P epsilon : ℝ} (hP : 0 ≤ P) (hepsilon : 0 < epsilon) :
       ∃ b : ℝ, 0 < b ∧ b ≤ epsilon ∧ b ≤ 1 / 8192 ∧
         ∀ t : ℝ, 0 ≤ t → t ≤ P → t * b ≤ min epsilon (1 / 8192) := by
   …