WeightedInwardConstants.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Removing affine constants in the current covector norm

theorem OAI.RegularPointCoordinates.weighted_affine_constants_le_envelope line 16

Source documentation

The inward tail is measured in the current radius and current covector norm. The fixed factor 9/16 combines radius decay and the proved 9/8 growth of the exact normalizing frames.

theorem weighted_affine_constants_le_envelope {ρ C : ℝ}
    (hρ : 0 < ρ) (hρ1 : ρ < 1) (hτρ : (9 / 16 : ℝ) < Real.sqrt ρ) (hC : 0 ≤ C)
    {P c r w : ℕ → ℝ} (hP : ∀ i, 0 ≤ P i) (hPs : Summable P)
    (hr : ∀ i, 0 ≤ r i) (hw : ∀ i, 0 ≤ w 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))
    (hstep : ∀ i, |c i - c (i + 1)| ≤
      C * r i * w i * (Real.sqrt (P i) + Real.sqrt (P (i + 1)))) (i : ℕ) :
    |c i| ≤ C * r i * w i * (1 - (9 / 16 : ℝ) / Real.sqrt ρ)⁻¹ *
      (1 + (Real.sqrt ρ)⁻¹) * Real.sqrt (symmetricDefect ρ P i) := by
…

Mentions: OAI.RegularPointCoordinates.symmetricDefect