exists_dual_vector'
theorem exists_dual_vector' :
ā (š : Type v) [inst : RCLike š] {E : Type u} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace š E]
[inst_3 : Nontrivial E] (x : E), ā g, āgā = 1 ā§ g x = āāxā
This theorem is a variant of the Hahn-Banach theorem, which in this case, removes the requirement that the vector `x` be nonzero, and provides an arbitrary selection for the dual element when `x = 0`. Specifically, for any type `š` that behaves like a normed field, and a normed vector space `E` over `š`, given any vector `x` from `E`, there exists a dual vector `g` such that its norm is 1 and its application to `x` gives the norm of `x`. The theorem also assumes that the vector space `E` is nontrivial, i.e., it contains at least two distinct elements.
More concisely: For any normed field `š` and nontrivial normed vector space `E` over `š`, for every vector `x` in `E`, there exists a dual vector `g` such that `||g|| = 1` and ` = ||x||`.
|
Submodule.ClosedComplemented.of_finiteDimensional
theorem Submodule.ClosedComplemented.of_finiteDimensional :
ā {š : Type u_1} [inst : RCLike š] {F : Type u_3} [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace š F]
(p : Submodule š F) [inst_3 : FiniteDimensional š ā„p], p.ClosedComplemented
This theorem states that for any type `š`, which is either the real numbers `ā` or the complex numbers `ā` (as indicated by `RCLike š`), and for any finite-dimensional submodule `p` of a normed additively commutative group `F` over `š` (a normed space), `p` is complemented in the topological sense, i.e., the whole space `F` can be decomposed as a direct sum of `p` and some other submodule. Here, "finite-dimensional" means that the submodule `p` is a vector space over `š` with a finite basis.
More concisely: For any normed space `F` over `ā` or `ā` with a finite-dimensional submodule `p`, there exists a complementary submodule such that `F` is the direct sum of `p` and this complementary submodule.
|
exists_dual_vector
theorem exists_dual_vector :
ā (š : Type v) [inst : RCLike š] {E : Type u} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace š E] (x : E),
x ā 0 ā ā g, āgā = 1 ā§ g x = āāxā
The theorem, known as a corollary of the Hahn-Banach theorem, states that for every nonzero element `x` in a normed space (a vector space with a function called a norm that assigns lengths to vectors), there exists a corresponding element in the dual space (a space of continuous linear functions that map from the original space to the field of scalars) with a norm of `1`, such that the value of the dual element evaluated at `x` is equal to the norm of `x`. This is a fundamental concept in functional analysis and has applications in various areas of mathematics and physics.
More concisely: For every nonzero x in a normed space, there exists an element in its dual space with norm 1 and evaluating to x's norm at x.
|
Real.exists_extension_norm_eq
theorem Real.exists_extension_norm_eq :
ā {E : Type u_1} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ā E] (p : Subspace ā E) (f : ā„p āL[ā] ā),
ā g, (ā (x : ā„p), g āx = f x) ā§ āgā = āfā
This is the Hahn-Banach theorem for continuous linear functions over the real numbers, `ā`. For any seminormed additive commutative group `E` that is a normed space over `ā`, and any subspace `p` of `E`, and any continuous linear function `f` from `p` to `ā`, there exists a linear function `g` such that `g` matches `f` on `p` (expressed as `ā (x : ā„p), g āx = f x`) and the norm of `g` equals the norm of `f` (expressed as `āgā = āfā`).
This theorem states that any continuous linear function defined on a subspace of a normed vector space can be extended to a function on the whole space without increasing its norm, which is a key result in functional analysis. There is a more general version of this theorem that works for both `ā` and `ā`.
More concisely: Given a normed space `E` over the real numbers, any continuous linear function on a subspace of `E` can be extended to a linear function on all of `E` with the same norm.
|
exists_extension_norm_eq
theorem exists_extension_norm_eq :
ā {š : Type u_1} [inst : RCLike š] {E : Type u_2} [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace š E]
(p : Subspace š E) (f : ā„p āL[š] š), ā g, (ā (x : ā„p), g āx = f x) ā§ āgā = āfā
This is the statement of the Hahn-Banach theorem for continuous linear functions over a type `š` which satisfies the `RCLike š` condition. Given any subspace `p` of a seminormed add-commutative group `E` which is also a normed space over `š`, and a continuous linear function `f` from `p` to `š`, there exists a function `g` such that `g` agrees with `f` on `p` (i.e., `g āx = f x` for all `x` in `p`), and the norm of `g` is equal to the norm of `f` (i.e., `āgā = āfā`).
More concisely: Given any subspace of a normed space over a RCLIKE field, and a continuous linear function on that subspace, there exists an extension of that function to the entire space with the same norm.
|
exists_dual_vector''
theorem exists_dual_vector'' :
ā (š : Type v) [inst : RCLike š] {E : Type u} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace š E] (x : E),
ā g, āgā ā¤ 1 ā§ g x = āāxā
This theorem is a variant of the Hahn-Banach theorem, which states that for any vector space `E` over a scalar field `š`, both of which have a norm structure, and any vector `x` in `E`, there exists a dual vector `g` such that the norm of `g` is less than or equal to `1` and the action of `g` on `x` is equal to the norm of `x`. It differs from the usual Hahn-Banach theorem by not requiring `x` to be non-zero. This result cannot be improved for the trivial vector space.
More concisely: For any normed vector space `(E, ||||)` over a scalar field `ā`, and any vector `x` in `E`, there exists a norm-1 functional `g` such that `g(x) = ||x||`. (This variant of the Hahn-Banach theorem allows `x` to be the zero vector.)
|