RelativeErrorNormalization.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Normalizing only after the outer residual bound

theorem OAI.RegularPointCoordinates.normalized_relative_bound line 13

theorem OAI.RegularPointCoordinates.normalized_relative_eventually_bounded line 22

Source documentation

Dividing the already proved unnormalized outer bound gives a uniform bound on every sufficiently late normalized residual.

theorem normalized_relative_eventually_bounded
    {H : ℕ → Type*} [∀ i, NormedAddCommGroup (H i)] [∀ i, NormedSpace ℝ (H i)]
    (x : ∀ i, H i) {α s : ℕ → ℝ} {C : ℝ} (hC : 0 ≤ C)
    (hα : ∀ i, 0 < α i) (hx : ∀ i, ‖x i‖ ≤ C * (α i + s i))
    (hratio : Tendsto (fun i => s i / α i) atTop (𝓝 0)) :
    ∀ᶠ i in atTop, ‖(α i)⁻¹ • x i‖ ≤ 2 * C := by
…

theorem OAI.RegularPointCoordinates.normalized_source_error_tendsto_zero line 34

Source documentation

The normalized forcing tends to zero when its original size is linear in a source error negligible relative to the residual.

theorem normalized_source_error_tendsto_zero
    {H : ℕ → Type*} [∀ i, NormedAddCommGroup (H i)] [∀ i, NormedSpace ℝ (H i)]
    (e : ∀ i, H i) {α s : ℕ → ℝ} {C : ℝ}
    (hα : ∀ i, 0 < α i) (he : ∀ i, ‖e i‖ ≤ C * s i)
    (hratio : Tendsto (fun i => s i / α i) atTop (𝓝 0)) :
    Tendsto (fun i => ‖(α i)⁻¹ • e i‖) atTop (𝓝 0) := by
…