AffineFitSmoothing.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Smoothing the actual past-source affine recurrence

The radial correction at scale i uses the defect P i, whereas its improved fit is at scale i+m. The strict contraction margin absorbs this lag.

theorem OAI.RegularPointCoordinates.affine_fit_past_source_envelope line 13

theorem OAI.RegularPointCoordinates.squared_fit_le_forwardDefect line 48

Source documentation

Apply the lagged estimate to the square of a normalized scalar fit. The only source is the original nonnegative Poisson-defect sequence.

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

Mentions: OAI.RegularPointCoordinates.forwardDefect