ContinuousLinearMap.is_weak_closed_closedBall
theorem ContinuousLinearMap.is_weak_closed_closedBall :
∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {F : Type u_6} [inst : NormedAddCommGroup F] [inst_1 : NontriviallyNormedField 𝕜]
[inst_2 : NontriviallyNormedField 𝕜₂] [inst_3 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} {E' : Type u_11}
[inst_4 : SeminormedAddCommGroup E'] [inst_5 : NormedSpace 𝕜 E'] [inst_6 : RingHomIsometric σ₁₂]
(f₀ : E' →SL[σ₁₂] F) (r : ℝ) ⦃f : E' →SL[σ₁₂] F⦄,
⇑f ∈ closure (DFunLike.coe '' Metric.closedBall f₀ r) → f ∈ Metric.closedBall f₀ r
This theorem states that a closed ball is closed in the weak-* topology. Specifically, for any normed additive commutative group `F`, any nontrivially normed fields `𝕜` and `𝕜₂`, a normed space over `𝕜₂` with type `F`, a seminormed additive commutative group `E'`, a normed space over `𝕜` with type `E'`, a ring homomorphism `σ₁₂` that is isometric, a continuous linear map `f₀` from `E'` to `F` under the ring homomorphism `σ₁₂`, and a real number `r`, if a function `f` is within the closure of the image of the function `DFunLike.coe` applied to the closed ball around `f₀` with radius `r`, then `f` is in the closed ball around `f₀` with radius `r` itself. In other words, the weak-* topology preserves the "closeness" of elements in a closed ball.
More concisely: In a normed additive commutative group `F` over a nontrivially normed field `𝕜₂`, a seminormed additive commutative group `E'` over a normed field `𝕜`, and for a ring homomorphism `σ₁₂` that is isometric, a continuous linear map `f₀` from `E'` to `F`, and real number `r`, the weak-* closed ball around `f₀` with radius `r` is closed under the weak-* topology, meaning that any function `f` in the closure of this ball belongs to the ball itself.
|
ContinuousLinearMap.isCompact_image_coe_closedBall
theorem ContinuousLinearMap.isCompact_image_coe_closedBall :
∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_6} [inst : NormedAddCommGroup E]
[inst_1 : NormedAddCommGroup F] [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
[inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [inst_6 : RingHomIsometric σ₁₂]
[inst_7 : ProperSpace F] (f₀ : E →SL[σ₁₂] F) (r : ℝ), IsCompact (DFunLike.coe '' Metric.closedBall f₀ r)
The Banach-Alaoglu theorem states that for any two normed additive commutative groups `E` and `F`, any two non-trivially normed fields `𝕜` and `𝕜₂`, a continuous linear map `f₀ : E →SL[σ₁₂] F`, a ring homomorphism `σ₁₂ : 𝕜 →+* 𝕜₂`, and a real number `r`, the set of functions `f : E → F` that represent continuous linear maps at a distance `≤ r` from `f₀` is compact in the topology of pointwise convergence. Here, compactness is defined as: for every nontrivial filter `f` that contains the set, there exists an element `a` in the set such that every set of `f` meets every neighborhood of `a`. The distance is calculated using the metric defined by the `dist` function. Other versions of this theorem can be found in `Analysis.NormedSpace.WeakDual`.
More concisely: The Banach-Alaoglu theorem states that the set of continuous linear maps from a normed space to another, with norm less than or equal to a given constant, forms a compact subset in the topology of pointwise convergence.
|
ContinuousLinearMap.tendsto_of_tendsto_pointwise_of_cauchySeq
theorem ContinuousLinearMap.tendsto_of_tendsto_pointwise_of_cauchySeq :
∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {F : Type u_6} [inst : NormedAddCommGroup F] [inst_1 : NontriviallyNormedField 𝕜]
[inst_2 : NontriviallyNormedField 𝕜₂] [inst_3 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} {E' : Type u_11}
[inst_4 : SeminormedAddCommGroup E'] [inst_5 : NormedSpace 𝕜 E'] [inst_6 : RingHomIsometric σ₁₂]
{f : ℕ → E' →SL[σ₁₂] F} {g : E' →SL[σ₁₂] F},
Filter.Tendsto (fun n x => (f n) x) Filter.atTop (nhds ⇑g) →
CauchySeq f → Filter.Tendsto f Filter.atTop (nhds g)
This theorem states that if a Cauchy sequence of continuous linear maps converges pointwise to a continuous linear map, then it also converges to the same map in norm. More formally, given a sequence `f` of continuous linear maps from space `E'` to `F`, and another continuous linear map `g` from `E'` to `F`, if for all `n` in `ℕ` and `x` in `E'` the sequence `f n x` tends to `g x` (meaning the function `f` applied to `n` and `x` approaches `g` applied to `x` as `n` tends to infinity), and `f` is a Cauchy sequence, then the sequence `f` tends to `g` (meaning the sequence of maps `f` approaches the map `g` as `n` tends to infinity). This result is important in demonstrating that the space of continuous linear maps is complete, provided that the codomain is a complete space.
More concisely: If a Cauchy sequence of continuous linear maps converges pointwise to a continuous linear map, then it converges to that map in the operator norm.
|
ContinuousLinearMap.isCompact_closure_image_coe_of_bounded
theorem ContinuousLinearMap.isCompact_closure_image_coe_of_bounded :
∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {F : Type u_6} [inst : NormedAddCommGroup F] [inst_1 : NontriviallyNormedField 𝕜]
[inst_2 : NontriviallyNormedField 𝕜₂] [inst_3 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} {E' : Type u_11}
[inst_4 : SeminormedAddCommGroup E'] [inst_5 : NormedSpace 𝕜 E'] [inst_6 : RingHomIsometric σ₁₂]
[inst_7 : ProperSpace F] {s : Set (E' →SL[σ₁₂] F)},
Bornology.IsBounded s → IsCompact (closure (DFunLike.coe '' s))
This theorem states that given a set `s` of continuous semi-linear maps from `E` to `F` with the property that `s` is bounded in the space of these maps, the closure of the image of `s` under the function-like coercion (which interprets `s` as a set of maps from `E` to `F` in the space with the topology of pointwise convergence) is a compact set. Here, `F` is a proper space, meaning it is a complete metric space in which every closed ball is compact. `𝕜` and `𝕜₂` are non-trivially normed fields, meaning that they are fields equipped with a norm such that there is a non-zero element with norm not equal to 1. `E'` is a semi-normed additively commutative group, and `σ₁₂` is an isometric ring homomorphism from `𝕜` to `𝕜₂`.
More concisely: Given a bounded set `s` of continuous semi-linear maps from a semi-normed additively commutative group `E` to a complete metric space `F` over non-trivially normed fields `𝕜` and `𝕜₂` with an isometric ring homomorphism `σ₁₂` from `𝕜` to `𝕜₂`, the closure of `s` under function-like coercion is a compact set.
|
ContinuousLinearMap.isClosed_image_coe_of_bounded_of_weak_closed
theorem ContinuousLinearMap.isClosed_image_coe_of_bounded_of_weak_closed :
∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {F : Type u_6} [inst : NormedAddCommGroup F] [inst_1 : NontriviallyNormedField 𝕜]
[inst_2 : NontriviallyNormedField 𝕜₂] [inst_3 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} {E' : Type u_11}
[inst_4 : SeminormedAddCommGroup E'] [inst_5 : NormedSpace 𝕜 E'] [inst_6 : RingHomIsometric σ₁₂]
{s : Set (E' →SL[σ₁₂] F)},
Bornology.IsBounded s →
(∀ (f : E' →SL[σ₁₂] F), ⇑f ∈ closure (DFunLike.coe '' s) → f ∈ s) → IsClosed (DFunLike.coe '' s)
This theorem states that given a set `s` of semilinear functions from `E'` to `F` (denoted as `E' →SL[σ₁₂] F`) over two nontrivially normed fields `𝕜` and `𝕜₂` with a ring homomorphism `σ₁₂` between them, if this set is bounded according to some bornology and is closed under the weak-* topology (that is, any limit point of the set under the weak-* topology is already in the set), then the image of `s` under the coercion to functions `E' → F` is a closed set. Here, a set is closed if its complement is open, and the weak-* topology is a particular kind of topology often used in functional analysis. The condition of closure in the weak-* topology is expressed in Lean as "every function `f` whose coerced function is in the closure of the coerced set `s` is itself in `s`".
More concisely: Given a set of semilinear functions from a nontrivially normed vector space over two fields with a ring homomorphism, if the set is bounded and closed under the weak-* topology, then its image under coercion is a closed set.
|
ContinuousLinearMap.isClosed_image_coe_closedBall
theorem ContinuousLinearMap.isClosed_image_coe_closedBall :
∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_6} [inst : NormedAddCommGroup E]
[inst_1 : NormedAddCommGroup F] [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
[inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [inst_6 : RingHomIsometric σ₁₂]
(f₀ : E →SL[σ₁₂] F) (r : ℝ), IsClosed (DFunLike.coe '' Metric.closedBall f₀ r)
This theorem states that for any two normed fields 𝕜 and 𝕜₂, types E and F with normed addition structures, a ring homomorphism (`σ₁₂`) between 𝕜 and 𝕜₂ which is also an isometry, a continuous linear map (`f₀`) from E to F, and a real number `r`, the set of all functions, which represent the continuous linear map (`E →SL[σ₁₂] F`), within distance `r` from `f₀`, is a closed set in the topology of pointwise convergence. This is a crucial step in the proof of the Banach-Alaoglu theorem. Here, the distance between functions is measured in a metric space sense, meaning that all functions in the set are at a distance less than or equal to `r` from `f₀`.
More concisely: Given normed fields 𝕜 and 𝕜₂, types E and F with normed additive structures, a ring homomorphism σ₁₂ between 𝕜 and 𝕜₂ that is an isometry, a continuous linear map f₀ from E to F, and a real number r, the set of all continuous linear maps from E to F with distance less than or equal to r from f₀ (in the topology of pointwise convergence) is a closed set.
|
ContinuousLinearMap.isCompact_image_coe_of_bounded_of_weak_closed
theorem ContinuousLinearMap.isCompact_image_coe_of_bounded_of_weak_closed :
∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {F : Type u_6} [inst : NormedAddCommGroup F] [inst_1 : NontriviallyNormedField 𝕜]
[inst_2 : NontriviallyNormedField 𝕜₂] [inst_3 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} {E' : Type u_11}
[inst_4 : SeminormedAddCommGroup E'] [inst_5 : NormedSpace 𝕜 E'] [inst_6 : RingHomIsometric σ₁₂]
[inst_7 : ProperSpace F] {s : Set (E' →SL[σ₁₂] F)},
Bornology.IsBounded s →
(∀ (f : E' →SL[σ₁₂] F), ⇑f ∈ closure (DFunLike.coe '' s) → f ∈ s) → IsCompact (DFunLike.coe '' s)
This theorem states that given a set `s` of semilinear functions from `E'` to `F` (specified by the type `E' →SL[σ₁₂] F`), if `s` is bounded (according to the definition of `Bornology.IsBounded`), and if it is closed in the weak-* topology (expressed in the condition `∀ (f : E' →SL[σ₁₂] F), ⇑f ∈ closure (DFunLike.coe '' s) → f ∈ s`), then the image of `s` under the coercion to functions from `E'` to `F` (indicated by `DFunLike.coe '' s`) is a compact set (according to the definition of `IsCompact`).
In other words, the theorem provides a sufficient condition for the compactness of the image set of a bounded and weak-* closed set of semilinear functions when these functions are considered as mappings from `E'` to `F`. The compactness here is in the sense of the standard topological definition, involving filters.
More concisely: If `s` is a bounded and weak-* closed set of semilinear functions from `E'` to `F`, then the image of `s` under the coercion to functions from `E'` to `F` is a compact set.
|
ContinuousLinearMap.isCompact_image_coe_of_bounded_of_closed_image
theorem ContinuousLinearMap.isCompact_image_coe_of_bounded_of_closed_image :
∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {F : Type u_6} [inst : NormedAddCommGroup F] [inst_1 : NontriviallyNormedField 𝕜]
[inst_2 : NontriviallyNormedField 𝕜₂] [inst_3 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} {E' : Type u_11}
[inst_4 : SeminormedAddCommGroup E'] [inst_5 : NormedSpace 𝕜 E'] [inst_6 : RingHomIsometric σ₁₂]
[inst_7 : ProperSpace F] {s : Set (E' →SL[σ₁₂] F)},
Bornology.IsBounded s → IsClosed (DFunLike.coe '' s) → IsCompact (DFunLike.coe '' s)
This theorem states that given a bounded set `s` in the space of continuous semilinear maps from `E` to `F` (`E →SL[σ] F`), where `F` is a proper space, if `s` is interpreted as a set in the space of maps from `E` to `F` and has the topology of pointwise convergence and is closed, then `s` is compact. This involves the notion of boundedness in a bornology, the condition of being closed, and the property of being compact. The theorem suggests a future reformulation in terms of a type synonym with the appropriate topology.
More concisely: A bounded, closed set of continuous semilinear maps from a space `E` to `F` (`E →SL[σ] F`), where `F` is a proper space, is compact in the topology of pointwise convergence.
|