Operators on complete normed spaces #
This file contains statements about norms of operators on complete normed spaces, such as a
version of the Banach-Alaoglu theorem (ContinuousLinearMap.isCompact_image_coe_closedBall).
Construct a bundled continuous (semi)linear map from a map f : E โ F and a proof of the fact
that it belongs to the closure of the image of a bounded set s : Set (E โSL[ฯโโ] F) under coercion
to function. Coercion to function of the result is definitionally equal to f.
Equations
- ContinuousLinearMap.ofMemClosureImageCoeBounded f hs hf = (linearMapOfMemClosureRangeCoe f โฏ).mkContinuousOfExistsBound โฏ
Instances For
Let f : E โ F be a map, let g : ฮฑ โ E โSL[ฯโโ] F be a family of continuous (semi)linear maps
that takes values in a bounded set and converges to f pointwise along a nontrivial filter. Then
f is a continuous (semi)linear map.
Equations
Instances For
If a Cauchy sequence of continuous linear map converges to a continuous linear map pointwise, then it converges to the same map in norm. This lemma is used to prove that the space of continuous linear maps is complete provided that the codomain is a complete space.
If the target space is complete, the space of continuous linear maps with its norm is also complete. This works also if the source space is seminormed.
Equations
- โฏ = โฏ
Let s be a bounded set in the space of continuous (semi)linear maps E โSL[ฯ] F taking values
in a proper space. Then s interpreted as a set in the space of maps E โ F with topology of
pointwise convergence is precompact: its closure is a compact set.
Let s be a bounded set in the space of continuous (semi)linear maps E โSL[ฯ] F taking values
in a proper space. If s interpreted as a set in the space of maps E โ F with topology of
pointwise convergence is closed, then it is compact.
TODO: reformulate this in terms of a type synonym with the right topology.
If a set s of semilinear functions is bounded and is closed in the weak-* topology, then its
image under coercion to functions E โ F is a closed set. We don't have a name for E โSL[ฯ] F
with weak-* topology in mathlib, so we use an equivalent condition (see isClosed_induced_iff').
TODO: reformulate this in terms of a type synonym with the right topology.
If a set s of semilinear functions is bounded and is closed in the weak-* topology, then its
image under coercion to functions E โ F is a compact set. We don't have a name for E โSL[ฯ] F
with weak-* topology in mathlib, so we use an equivalent condition (see isClosed_induced_iff').
A closed ball is closed in the weak-* topology. We don't have a name for E โSL[ฯ] F with
weak-* topology in mathlib, so we use an equivalent condition (see isClosed_induced_iff').
The set of functions f : E โ F that represent continuous linear maps f : E โSL[ฯโโ] F
at distance โค r from fโ : E โSL[ฯโโ] F is closed in the topology of pointwise convergence.
This is one of the key steps in the proof of the Banach-Alaoglu theorem.
Banach-Alaoglu theorem. The set of functions f : E โ F that represent continuous linear
maps f : E โSL[ฯโโ] F at distance โค r from fโ : E โSL[ฯโโ] F is compact in the topology of
pointwise convergence. Other versions of this theorem can be found in
Analysis.Normed.Module.WeakDual.
Extension of a continuous linear map f : E โSL[ฯโโ] F, with E a normed space and F a
complete normed space, along a uniform and dense embedding e : E โL[๐] Fโ.
Equations
- f.extend e h_dense h_e = let_fun cont := โฏ; let_fun eq := โฏ; { toFun := โฏ.extend โf, map_add' := โฏ, map_smul' := โฏ, cont := cont }
Instances For
If a dense embedding e : E โL[๐] G expands the norm by a constant factor Nโปยน, then the
norm of the extension of f along e is bounded by N * โfโ.
Alias of ContinuousLinearMap.opNorm_extend_le.
If a dense embedding e : E โL[๐] G expands the norm by a constant factor Nโปยน, then the
norm of the extension of f along e is bounded by N * โfโ.