# 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).

noncomputable def ContinuousLinearMap.ofMemClosureImageCoeBounded {๐ : Type u_1} {๐โ : Type u_2} {F : Type u_6} [] [NontriviallyNormedField ๐โ] [NormedSpace ๐โ F] {ฯโโ : ๐ โ+* ๐โ} {E' : Type u_11} [NormedSpace ๐ E'] [RingHomIsometric ฯโโ] (f : E' โ F) {s : Set (E' โSL[ฯโโ] F)} (hs : ) (hf : f โ closure (DFunLike.coe '' s)) :
E' โSL[ฯโโ] F

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
• = ().mkContinuousOfExistsBound โฏ
Instances For
@[simp]
theorem ContinuousLinearMap.ofMemClosureImageCoeBounded_apply {๐ : Type u_1} {๐โ : Type u_2} {F : Type u_6} [] [NontriviallyNormedField ๐โ] [NormedSpace ๐โ F] {ฯโโ : ๐ โ+* ๐โ} {E' : Type u_11} [NormedSpace ๐ E'] [RingHomIsometric ฯโโ] (f : E' โ F) {s : Set (E' โSL[ฯโโ] F)} (hs : ) (hf : f โ closure (DFunLike.coe '' s)) :
โ = f
noncomputable def ContinuousLinearMap.ofTendstoOfBoundedRange {๐ : Type u_1} {๐โ : Type u_2} {F : Type u_6} [] [NontriviallyNormedField ๐โ] [NormedSpace ๐โ F] {ฯโโ : ๐ โ+* ๐โ} {E' : Type u_11} [NormedSpace ๐ E'] [RingHomIsometric ฯโโ] {ฮฑ : Type u_12} {l : Filter ฮฑ} [l.NeBot] (f : E' โ F) (g : ฮฑ โ E' โSL[ฯโโ] F) (hf : Filter.Tendsto (fun (a : ฮฑ) (x : E') => (g a) x) l (nhds f)) (hg : ) :
E' โSL[ฯโโ] F

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
@[simp]
theorem ContinuousLinearMap.ofTendstoOfBoundedRange_apply {๐ : Type u_1} {๐โ : Type u_2} {F : Type u_6} [] [NontriviallyNormedField ๐โ] [NormedSpace ๐โ F] {ฯโโ : ๐ โ+* ๐โ} {E' : Type u_11} [NormedSpace ๐ E'] [RingHomIsometric ฯโโ] {ฮฑ : Type u_12} {l : Filter ฮฑ} [l.NeBot] (f : E' โ F) (g : ฮฑ โ E' โSL[ฯโโ] F) (hf : Filter.Tendsto (fun (a : ฮฑ) (x : E') => (g a) x) l (nhds f)) (hg : ) :
โ() = f
theorem ContinuousLinearMap.tendsto_of_tendsto_pointwise_of_cauchySeq {๐ : Type u_1} {๐โ : Type u_2} {F : Type u_6} [] [NontriviallyNormedField ๐โ] [NormedSpace ๐โ F] {ฯโโ : ๐ โ+* ๐โ} {E' : Type u_11} [NormedSpace ๐ E'] [RingHomIsometric ฯโโ] {f : โ โ E' โSL[ฯโโ] F} {g : E' โSL[ฯโโ] F} (hg : Filter.Tendsto (fun (n : โ) (x : E') => (f n) x) Filter.atTop (nhds โg)) (hf : ) :
Filter.Tendsto f Filter.atTop (nhds g)

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.

noncomputable instance ContinuousLinearMap.instCompleteSpace {๐ : Type u_1} {๐โ : Type u_2} {F : Type u_6} [] [NontriviallyNormedField ๐โ] [NormedSpace ๐โ F] {ฯโโ : ๐ โ+* ๐โ} {E' : Type u_11} [NormedSpace ๐ E'] [RingHomIsometric ฯโโ] [] :
CompleteSpace (E' โSL[ฯโโ] F)

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
• โฏ = โฏ
theorem ContinuousLinearMap.isCompact_closure_image_coe_of_bounded {๐ : Type u_1} {๐โ : Type u_2} {F : Type u_6} [] [NontriviallyNormedField ๐โ] [NormedSpace ๐โ F] {ฯโโ : ๐ โ+* ๐โ} {E' : Type u_11} [NormedSpace ๐ E'] [RingHomIsometric ฯโโ] [] {s : Set (E' โSL[ฯโโ] F)} (hb : ) :
IsCompact (closure (DFunLike.coe '' s))

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.

theorem ContinuousLinearMap.isCompact_image_coe_of_bounded_of_closed_image {๐ : Type u_1} {๐โ : Type u_2} {F : Type u_6} [] [NontriviallyNormedField ๐โ] [NormedSpace ๐โ F] {ฯโโ : ๐ โ+* ๐โ} {E' : Type u_11} [NormedSpace ๐ E'] [RingHomIsometric ฯโโ] [] {s : Set (E' โSL[ฯโโ] F)} (hb : ) (hc : IsClosed (DFunLike.coe '' s)) :
IsCompact (DFunLike.coe '' s)

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.

theorem ContinuousLinearMap.isClosed_image_coe_of_bounded_of_weak_closed {๐ : Type u_1} {๐โ : Type u_2} {F : Type u_6} [] [NontriviallyNormedField ๐โ] [NormedSpace ๐โ F] {ฯโโ : ๐ โ+* ๐โ} {E' : Type u_11} [NormedSpace ๐ E'] [RingHomIsometric ฯโโ] {s : Set (E' โSL[ฯโโ] F)} (hb : ) (hc : โ (f : E' โSL[ฯโโ] F), โf โ closure (DFunLike.coe '' s) โ f โ s) :
IsClosed (DFunLike.coe '' s)

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.

theorem ContinuousLinearMap.isCompact_image_coe_of_bounded_of_weak_closed {๐ : Type u_1} {๐โ : Type u_2} {F : Type u_6} [] [NontriviallyNormedField ๐โ] [NormedSpace ๐โ F] {ฯโโ : ๐ โ+* ๐โ} {E' : Type u_11} [NormedSpace ๐ E'] [RingHomIsometric ฯโโ] [] {s : Set (E' โSL[ฯโโ] F)} (hb : ) (hc : โ (f : E' โSL[ฯโโ] F), โf โ closure (DFunLike.coe '' s) โ f โ s) :
IsCompact (DFunLike.coe '' s)

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').

theorem ContinuousLinearMap.is_weak_closed_closedBall {๐ : Type u_1} {๐โ : Type u_2} {F : Type u_6} [] [NontriviallyNormedField ๐โ] [NormedSpace ๐โ F] {ฯโโ : ๐ โ+* ๐โ} {E' : Type u_11} [NormedSpace ๐ E'] [RingHomIsometric ฯโโ] (fโ : E' โSL[ฯโโ] F) (r : โ) โฆf : E' โSL[ฯโโ] Fโฆ (hf : โf โ closure (DFunLike.coe '' Metric.closedBall fโ r)) :

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').

theorem ContinuousLinearMap.isClosed_image_coe_closedBall {๐ : Type u_1} {๐โ : Type u_2} {E : Type u_4} {F : Type u_6} [] [NontriviallyNormedField ๐โ] [NormedSpace ๐ E] [NormedSpace ๐โ F] {ฯโโ : ๐ โ+* ๐โ} [RingHomIsometric ฯโโ] (fโ : E โSL[ฯโโ] F) (r : โ) :
IsClosed (DFunLike.coe '' Metric.closedBall fโ r)

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.

theorem ContinuousLinearMap.isCompact_image_coe_closedBall {๐ : Type u_1} {๐โ : Type u_2} {E : Type u_4} {F : Type u_6} [] [NontriviallyNormedField ๐โ] [NormedSpace ๐ E] [NormedSpace ๐โ F] {ฯโโ : ๐ โ+* ๐โ} [RingHomIsometric ฯโโ] [] (fโ : E โSL[ฯโโ] F) (r : โ) :
IsCompact (DFunLike.coe '' Metric.closedBall fโ r)

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.NormedSpace.WeakDual.

noncomputable def ContinuousLinearMap.extend {๐ : Type u_1} {๐โ : Type u_2} {E : Type u_4} {F : Type u_6} {Fโ : Type u_7} [] [] [NontriviallyNormedField ๐โ] [NormedSpace ๐ E] [NormedSpace ๐โ F] [NormedSpace ๐ Fโ] {ฯโโ : ๐ โ+* ๐โ} (f : E โSL[ฯโโ] F) [] (e : E โL[๐] Fโ) (h_dense : DenseRange โe) (h_e : UniformInducing โe) :
Fโ โSL[ฯโโ] F

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
@[simp]
theorem ContinuousLinearMap.extend_eq {๐ : Type u_1} {๐โ : Type u_2} {E : Type u_4} {F : Type u_6} {Fโ : Type u_7} [] [] [NontriviallyNormedField ๐โ] [NormedSpace ๐ E] [NormedSpace ๐โ F] [NormedSpace ๐ Fโ] {ฯโโ : ๐ โ+* ๐โ} (f : E โSL[ฯโโ] F) [] (e : E โL[๐] Fโ) (h_dense : DenseRange โe) (h_e : UniformInducing โe) (x : E) :
(f.extend e h_dense h_e) (e x) = f x
theorem ContinuousLinearMap.extend_unique {๐ : Type u_1} {๐โ : Type u_2} {E : Type u_4} {F : Type u_6} {Fโ : Type u_7} [] [] [NontriviallyNormedField ๐โ] [NormedSpace ๐ E] [NormedSpace ๐โ F] [NormedSpace ๐ Fโ] {ฯโโ : ๐ โ+* ๐โ} (f : E โSL[ฯโโ] F) [] (e : E โL[๐] Fโ) (h_dense : DenseRange โe) (h_e : UniformInducing โe) (g : Fโ โSL[ฯโโ] F) (H : g.comp e = f) :
f.extend e h_dense h_e = g
@[simp]
theorem ContinuousLinearMap.extend_zero {๐ : Type u_1} {๐โ : Type u_2} {E : Type u_4} {F : Type u_6} {Fโ : Type u_7} [] [] [NontriviallyNormedField ๐โ] [NormedSpace ๐ E] [NormedSpace ๐โ F] [NormedSpace ๐ Fโ] {ฯโโ : ๐ โ+* ๐โ} [] (e : E โL[๐] Fโ) (h_dense : DenseRange โe) (h_e : UniformInducing โe) :
ContinuousLinearMap.extend 0 e h_dense h_e = 0
theorem ContinuousLinearMap.opNorm_extend_le {๐ : Type u_1} {๐โ : Type u_2} {E : Type u_4} {F : Type u_6} {Fโ : Type u_7} [] [] [NontriviallyNormedField ๐โ] [NormedSpace ๐ E] [NormedSpace ๐โ F] [NormedSpace ๐ Fโ] {ฯโโ : ๐ โ+* ๐โ} (f : E โSL[ฯโโ] F) [] (e : E โL[๐] Fโ) (h_dense : DenseRange โe) {N : NNReal} (h_e : โ (x : E), โค โN * โe xโ) [RingHomIsometric ฯโโ] :
โf.extend e h_dense โฏโ โค โN *

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โ.

@[deprecated ContinuousLinearMap.opNorm_extend_le]
theorem ContinuousLinearMap.op_norm_extend_le {๐ : Type u_1} {๐โ : Type u_2} {E : Type u_4} {F : Type u_6} {Fโ : Type u_7} [] [] [NontriviallyNormedField ๐โ] [NormedSpace ๐ E] [NormedSpace ๐โ F] [NormedSpace ๐ Fโ] {ฯโโ : ๐ โ+* ๐โ} (f : E โSL[ฯโโ] F) [] (e : E โL[๐] Fโ) (h_dense : DenseRange โe) {N : NNReal} (h_e : โ (x : E), โค โN * โe xโ) [RingHomIsometric ฯโโ] :
โf.extend e h_dense โฏโ โค โN *

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โ.