NormedSpace.isBounded_polar_of_mem_nhds_zero
theorem NormedSpace.isBounded_polar_of_mem_nhds_zero :
โ (๐ : Type u_1) [inst : NontriviallyNormedField ๐] {E : Type u_2} [inst_1 : SeminormedAddCommGroup E]
[inst_2 : NormedSpace ๐ E] {s : Set E}, s โ nhds 0 โ Bornology.IsBounded (NormedSpace.polar ๐ s)
This theorem states that, given a neighborhood `s` of the origin in a normed space `E` over a non-trivially normed field `๐`, all elements of the polar of `s` are bounded with respect to the ambient bornology. In other words, the dual norms of all functionals in the polar subset of `s` (i.e. those functionals which evaluate to something of norm at most one at all points `z` in `s`) are bounded by a constant. That is to say, there exists a real number such that the dual norm of any functional in the polar subset of `s` is less than or equal to this constant.
More concisely: Given a neighborhood `s` of the origin in a normed space `E` over a non-trivially normed field `๐`, there exists a constant `C` such that the dual norm of any functional in the polar subset of `s` is bounded by `C`.
|
NormedSpace.polar_closedBall
theorem NormedSpace.polar_closedBall :
โ {๐ : Type u_3} {E : Type u_4} [inst : RCLike ๐] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ๐ E]
{r : โ}, 0 < r โ NormedSpace.polar ๐ (Metric.closedBall 0 r) = Metric.closedBall 0 rโปยน
This theorem states that in a normed space `E` (over a ring-like structure `๐`), the polar of the closed ball centered at the origin with radius `r` is equivalent to the closed ball of the dual space, also centered at the origin, but with the inverse of the original radius. This is under the condition that `r` is a positive real number. The polar of a set, here the closed ball, in the normed space is defined as the subset of functionals in the dual space that evaluate to a value with norm at most one for all points in the set. The closed ball in a space is defined as the set of all points whose distance to a specified point (in this case the origin) is less than or equal to a given value (here `r` or its reciprocal).
More concisely: In a normed space, the polar of the closed ball centered at the origin with radius $r$ is equal to the closed ball of the dual space, centered at the origin, with radius $1/r$ for $r > 0$.
|
NormedSpace.smul_mem_polar
theorem NormedSpace.smul_mem_polar :
โ {๐ : Type u_1} [inst : NontriviallyNormedField ๐] {E : Type u_2} [inst_1 : SeminormedAddCommGroup E]
[inst_2 : NormedSpace ๐ E] {s : Set E} {x' : NormedSpace.Dual ๐ E} {c : ๐},
(โ z โ s, โx' zโ โค โcโ) โ cโปยน โข x' โ NormedSpace.polar ๐ s
The theorem `NormedSpace.smul_mem_polar` states that for a non-trivially normed field `๐` and a semi-normed add commutative group `E` that forms a normed space over `๐`, if `x'` is an element of the dual space of `E` such that for all `z` in a given subset `s` of `E`, the norms `โx' zโ` are bounded by the norm of a scalar `c`, then a scalar multiple `cโปยน โข x'` belongs to the polar of `s` with respect to `๐`. In other words, if `x'` is a functional that has bounded evaluations at every point of `s`, then a scaled version of this functional using the inverse of the bounding scalar is in the polar set of `s`.
More concisely: If a functional in the dual space of a normed space is bounded on a subset, then a scaled version of the functional is in the polar set of that subset.
|
NormedSpace.eq_iff_forall_dual_eq
theorem NormedSpace.eq_iff_forall_dual_eq :
โ (๐ : Type v) [inst : RCLike ๐] {E : Type u} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ๐ E] {x y : E},
x = y โ โ (g : NormedSpace.Dual ๐ E), g x = g y
This theorem, named `NormedSpace.eq_iff_forall_dual_eq`, states that for any nontrivially normed field `๐`, and any elements `x` and `y` of a seminormed additive commutative group `E` which is also a normed space over `๐`, `x` and `y` are equal if and only if for all elements `g` of the topological dual of the seminormed space `E`, the result of applying `g` to `x` is equal to the result of applying `g` to `y`. In simpler terms, two elements in this specific mathematical structure are identical if they produce the same results when evaluated under all possible elements of the dual space. This theorem is also related to the `geometric_hahn_banach_point_point` theorem.
More concisely: For any nontrivially normed field `๐` and normed space `E` over `๐`, two elements `x` and `y` in `E` are equal if and only if for all `g` in the topological dual of `E`, `g(x) = g(y)`.
|
NormedSpace.norm_le_dual_bound
theorem NormedSpace.norm_le_dual_bound :
โ (๐ : Type v) [inst : RCLike ๐] {E : Type u} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ๐ E] (x : E)
{M : โ}, 0 โค M โ (โ (f : NormedSpace.Dual ๐ E), โf xโ โค M * โfโ) โ โxโ โค M
The theorem `NormedSpace.norm_le_dual_bound` states that for any scalars in a certain type `๐`, which is a real or complex-like type, and any element `x` in a seminormed space `E` that is a normed space over `๐`, if there is a nonnegative real number `M` such that the norm of `f x` is less than or equal to `M` times the norm of `f` for every `f` in the topological dual space of `E`, then the norm of `x` is less than or equal to `M`. This theorem can be used to control the norm of `x` through controlling the norm of `f x` in the context of seminormed and normed spaces.
More concisely: If an element in a normed space satisfies the condition that the norm of its dual image is less than or equal to the product of its norm and the norm of the dual element for all dual elements, then its own norm is bounded by that constant.
|