exists_norm_le_le_norm_sub_of_finset
theorem exists_norm_le_le_norm_sub_of_finset :
β {π : Type u} [inst : NontriviallyNormedField π] {E : Type v} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] [inst_3 : CompleteSpace π] {c : π},
1 < βcβ β β {R : β}, βcβ < R β Β¬FiniteDimensional π E β β (s : Finset E), β x, βxβ β€ R β§ β y β s, 1 β€ βy - xβ
This theorem states that in an infinite dimensional space over a nontrivially normed field, given any finite set of points and a vector with norm greater than one but less than some real number R, we can always find a point with norm less than or equal to R that is at least unit distance away from all the points in the given set. Note that this theorem does not hold if the space is finite-dimensional.
More concisely: In an infinite-dimensional, normed space over a nontrivially valued field, given any finite set of points and a vector with norm strictly between 1 and some real number R, there exists a point with norm <= R that is at least 1 unit away from all points in the set.
|
HasCompactSupport.eq_zero_or_finiteDimensional
theorem HasCompactSupport.eq_zero_or_finiteDimensional :
β (π : Type u) [inst : NontriviallyNormedField π] {E : Type v} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] [inst_3 : CompleteSpace π] {X : Type u_1} [inst_4 : TopologicalSpace X]
[inst_5 : Zero X] [inst_6 : T1Space X] {f : E β X},
HasCompactSupport f β Continuous f β f = 0 β¨ FiniteDimensional π E
This theorem states that if a function, `f`, has compact support, meaning the closure of the set of points where `f` is non-zero is a compact set, then one of two conditions must hold. Either the function `f` is the zero function (it equals to zero for all inputs), or the vector space `E` over the field `π` is finite-dimensional. This theorem assumes that `π` is a non-trivially normed field, `E` is a normed additive commutative group with a `π`-vector space structure, the space `π` is complete, `X` is a topological space with a zero element, `X` is a T1 space, and the function `f` is continuous.
More concisely: If `f` is a continuous function from a T1 topological space `X` to a finite-dimensional normed vector space `E` over a complete, non-trivially normed field `π` with compact support, then `f` is the zero function or `E` is finite-dimensional.
|
IsCompact.exists_mem_frontier_infDist_compl_eq_dist
theorem IsCompact.exists_mem_frontier_infDist_compl_eq_dist :
β {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace β E] [inst_2 : Nontrivial E] {x : E}
{K : Set E}, IsCompact K β x β K β β y β frontier K, Metric.infDist x KαΆ = dist x y
The theorem `IsCompact.exists_mem_frontier_infDist_compl_eq_dist` states that, for a compact set `K` in a nontrivial real normed space, if a point `x` belongs to `K`, then there exists a point `y` on the boundary of `K` such that the minimum distance from `x` to the complement of `K` is equal to the distance from `x` to `y`. In other words, the closest point to `x` outside of `K` is on the boundary of `K`.
More concisely: For a compact set K in a nontrivial real normed space, if x is an element of K, then there exists a boundary point y of K such that the distance from x to y equals the minimum distance from x to K^c.
|
Basis.exists_op_norm_le
theorem Basis.exists_op_norm_le :
β {π : Type u} [inst : NontriviallyNormedField π] {E : Type v} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type w} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F]
[inst_5 : CompleteSpace π] {ΞΉ : Type u_1} [inst_6 : Finite ΞΉ] (v : Basis ΞΉ π E),
β C > 0, β {u : E βL[π] F} {M : β}, 0 β€ M β (β (i : ΞΉ), βu (v i)β β€ M) β βuβ β€ C * M
This theorem, known as `Basis.exists_op_norm_le`, asserts that for a given basis `v` of a normed vector space `E` over a nontrivially normed field `π`, there exists some positive constant `C` such that for every bounded linear map `u` from `E` to another normed space `F` over `π`, and every nonnegative real number `M` satisfying the condition that the norm of `u` applied to each basis vector `v i` is less than or equal to `M`, the norm of `u` is less than or equal to `C * M`. This theorem abstracts away the value of `C` and is a weaker version of `Basis.opNorm_le`.
More concisely: For any bounded linear map between normed vector spaces over a nontrivially normed field and any basis of the domain, there exists a constant such that the map's norm is less than or equal to the constant times the supremum of its norms applied to the basis vectors.
|
Summable.norm
theorem Summable.norm :
β {Ξ± : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace β E]
[inst_2 : FiniteDimensional β E] {f : Ξ± β E}, Summable f β Summable fun x => βf xβ
This theorem, named `Summable.norm`, states that in a finite-dimensional vector space over the real numbers (`β`), a series whose terms are the norm of the function `f(x)`, denoted as `β x, βf xβ`, is unconditionally summable if and only if the series whose terms are the function `f(x)` itself, denoted as `β x, f x`, is unconditionally summable. It is important to note that one implication of this theorem is valid in any complete normed space, while the other implication is only valid in finite-dimensional spaces.
More concisely: In a finite-dimensional real vector space, the unconditional summability of series of the functions' norms is equivalent to the unconditional summability of the functions themselves.
|
FiniteDimensional.of_locallyCompactSpace
theorem FiniteDimensional.of_locallyCompactSpace :
β (π : Type u) [inst : NontriviallyNormedField π] {E : Type v} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] [inst_3 : CompleteSpace π] [inst_4 : LocallyCompactSpace E], FiniteDimensional π E
**Riesz's theorem**: This theorem states that any locally compact normed vector space is also a finite-dimensional vector space. Specifically, given any type `π` which forms a non-trivially normed field and a type `E` which forms a normed additively commutative group and a normed space over `π`, if `π` is a complete space and `E` is a locally compact space, then `E` is a finite-dimensional vector space over `π`.
More concisely: Any locally compact, normed vector space over a complete, non-trivially normed field is finite-dimensional.
|
ProperSpace.of_locallyCompactSpace
theorem ProperSpace.of_locallyCompactSpace :
β (π : Type u_1) [inst : NontriviallyNormedField π] {E : Type u_2} [inst_1 : SeminormedAddCommGroup E]
[inst : NormedSpace π E] [inst : LocallyCompactSpace E], ProperSpace E
This theorem states that a locally compact normed vector space is proper. Specifically, for any nontrivial normed field `π` and any type `E` that forms a seminormed additive commutative group as well as a normed space over `π` and is locally compact, `E` is a proper space. In mathematics, a proper space is a space where every closed ball is compact. This theorem thus connects the notions of local compactness and properness in the context of vector spaces.
More concisely: A locally compact normed vector space is a proper space, i.e., every closed ball is compact.
|
finiteDimensional_of_locallyCompactSpace
theorem finiteDimensional_of_locallyCompactSpace :
β (π : Type u) [inst : NontriviallyNormedField π] {E : Type v} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] [inst_3 : CompleteSpace π] [inst_4 : LocallyCompactSpace E], FiniteDimensional π E
**Riesz's Theorem**: For any type `π` that is a non-trivially normed field, and any type `E` that is a normed additive commutative group, which is also a normed space over `π` and a locally compact space, it is stated that the space `E` is a finite-dimensional vector space over the field `π`. In other words, a vector space that is locally compact and equipped with a norm is necessarily finite-dimensional. This theorem is also known as an alias of `FiniteDimensional.of_locallyCompactSpace`.
More concisely: A locally compact, normed additive commutative group that is also a normed vector space over a non-trivially normed field is finite-dimensional.
|
continuousOn_clm_apply
theorem continuousOn_clm_apply :
β {π : Type u} [inst : NontriviallyNormedField π] {E : Type v} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type w} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F]
[inst_5 : CompleteSpace π] {X : Type u_1} [inst_6 : TopologicalSpace X] [inst_7 : FiniteDimensional π E]
{f : X β E βL[π] F} {s : Set X}, ContinuousOn f s β β (y : E), ContinuousOn (fun x => (f x) y) s
The theorem `continuousOn_clm_apply` states that a family of continuous linear maps, denoted by f, is continuous on a set s in a topological space X if and only if all of its applications are continuous on s. Here, the linear maps are from a normed vector space E over the scalar field π to another normed vector space F over the same scalar field. The space E is assumed to be finite-dimensional, and the scalar field is assumed to be a nontrivially normed field with complete metric space. In simpler terms, this theorem is establishing a condition for the continuity of a family of continuous linear maps on a particular set.
More concisely: A family of continuous linear maps from a finite-dimensional normed vector space to another normed vector space over a complete, nontrivially normed field is continuous on a set if and only if all of its applications are continuous on that set.
|
exists_seq_norm_le_one_le_norm_sub'
theorem exists_seq_norm_le_one_le_norm_sub' :
β {π : Type u} [inst : NontriviallyNormedField π] {E : Type v} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] [inst_3 : CompleteSpace π] {c : π},
1 < βcβ β
β {R : β},
βcβ < R β Β¬FiniteDimensional π E β β f, (β (n : β), βf nβ β€ R) β§ Pairwise fun m n => 1 β€ βf m - f nβ
In any infinite-dimensional normed space over a nontrivially normed field, given a point `c` in the field where the norm of `c` is strictly greater than 1 and strictly less than a real number `R`, there exists a sequence of points `f` such that, for every natural number `n`, the norm of `f n` is at most `R` and for every pair of distinct natural numbers `m` and `n`, the norm of the difference between `f m` and `f n` is at least 1. This is a version of the theorem with assumptions on `c` and `R`. There's another version of this theorem, `exists_seq_norm_le_one_le_norm_sub`, which doesn't make these assumptions.
More concisely: In an infinite-dimensional normed space over a nontrivially normed field, there exists a sequence of points with norms less than a given real number and pairwise norm-distance greater than 1.
|
summable_norm_iff
theorem summable_norm_iff :
β {Ξ± : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace β E]
[inst_2 : FiniteDimensional β E] {f : Ξ± β E}, (Summable fun x => βf xβ) β Summable f
The theorem `summable_norm_iff` states that in a finite-dimensional vector space over the real numbers β, a series denoted by `β x, βf xβ` (the sum of the norms of `f(x)`) is unconditionally summable if and only if the series `β x, f x` (the sum of `f(x)`) is unconditionally summable. This means that the convergence of the series doesn't depend on the order of summation. The theorem tells us that one direction of this implication holds in any complete normed space, while the other direction is specific to finite-dimensional spaces.
More concisely: In a finite-dimensional real vector space, a series of norms is unconditionally summable if and only if the original series is.
|
properSpace_of_locallyCompactSpace
theorem properSpace_of_locallyCompactSpace :
β (π : Type u_1) [inst : NontriviallyNormedField π] {E : Type u_2} [inst_1 : SeminormedAddCommGroup E]
[inst : NormedSpace π E] [inst : LocallyCompactSpace E], ProperSpace E
This theorem is an alias of `ProperSpace.of_locallyCompactSpace` and it states that a locally compact normed vector space is a proper space. Specifically, for any nontrivially normed field `π` and any semi-normed additive commutative group `E` such that `E` is also a normed space over `π` and a locally compact space, then `E` is a proper space.
More concisely: A locally compact normed vector space is a proper space.
|
FiniteDimensional.of_isCompact_closedBallβ
theorem FiniteDimensional.of_isCompact_closedBallβ :
β (π : Type u) [inst : NontriviallyNormedField π] {E : Type v} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] [inst_3 : CompleteSpace π] {r : β},
0 < r β IsCompact (Metric.closedBall 0 r) β FiniteDimensional π E
**Riesz's theorem**: For any nontrivially normed field `π` and any normed additive commutative group `E` that is also a normed space over `π` and is complete with respect to `π`, if there exists a positive real number `r` such that the closed ball in `E` with center at zero and radius `r` is a compact set, then `E` is a finite-dimensional vector space over `π`. In other words, this theorem states that compactness of a closed ball in a vector space implies finiteness of the dimension of the vector space.
More concisely: If a complete, normed vector space over a nontrivially normed field with a compact closed ball has finite radius, then the space is finite-dimensional.
|
FiniteDimensional.proper
theorem FiniteDimensional.proper :
β (π : Type u) [inst : NontriviallyNormedField π] (E : Type v) [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] [inst_3 : LocallyCompactSpace π] [inst : FiniteDimensional π E], ProperSpace E
The theorem `FiniteDimensional.proper` states that any finite-dimensional vector space over a locally compact field is a proper space. This means that for any vector space `E` over a field `π` where `π` is a non-trivially normed field and a locally compact space, and `E` is a normed add commutative group as well as a normed space over `π`, if the vector space `E` is also finite-dimensional over `π`, then `E` has the property of being a proper space. This theorem is not registered as an instance to prevent instance loops when attempting to prove the properness of `π`, and the search for `π` as an unknown metavariable. The instance needs to be declared explicitly when it is necessary.
More concisely: A finite-dimensional vector space over a locally compact, non-trivially normed field is a proper space.
|
HasCompactMulSupport.eq_one_or_finiteDimensional
theorem HasCompactMulSupport.eq_one_or_finiteDimensional :
β (π : Type u) [inst : NontriviallyNormedField π] {E : Type v} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] [inst_3 : CompleteSpace π] {X : Type u_1} [inst_4 : TopologicalSpace X]
[inst_5 : One X] [inst_6 : T1Space X] {f : E β X},
HasCompactMulSupport f β Continuous f β f = 1 β¨ FiniteDimensional π E
The theorem states that for any non-trivially normed field `π`, normed addition commutative group `E`, and any type `X` with a topological space structure, `One X` structure, and `T1Space X` structure, if a function `f` from `E` to `X` has compact multiplicative support and is continuous, then either the function `f` is the constant function 1 (i.e., `f = 1`), or `E`, the domain of `f`, is a finite-dimensional vector space over `π`. In a nutshell, this theorem puts constraints on the function and the domain space given the condition of having compact multiplicative support.
More concisely: If `f` is a continuous function from a normed additive commutative group `E` (over a non-trivially normed field) to a T1 topological space `X` with a One structure, having compact multiplicative support, then `f` is constant or `E` is finite-dimensional.
|
properSpace_of_locallyCompact_module
theorem properSpace_of_locallyCompact_module :
β (π : Type u) [inst : NontriviallyNormedField π] (E : Type v) [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] [inst_3 : CompleteSpace π] [inst_4 : Nontrivial E] [inst_5 : LocallyCompactSpace E],
ProperSpace π
This theorem, named `properSpace_of_locallyCompact_module`, states that for any type π that has a non-trivial normed field structure, any type E that is a normed add commutative group, is a normed space over π, is complete, is non-trivial, and is locally compact, the type π is a proper space. In other words, if we have a locally compact module over a non-trivially normed field, then the field is a proper space. A "proper space" in this context means that every closed ball is compact.
More concisely: If E is a locally compact, normed add commutative group over a non-trivially normed field π, then π is a properly dense, complete metric space. (Equivalently, every closed ball in π is compact.)
|
finiteDimensional_of_isCompact_closedBallβ
theorem finiteDimensional_of_isCompact_closedBallβ :
β (π : Type u) [inst : NontriviallyNormedField π] {E : Type v} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] [inst_3 : CompleteSpace π] {r : β},
0 < r β IsCompact (Metric.closedBall 0 r) β FiniteDimensional π E
**Riesz's Theorem**: For any nonzero normed field `π` and normed additively commutative group `E` (which forms a normed vector space over `π`), and for any positive real number `r`, if the closed ball of radius `r` centered at zero is a compact set (in the topological sense that, for any nontrivial filter `f` containing this ball, there exists a point `a` in the ball such that every set of `f` meets every neighborhood of `a`), then this vector space `E` is finite-dimensional (meaning it is a finite module over the field `π`). This theorem also assumes `π` is a complete space, meaning every Cauchy sequence in `π` converges to a limit in `π`.
More concisely: If a normed vector space over a complete, nonzero normed field with a compact closed ball of positive radius around the origin is a topologically compact Hausdorff space, then it is finite-dimensional.
|
exists_mem_frontier_infDist_compl_eq_dist
theorem exists_mem_frontier_infDist_compl_eq_dist :
β {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace β E] [inst_2 : FiniteDimensional β E] {x : E}
{s : Set E}, x β s β s β Set.univ β β y β frontier s, Metric.infDist x sαΆ = dist x y
The theorem `exists_mem_frontier_infDist_compl_eq_dist` states that for any finite dimensional normed real vector space `E`, given a point `x` in `E` and a neighborhood `s` of `x` that is not equal to the entire space, there exists a point `y` on the frontier of `s` such that the infimum distance from `x` to the complement of `s` is equal to the distance from `x` to `y`. In other words, there is a point on the boundary of the neighborhood whose distance from `x` is the smallest possible distance from `x` to any point outside the neighborhood.
More concisely: For any finite dimensional normed real vector space, given a point and a neighborhood that is not the entire space, there exists a boundary point with minimal distance to the complement.
|
Basis.exists_op_nnnorm_le
theorem Basis.exists_op_nnnorm_le :
β {π : Type u} [inst : NontriviallyNormedField π] {E : Type v} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type w} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F]
[inst_5 : CompleteSpace π] {ΞΉ : Type u_1} [inst_6 : Finite ΞΉ] (v : Basis ΞΉ π E),
β C > 0, β {u : E βL[π] F} (M : NNReal), (β (i : ΞΉ), βu (v i)ββ β€ M) β βuββ β€ C * M
This theorem, named `Basis.exists_op_nnnorm_le`, asserts that for any nontrivially normed field `π`, normed additive commutative groups `E` and `F` over `π`, such that `π` is a complete space, and any finite set `ΞΉ`, given a basis `v` for `E` over `π`, there exists a positive real number `C` such that for any bounded linear function `u` from `E` to `F` and any nonnegative real number `M` satisfying the condition that the semi-norm of `u` applied to each basis vector is less than or equal to `M`, the semi-norm of `u` itself is less than or equal to `C` times `M`. In other words, there is an upper bound, proportional to `M`, on the norm of any linear map from `E` to `F` when applied to the basis vectors of `E`.
More concisely: Given a complete, nontrivially normed field `π`, normed additive commutative groups `E` and `F` over `π`, a finite set `ΞΉ`, and a basis `v` for `E` over `π`, there exists a constant `C` such that for any bounded linear map `u` from `E` to `F` and real number `M` satisfying `β₯u(v_i)β₯ β€ M` for all `i β ΞΉ`, it holds that `β₯uβ₯ β€ C Γ M`.
|
LipschitzOnWith.extend_finite_dimension
theorem LipschitzOnWith.extend_finite_dimension :
β {Ξ± : Type u_1} [inst : PseudoMetricSpace Ξ±] {E' : Type u_2} [inst_1 : NormedAddCommGroup E']
[inst_2 : NormedSpace β E'] [inst_3 : FiniteDimensional β E'] {s : Set Ξ±} {f : Ξ± β E'} {K : NNReal},
LipschitzOnWith K f s β β g, LipschitzWith (lipschitzExtensionConstant E' * K) g β§ Set.EqOn f g s
This theorem states that any function `f` that is `K`-Lipschitz continuous on a subset `s` of a pseudometric space `Ξ±`, mapping into a finite-dimensional real vector space `E'`, can be extended to a function `g` that is Lipschitz continuous on the entire space `Ξ±`. The Lipschitz constant for `g` is `lipschitzExtensionConstant E' * K`, which may be slightly larger than `K`. The functions `f` and `g` are equal on the subset `s`.
In other words, `f` can be smoothly extended beyond the subset `s` while retaining its Lipschitz continuity, albeit with a potentially larger Lipschitz constant.
More concisely: Given a `K`-Lipschitz continuous function `f` on a subset `s` of a pseudometric space `Ξ±` mapping into a finite-dimensional real vector space `E'`, there exists an extension `g` of `f` to all of `Ξ±` that is Lipschitz continuous with constant `lipschitzExtensionConstant E' * K`.
|
finiteDimensional_of_isCompact_closedBall
theorem finiteDimensional_of_isCompact_closedBall :
β (π : Type u) [inst : NontriviallyNormedField π] {E : Type v} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] [inst_3 : CompleteSpace π] {r : β},
0 < r β β {c : E}, IsCompact (Metric.closedBall c r) β FiniteDimensional π E
**Riesz's theorem**: Given a nontrivially normed field `π` and a normed additive commutative group `E` where `E` is a normed space over `π`, and `π` is a complete space, the theorem asserts that if there exists a closed ball of positive radius `r` in `E` which is compact, then the vector space `E` is finite-dimensional. In other words, compactness of a closed ball in the vector space implies the finite-dimensionality of the space.
More concisely: If a normed space over a complete nontrivially normed field has a compact closed ball of positive radius, then the space is finite-dimensional.
|