Local Preimage Control for a Firmly Monotone Resolvent

This lemma is a technical local inverse estimate.

Let $E$ be a real inner-product space, let $P:E\to E$, and assume the firm monotonicity inequality

$$\|P(a)-P(b)\|^2\le\langle P(a)-P(b),a-b\rangle.$$

Let $z\in E$ and let $c,\delta>0$. Suppose that every $w$ with $\|w-z\|<\delta$ satisfies

$$c\|w-z\|\le\|P(w)-P(z)\|.$$

Then any $a\in E$ satisfying

$$\|P(a)-P(z)\|<\frac{c^2\delta}{2}$$

must also satisfy

$$\|a-z\|<\delta.$$

The auxiliary declaration resolvent_preimage_near_readable is used to transfer a sufficiently small image neighborhood into the corresponding domain neighborhood.

Original Lean declaration header

Within namespace FunctionalInequalities.Analysis. Shown in its original module context. Proof omitted.

set_option maxHeartbeats 800000 in
private lemma resolvent_preimage_near {P : E → E} {z : E}
    (hm : ∀ a b, ‖P a - P b‖ ^ 2 ≤ ⟪P a - P b, a - b⟫)
    {c δ : ℝ} (hc : 0 < c) (hδ : 0 < δ)
    (hl : ∀ w, ‖w - z‖ < δ → c * ‖w - z‖ ≤ ‖P w - P z‖)
    (a : E) (ha : ‖P a - P z‖ < c ^ 2 * δ / 2) :
    ‖a - z‖ < δ

Module navigation

Module: Analysis/Convex/SecondOrder.

Next: subgradient_expansion_of_hasFDerivAt_resolvent.

Source excerpt, lines 73–79 · Frozen source 408915f.

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Convex_SecondOrder

open scoped RealInnerProductSpace Topology
variable {E : Type*}
variable [NormedAddCommGroup E] [InnerProductSpace ℝ E]
set_option maxHeartbeats 800000

 lemma FunctionalInequalities.Analysis.resolvent_preimage_near_readable {P : E → E} {z : E}
    (hm : ∀ a b, ‖P a - P b‖ ^ 2 ≤ ⟪P a - P b, a - b⟫)
    {c δ : ℝ} (hc : 0 < c) (hδ : 0 < δ)
    (hl : ∀ w, ‖w - z‖ < δ → c * ‖w - z‖ ≤ ‖P w - P z‖)
    (a : E) (ha : ‖P a - P z‖ < c ^ 2 * δ / 2) :
    ‖a - z‖ < δ := by sorry