GaussianErrorBudget.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Finite normalization ranges and uniform Gaussian tails

Only finitely many outward scales need the small splitting error. Beyond that range a fixed geometric bound suffices, and its Gaussian tail tends to zero uniformly as the range grows.

def OAI.RegularPointCoordinates.splitSeriesTerm line 21
Source documentation
A finite prefix has the small analytic error; only a fixed bound is used beyond the last controlled scale.
```
def splitSeriesTerm (a : ℕ → ℝ) (ε : ℝ) (N j : ℕ) : ℝ :=
…
```
theorem OAI.RegularPointCoordinates.summable_splitSeriesTerm line 24
theorem OAI.RegularPointCoordinates.tsum_splitSeriesTerm line 30
theorem OAI.RegularPointCoordinates.tsum_splitSeriesTerm_le line 47

theorem OAI.RegularPointCoordinates.exists_small_splitSeriesTerm line 57

Source documentation

Small local errors and a sufficiently remote tail give any prescribed uniform tolerance. Both choices are made before selecting a scale.

theorem exists_small_splitSeriesTerm {a : ℕ → ℝ} (ha : Summable a)
    (hpos : ∀ j, 0 ≤ a j) {η : ℝ} (hη : 0 < η) :
    ∃ N : ℕ, ∃ ε : ℝ, 0 < ε ∧ ∀ M, N ≤ M → ∀ e, 0 ≤ e → e ≤ ε →
      (∑' j, splitSeriesTerm a e M j) < η := by
…

Mentions: OAI.RegularPointCoordinates.splitSeriesTerm