AffineFitRecurrence.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The squared affine-fit recurrence and its geometric envelope

theorem OAI.RegularPointCoordinates.affine_fit_squared_step line 13

Source documentation

Squaring a single affine-improvement estimate costs a fixed factor, and preserves the Poisson defect without taking its square root.

theorem affine_fit_squared_step {e e' a C P : ℝ}
    (he : 0 ≤ e) (he' : 0 ≤ e') (ha : 0 ≤ a) (hC : 0 ≤ C) (hP : 0 ≤ P)
    (hfit : e' ≤ a * e + C * Real.sqrt P) :
    e' ^ 2 ≤ 2 * a ^ 2 * e ^ 2 + 2 * C ^ 2 * P := by
…

theorem OAI.RegularPointCoordinates.forwardDefect_succ line 22
theorem OAI.RegularPointCoordinates.forwardDefect_propagates line 37
theorem OAI.RegularPointCoordinates.forwardDefect_stride line 49
Source documentation
A stride of m leaves the final new source term available, even though all intermediate source terms are discarded from the bound.
```
theorem forwardDefect_stride {σ η : ℝ} (hσ : 0 ≤ σ)
    {P : ℕ → ℝ} (hP : ∀ i, 0 ≤ P i) {m : ℕ} (hm : 0 < m) (i : ℕ) :
    σ ^ m * forwardDefect σ η P i + P (i + m) ≤
      forwardDefect σ η P (i + m) := by
…
```
Mentions: OAI.RegularPointCoordinates.forwardDefect
theorem OAI.RegularPointCoordinates.affine_fit_le_forwardDefect line 61
Source documentation
The same comparison works simultaneously in all residue classes of the affine-improvement stride. This is the discrete step used before the two-sided smoothing in radial pinching.
```
theorem affine_fit_le_forwardDefect {σ η : ℝ} (hσ : 0 ≤ σ)
    {P F : ℕ → ℝ} (hP : ∀ i, 0 ≤ P i) {m : ℕ} (hm : 0 < m)
    (hinitial : ∀ i < m, F i ≤ η * σ ^ i)
    (hstep : ∀ i, F (i + m) ≤ σ ^ m * F i + P (i + m)) :
    ∀ i, F i ≤ forwardDefect σ η P i := by
…
```
Mentions: OAI.RegularPointCoordinates.forwardDefect