OAI/Geometry/RCD/Harmonic/InwardConstantEstimate.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.affine_constants_le_envelope line 16

   Source documentation

   A vanishing sequence with the consecutive-fit estimate is bounded by the square root of the two-sided defect envelope. No summability of the square roots is assumed.

   theorem affine_constants_le_envelope {ρ τ C : ℝ}
       (hρ : 0 < ρ) (hρ1 : ρ < 1) (hτ : 0 ≤ τ) (hτρ : τ < Real.sqrt ρ) (hC : 0 ≤ C)
       {P c : ℕ → ℝ} (hP : ∀ i, 0 ≤ P i) (hPs : Summable P)
       (hc : Tendsto c atTop (𝓝 0))
       (hstep : ∀ i, |c i - c (i + 1)| ≤
         C * τ ^ i * (Real.sqrt (P i) + Real.sqrt (P (i + 1)))) (i : ℕ) :
       |c i| ≤ C * τ ^ i * (1 - τ / Real.sqrt ρ)⁻¹ *
         (1 + (Real.sqrt ρ)⁻¹) * Real.sqrt (symmetricDefect ρ P i) := by
   …

   Mentions: OAI.RegularPointCoordinates.symmetricDefect