SourceStoppedError.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The marked prediction errors have a uniform total logarithmic budget along an active path. The source cutoff is exactly M = L^A_M; the last active index is included even when its drop crosses the cutoff.

theorem OAI.LipschitzHilbert.source_error_of_drop_comparability line 18

Source documentation

Transfer from the fixed snapshot drop to the moving point, using the factor two furnished by actual source path-drop comparability.

theorem source_error_of_drop_comparability {error ρ snapshotDrop pointDrop : ℝ}
    (hρ : 0 ≤ ρ) (hdrop : snapshotDrop/2 ≤ pointDrop)
    (herror : error ≤ ρ*snapshotDrop) : error ≤ (2*ρ)*pointDrop := by
…

theorem OAI.LipschitzHilbert.stopped_source_error_transfer line 24
theorem OAI.LipschitzHilbert.eventually_source_drop_budget line 36

theorem OAI.LipschitzHilbert.eventually_source_stopped_error line 61

Source documentation

The original mass bound L^C N^2 gives the source active-drop estimate. No lower bound on the initial mass is required when there are no active indices. The terminal mass is allowed to be zero.

theorem eventually_source_stopped_error (C A_M : ℝ) (hC : 0 ≤ C) (hAM : 0 ≤ A_M) :
    ∀ᶠ L : ℝ in atTop, ∀ (n e : ℕ → ℝ) (count stop : ℕ), stop ≤ count →
      ∀ N : ℝ, 0 < N → Real.log N ≤ 2*L → n 0 ≤ L^C*N^2 →
      (∀ j < stop, L^A_M < n j) → 0 ≤ n stop →
      (∀ j < count, e j ≤ if j < stop then
        (2*SourceParameters.step L^(-(1/32:ℝ)))*pathDrop n j else 0) →
      (∑ j ∈ Finset.range count, e j) ≤ 1 := by
…

Mentions: OAI.LipschitzHilbert.SourceParameters.step, OAI.LipschitzHilbert.pathDrop

theorem OAI.LipschitzHilbert.eventually_source_snapshot_stopped_error line 104

Source documentation

Snapshot errors from the marked-cell comparison have total cost at most one after the actual factor-two drop comparison.

theorem eventually_source_snapshot_stopped_error (C A_M : ℝ)
    (hC : 0 ≤ C) (hAM : 0 ≤ A_M) :
    ∀ᶠ L : ℝ in atTop, ∀ (n e snapshot : ℕ → ℝ) (count stop : ℕ), stop ≤ count →
      ∀ N : ℝ, 0 < N → Real.log N ≤ 2*L → n 0 ≤ L^C*N^2 →
      (∀ j < stop, L^A_M < n j) → 0 ≤ n stop →
      (∀ j < stop, snapshot j/2 ≤ pathDrop n j) →
      (∀ j < count, e j ≤ if j < stop then
        SourceParameters.step L^(-(1/32:ℝ))*snapshot j else 0) →
      (∑ j ∈ Finset.range count, e j) ≤ 1 := by
…

Mentions: OAI.LipschitzHilbert.pathDrop, OAI.LipschitzHilbert.SourceParameters.step