Weak topology and weak convergence

TheoremWeakly convergent sequences are norm-bounded#✓fully proved

Let \(E\) be a normed space over \(\mathbb{K} = \mathbb{R}\) or \(\mathbb{C}\), let \((u_n)_{n \in \mathbb{N}}\) be a sequence in \(E\) and let \(x \in E\). If \(f(u_n) \to f(x)\) as \(n \to \infty\) for every continuous linear functional \(f \colon E \to \mathbb{K}\), then the norms are bounded above: there is a real number \(C\) with \(\|u_n\| \le C\) for all \(n\).

theorem bddAbove_norm_range_of_forall_tendsto {u : ℕ → E} {x : E}
    (h : ∀ f : StrongDual 𝕜 E, Tendsto (fun n => f (u n)) atTop (𝓝 (f x))) :
    BddAbove (Set.range fun n => ‖u n‖)

Used by 3

Used byWeakly convergent sequences are norm-bounded (weak topology form) · Weak lower semicontinuity of the norm · Complete continuity of compact operators

TheoremWeak lower semicontinuity of the norm#✓fully proved

Let \(E\) be a normed space over \(\mathbb{K} = \mathbb{R}\) or \(\mathbb{C}\), let \((u_n)_{n \in \mathbb{N}}\) be a sequence in \(E\) and let \(x \in E\). If \(f(u_n) \to f(x)\) as \(n \to \infty\) for every continuous linear functional \(f \colon E \to \mathbb{K}\), that is, \(u_n\) converges weakly to \(x\), then \(\|x\| \le \liminf_{n \to \infty} \|u_n\|\).

theorem norm_le_liminf_norm_of_forall_tendsto {u : ℕ → E} {x : E}
    (h : ∀ f : StrongDual 𝕜 E, Tendsto (fun n => f (u n)) atTop (𝓝 (f x))) :
    ‖x‖ ≤ liminf (fun n => ‖u n‖) atTop

Uses 1 · Used by 1

Proof usesWeakly convergent sequences are norm-bounded

Used byWeak lower semicontinuity of the norm (weak topology form)

TheoremBounded operators preserve weak convergence#✓fully proved

Let \(E\) and \(F\) be normed spaces over \(\mathbb{K} = \mathbb{R}\) or \(\mathbb{C}\), let \(T \colon E \to F\) be a continuous linear map, let \((u_n)_{n \in \mathbb{N}}\) be a sequence in \(E\) and let \(x \in E\). If \(f(u_n) \to f(x)\) for every continuous linear functional \(f \colon E \to \mathbb{K}\), then \(g(T u_n) \to g(T x)\) for every continuous linear functional \(g \colon F \to \mathbb{K}\).

theorem tendsto_apply_of_forall_tendsto {F : Type*} [NormedAddCommGroup F] [NormedSpace 𝕜 F]
    {u : ℕ → E} {x : E} (T : E →L[𝕜] F)
    (h : ∀ f : StrongDual 𝕜 E, Tendsto (fun n => f (u n)) atTop (𝓝 (f x))) :
    ∀ g : StrongDual 𝕜 F, Tendsto (fun n => g (T (u n))) atTop (𝓝 (g (T x)))

Used by 2

Used byBounded operators preserve weak convergence (weak topology form) · Complete continuity of compact operators

TheoremWeak convergence gives convergence under every functional#✓fully proved

Let \(E\) be a normed space over \(\mathbb{K} = \mathbb{R}\) or \(\mathbb{C}\), let \((u_n)_{n \in \mathbb{N}}\) be a sequence in \(E\) and let \(x \in E\). If \(u_n \to x\) in the weak topology of \(E\) (the topology induced by all continuous linear functionals \(E \to \mathbb{K}\)), then \(f(u_n) \to f(x)\) as \(n \to \infty\) for every continuous linear functional \(f \colon E \to \mathbb{K}\).

theorem forall_tendsto_of_tendsto_weakSpace {u : ℕ → E} {x : E}
    (h : Tendsto (fun n => toWeakSpace 𝕜 E (u n)) atTop (𝓝 (toWeakSpace 𝕜 E x))) :
    ∀ f : StrongDual 𝕜 E, Tendsto (fun n => f (u n)) atTop (𝓝 (f x))

Used by 5

Used byWeakly convergent sequences are norm-bounded (weak topology form) · Weak lower semicontinuity of the norm (weak topology form) · Bounded operators preserve weak convergence (weak topology form) · Kadec–Klee property, weak-topology form · Complete continuity of compact operators, weak-topology form

TheoremConvergence under every functional gives weak convergence#✓fully proved

Let \(E\) be a normed space over \(\mathbb{K} = \mathbb{R}\) or \(\mathbb{C}\), let \((u_n)_{n \in \mathbb{N}}\) be a sequence in \(E\) and let \(x \in E\). If \(f(u_n) \to f(x)\) as \(n \to \infty\) for every continuous linear functional \(f \colon E \to \mathbb{K}\), then \(u_n \to x\) in the weak topology of \(E\) (the topology induced by all continuous linear functionals \(E \to \mathbb{K}\)).

