Cocoercivity guards hold above the true smoothness scale, so failure certifies a smaller estimate.
theorem
V7.Stage2.cocoercivityGuard_of_scale_ge
{d : ℕ}
{x0 : Point d}
{p L M : ℝ}
(hp : 1 < p)
(inst : PositiveInstance p d x0)
(hLM : L ≤ M)
(hL : inst.L = L)
(x y : Point d)
:
CocoercivityGuard p M inst.oracle x y
Current-oriented Banach cocoercivity. The Bregman remainder is based at
y, so its linear term uses gradient y.
theorem
V7.Stage2.failed_cocoercivityGuard_lt_trueScale
{d : ℕ}
{x0 : Point d}
{p L M : ℝ}
(hp : 1 < p)
(inst : PositiveInstance p d x0)
(hL : inst.L = L)
(x y : Point d)
(hfail : ¬CocoercivityGuard p M inst.oracle x y)
: