TopMovingLogAbsorption.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The squared logarithmic loss in moving endpoint weights is absorbed by four inverse powers of the original positive top weight.

theorem OAI.LipschitzHilbert.top_inverse_log_squared_absorption line 11

theorem OAI.LipschitzHilbert.moving_weight_budget_absorption line 57

Source documentation

The precise polynomial produced by moving endpoint variation has the four-inverse-power envelope used in the amplitude-motion argument.

theorem moving_weight_budget_absorption {A h S C Q a δ ε V : ℝ}
    (hh : 0 < h) (hhS : h ≤ S) (hC : 1 ≤ C) (hhC : h ≤ C)
    (hQ : 0 ≤ Q) (ha0 : 0 ≤ a) (ha1 : a ≤ 1)
    (hδ : 0 ≤ δ) (hε : 0 ≤ ε) (hV : 0 ≤ V) (hVQ : V ≤ Q*Real.log (S/h))
    (hA : A ≤ (Real.exp (a*δ)*h^(-a))*((a*δ+ε*V)+ε*V+(a*δ+ε*V)*V)) :
    A ≤ Real.exp (a*δ)*(δ+ε)*C^4*(1+Q*(Real.log (max 1 S)+1))^2*h^(-(4:ℝ)) := by
…