OAI/Geometry/RCD/Coordinates/RadialFitEnvelope.lean
2 declarations, 0 contain sorry, 0 declared as axioms
Summable squared radial errors from the actual contraction
- theorem
OAI.RegularPointCoordinates.normalized_squared_fit_budgetline 11Source documentation
A weighted pointwise envelope bounds the total normalized squared error by the total original defect and the qualitative error floor.
theorem normalized_squared_fit_budget {σ η A : ℝ} (hσ : 0 ≤ σ) (hσ1 : σ < 1) (hη : 0 ≤ η) (hA : 0 ≤ A) {P e w : ℕ → ℝ} (hP : ∀ i, 0 ≤ P i) (hPs : Summable P) (hw : ∀ i, 0 < w i) (hbound : ∀ i, (e i) ^ 2 ≤ A * forwardDefect σ η P i * (w i) ^ 2) : Summable (fun i => (e i / w i) ^ 2) ∧ (∑' i, (e i / w i) ^ 2) ≤ A * (1 - σ)⁻¹ * (η + ∑' i, P i) := by … - theorem
OAI.RegularPointCoordinates.radial_fit_forward_envelopeline 33Source documentation
The fixed harmonic contraction dominates the slow change of covector norm. The coefficient is chosen before the defect sequence and the size of the qualitative error.
theorem radial_fit_forward_envelope {m : ℕ} (hm : 0 < m) {C : ℝ} (hC : 0 ≤ C) : ∃ A : ℝ, 0 < A ∧ ∀ {η : ℝ}, 0 ≤ η → ∀ {P e w : ℕ → ℝ}, (∀ i, 0 ≤ P i) → (∀ i, 0 ≤ e i) → (∀ i, 0 < w i) → (∀ i, (e i) ^ 2 ≤ η * (w i) ^ 2) → (∀ i, w i ≤ (9 / 8 : ℝ) ^ m * w (i + m)) → (∀ i, e (i + m) ≤ (1 / 2 : ℝ) * Real.sqrt ((1 / 2 : ℝ) ^ m) * e i + C * w i * Real.sqrt (P i)) → ∀ i, (e i) ^ 2 ≤ A * forwardDefect (3 / 4) η P i * (w i) ^ 2 := by …