Documentation

Mathlib.Analysis.NormedSpace.OperatorNorm.Completeness

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} [NormedAddCommGroup F] [NontriviallyNormedField ๐•œ] [NontriviallyNormedField ๐•œโ‚‚] [NormedSpace ๐•œโ‚‚ F] {ฯƒโ‚โ‚‚ : ๐•œ โ†’+* ๐•œโ‚‚} {E' : Type u_11} [SeminormedAddCommGroup E'] [NormedSpace ๐•œ E'] [RingHomIsometric ฯƒโ‚โ‚‚] (f : E' โ†’ F) {s : Set (E' โ†’SL[ฯƒโ‚โ‚‚] F)} (hs : Bornology.IsBounded s) (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
Instances For
    @[simp]
    theorem ContinuousLinearMap.ofMemClosureImageCoeBounded_apply {๐•œ : Type u_1} {๐•œโ‚‚ : Type u_2} {F : Type u_6} [NormedAddCommGroup F] [NontriviallyNormedField ๐•œ] [NontriviallyNormedField ๐•œโ‚‚] [NormedSpace ๐•œโ‚‚ F] {ฯƒโ‚โ‚‚ : ๐•œ โ†’+* ๐•œโ‚‚} {E' : Type u_11} [SeminormedAddCommGroup E'] [NormedSpace ๐•œ E'] [RingHomIsometric ฯƒโ‚โ‚‚] (f : E' โ†’ F) {s : Set (E' โ†’SL[ฯƒโ‚โ‚‚] F)} (hs : Bornology.IsBounded s) (hf : f โˆˆ closure (DFunLike.coe '' s)) :
    noncomputable def ContinuousLinearMap.ofTendstoOfBoundedRange {๐•œ : Type u_1} {๐•œโ‚‚ : Type u_2} {F : Type u_6} [NormedAddCommGroup F] [NontriviallyNormedField ๐•œ] [NontriviallyNormedField ๐•œโ‚‚] [NormedSpace ๐•œโ‚‚ F] {ฯƒโ‚โ‚‚ : ๐•œ โ†’+* ๐•œโ‚‚} {E' : Type u_11} [SeminormedAddCommGroup E'] [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 : Bornology.IsBounded (Set.range g)) :
    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} [NormedAddCommGroup F] [NontriviallyNormedField ๐•œ] [NontriviallyNormedField ๐•œโ‚‚] [NormedSpace ๐•œโ‚‚ F] {ฯƒโ‚โ‚‚ : ๐•œ โ†’+* ๐•œโ‚‚} {E' : Type u_11} [SeminormedAddCommGroup E'] [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 : Bornology.IsBounded (Set.range g)) :
      theorem ContinuousLinearMap.tendsto_of_tendsto_pointwise_of_cauchySeq {๐•œ : Type u_1} {๐•œโ‚‚ : Type u_2} {F : Type u_6} [NormedAddCommGroup F] [NontriviallyNormedField ๐•œ] [NontriviallyNormedField ๐•œโ‚‚] [NormedSpace ๐•œโ‚‚ F] {ฯƒโ‚โ‚‚ : ๐•œ โ†’+* ๐•œโ‚‚} {E' : Type u_11} [SeminormedAddCommGroup E'] [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 : CauchySeq f) :
      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} [NormedAddCommGroup F] [NontriviallyNormedField ๐•œ] [NontriviallyNormedField ๐•œโ‚‚] [NormedSpace ๐•œโ‚‚ F] {ฯƒโ‚โ‚‚ : ๐•œ โ†’+* ๐•œโ‚‚} {E' : Type u_11} [SeminormedAddCommGroup E'] [NormedSpace ๐•œ E'] [RingHomIsometric ฯƒโ‚โ‚‚] [CompleteSpace F] :
      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} [NormedAddCommGroup F] [NontriviallyNormedField ๐•œ] [NontriviallyNormedField ๐•œโ‚‚] [NormedSpace ๐•œโ‚‚ F] {ฯƒโ‚โ‚‚ : ๐•œ โ†’+* ๐•œโ‚‚} {E' : Type u_11} [SeminormedAddCommGroup E'] [NormedSpace ๐•œ E'] [RingHomIsometric ฯƒโ‚โ‚‚] [ProperSpace F] {s : Set (E' โ†’SL[ฯƒโ‚โ‚‚] F)} (hb : Bornology.IsBounded s) :
      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} [NormedAddCommGroup F] [NontriviallyNormedField ๐•œ] [NontriviallyNormedField ๐•œโ‚‚] [NormedSpace ๐•œโ‚‚ F] {ฯƒโ‚โ‚‚ : ๐•œ โ†’+* ๐•œโ‚‚} {E' : Type u_11} [SeminormedAddCommGroup E'] [NormedSpace ๐•œ E'] [RingHomIsometric ฯƒโ‚โ‚‚] [ProperSpace F] {s : Set (E' โ†’SL[ฯƒโ‚โ‚‚] F)} (hb : Bornology.IsBounded s) (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} [NormedAddCommGroup F] [NontriviallyNormedField ๐•œ] [NontriviallyNormedField ๐•œโ‚‚] [NormedSpace ๐•œโ‚‚ F] {ฯƒโ‚โ‚‚ : ๐•œ โ†’+* ๐•œโ‚‚} {E' : Type u_11} [SeminormedAddCommGroup E'] [NormedSpace ๐•œ E'] [RingHomIsometric ฯƒโ‚โ‚‚] {s : Set (E' โ†’SL[ฯƒโ‚โ‚‚] F)} (hb : Bornology.IsBounded s) (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} [NormedAddCommGroup F] [NontriviallyNormedField ๐•œ] [NontriviallyNormedField ๐•œโ‚‚] [NormedSpace ๐•œโ‚‚ F] {ฯƒโ‚โ‚‚ : ๐•œ โ†’+* ๐•œโ‚‚} {E' : Type u_11} [SeminormedAddCommGroup E'] [NormedSpace ๐•œ E'] [RingHomIsometric ฯƒโ‚โ‚‚] [ProperSpace F] {s : Set (E' โ†’SL[ฯƒโ‚โ‚‚] F)} (hb : Bornology.IsBounded s) (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} [NormedAddCommGroup F] [NontriviallyNormedField ๐•œ] [NontriviallyNormedField ๐•œโ‚‚] [NormedSpace ๐•œโ‚‚ F] {ฯƒโ‚โ‚‚ : ๐•œ โ†’+* ๐•œโ‚‚} {E' : Type u_11} [SeminormedAddCommGroup E'] [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} [NormedAddCommGroup E] [NormedAddCommGroup F] [NontriviallyNormedField ๐•œ] [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} [NormedAddCommGroup E] [NormedAddCommGroup F] [NontriviallyNormedField ๐•œ] [NontriviallyNormedField ๐•œโ‚‚] [NormedSpace ๐•œ E] [NormedSpace ๐•œโ‚‚ F] {ฯƒโ‚โ‚‚ : ๐•œ โ†’+* ๐•œโ‚‚} [RingHomIsometric ฯƒโ‚โ‚‚] [ProperSpace F] (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.Normed.Module.WeakDual.

      noncomputable def ContinuousLinearMap.extend {๐•œ : Type u_1} {๐•œโ‚‚ : Type u_2} {E : Type u_4} {F : Type u_6} {Fโ‚— : Type u_7} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup Fโ‚—] [NontriviallyNormedField ๐•œ] [NontriviallyNormedField ๐•œโ‚‚] [NormedSpace ๐•œ E] [NormedSpace ๐•œโ‚‚ F] [NormedSpace ๐•œ Fโ‚—] {ฯƒโ‚โ‚‚ : ๐•œ โ†’+* ๐•œโ‚‚} (f : E โ†’SL[ฯƒโ‚โ‚‚] F) [CompleteSpace 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 = { toFun := โ‹ฏ.extend โ‡‘f, map_add' := โ‹ฏ, map_smul' := โ‹ฏ, 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} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup Fโ‚—] [NontriviallyNormedField ๐•œ] [NontriviallyNormedField ๐•œโ‚‚] [NormedSpace ๐•œ E] [NormedSpace ๐•œโ‚‚ F] [NormedSpace ๐•œ Fโ‚—] {ฯƒโ‚โ‚‚ : ๐•œ โ†’+* ๐•œโ‚‚} (f : E โ†’SL[ฯƒโ‚โ‚‚] F) [CompleteSpace 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} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup Fโ‚—] [NontriviallyNormedField ๐•œ] [NontriviallyNormedField ๐•œโ‚‚] [NormedSpace ๐•œ E] [NormedSpace ๐•œโ‚‚ F] [NormedSpace ๐•œ Fโ‚—] {ฯƒโ‚โ‚‚ : ๐•œ โ†’+* ๐•œโ‚‚} (f : E โ†’SL[ฯƒโ‚โ‚‚] F) [CompleteSpace 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} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup Fโ‚—] [NontriviallyNormedField ๐•œ] [NontriviallyNormedField ๐•œโ‚‚] [NormedSpace ๐•œ E] [NormedSpace ๐•œโ‚‚ F] [NormedSpace ๐•œ Fโ‚—] {ฯƒโ‚โ‚‚ : ๐•œ โ†’+* ๐•œโ‚‚} [CompleteSpace 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} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup Fโ‚—] [NontriviallyNormedField ๐•œ] [NontriviallyNormedField ๐•œโ‚‚] [NormedSpace ๐•œ E] [NormedSpace ๐•œโ‚‚ F] [NormedSpace ๐•œ Fโ‚—] {ฯƒโ‚โ‚‚ : ๐•œ โ†’+* ๐•œโ‚‚} (f : E โ†’SL[ฯƒโ‚โ‚‚] F) [CompleteSpace F] (e : E โ†’L[๐•œ] Fโ‚—) (h_dense : DenseRange โ‡‘e) {N : NNReal} (h_e : โˆ€ (x : E), โ€–xโ€– โ‰ค โ†‘N * โ€–e xโ€–) [RingHomIsometric ฯƒโ‚โ‚‚] :
        โ€–f.extend e h_dense โ‹ฏโ€– โ‰ค โ†‘N * โ€–fโ€–

        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} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup Fโ‚—] [NontriviallyNormedField ๐•œ] [NontriviallyNormedField ๐•œโ‚‚] [NormedSpace ๐•œ E] [NormedSpace ๐•œโ‚‚ F] [NormedSpace ๐•œ Fโ‚—] {ฯƒโ‚โ‚‚ : ๐•œ โ†’+* ๐•œโ‚‚} (f : E โ†’SL[ฯƒโ‚โ‚‚] F) [CompleteSpace F] (e : E โ†’L[๐•œ] Fโ‚—) (h_dense : DenseRange โ‡‘e) {N : NNReal} (h_e : โˆ€ (x : E), โ€–xโ€– โ‰ค โ†‘N * โ€–e xโ€–) [RingHomIsometric ฯƒโ‚โ‚‚] :
        โ€–f.extend e h_dense โ‹ฏโ€– โ‰ค โ†‘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โ€–.