SourceBoundaryIntegratedGain.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The entropy prefactor in the original boundary error fits any prescribed negative-power budget after all fixed exponents are chosen.

theorem OAI.LipschitzHilbert.eventually_boundary_integrated_gain line 13

theorem OAI.LipschitzHilbert.eventually_boundary_integrated_gain_wide line 49

Source documentation

The boundary budget with the polynomial slack required at log ratio 2L.

theorem eventually_boundary_integrated_gain_wide (D q m Q : ℝ) :
    ∀ᶠ L : ℝ in atTop, ∀ a Nmass Fmass S : ℝ,
      0 ≤ a → a ≤ 1 → 0 ≤ Nmass → 0 ≤ Fmass → S ≤ L^m*Nmass*Fmass →
      (8*a*L^q*(4*SourceParameters.step L^(-(1/4:ℝ)))*((2:ℝ)^D)^7*(1+3*L))*S ≤
        L^(-Q)*Nmass*Fmass := by
…

Mentions: OAI.LipschitzHilbert.SourceParameters.step