ResidualBudget.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Final source-parameter budgets for the marked and unary residual costs.

theorem OAI.LipschitzHilbert.residual_polynomial_budget line 17

Source documentation

The mass cutoff is chosen after the fixed polynomial losses. Both residual exponents in §10 are at most -1/4.

theorem residual_polynomial_budget {L A C μ : ℝ}
    (hL : 1 ≤ L) (hμ : μ ≤ 1 / 12) (hA : 0 ≤ A)
    (hchoice : 4 * (C + 1 / 2) ≤ A) :
    L ^ (1 / 2 : ℝ) * L ^ C * (L ^ A) ^ (-(1 / 3 : ℝ) + μ) ≤ 1 ∧
      L ^ (1 / 2 : ℝ) * L ^ C * (L ^ A) ^ (-(1 / 2 : ℝ) + μ) ≤ 1 := by
…

theorem OAI.LipschitzHilbert.eventually_discarded_residual_small line 37
Source documentation
The discarded-top error stays negligible after the source's exp(C sqrt L) mass bound and any fixed polynomial loss.
```
theorem eventually_discarded_residual_small (p C : ℝ) :
    ∀ᶠ L : ℝ in atTop,
      Real.exp (-L) * Real.exp (C * Real.sqrt L) * L ^ p ≤ 1 := by
…
```
theorem OAI.LipschitzHilbert.source_polynomial_step_decay line 58
Source documentation
Any fixed polynomial times the source step's negative power tends to zero. This pays for the cumulative marked prediction losses.
```
theorem source_polynomial_step_decay (a c : ℝ) (hc : 0 < c) :
    Tendsto (fun L : ℝ => L ^ a * SourceParameters.step L ^ (-c)) atTop (𝓝 0) := by
…
```
Mentions: OAI.LipschitzHilbert.SourceParameters.step