OAI/Geometry/RCD/Coordinates/WeightedSquaredFitCenters.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.weighted_centers_from_squared_fit line 15

   Source documentation

   The actual two-fit center estimate and the squared radial fit bound give a quantitative center bound in the current covector norm.

   theorem weighted_centers_from_squared_fit {ρ M Λ Z : ℝ}
       (hρ : 0 < ρ) (hρ1 : ρ < 1) (hτρ : (9 / 16 : ℝ) < Real.sqrt ρ)
       (hM : 0 ≤ M) (hΛ : 0 ≤ Λ) (hZ : 0 ≤ Z)
       {P c r w e : ℕ → ℝ} (hP : ∀ i, 0 ≤ P i) (hPs : Summable P)
       (hr : ∀ i, 0 ≤ r i) (hw : ∀ i, 0 ≤ w i) (he : ∀ i, 0 ≤ e i)
       (hradius : ∀ i k, r (i + k) = (1 / 2 : ℝ) ^ k * r i)
       (hgrowth : ∀ i k, w (i + k) ≤ (9 / 8 : ℝ) ^ k * w i)
       (hc : Tendsto c atTop (𝓝 0))
       (hsquare : ∀ i, (e i) ^ 2 ≤ Z * P i * (w i) ^ 2)
       (hstep : ∀ i, |c i - c (i + 1)| ≤ M * Λ * r i * e i + M * r (i + 1) * e (i + 1))
       (i : ℕ) :
       |c i| ≤ (M * (Λ + 1) * Real.sqrt Z) * r i * w i *
   …