theorem tendsto_weakSpace_of_forall_tendsto {u : ℕ → E} {x : E}
    (h : ∀ f : StrongDual 𝕜 E, Tendsto (fun n => f (u n)) atTop (𝓝 (f x))) :
    Tendsto (fun n => toWeakSpace 𝕜 E (u n)) atTop (𝓝 (toWeakSpace 𝕜 E x))

Used by 2

Used byBounded operators preserve weak convergence (weak topology form) · Kadec–Klee iff, weak-topology form

TheoremWeakly convergent sequences are norm-bounded (weak topology form)#✓fully proved

Let \(E\) be a normed space over \(\mathbb{K} = \mathbb{R}\) or \(\mathbb{C}\), let \((u_n)_{n \in \mathbb{N}}\) be a sequence in \(E\) and let \(x \in E\). If \(u_n \to x\) in the weak topology of \(E\) (the topology induced by all continuous linear functionals \(E \to \mathbb{K}\)), then there is a real number \(C\) with \(\|u_n\| \le C\) for all \(n\).

theorem bddAbove_norm_range_of_tendsto_weakSpace {u : ℕ → E} {x : E}
    (h : Tendsto (fun n => toWeakSpace 𝕜 E (u n)) atTop (𝓝 (toWeakSpace 𝕜 E x))) :
    BddAbove (Set.range fun n => ‖u n‖)

Uses 2

Proof usesWeakly convergent sequences are norm-bounded · Weak convergence gives convergence under every functional

TheoremWeak lower semicontinuity of the norm (weak topology form)#✓fully proved

Let \(E\) be a normed space over \(\mathbb{K} = \mathbb{R}\) or \(\mathbb{C}\), let \((u_n)_{n \in \mathbb{N}}\) be a sequence in \(E\) and let \(x \in E\). If \(u_n \to x\) in the weak topology of \(E\) (the topology induced by all continuous linear functionals \(E \to \mathbb{K}\)), then \(\|x\| \le \liminf_{n \to \infty} \|u_n\|\).

theorem norm_le_liminf_norm_of_tendsto_weakSpace {u : ℕ → E} {x : E}
    (h : Tendsto (fun n => toWeakSpace 𝕜 E (u n)) atTop (𝓝 (toWeakSpace 𝕜 E x))) :
    ‖x‖ ≤ liminf (fun n => ‖u n‖) atTop

Uses 2

Proof usesWeak convergence gives convergence under every functional · Weak lower semicontinuity of the norm

TheoremBounded operators preserve weak convergence (weak topology form)#✓fully proved

Let \(E\) and \(F\) be normed spaces over \(\mathbb{K} = \mathbb{R}\) or \(\mathbb{C}\), let \(T \colon E \to F\) be a continuous linear map, let \((u_n)_{n \in \mathbb{N}}\) be a sequence in \(E\) and let \(x \in E\). If \(u_n \to x\) in the weak topology of \(E\), then \(T u_n \to T x\) in the weak topology of \(F\); here the weak topology of a space is the one induced by its continuous linear functionals.

theorem tendsto_weakSpace_apply_of_tendsto_weakSpace {F : Type*}
    [NormedAddCommGroup F] [NormedSpace 𝕜 F] {u : ℕ → E} {x : E} (T : E →L[𝕜] F)
    (h : Tendsto (fun n => toWeakSpace 𝕜 E (u n)) atTop (𝓝 (toWeakSpace 𝕜 E x))) :
    Tendsto (fun n => toWeakSpace 𝕜 F (T (u n))) atTop (𝓝 (toWeakSpace 𝕜 F (T x)))

Uses 3

Proof usesWeak convergence gives convergence under every functional · Bounded operators preserve weak convergence · Convergence under every functional gives weak convergence

TheoremFinitely many functionals have a common nonzero kernel vector#✓fully proved

Finitely many continuous linear functionals on an infinite-dimensional normed space have a common nonzero kernel vector.

theorem exists_ne_zero_forall_dual_apply_eq_zero (hInf : ¬ FiniteDimensional 𝕜 E)
    (S : Finset (E →L[𝕜] 𝕜)) :
    ∃ v : E, v ≠ 0 ∧ ∀ f ∈ S, f v = 0

Used by 2

Used byWeak closure of the unit sphere is the closed unit ball · Weakly open sets contain lines through each point

TheoremWeakly open sets contain lines through each point#✓fully proved

Every nonempty weakly open set contains a whole line through each of its points: if U is weakly open and x ∈ U, then x + t • v ∈ U for all scalars t and some nonzero v (a common kernel vector of the finitely many functionals constraining a basic weak neighbourhood of x).

