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} {π•œ' : Type u_2} [NontriviallyNormedField π•œ] [NontriviallyNormedField π•œ'] {Οƒ : π•œ β†’+* π•œ'} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace π•œ' F] (f : E β†’SL[Οƒ] F) :
Type (max u_3 u_4)

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
    theorem ContinuousLinearMap.NonlinearRightInverse.bound' {π•œ : Type u_1} {π•œ' : Type u_2} [NontriviallyNormedField π•œ] [NontriviallyNormedField π•œ'] {Οƒ : π•œ β†’+* π•œ'} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace π•œ' F] {f : E β†’SL[Οƒ] F} (self : f.NonlinearRightInverse) (y : F) :
    β€–self.toFun yβ€– ≀ ↑self.nnnorm * β€–yβ€–
    theorem ContinuousLinearMap.NonlinearRightInverse.right_inv' {π•œ : Type u_1} {π•œ' : Type u_2} [NontriviallyNormedField π•œ] [NontriviallyNormedField π•œ'] {Οƒ : π•œ β†’+* π•œ'} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace π•œ' F] {f : E β†’SL[Οƒ] F} (self : f.NonlinearRightInverse) (y : F) :
    f (self.toFun y) = y
    instance ContinuousLinearMap.instCoeFunNonlinearRightInverseForall {π•œ : Type u_1} {π•œ' : Type u_2} [NontriviallyNormedField π•œ] [NontriviallyNormedField π•œ'] {Οƒ : π•œ β†’+* π•œ'} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace π•œ' F] (f : E β†’SL[Οƒ] F) :
    CoeFun f.NonlinearRightInverse fun (x : f.NonlinearRightInverse) => F β†’ E
    Equations
    • f.instCoeFunNonlinearRightInverseForall = { coe := fun (fsymm : f.NonlinearRightInverse) => fsymm.toFun }
    @[simp]
    theorem ContinuousLinearMap.NonlinearRightInverse.right_inv {π•œ : Type u_1} {π•œ' : Type u_2} [NontriviallyNormedField π•œ] [NontriviallyNormedField π•œ'] {Οƒ : π•œ β†’+* π•œ'} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace π•œ' F] {f : E β†’SL[Οƒ] F} (fsymm : f.NonlinearRightInverse) (y : F) :
    f (fsymm.toFun y) = y
    theorem ContinuousLinearMap.NonlinearRightInverse.bound {π•œ : Type u_1} {π•œ' : Type u_2} [NontriviallyNormedField π•œ] [NontriviallyNormedField π•œ'] {Οƒ : π•œ β†’+* π•œ'} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace π•œ' F] {f : E β†’SL[Οƒ] F} (fsymm : f.NonlinearRightInverse) (y : F) :
    β€–fsymm.toFun yβ€– ≀ ↑fsymm.nnnorm * β€–yβ€–
    noncomputable def ContinuousLinearEquiv.toNonlinearRightInverse {π•œ : Type u_1} {π•œ' : Type u_2} [NontriviallyNormedField π•œ] [NontriviallyNormedField π•œ'] {Οƒ : π•œ β†’+* π•œ'} {Οƒ' : π•œ' β†’+* π•œ} [RingHomInvPair Οƒ Οƒ'] [RingHomInvPair Οƒ' Οƒ] [RingHomIsometric Οƒ'] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace π•œ' F] (f : E ≃SL[Οƒ] F) :
    (↑f).NonlinearRightInverse

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

    Equations
    • f.toNonlinearRightInverse = { toFun := f.invFun, nnnorm := ‖↑f.symmβ€–β‚Š, bound' := β‹―, right_inv' := β‹― }
    Instances For
      noncomputable instance instInhabitedNonlinearRightInverseToContinuousLinearMap {π•œ : Type u_1} {π•œ' : Type u_2} [NontriviallyNormedField π•œ] [NontriviallyNormedField π•œ'] {Οƒ : π•œ β†’+* π•œ'} {Οƒ' : π•œ' β†’+* π•œ} [RingHomInvPair Οƒ Οƒ'] [RingHomInvPair Οƒ' Οƒ] [RingHomIsometric Οƒ'] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace π•œ' F] (f : E ≃SL[Οƒ] F) :
      Inhabited (↑f).NonlinearRightInverse
      Equations

      Proof of the Banach open mapping theorem #

      theorem ContinuousLinearMap.exists_approx_preimage_norm_le {π•œ : Type u_1} {π•œ' : Type u_2} [NontriviallyNormedField π•œ] [NontriviallyNormedField π•œ'] {Οƒ : π•œ β†’+* π•œ'} {Οƒ' : π•œ' β†’+* π•œ} [RingHomInvPair Οƒ Οƒ'] [RingHomIsometric Οƒ] [RingHomIsometric Οƒ'] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace π•œ' F] (f : E β†’SL[Οƒ] 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} {π•œ' : Type u_2} [NontriviallyNormedField π•œ] [NontriviallyNormedField π•œ'] {Οƒ : π•œ β†’+* π•œ'} {Οƒ' : π•œ' β†’+* π•œ} [RingHomInvPair Οƒ Οƒ'] [RingHomIsometric Οƒ] [RingHomIsometric Οƒ'] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace π•œ' F] (f : E β†’SL[Οƒ] 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} {π•œ' : Type u_2} [NontriviallyNormedField π•œ] [NontriviallyNormedField π•œ'] {Οƒ : π•œ β†’+* π•œ'} {Οƒ' : π•œ' β†’+* π•œ} [RingHomInvPair Οƒ Οƒ'] [RingHomIsometric Οƒ] [RingHomIsometric Οƒ'] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace π•œ' F] (f : E β†’SL[Οƒ] 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} {π•œ' : Type u_2} [NontriviallyNormedField π•œ] [NontriviallyNormedField π•œ'] {Οƒ : π•œ β†’+* π•œ'} {Οƒ' : π•œ' β†’+* π•œ} [RingHomInvPair Οƒ Οƒ'] [RingHomIsometric Οƒ] [RingHomIsometric Οƒ'] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace π•œ' F] (f : E β†’SL[Οƒ] F) [CompleteSpace F] [CompleteSpace E] (surj : Function.Surjective ⇑f) :
      QuotientMap ⇑f
      theorem AffineMap.isOpenMap {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] [CompleteSpace E] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace π•œ F] [CompleteSpace F] {P : Type u_6} {Q : Type u_7} [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} {π•œ' : Type u_2} [NontriviallyNormedField π•œ] [NontriviallyNormedField π•œ'] {Οƒ : π•œ β†’+* π•œ'} {Οƒ' : π•œ' β†’+* π•œ} [RingHomInvPair Οƒ Οƒ'] [RingHomIsometric Οƒ] [RingHomIsometric Οƒ'] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace π•œ' F] (f : E β†’SL[Οƒ] 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} {π•œ' : Type u_2} [NontriviallyNormedField π•œ] [NontriviallyNormedField π•œ'] {Οƒ : π•œ β†’+* π•œ'} {Οƒ' : π•œ' β†’+* π•œ} [RingHomInvPair Οƒ Οƒ'] [RingHomIsometric Οƒ] [RingHomIsometric Οƒ'] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace π•œ' F] (f : E β†’SL[Οƒ] 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} {π•œ' : Type u_2} [NontriviallyNormedField π•œ] [NontriviallyNormedField π•œ'] {Οƒ : π•œ β†’+* π•œ'} {Οƒ' : π•œ' β†’+* π•œ} [RingHomInvPair Οƒ Οƒ'] [RingHomIsometric Οƒ] [RingHomIsometric Οƒ'] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace π•œ' F] (f : E β†’SL[Οƒ] 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} {π•œ' : Type u_2} [NontriviallyNormedField π•œ] [NontriviallyNormedField π•œ'] {Οƒ : π•œ β†’+* π•œ'} {Οƒ' : π•œ' β†’+* π•œ} [RingHomInvPair Οƒ Οƒ'] [RingHomIsometric Οƒ] [RingHomIsometric Οƒ'] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace π•œ' F] [CompleteSpace F] [CompleteSpace E] (f : E β†’SL[Οƒ] F) (hsurj : LinearMap.range f = ⊀) :
      βˆƒ (fsymm : f.NonlinearRightInverse), 0 < fsymm.nnnorm
      theorem ContinuousLinearMap.nonlinearRightInverseOfSurjective_def {π•œ : Type u_5} {π•œ' : Type u_6} [NontriviallyNormedField π•œ] [NontriviallyNormedField π•œ'] {Οƒ : π•œ β†’+* π•œ'} {Οƒ' : π•œ' β†’+* π•œ} [RingHomInvPair Οƒ Οƒ'] [RingHomIsometric Οƒ] [RingHomIsometric Οƒ'] {E : Type u_7} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_8} [NormedAddCommGroup F] [NormedSpace π•œ' F] [CompleteSpace F] [CompleteSpace E] (f : E β†’SL[Οƒ] F) (hsurj : LinearMap.range f = ⊀) :
      f.nonlinearRightInverseOfSurjective hsurj = Classical.choose β‹―
      @[irreducible]
      noncomputable def ContinuousLinearMap.nonlinearRightInverseOfSurjective {π•œ : Type u_5} {π•œ' : Type u_6} [NontriviallyNormedField π•œ] [NontriviallyNormedField π•œ'] {Οƒ : π•œ β†’+* π•œ'} {Οƒ' : π•œ' β†’+* π•œ} [RingHomInvPair Οƒ Οƒ'] [RingHomIsometric Οƒ] [RingHomIsometric Οƒ'] {E : Type u_7} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_8} [NormedAddCommGroup F] [NormedSpace π•œ' F] [CompleteSpace F] [CompleteSpace E] (f : E β†’SL[Οƒ] F) (hsurj : LinearMap.range f = ⊀) :
      f.NonlinearRightInverse

      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 ContinuousLinearMap.nonlinearRightInverseOfSurjective_nnnorm_pos {π•œ : Type u_1} {π•œ' : Type u_2} [NontriviallyNormedField π•œ] [NontriviallyNormedField π•œ'] {Οƒ : π•œ β†’+* π•œ'} {Οƒ' : π•œ' β†’+* π•œ} [RingHomInvPair Οƒ Οƒ'] [RingHomIsometric Οƒ] [RingHomIsometric Οƒ'] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace π•œ' F] [CompleteSpace F] [CompleteSpace E] (f : E β†’SL[Οƒ] F) (hsurj : LinearMap.range f = ⊀) :
        0 < (f.nonlinearRightInverseOfSurjective hsurj).nnnorm
        theorem LinearEquiv.continuous_symm {π•œ : Type u_1} {π•œ' : Type u_2} [NontriviallyNormedField π•œ] [NontriviallyNormedField π•œ'] {Οƒ : π•œ β†’+* π•œ'} {Οƒ' : π•œ' β†’+* π•œ} [RingHomInvPair Οƒ Οƒ'] [RingHomInvPair Οƒ' Οƒ] [RingHomIsometric Οƒ] [RingHomIsometric Οƒ'] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace π•œ' F] [CompleteSpace F] [CompleteSpace E] (e : E ≃ₛₗ[Οƒ] F) (h : Continuous ⇑e) :
        Continuous ⇑e.symm

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

        def LinearEquiv.toContinuousLinearEquivOfContinuous {π•œ : Type u_1} {π•œ' : Type u_2} [NontriviallyNormedField π•œ] [NontriviallyNormedField π•œ'] {Οƒ : π•œ β†’+* π•œ'} {Οƒ' : π•œ' β†’+* π•œ} [RingHomInvPair Οƒ Οƒ'] [RingHomInvPair Οƒ' Οƒ] [RingHomIsometric Οƒ] [RingHomIsometric Οƒ'] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace π•œ' F] [CompleteSpace F] [CompleteSpace E] (e : E ≃ₛₗ[Οƒ] F) (h : Continuous ⇑e) :
        E ≃SL[Οƒ] 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
        • e.toContinuousLinearEquivOfContinuous h = { toLinearEquiv := e, continuous_toFun := h, continuous_invFun := β‹― }
        Instances For
          @[simp]
          theorem LinearEquiv.coeFn_toContinuousLinearEquivOfContinuous {π•œ : Type u_1} {π•œ' : Type u_2} [NontriviallyNormedField π•œ] [NontriviallyNormedField π•œ'] {Οƒ : π•œ β†’+* π•œ'} {Οƒ' : π•œ' β†’+* π•œ} [RingHomInvPair Οƒ Οƒ'] [RingHomInvPair Οƒ' Οƒ] [RingHomIsometric Οƒ] [RingHomIsometric Οƒ'] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace π•œ' F] [CompleteSpace F] [CompleteSpace E] (e : E ≃ₛₗ[Οƒ] F) (h : Continuous ⇑e) :
          ⇑(e.toContinuousLinearEquivOfContinuous h) = ⇑e
          @[simp]
          theorem LinearEquiv.coeFn_toContinuousLinearEquivOfContinuous_symm {π•œ : Type u_1} {π•œ' : Type u_2} [NontriviallyNormedField π•œ] [NontriviallyNormedField π•œ'] {Οƒ : π•œ β†’+* π•œ'} {Οƒ' : π•œ' β†’+* π•œ} [RingHomInvPair Οƒ Οƒ'] [RingHomInvPair Οƒ' Οƒ] [RingHomIsometric Οƒ] [RingHomIsometric Οƒ'] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace π•œ' F] [CompleteSpace F] [CompleteSpace E] (e : E ≃ₛₗ[Οƒ] F) (h : Continuous ⇑e) :
          ⇑(e.toContinuousLinearEquivOfContinuous h).symm = ⇑e.symm
          noncomputable def ContinuousLinearMap.equivRange {π•œ : Type u_1} {π•œ' : Type u_2} [NontriviallyNormedField π•œ] [NontriviallyNormedField π•œ'] {Οƒ : π•œ β†’+* π•œ'} {Οƒ' : π•œ' β†’+* π•œ} [RingHomInvPair Οƒ Οƒ'] [RingHomInvPair Οƒ' Οƒ] [RingHomIsometric Οƒ] [RingHomIsometric Οƒ'] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace π•œ' F] [CompleteSpace F] [CompleteSpace E] (f : E β†’SL[Οƒ] F) (hinj : Function.Injective ⇑f) (hclo : IsClosed (Set.range ⇑f)) :
          E ≃SL[Οƒ] β†₯(LinearMap.range f)

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

          Equations
          • f.equivRange hinj hclo = let_fun this := β‹―; (LinearEquiv.ofInjective (↑f) hinj).toContinuousLinearEquivOfContinuous β‹―
          Instances For
            @[simp]
            theorem ContinuousLinearMap.coe_linearMap_equivRange {π•œ : Type u_1} {π•œ' : Type u_2} [NontriviallyNormedField π•œ] [NontriviallyNormedField π•œ'] {Οƒ : π•œ β†’+* π•œ'} {Οƒ' : π•œ' β†’+* π•œ} [RingHomInvPair Οƒ Οƒ'] [RingHomInvPair Οƒ' Οƒ] [RingHomIsometric Οƒ] [RingHomIsometric Οƒ'] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace π•œ' F] [CompleteSpace F] [CompleteSpace E] (f : E β†’SL[Οƒ] F) (hinj : Function.Injective ⇑f) (hclo : IsClosed (Set.range ⇑f)) :
            ↑(f.equivRange hinj hclo) = f.rangeRestrict
            @[simp]
            theorem ContinuousLinearMap.coe_equivRange {π•œ : Type u_1} {π•œ' : Type u_2} [NontriviallyNormedField π•œ] [NontriviallyNormedField π•œ'] {Οƒ : π•œ β†’+* π•œ'} {Οƒ' : π•œ' β†’+* π•œ} [RingHomInvPair Οƒ Οƒ'] [RingHomInvPair Οƒ' Οƒ] [RingHomIsometric Οƒ] [RingHomIsometric Οƒ'] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace π•œ' F] [CompleteSpace F] [CompleteSpace E] (f : E β†’SL[Οƒ] F) (hinj : Function.Injective ⇑f) (hclo : IsClosed (Set.range ⇑f)) :
            ⇑(f.equivRange hinj hclo) = ⇑f.rangeRestrict
            noncomputable def ContinuousLinearEquiv.ofBijective {π•œ : Type u_1} {π•œ' : Type u_2} [NontriviallyNormedField π•œ] [NontriviallyNormedField π•œ'] {Οƒ : π•œ β†’+* π•œ'} {Οƒ' : π•œ' β†’+* π•œ} [RingHomInvPair Οƒ Οƒ'] [RingHomInvPair Οƒ' Οƒ] [RingHomIsometric Οƒ] [RingHomIsometric Οƒ'] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace π•œ' F] [CompleteSpace F] [CompleteSpace E] (f : E β†’SL[Οƒ] F) (hinj : LinearMap.ker f = βŠ₯) (hsurj : LinearMap.range f = ⊀) :
            E ≃SL[Οƒ] F

            Convert a bijective continuous linear map f : E β†’SL[Οƒ] 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} {π•œ' : Type u_2} [NontriviallyNormedField π•œ] [NontriviallyNormedField π•œ'] {Οƒ : π•œ β†’+* π•œ'} {Οƒ' : π•œ' β†’+* π•œ} [RingHomInvPair Οƒ Οƒ'] [RingHomInvPair Οƒ' Οƒ] [RingHomIsometric Οƒ] [RingHomIsometric Οƒ'] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace π•œ' F] [CompleteSpace F] [CompleteSpace E] (f : E β†’SL[Οƒ] F) (hinj : LinearMap.ker f = βŠ₯) (hsurj : LinearMap.range f = ⊀) :
              ⇑(ContinuousLinearEquiv.ofBijective f hinj hsurj) = ⇑f
              theorem ContinuousLinearEquiv.coe_ofBijective {π•œ : Type u_1} {π•œ' : Type u_2} [NontriviallyNormedField π•œ] [NontriviallyNormedField π•œ'] {Οƒ : π•œ β†’+* π•œ'} {Οƒ' : π•œ' β†’+* π•œ} [RingHomInvPair Οƒ Οƒ'] [RingHomInvPair Οƒ' Οƒ] [RingHomIsometric Οƒ] [RingHomIsometric Οƒ'] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace π•œ' F] [CompleteSpace F] [CompleteSpace E] (f : E β†’SL[Οƒ] 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} {π•œ' : Type u_2} [NontriviallyNormedField π•œ] [NontriviallyNormedField π•œ'] {Οƒ : π•œ β†’+* π•œ'} {Οƒ' : π•œ' β†’+* π•œ} [RingHomInvPair Οƒ Οƒ'] [RingHomInvPair Οƒ' Οƒ] [RingHomIsometric Οƒ] [RingHomIsometric Οƒ'] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace π•œ' F] [CompleteSpace F] [CompleteSpace E] (f : E β†’SL[Οƒ] F) (hinj : LinearMap.ker f = βŠ₯) (hsurj : LinearMap.range f = ⊀) (x : E) :
              (ContinuousLinearEquiv.ofBijective f hinj hsurj).symm (f x) = x
              @[simp]
              theorem ContinuousLinearEquiv.ofBijective_apply_symm_apply {π•œ : Type u_1} {π•œ' : Type u_2} [NontriviallyNormedField π•œ] [NontriviallyNormedField π•œ'] {Οƒ : π•œ β†’+* π•œ'} {Οƒ' : π•œ' β†’+* π•œ} [RingHomInvPair Οƒ Οƒ'] [RingHomInvPair Οƒ' Οƒ] [RingHomIsometric Οƒ] [RingHomIsometric Οƒ'] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace π•œ' F] [CompleteSpace F] [CompleteSpace E] (f : E β†’SL[Οƒ] F) (hinj : LinearMap.ker f = βŠ₯) (hsurj : LinearMap.range f = ⊀) (y : F) :
              f ((ContinuousLinearEquiv.ofBijective f hinj hsurj).symm y) = y
              theorem ContinuousLinearMap.isUnit_iff_bijective {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] [CompleteSpace E] {f : E β†’L[π•œ] E} :
              noncomputable def ContinuousLinearMap.coprodSubtypeLEquivOfIsCompl {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] [CompleteSpace E] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace π•œ F] [CompleteSpace F] (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.range_eq_map_coprodSubtypeLEquivOfIsCompl {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] [CompleteSpace E] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace π•œ F] [CompleteSpace F] (f : E β†’L[π•œ] F) {G : Submodule π•œ F} (h : IsCompl (LinearMap.range f) G) [CompleteSpace β†₯G] (hker : LinearMap.ker f = βŠ₯) :
                LinearMap.range f = Submodule.map (↑↑(f.coprodSubtypeLEquivOfIsCompl h hker)) (⊀.prod βŠ₯)
                theorem ContinuousLinearMap.closed_complemented_range_of_isCompl_of_ker_eq_bot {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] [CompleteSpace E] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace π•œ F] [CompleteSpace F] (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_3} [NormedAddCommGroup E] [NormedSpace π•œ E] [CompleteSpace E] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace π•œ F] [CompleteSpace F] (g : E β†’β‚—[π•œ] F) (hg : IsClosed ↑g.graph) :
                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_3} [NormedAddCommGroup E] [NormedSpace π•œ E] [CompleteSpace E] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace π•œ F] [CompleteSpace F] (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_3} [NormedAddCommGroup E] [NormedSpace π•œ E] [CompleteSpace E] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace π•œ F] [CompleteSpace F] {g : E β†’β‚—[π•œ] F} (hg : IsClosed ↑g.graph) :
                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_3} [NormedAddCommGroup E] [NormedSpace π•œ E] [CompleteSpace E] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace π•œ F] [CompleteSpace F] {g : E β†’β‚—[π•œ] F} (hg : IsClosed ↑g.graph) :
                  theorem ContinuousLinearMap.coe_ofIsClosedGraph {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] [CompleteSpace E] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace π•œ F] [CompleteSpace F] {g : E β†’β‚—[π•œ] F} (hg : IsClosed ↑g.graph) :
                  def ContinuousLinearMap.ofSeqClosedGraph {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] [CompleteSpace E] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace π•œ F] [CompleteSpace F] {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_3} [NormedAddCommGroup E] [NormedSpace π•œ E] [CompleteSpace E] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace π•œ F] [CompleteSpace F] {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_3} [NormedAddCommGroup E] [NormedSpace π•œ E] [CompleteSpace E] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace π•œ F] [CompleteSpace F] {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.closed_range_of_antilipschitz {π•œ : Type u_1} {π•œ' : Type u_2} [NontriviallyNormedField π•œ] [NontriviallyNormedField π•œ'] {Οƒ : π•œ β†’+* π•œ'} {Οƒ' : π•œ' β†’+* π•œ} [RingHomInvPair Οƒ Οƒ'] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace π•œ' F] [CompleteSpace E] {f : E β†’SL[Οƒ] F} {c : NNReal} (hf : AntilipschitzWith c ⇑f) :
                    (LinearMap.range f).topologicalClosure = LinearMap.range f
                    theorem ContinuousLinearMap.bijective_iff_dense_range_and_antilipschitz {π•œ : Type u_1} {π•œ' : Type u_2} [NontriviallyNormedField π•œ] [NontriviallyNormedField π•œ'] {Οƒ : π•œ β†’+* π•œ'} {Οƒ' : π•œ' β†’+* π•œ} [RingHomInvPair Οƒ Οƒ'] [RingHomInvPair Οƒ' Οƒ] [RingHomIsometric Οƒ] [RingHomIsometric Οƒ'] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace π•œ' F] [CompleteSpace F] [CompleteSpace E] (f : E β†’SL[Οƒ] F) :
                    Function.Bijective ⇑f ↔ (LinearMap.range f).topologicalClosure = ⊀ ∧ βˆƒ (c : NNReal), AntilipschitzWith c ⇑f
                    theorem AntilipschitzWith.completeSpace_range_clm {π•œ : Type u_1} {π•œ' : Type u_2} [NontriviallyNormedField π•œ] [NontriviallyNormedField π•œ'] {Οƒ : π•œ β†’+* π•œ'} {Οƒ' : π•œ' β†’+* π•œ} [RingHomInvPair Οƒ Οƒ'] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace π•œ' F] [CompleteSpace F] [CompleteSpace E] {f : E β†’SL[Οƒ] F} {c : NNReal} (hf : AntilipschitzWith c ⇑f) :