CorrectionScales.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Summability of the exact-correction scales

The iteration uses t ↦ t^(6/5). For an explicit sufficiently small initial scale, the entire sequence is dominated by a geometric series. This gives the displacement budget needed for the exact correction.

def OAI.ClosedSurfaceR4.ExactCorrection.correctionScale line 19
Source documentation
The fast-decaying scale used in successive smoothing steps.
```
noncomputable def correctionScale (t : ℝ) : ℕ → ℝ
  | 0 => t
  | n + 1 => (correctionScale t n) ^ (6 / 5 : ℝ)
```
lemma OAI.ClosedSurfaceR4.ExactCorrection.correctionScale_nonneg line 23
lemma OAI.ClosedSurfaceR4.ExactCorrection.scale_step_le_half line 29
theorem OAI.ClosedSurfaceR4.ExactCorrection.correctionScale_le_geometric line 49
Source documentation
A concrete geometric majorant, independent of the later block lengths.
```
theorem correctionScale_le_geometric {t : ℝ} (ht : 0 ≤ t) (hsmall : t ≤ 1 / 32)
    (n : ℕ) : correctionScale t n ≤ t * (1 / 2 : ℝ) ^ n := by
…
```
Mentions: OAI.ClosedSurfaceR4.ExactCorrection.correctionScale
theorem OAI.ClosedSurfaceR4.ExactCorrection.correctionScale_summable line 64
Source documentation
The exact-correction scales have total mass strictly less than 1/4.
```
theorem correctionScale_summable {t : ℝ} (ht : 0 ≤ t) (hsmall : t ≤ 1 / 32) :
    Summable (correctionScale t) ∧ (∑' n, correctionScale t n) < 1 / 4 := by
…
```
Mentions: OAI.ClosedSurfaceR4.ExactCorrection.correctionScale