Browder's demiclosedness principle

TheoremBrowder's demiclosedness principle#✓fully proved

If T is nonexpansive, u n ⇀ x weakly, and u n - T (u n) → 0, then T x = x.

theorem demiclosedness_of_lipschitzWith_one (T : E → E) (hT : LipschitzWith 1 T)
    (u : ℕ → E) (x : E)
    (hw : ∀ f : E →L[𝕜] 𝕜, Tendsto (fun n => f (u n)) atTop (𝓝 (f x)))
    (hres : Tendsto (fun n => u n - T (u n)) atTop (𝓝 0)) :
    T x = x

Uses 2 · Used by 1

Proof usesWeakly convergent sequences are norm-bounded · Cross term vanishes under weak convergence

Used byFixed points of a nonexpansive map are weakly sequentially closed

TheoremFixed points of a nonexpansive map are weakly sequentially closed#✓fully proved

The fixed-point set of a nonexpansive map is weakly sequentially closed: if every u n is a fixed point of T and u n ⇀ x weakly, then T x = x.

theorem fixedPoint_of_weakly_tendsto_of_forall_fixedPoint (T : E → E)
    (hT : LipschitzWith 1 T) (u : ℕ → E) (x : E)
    (hw : ∀ f : E →L[𝕜] 𝕜, Tendsto (fun n => f (u n)) atTop (𝓝 (f x)))
    (hfix : ∀ n, T (u n) = u n) :
    T x = x

Uses 1

Proof usesBrowder's demiclosedness principle

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.