OAI/Geometry/RCD/Harmonic/AffineScaleChoice.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.exists_dyadic_affine_contraction line 16

   Source documentation

   A quadratic Taylor error is strictly smaller than the required three-halves decay at one fixed dyadic scale, independent of the function.

   theorem exists_dyadic_affine_contraction (C : ℝ) :
       ∃ m : ℕ, 3 ≤ m ∧
         C * ((1 / 2 : ℝ) ^ m) ^ 2 <
           (1 / 4 : ℝ) * (1 / 2 : ℝ) ^ m * Real.sqrt ((1 / 2 : ℝ) ^ m) := by
   …