LeanAide documentation

LeanAide GPT-4 documentation

Module: Mathlib.Analysis.NormedSpace.WeakDual

`WeakDual.isCompact_closedBall` theorem WeakDual.isCompact_closedBall : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : ProperSpace 𝕜] (x' : NormedSpace.Dual 𝕜 E) (r : ℝ), IsCompact (⇑WeakDual.toNormedDual ⁻¹' Metric.closedBall x' r) The theorem Banach-Alaoglu theorem states that for any nontrivially normed field `𝕜`, any seminormed additive commutative group `E`, and any normed space over `𝕜` and `E`, assuming that `𝕜` is a proper space, a closed ball in the dual of `E` is compact in the weak-star topology. More specifically, given any element `x'` of the dual space and any real number `r`, the preimage of the closed ball with center `x'` and radius `r` under the canonical mapping from the weak dual to the normed dual is a compact set. More concisely: The closed unit ball in the dual space of a normed vector space, with respect to the weak-star topology, is compact.
`WeakDual.isClosed_image_coe_of_bounded_of_closed` theorem WeakDual.isClosed_image_coe_of_bounded_of_closed : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {s : Set (WeakDual 𝕜 E)}, Bornology.IsBounded (⇑NormedSpace.Dual.toWeakDual ⁻¹' s) → IsClosed s → IsClosed (DFunLike.coe '' s) This theorem states that for any non-trivially normed field `𝕜` and any seminormed add commutative group `E` that is also a normed space over `𝕜`, if `s` is a set of the weak dual of `𝕜` and `E` that is bounded and closed, then the image of `s` under the coercion function from the weak dual to the function from `E` to `𝕜` is also a closed set. In simpler terms, while the function that coverts elements of the weak dual space (which are linear functionals) to functions from `E` to `𝕜` may not always preserve the property of being a closed set, if the set it is acting on is both bounded and closed, then the output set will be closed as well. More concisely: If `s` is a bounded and closed subset of the weak dual of a non-trivially normed field and a seminormed add commutative group that is also a normed space over the field, then the image of `s` under the coercion function is a closed subset of the functions from the group to the field.
`WeakDual.isClosed_polar` theorem WeakDual.isClosed_polar : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] (s : Set E), IsClosed (WeakDual.polar 𝕜 s) This theorem states that the polar of a set `s` (denoted as `polar 𝕜 s`), when considered as a subset of the dual space of `E` with the weak-star topology, is a closed set. Here, `𝕜` is a non-trivially normed field and `E` is a seminormed additively commutative group that also is a normed space over `𝕜`. The polar of a set in this context is defined using the concept of polar sets in the dual of a normed space. More concisely: The polar of a set in a seminormed additively commutative group and normed space over a non-trivially normed field, considered as a subset of the dual space with the weak-star topology, is a closed set.
`NormedSpace.Dual.dual_norm_topology_le_weak_dual_topology` theorem NormedSpace.Dual.dual_norm_topology_le_weak_dual_topology : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E], UniformSpace.toTopologicalSpace ≤ WeakDual.instTopologicalSpace The theorem `NormedSpace.Dual.dual_norm_topology_le_weak_dual_topology` states that for any nontrivially normed field 𝕜 and any seminormed additive commutative group E that is also a normed space over 𝕜, the topology generated by the uniform structure (or the dual-norm topology) on the dual space of E is coarser than or equal to the weak-star topology on the dual space of E. In other words, in this context, "coarser than" means that the weak-star topology has fewer open sets or the same number of open sets as the dual-norm topology. More concisely: The dual-norm topology on a normed space's dual is coarser than or equal to the weak-star topology.
`WeakDual.isCompact_polar` theorem WeakDual.isCompact_polar : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : ProperSpace 𝕜] {s : Set E}, s ∈ nhds 0 → IsCompact (WeakDual.polar 𝕜 s) The Banach-Alaoglu theorem states that for any normed space `E` over a nontrivially normed field `𝕜`, and for any neighborhood `s` of the origin in `E`, the polar set of `s` is a compact subset in the weak dual of `E`. Here, the polar set of `s` is defined as the preimage under the mapping to the normed dual of the polar set of `s` in `𝕜`. A set is said to be compact if, for every nontrivial filter that contains the set, there exists an element in the set such that every set of the filter intersects every neighborhood of that element. The neighborhood of a point in a topological space is defined as a set that contains an open set around that point. More concisely: The Banach-Alaoglu theorem asserts that for any normed space and any neighborhood of the origin, the polar set in the weak dual is a compact subset.
`WeakDual.isClosed_image_polar_of_mem_nhds` theorem WeakDual.isClosed_image_polar_of_mem_nhds : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {s : Set E}, s ∈ nhds 0 → IsClosed (DFunLike.coe '' WeakDual.polar 𝕜 s) This theorem states that for any nontrivially normed field `𝕜` and any seminormed add commutative group `E` that is also a normed space over `𝕜`, if `s` is a set in the neighborhood of the origin, then the image of the polar `WeakDual.polar 𝕜 s` under the function `DFunLike.coe` (which coerces the polar to a function) is a closed set. Essentially, it ensures that in this mathematical structure, a specific transformation of a neighborhood set of the origin results in a closed set. More concisely: Given a nontrivially normed field `𝕜` and a seminormed add commutative group `E` that is also a normed space over `𝕜`, the polar of any neighborhood `s` of the origin in `E` under `WeakDual.polar 𝕜` is a closed set when regarded as a function using `DFunLike.coe`.
`NormedSpace.Dual.isClosed_image_polar_of_mem_nhds` theorem NormedSpace.Dual.isClosed_image_polar_of_mem_nhds : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {s : Set E}, s ∈ nhds 0 → IsClosed (DFunLike.coe '' NormedSpace.polar 𝕜 s) The theorem `NormedSpace.Dual.isClosed_image_polar_of_mem_nhds` states that for any nontrivially normed field `𝕜`, any seminormed add-commutative group `E`, and any neighborhood `s` of the origin in `E` (that is, a set `s` that contains an open set around the origin), the image under the embedding from `NormedSpace.Dual 𝕜 E` to `(E → 𝕜)` of the polar of `s` is a closed set. Here, the polar of `s` is the set of all functionals in `NormedSpace.Dual 𝕜 E` that evaluate to something of norm at most one at all points in `s`. More concisely: The image under the embedding of the polar of a neighborhood of the origin in a seminormed add-commutative group with respect to a nontrivially normed field is a closed set in the dual space.