OAI/Geometry/RCD/Coordinates/WeightedFitSmoothing.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.weighted_fit_normalized_step line 11

   Source documentation

   Dividing by the current covector norm introduces only the proved growth loss across the fixed lag. No uniform Euclidean norm is required.

   theorem weighted_fit_normalized_step {e w P : ℕ → ℝ} {a C G : ℝ} {m : ℕ}
       (ha : 0 ≤ a) (hC : 0 ≤ C)
       (he : ∀ i, 0 ≤ e i) (hw : ∀ i, 0 < w i)
       (hgrowth : ∀ i, w i ≤ G * w (i + m))
       (hstep : ∀ i, e (i + m) ≤ a * e i + C * w i * Real.sqrt (P i)) (i : ℕ) :
       e (i + m) / w (i + m) ≤ (a * G) * (e i / w i) + (C * G) * Real.sqrt (P i) := by
   …

2. theorem OAI.RegularPointCoordinates.weighted_squared_fit_le_forwardDefect line 33

   Source documentation

   The smoothed error controls each original fit in its own covector norm. The defect sequence is unchanged by normalization.

   theorem weighted_squared_fit_le_forwardDefect {σ η A a C G : ℝ}
       (hσ : 0 ≤ σ) (hη : 0 ≤ η) (hA : 0 ≤ A)
       (ha : 0 ≤ a) (hC : 0 ≤ C) (hG : 0 ≤ G)
       {P e w : ℕ → ℝ} (hP : ∀ i, 0 ≤ P i) (he : ∀ i, 0 ≤ e i) (hw : ∀ i, 0 < w i)
       {m : ℕ} (hm : 0 < m)
       (hmargin : (2 * (a * G) ^ 2) * A + 2 * (C * G) ^ 2 ≤ σ ^ m * A)
       (hinitial : ∀ i < m, (e i / w i) ^ 2 ≤ A * (η * σ ^ i))
       (hgrowth : ∀ i, w i ≤ G * w (i + m))
       (hstep : ∀ i, e (i + m) ≤ a * e i + C * w i * Real.sqrt (P i)) :
       ∀ i, (e i) ^ 2 ≤ A * forwardDefect σ η P i * (w i) ^ 2 := by
   …

   Mentions: OAI.RegularPointCoordinates.forwardDefect