SourceUnaryErrorBudget.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The mask error stays negligible after the phase-mass factor and the entire logarithmic path-drop sum.

theorem OAI.LipschitzHilbert.eventually_source_unary_error_scale line 14

theorem OAI.LipschitzHilbert.eventually_source_unary_error_budget line 52

Source documentation

Uniformly over a finite active prefix and any subcollection of its indices, the physical off-child contribution costs at most one.

theorem eventually_source_unary_error_budget (q C : ℝ) :
    ∀ᶠ L : ℝ in atTop, ∀ (n : ℕ → ℝ) (count : ℕ) (S : Finset ℕ),
      S ⊆ Finset.range count → Antitone n →
    ∀ (M p ε Q : ℝ), 1 ≤ M → 0 ≤ p → p ≤ Real.sqrt L →
      0 ≤ ε → ε ≤ L^q*Real.exp (-L*Real.log L) →
      0 ≤ Q → Q ≤ Real.exp (C*Real.sqrt L) →
      (∀ j < count, M < n j) → 0 ≤ n count → Real.log (n 0) ≤ 3*L →
      4*p*ε*(Q*∑ j ∈ S, pathDrop n j) ≤ 1 := by
…

Mentions: OAI.LipschitzHilbert.pathDrop