theorem exists_line_subset_of_isOpen (hInf : ¬ FiniteDimensional 𝕜 E)
    {U : Set (WeakSpace 𝕜 E)} (hU : IsOpen U) {x : E}
    (hx : toWeakSpace 𝕜 E x ∈ U) :
    ∃ v : E, v ≠ 0 ∧ ∀ t : 𝕜, toWeakSpace 𝕜 E (x + t • v) ∈ U

Uses 1 · Used by 1

Proof usesFinitely many functionals have a common nonzero kernel vector

Used byWeakly open sets are unbounded in infinite dimensions

TheoremWeakly open sets are unbounded in infinite dimensions#✓fully proved

Every nonempty weakly open set in an infinite-dimensional normed space is unbounded in norm.

theorem exists_norm_gt_of_isOpen (hInf : ¬ FiniteDimensional 𝕜 E)
    {U : Set (WeakSpace 𝕜 E)} (hU : IsOpen U) (hne : U.Nonempty) (R : ℝ) :
    ∃ y ∈ U, R < ‖(toWeakSpace 𝕜 E).symm y‖

Uses 1 · Used by 2

Proof usesWeakly open sets contain lines through each point

Used byOpen unit ball is not weakly open in infinite dimensions · Unit sphere is not weakly open in infinite dimensions

TheoremOpen unit ball is not weakly open in infinite dimensions#✓fully proved

The open unit ball is not weakly open in infinite dimensions.

theorem not_isOpen_image_ball (hInf : ¬ FiniteDimensional 𝕜 E) :
    ¬ IsOpen ((toWeakSpace 𝕜 E) '' Metric.ball (0 : E) 1)

Uses 1 · Used by 1

Proof usesWeakly open sets are unbounded in infinite dimensions

Used byWeak topology is strictly coarser in infinite dimensions

TheoremUnit sphere is not weakly open in infinite dimensions#✓fully proved

The unit sphere is not weakly open in infinite dimensions.

theorem not_isOpen_image_sphere (hInf : ¬ FiniteDimensional 𝕜 E) :
    ¬ IsOpen ((toWeakSpace 𝕜 E) '' Metric.sphere (0 : E) 1)

Uses 1

Proof usesWeakly open sets are unbounded in infinite dimensions

TheoremWeak closure of the unit sphere is the closed unit ball#✓fully proved

In an infinite-dimensional normed space, the weak closure of the unit sphere is the closed unit ball.

theorem closure_image_sphere_eq_image_closedBall (hInf : ¬ FiniteDimensional 𝕜 E) :
    closure ((toWeakSpace 𝕜 E) '' Metric.sphere (0 : E) 1)
      = (toWeakSpace 𝕜 E) '' Metric.closedBall (0 : E) 1

Uses 1 · Used by 1

Proof usesFinitely many functionals have a common nonzero kernel vector

Used byUnit sphere is not weakly closed in infinite dimensions

TheoremUnit sphere is not weakly closed in infinite dimensions#✓fully proved

The unit sphere is not weakly closed in infinite dimensions: its weak closure is the whole closed unit ball.

theorem not_isClosed_image_sphere (hInf : ¬ FiniteDimensional 𝕜 E) :
    ¬ IsClosed ((toWeakSpace 𝕜 E) '' Metric.sphere (0 : E) 1)

Uses 1 · Used by 1

Proof usesWeak closure of the unit sphere is the closed unit ball

Used byUnit sphere is not weakly compact in infinite dimensions

TheoremUnit sphere is not weakly compact in infinite dimensions#✓fully proved

The unit sphere is not weakly compact in infinite dimensions.

theorem not_isCompact_image_sphere (hInf : ¬ FiniteDimensional 𝕜 E) :
    ¬ IsCompact ((toWeakSpace 𝕜 E) '' Metric.sphere (0 : E) 1)

Uses 1

Proof usesUnit sphere is not weakly closed in infinite dimensions

TheoremWeak topology equals norm topology in finite dimensions#✓fully proved

In finite dimensions the identity map from the norm topology to the weak topology is an open map: the weak topology agrees with the norm topology.

theorem isOpenMap_toWeakSpaceCLM_of_finiteDimensional [FiniteDimensional 𝕜 E] :
    IsOpenMap (toWeakSpaceCLM 𝕜 E)

TheoremWeak topology is strictly coarser in infinite dimensions#✓fully proved

In infinite dimensions the identity map from the norm topology to the weak topology is not an open map: the open unit ball is norm-open but not weakly open.

theorem not_isOpenMap_toWeakSpaceCLM_of_infiniteDimensional
    (hInf : ¬ FiniteDimensional 𝕜 E) :
    ¬ IsOpenMap (toWeakSpaceCLM 𝕜 E)

Uses 1

Proof usesOpen unit ball is not weakly open in infinite dimensions

18 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.