Opial property

TheoremWeakly convergent sequences are norm-bounded#✓fully proved

A weakly convergent sequence is norm-bounded (Banach–Steinhaus applied to the evaluation maps on the dual space).

theorem bddAbove_norm_of_weakly_tendsto (u : ℕ → E) (x : E)
    (hw : ∀ f : E →L[𝕜] 𝕜, Tendsto (fun n => f (u n)) atTop (𝓝 (f x))) :
    BddAbove (Set.range fun n => ‖u n‖)

Used by 3

Used byBrowder's demiclosedness principle · Opial's property · Opial's property, squared-norm form

TheoremCross term vanishes under weak convergence#✓fully proved

The cross term in the squared-norm identity tends to 0 under weak convergence, via the Fréchet–Riesz representation of the functional z ↦ ⟪x - y, z⟫.

theorem tendsto_re_inner_sub_of_weakly_tendsto (u : ℕ → E) (x : E)
    (hw : ∀ f : E →L[𝕜] 𝕜, Tendsto (fun n => f (u n)) atTop (𝓝 (f x)))
    (y : E) :
    Tendsto (fun n => RCLike.re ⟪u n - x, x - y⟫_𝕜) atTop (𝓝 0)

Used by 2

Used byBrowder's demiclosedness principle · Opial's property, squared-norm form

TheoremOpial's property, squared-norm form#✓fully proved

If u n ⇀ x weakly and y ≠ x, then liminf ‖u n - x‖² < liminf ‖u n - y‖².

theorem opial_liminf_sq (u : ℕ → E) (x y : E) (hxy : x ≠ y)
    (hw : ∀ f : E →L[𝕜] 𝕜, Tendsto (fun n => f (u n)) atTop (𝓝 (f x))) :
    liminf (fun n => ‖u n - x‖ ^ 2) atTop < liminf (fun n => ‖u n - y‖ ^ 2) atTop

Uses 2 · Used by 1

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

Used byOpial's property

TheoremOpial's property#✓fully proved

If u n ⇀ x weakly and y ≠ x, then liminf ‖u n - x‖ < liminf ‖u n - y‖.

theorem opial_liminf (u : ℕ → E) (x y : E) (hxy : x ≠ y)
    (hw : ∀ f : E →L[𝕜] 𝕜, Tendsto (fun n => f (u n)) atTop (𝓝 (f x))) :
    liminf (fun n => ‖u n - x‖) atTop < liminf (fun n => ‖u n - y‖) atTop

Uses 2

Proof usesWeakly convergent sequences are norm-bounded · Opial's property, squared-norm form

4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.