OAI/Geometry/RCD/Coordinates/DyadicCenterDecay.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.dyadic_affine_center_tendsto_zero line 16

   Source documentation

   The actual dyadic radius decays faster than the proved covector growth. Thus the size estimate for affine fit centers forces a zero limit.

   theorem dyadic_affine_center_tendsto_zero {n : ℕ} {r0 M : ℝ}
       (hr0 : 0 ≤ r0) (hM : 0 ≤ M)
       (F : ℕ → Euclidean n ≃L[ℝ] Euclidean n) (b : Euclidean n)
       (hgrowth : ∀ i, ‖(F i).symm b‖ ≤ (9 / 8 : ℝ) ^ i * ‖(F 0).symm b‖)
       (c : ℕ → ℝ)
       (hsize : ∀ i, |c i| ≤ M * (distanceSourceRadius r0 i / 64) * ‖(F i).symm b‖) :
       Tendsto c atTop (𝓝 0) := by
   …

   Mentions: OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.distanceSourceRadius