Documentation

Mathlib.Analysis.NormedSpace.Banach

Banach open mapping theorem #

This file contains the Banach open mapping theorem, i.e., the fact that a bijective bounded linear map between Banach spaces has a bounded inverse.

structure ContinuousLinearMap.NonlinearRightInverse {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] (f : E β†’L[π•œ] F) :
Type (max u_2 u_3)

A (possibly nonlinear) right inverse to a continuous linear map, which doesn't have to be linear itself but which satisfies a bound β€–inverse xβ€– ≀ C * β€–xβ€–. A surjective continuous linear map doesn't always have a continuous linear right inverse, but it always has a nonlinear inverse in this sense, by Banach's open mapping theorem.

Instances For
    @[simp]
    theorem ContinuousLinearMap.NonlinearRightInverse.right_inv {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’L[π•œ] F} (fsymm : ContinuousLinearMap.NonlinearRightInverse f) (y : F) :
    f (fsymm.toFun y) = y
    theorem ContinuousLinearMap.NonlinearRightInverse.bound {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’L[π•œ] F} (fsymm : ContinuousLinearMap.NonlinearRightInverse f) (y : F) :
    β€–fsymm.toFun yβ€– ≀ ↑fsymm.nnnorm * β€–yβ€–
    noncomputable def ContinuousLinearEquiv.toNonlinearRightInverse {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] (f : E ≃L[π•œ] F) :

    Given a continuous linear equivalence, the inverse is in particular an instance of ContinuousLinearMap.NonlinearRightInverse (which turns out to be linear).

    Equations
    Instances For

      Proof of the Banach open mapping theorem #

      theorem ContinuousLinearMap.exists_approx_preimage_norm_le {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] (f : E β†’L[π•œ] F) [CompleteSpace F] (surj : Function.Surjective ⇑f) :
      βˆƒ C β‰₯ 0, βˆ€ (y : F), βˆƒ (x : E), dist (f x) y ≀ 1 / 2 * β€–yβ€– ∧ β€–xβ€– ≀ C * β€–yβ€–

      First step of the proof of the Banach open mapping theorem (using completeness of F): by Baire's theorem, there exists a ball in E whose image closure has nonempty interior. Rescaling everything, it follows that any y ∈ F is arbitrarily well approached by images of elements of norm at most C * β€–yβ€–. For further use, we will only need such an element whose image is within distance β€–yβ€–/2 of y, to apply an iterative process.

      theorem ContinuousLinearMap.exists_preimage_norm_le {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] (f : E β†’L[π•œ] F) [CompleteSpace F] [CompleteSpace E] (surj : Function.Surjective ⇑f) :
      βˆƒ C > 0, βˆ€ (y : F), βˆƒ (x : E), f x = y ∧ β€–xβ€– ≀ C * β€–yβ€–

      The Banach open mapping theorem: if a bounded linear map between Banach spaces is onto, then any point has a preimage with controlled norm.

      theorem ContinuousLinearMap.isOpenMap {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] (f : E β†’L[π•œ] F) [CompleteSpace F] [CompleteSpace E] (surj : Function.Surjective ⇑f) :
      IsOpenMap ⇑f

      The Banach open mapping theorem: a surjective bounded linear map between Banach spaces is open.

      theorem ContinuousLinearMap.quotientMap {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] (f : E β†’L[π•œ] F) [CompleteSpace F] [CompleteSpace E] (surj : Function.Surjective ⇑f) :
      QuotientMap ⇑f
      theorem AffineMap.isOpenMap {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] [CompleteSpace F] [CompleteSpace E] {P : Type u_4} {Q : Type u_5} [MetricSpace P] [NormedAddTorsor E P] [MetricSpace Q] [NormedAddTorsor F Q] (f : P →ᡃ[π•œ] Q) (hf : Continuous ⇑f) (surj : Function.Surjective ⇑f) :
      IsOpenMap ⇑f

      Applications of the Banach open mapping theorem #

      theorem ContinuousLinearMap.interior_preimage {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] (f : E β†’L[π•œ] F) [CompleteSpace F] [CompleteSpace E] (hsurj : Function.Surjective ⇑f) (s : Set F) :
      interior (⇑f ⁻¹' s) = ⇑f ⁻¹' interior s
      theorem ContinuousLinearMap.closure_preimage {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] (f : E β†’L[π•œ] F) [CompleteSpace F] [CompleteSpace E] (hsurj : Function.Surjective ⇑f) (s : Set F) :
      closure (⇑f ⁻¹' s) = ⇑f ⁻¹' closure s
      theorem ContinuousLinearMap.frontier_preimage {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] (f : E β†’L[π•œ] F) [CompleteSpace F] [CompleteSpace E] (hsurj : Function.Surjective ⇑f) (s : Set F) :
      frontier (⇑f ⁻¹' s) = ⇑f ⁻¹' frontier s
      theorem ContinuousLinearMap.exists_nonlinearRightInverse_of_surjective {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] [CompleteSpace F] [CompleteSpace E] (f : E β†’L[π•œ] F) (hsurj : LinearMap.range f = ⊀) :
      βˆƒ (fsymm : ContinuousLinearMap.NonlinearRightInverse f), 0 < fsymm.nnnorm
      @[irreducible]

      A surjective continuous linear map between Banach spaces admits a (possibly nonlinear) controlled right inverse. In general, it is not possible to ensure that such a right inverse is linear (take for instance the map from E to E/F where F is a closed subspace of E without a closed complement. Then it doesn't have a continuous linear right inverse.)

      Equations
      Instances For
        theorem LinearEquiv.continuous_symm {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] [CompleteSpace F] [CompleteSpace E] (e : E ≃ₗ[π•œ] F) (h : Continuous ⇑e) :

        If a bounded linear map is a bijection, then its inverse is also a bounded linear map.

        def LinearEquiv.toContinuousLinearEquivOfContinuous {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] [CompleteSpace F] [CompleteSpace E] (e : E ≃ₗ[π•œ] F) (h : Continuous ⇑e) :
        E ≃L[π•œ] F

        Associating to a linear equivalence between Banach spaces a continuous linear equivalence when the direct map is continuous, thanks to the Banach open mapping theorem that ensures that the inverse map is also continuous.

        Equations
        Instances For
          @[simp]
          theorem LinearEquiv.coeFn_toContinuousLinearEquivOfContinuous {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] [CompleteSpace F] [CompleteSpace E] (e : E ≃ₗ[π•œ] F) (h : Continuous ⇑e) :
          noncomputable def ContinuousLinearMap.equivRange {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] [CompleteSpace F] [CompleteSpace E] (f : E β†’L[π•œ] F) (hinj : Function.Injective ⇑f) (hclo : IsClosed (Set.range ⇑f)) :
          E ≃L[π•œ] β†₯(LinearMap.range f)

          An injective continuous linear map with a closed range defines a continuous linear equivalence between its domain and its range.

          Equations
          Instances For
            @[simp]
            theorem ContinuousLinearMap.coe_linearMap_equivRange {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] [CompleteSpace F] [CompleteSpace E] (f : E β†’L[π•œ] F) (hinj : Function.Injective ⇑f) (hclo : IsClosed (Set.range ⇑f)) :
            @[simp]
            theorem ContinuousLinearMap.coe_equivRange {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] [CompleteSpace F] [CompleteSpace E] (f : E β†’L[π•œ] F) (hinj : Function.Injective ⇑f) (hclo : IsClosed (Set.range ⇑f)) :
            noncomputable def ContinuousLinearEquiv.ofBijective {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] [CompleteSpace F] [CompleteSpace E] (f : E β†’L[π•œ] F) (hinj : LinearMap.ker f = βŠ₯) (hsurj : LinearMap.range f = ⊀) :
            E ≃L[π•œ] F

            Convert a bijective continuous linear map f : E β†’L[π•œ] F from a Banach space to a normed space to a continuous linear equivalence.

            Equations
            Instances For
              @[simp]
              theorem ContinuousLinearEquiv.coeFn_ofBijective {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] [CompleteSpace F] [CompleteSpace E] (f : E β†’L[π•œ] F) (hinj : LinearMap.ker f = βŠ₯) (hsurj : LinearMap.range f = ⊀) :
              ⇑(ContinuousLinearEquiv.ofBijective f hinj hsurj) = ⇑f
              theorem ContinuousLinearEquiv.coe_ofBijective {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] [CompleteSpace F] [CompleteSpace E] (f : E β†’L[π•œ] F) (hinj : LinearMap.ker f = βŠ₯) (hsurj : LinearMap.range f = ⊀) :
              ↑(ContinuousLinearEquiv.ofBijective f hinj hsurj) = f
              @[simp]
              theorem ContinuousLinearEquiv.ofBijective_symm_apply_apply {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] [CompleteSpace F] [CompleteSpace E] (f : E β†’L[π•œ] F) (hinj : LinearMap.ker f = βŠ₯) (hsurj : LinearMap.range f = ⊀) (x : E) :
              @[simp]
              theorem ContinuousLinearEquiv.ofBijective_apply_symm_apply {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] [CompleteSpace F] [CompleteSpace E] (f : E β†’L[π•œ] F) (hinj : LinearMap.ker f = βŠ₯) (hsurj : LinearMap.range f = ⊀) (y : F) :
              noncomputable def ContinuousLinearMap.coprodSubtypeLEquivOfIsCompl {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] [CompleteSpace F] [CompleteSpace E] (f : E β†’L[π•œ] F) {G : Submodule π•œ F} (h : IsCompl (LinearMap.range f) G) [CompleteSpace β†₯G] (hker : LinearMap.ker f = βŠ₯) :
              (E Γ— β†₯G) ≃L[π•œ] F

              Intermediate definition used to show ContinuousLinearMap.closed_complemented_range_of_isCompl_of_ker_eq_bot.

              This is f.coprod G.subtypeL as a ContinuousLinearEquiv.

              Equations
              Instances For
                theorem ContinuousLinearMap.closed_complemented_range_of_isCompl_of_ker_eq_bot {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] [CompleteSpace F] [CompleteSpace E] (f : E β†’L[π•œ] F) (G : Submodule π•œ F) (h : IsCompl (LinearMap.range f) G) (hG : IsClosed ↑G) (hker : LinearMap.ker f = βŠ₯) :
                theorem LinearMap.continuous_of_isClosed_graph {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] [CompleteSpace F] [CompleteSpace E] (g : E β†’β‚—[π•œ] F) (hg : IsClosed ↑(LinearMap.graph g)) :
                Continuous ⇑g

                The closed graph theorem : a linear map between two Banach spaces whose graph is closed is continuous.

                theorem LinearMap.continuous_of_seq_closed_graph {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] [CompleteSpace F] [CompleteSpace E] (g : E β†’β‚—[π•œ] F) (hg : βˆ€ (u : β„• β†’ E) (x : E) (y : F), Filter.Tendsto u Filter.atTop (nhds x) β†’ Filter.Tendsto (⇑g ∘ u) Filter.atTop (nhds y) β†’ y = g x) :
                Continuous ⇑g

                A useful form of the closed graph theorem : let f be a linear map between two Banach spaces. To show that f is continuous, it suffices to show that for any convergent sequence uβ‚™ ⟢ x, if f(uβ‚™) ⟢ y then y = f(x).

                def ContinuousLinearMap.ofIsClosedGraph {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] [CompleteSpace F] [CompleteSpace E] {g : E β†’β‚—[π•œ] F} (hg : IsClosed ↑(LinearMap.graph g)) :
                E β†’L[π•œ] F

                Upgrade a LinearMap to a ContinuousLinearMap using the closed graph theorem.

                Equations
                Instances For
                  @[simp]
                  theorem ContinuousLinearMap.coeFn_ofIsClosedGraph {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] [CompleteSpace F] [CompleteSpace E] {g : E β†’β‚—[π•œ] F} (hg : IsClosed ↑(LinearMap.graph g)) :
                  theorem ContinuousLinearMap.coe_ofIsClosedGraph {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] [CompleteSpace F] [CompleteSpace E] {g : E β†’β‚—[π•œ] F} (hg : IsClosed ↑(LinearMap.graph g)) :
                  def ContinuousLinearMap.ofSeqClosedGraph {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] [CompleteSpace F] [CompleteSpace E] {g : E β†’β‚—[π•œ] F} (hg : βˆ€ (u : β„• β†’ E) (x : E) (y : F), Filter.Tendsto u Filter.atTop (nhds x) β†’ Filter.Tendsto (⇑g ∘ u) Filter.atTop (nhds y) β†’ y = g x) :
                  E β†’L[π•œ] F

                  Upgrade a LinearMap to a ContinuousLinearMap using a variation on the closed graph theorem.

                  Equations
                  Instances For
                    @[simp]
                    theorem ContinuousLinearMap.coeFn_ofSeqClosedGraph {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] [CompleteSpace F] [CompleteSpace E] {g : E β†’β‚—[π•œ] F} (hg : βˆ€ (u : β„• β†’ E) (x : E) (y : F), Filter.Tendsto u Filter.atTop (nhds x) β†’ Filter.Tendsto (⇑g ∘ u) Filter.atTop (nhds y) β†’ y = g x) :
                    theorem ContinuousLinearMap.coe_ofSeqClosedGraph {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] [CompleteSpace F] [CompleteSpace E] {g : E β†’β‚—[π•œ] F} (hg : βˆ€ (u : β„• β†’ E) (x : E) (y : F), Filter.Tendsto u Filter.atTop (nhds x) β†’ Filter.Tendsto (⇑g ∘ u) Filter.atTop (nhds y) β†’ y = g x) :