Documentation

Mathlib.Analysis.NormedSpace.BoundedLinearMaps

Bounded linear maps #

This file defines a class stating that a map between normed vector spaces is (bi)linear and continuous. Instead of asking for continuity, the definition takes the equivalent condition (because the space is normed) that ‖f x‖ is bounded by a multiple of ‖x‖. Hence the "bounded" in the name refers to ‖f x‖/‖x‖ rather than ‖f x‖ itself.

Main definitions #

Main theorems #

Notes #

The main use of this file is IsBoundedBilinearMap. The file Analysis.NormedSpace.Multilinear.Basic already expounds the theory of multilinear maps, but the 2-variables case is sufficiently simpler to currently deserve its own treatment.

IsBoundedLinearMap is effectively an unbundled version of ContinuousLinearMap (defined in Topology.Algebra.Module.Basic, theory over normed spaces developed in Analysis.NormedSpace.OperatorNorm), albeit the name disparity. A bundled ContinuousLinearMap is to be preferred over an IsBoundedLinearMap hypothesis. Historical artifact, really.

structure IsBoundedLinearMap (𝕜 : Type u_5) [NormedField 𝕜] {E : Type u_6} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_7} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : EF) extends IsLinearMap :

A function f satisfies IsBoundedLinearMap 𝕜 f if it is linear and satisfies the inequality ‖f x‖ ≤ M * ‖x‖ for some positive constant M.

  • map_add : ∀ (x y : E), f (x + y) = f x + f y
  • map_smul : ∀ (c : 𝕜) (x : E), f (c x) = c f x
  • bound : ∃ (M : ), 0 < M ∀ (x : E), f x M * x
Instances For
    theorem IsBoundedLinearMap.bound {𝕜 : Type u_5} [NormedField 𝕜] {E : Type u_6} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_7} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} (self : IsBoundedLinearMap 𝕜 f) :
    ∃ (M : ), 0 < M ∀ (x : E), f x M * x
    theorem IsLinearMap.with_bound {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} (hf : IsLinearMap 𝕜 f) (M : ) (h : ∀ (x : E), f x M * x) :
    theorem ContinuousLinearMap.isBoundedLinearMap {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E →L[𝕜] F) :

    A continuous linear map satisfies IsBoundedLinearMap

    def IsBoundedLinearMap.toLinearMap {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : EF) (h : IsBoundedLinearMap 𝕜 f) :
    E →ₗ[𝕜] F

    Construct a linear map from a function f satisfying IsBoundedLinearMap 𝕜 f.

    Equations
    Instances For
      def IsBoundedLinearMap.toContinuousLinearMap {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} (hf : IsBoundedLinearMap 𝕜 f) :
      E →L[𝕜] F

      Construct a continuous linear map from IsBoundedLinearMap.

      Equations
      Instances For
        theorem IsBoundedLinearMap.zero {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] :
        IsBoundedLinearMap 𝕜 fun (x : E) => 0
        theorem IsBoundedLinearMap.id {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] :
        IsBoundedLinearMap 𝕜 fun (x : E) => x
        theorem IsBoundedLinearMap.fst {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] :
        IsBoundedLinearMap 𝕜 fun (x : E × F) => x.1
        theorem IsBoundedLinearMap.snd {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] :
        IsBoundedLinearMap 𝕜 fun (x : E × F) => x.2
        theorem IsBoundedLinearMap.smul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} (c : 𝕜) (hf : IsBoundedLinearMap 𝕜 f) :
        theorem IsBoundedLinearMap.neg {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} (hf : IsBoundedLinearMap 𝕜 f) :
        IsBoundedLinearMap 𝕜 fun (e : E) => -f e
        theorem IsBoundedLinearMap.add {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {g : EF} (hf : IsBoundedLinearMap 𝕜 f) (hg : IsBoundedLinearMap 𝕜 g) :
        IsBoundedLinearMap 𝕜 fun (e : E) => f e + g e
        theorem IsBoundedLinearMap.sub {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {g : EF} (hf : IsBoundedLinearMap 𝕜 f) (hg : IsBoundedLinearMap 𝕜 g) :
        IsBoundedLinearMap 𝕜 fun (e : E) => f e - g e
        theorem IsBoundedLinearMap.comp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : EF} {g : FG} (hg : IsBoundedLinearMap 𝕜 g) (hf : IsBoundedLinearMap 𝕜 f) :
        theorem IsBoundedLinearMap.tendsto {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} (x : E) (hf : IsBoundedLinearMap 𝕜 f) :
        Filter.Tendsto f (nhds x) (nhds (f x))
        theorem IsBoundedLinearMap.continuous {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} (hf : IsBoundedLinearMap 𝕜 f) :
        theorem IsBoundedLinearMap.lim_zero_bounded_linear_map {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} (hf : IsBoundedLinearMap 𝕜 f) :
        theorem IsBoundedLinearMap.isBigO_id {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} (h : IsBoundedLinearMap 𝕜 f) (l : Filter E) :
        f =O[l] fun (x : E) => x
        theorem IsBoundedLinearMap.isBigO_comp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {E : Type u_5} {g : FG} (hg : IsBoundedLinearMap 𝕜 g) {f : EF} (l : Filter E) :
        (fun (x' : E) => g (f x')) =O[l] f
        theorem IsBoundedLinearMap.isBigO_sub {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} (h : IsBoundedLinearMap 𝕜 f) (l : Filter E) (x : E) :
        (fun (x' : E) => f (x' - x)) =O[l] fun (x' : E) => x' - x
        theorem isBoundedLinearMap_prod_multilinear {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {ι : Type u_5} [Fintype ι] {E : ιType u_6} [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] :
        IsBoundedLinearMap 𝕜 fun (p : ContinuousMultilinearMap 𝕜 E F × ContinuousMultilinearMap 𝕜 E G) => p.1.prod p.2

        Taking the cartesian product of two continuous multilinear maps is a bounded linear operation.

        theorem isBoundedLinearMap_continuousMultilinearMap_comp_linear {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {ι : Type u_5} [Fintype ι] (g : G →L[𝕜] E) :
        IsBoundedLinearMap 𝕜 fun (f : ContinuousMultilinearMap 𝕜 (fun (x : ι) => E) F) => f.compContinuousLinearMap fun (x : ι) => g

        Given a fixed continuous linear map g, associating to a continuous multilinear map f the continuous multilinear map f (g m₁, ..., g mₙ) is a bounded linear operation.

        We prove some computation rules for continuous (semi-)bilinear maps in their first argument. If f is a continuous bilinear map, to use the corresponding rules for the second argument, use (f _).map_add and similar.

        We have to assume that F and G are normed spaces in this section, to use ContinuousLinearMap.toNormedAddCommGroup, but we don't need to assume this for the first argument of f.

        theorem ContinuousLinearMap.map_add₂ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {R : Type u_5} {𝕜₂ : Type u_6} {𝕜' : Type u_7} [NontriviallyNormedField 𝕜'] [NontriviallyNormedField 𝕜₂] {M : Type u_8} [TopologicalSpace M] {σ₁₂ : 𝕜 →+* 𝕜₂} {G' : Type u_9} [NormedAddCommGroup G'] [NormedSpace 𝕜₂ G'] [NormedSpace 𝕜' G'] [SMulCommClass 𝕜₂ 𝕜' G'] [Semiring R] [AddCommMonoid M] [Module R M] {ρ₁₂ : R →+* 𝕜'} (f : M →SL[ρ₁₂] F →SL[σ₁₂] G') (x : M) (x' : M) (y : F) :
        (f (x + x')) y = (f x) y + (f x') y
        theorem ContinuousLinearMap.map_zero₂ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {R : Type u_5} {𝕜₂ : Type u_6} {𝕜' : Type u_7} [NontriviallyNormedField 𝕜'] [NontriviallyNormedField 𝕜₂] {M : Type u_8} [TopologicalSpace M] {σ₁₂ : 𝕜 →+* 𝕜₂} {G' : Type u_9} [NormedAddCommGroup G'] [NormedSpace 𝕜₂ G'] [NormedSpace 𝕜' G'] [SMulCommClass 𝕜₂ 𝕜' G'] [Semiring R] [AddCommMonoid M] [Module R M] {ρ₁₂ : R →+* 𝕜'} (f : M →SL[ρ₁₂] F →SL[σ₁₂] G') (y : F) :
        (f 0) y = 0
        theorem ContinuousLinearMap.map_smulₛₗ₂ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {R : Type u_5} {𝕜₂ : Type u_6} {𝕜' : Type u_7} [NontriviallyNormedField 𝕜'] [NontriviallyNormedField 𝕜₂] {M : Type u_8} [TopologicalSpace M] {σ₁₂ : 𝕜 →+* 𝕜₂} {G' : Type u_9} [NormedAddCommGroup G'] [NormedSpace 𝕜₂ G'] [NormedSpace 𝕜' G'] [SMulCommClass 𝕜₂ 𝕜' G'] [Semiring R] [AddCommMonoid M] [Module R M] {ρ₁₂ : R →+* 𝕜'} (f : M →SL[ρ₁₂] F →SL[σ₁₂] G') (c : R) (x : M) (y : F) :
        (f (c x)) y = ρ₁₂ c (f x) y
        theorem ContinuousLinearMap.map_sub₂ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {R : Type u_5} {𝕜₂ : Type u_6} {𝕜' : Type u_7} [NontriviallyNormedField 𝕜'] [NontriviallyNormedField 𝕜₂] {M : Type u_8} [TopologicalSpace M] {σ₁₂ : 𝕜 →+* 𝕜₂} {G' : Type u_9} [NormedAddCommGroup G'] [NormedSpace 𝕜₂ G'] [NormedSpace 𝕜' G'] [SMulCommClass 𝕜₂ 𝕜' G'] [Ring R] [AddCommGroup M] [Module R M] {ρ₁₂ : R →+* 𝕜'} (f : M →SL[ρ₁₂] F →SL[σ₁₂] G') (x : M) (x' : M) (y : F) :
        (f (x - x')) y = (f x) y - (f x') y
        theorem ContinuousLinearMap.map_neg₂ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {R : Type u_5} {𝕜₂ : Type u_6} {𝕜' : Type u_7} [NontriviallyNormedField 𝕜'] [NontriviallyNormedField 𝕜₂] {M : Type u_8} [TopologicalSpace M] {σ₁₂ : 𝕜 →+* 𝕜₂} {G' : Type u_9} [NormedAddCommGroup G'] [NormedSpace 𝕜₂ G'] [NormedSpace 𝕜' G'] [SMulCommClass 𝕜₂ 𝕜' G'] [Ring R] [AddCommGroup M] [Module R M] {ρ₁₂ : R →+* 𝕜'} (f : M →SL[ρ₁₂] F →SL[σ₁₂] G') (x : M) (y : F) :
        (f (-x)) y = -(f x) y
        theorem ContinuousLinearMap.map_smul₂ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (f : E →L[𝕜] F →L[𝕜] G) (c : 𝕜) (x : E) (y : F) :
        (f (c x)) y = c (f x) y
        structure IsBoundedBilinearMap (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (f : E × FG) :

        A map f : E × F → G satisfies IsBoundedBilinearMap 𝕜 f if it is bilinear and continuous.

        • add_left : ∀ (x₁ x₂ : E) (y : F), f (x₁ + x₂, y) = f (x₁, y) + f (x₂, y)
        • smul_left : ∀ (c : 𝕜) (x : E) (y : F), f (c x, y) = c f (x, y)
        • add_right : ∀ (x : E) (y₁ y₂ : F), f (x, y₁ + y₂) = f (x, y₁) + f (x, y₂)
        • smul_right : ∀ (c : 𝕜) (x : E) (y : F), f (x, c y) = c f (x, y)
        • bound : C > 0, ∀ (x : E) (y : F), f (x, y) C * x * y
        Instances For
          theorem IsBoundedBilinearMap.add_left {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : E × FG} (self : IsBoundedBilinearMap 𝕜 f) (x₁ : E) (x₂ : E) (y : F) :
          f (x₁ + x₂, y) = f (x₁, y) + f (x₂, y)
          theorem IsBoundedBilinearMap.smul_left {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : E × FG} (self : IsBoundedBilinearMap 𝕜 f) (c : 𝕜) (x : E) (y : F) :
          f (c x, y) = c f (x, y)
          theorem IsBoundedBilinearMap.add_right {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : E × FG} (self : IsBoundedBilinearMap 𝕜 f) (x : E) (y₁ : F) (y₂ : F) :
          f (x, y₁ + y₂) = f (x, y₁) + f (x, y₂)
          theorem IsBoundedBilinearMap.smul_right {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : E × FG} (self : IsBoundedBilinearMap 𝕜 f) (c : 𝕜) (x : E) (y : F) :
          f (x, c y) = c f (x, y)
          theorem IsBoundedBilinearMap.bound {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : E × FG} (self : IsBoundedBilinearMap 𝕜 f) :
          C > 0, ∀ (x : E) (y : F), f (x, y) C * x * y
          theorem ContinuousLinearMap.isBoundedBilinearMap {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (f : E →L[𝕜] F →L[𝕜] G) :
          IsBoundedBilinearMap 𝕜 fun (x : E × F) => (f x.1) x.2
          def IsBoundedBilinearMap.toContinuousLinearMap {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : E × FG} (hf : IsBoundedBilinearMap 𝕜 f) :
          E →L[𝕜] F →L[𝕜] G

          A bounded bilinear map f : E × F → G defines a continuous linear map f : E →L[𝕜] F →L[𝕜] G.

          Equations
          Instances For
            theorem IsBoundedBilinearMap.isBigO {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : E × FG} (h : IsBoundedBilinearMap 𝕜 f) :
            f =O[] fun (p : E × F) => p.1 * p.2
            theorem IsBoundedBilinearMap.isBigO_comp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : E × FG} {α : Type u_5} (H : IsBoundedBilinearMap 𝕜 f) {g : αE} {h : αF} {l : Filter α} :
            (fun (x : α) => f (g x, h x)) =O[l] fun (x : α) => g x * h x
            theorem IsBoundedBilinearMap.isBigO' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : E × FG} (h : IsBoundedBilinearMap 𝕜 f) :
            f =O[] fun (p : E × F) => p * p
            theorem IsBoundedBilinearMap.map_sub_left {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : E × FG} (h : IsBoundedBilinearMap 𝕜 f) {x : E} {y : E} {z : F} :
            f (x - y, z) = f (x, z) - f (y, z)
            theorem IsBoundedBilinearMap.map_sub_right {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : E × FG} (h : IsBoundedBilinearMap 𝕜 f) {x : E} {y : F} {z : F} :
            f (x, y - z) = f (x, y) - f (x, z)
            theorem IsBoundedBilinearMap.continuous {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : E × FG} (h : IsBoundedBilinearMap 𝕜 f) :

            Useful to use together with Continuous.comp₂.

            theorem IsBoundedBilinearMap.continuous_left {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : E × FG} (h : IsBoundedBilinearMap 𝕜 f) {e₂ : F} :
            Continuous fun (e₁ : E) => f (e₁, e₂)
            theorem IsBoundedBilinearMap.continuous_right {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : E × FG} (h : IsBoundedBilinearMap 𝕜 f) {e₁ : E} :
            Continuous fun (e₂ : F) => f (e₁, e₂)
            theorem ContinuousLinearMap.continuous₂ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (f : E →L[𝕜] F →L[𝕜] G) :
            Continuous (Function.uncurry fun (x : E) (y : F) => (f x) y)

            Useful to use together with Continuous.comp₂.

            theorem IsBoundedBilinearMap.isBoundedLinearMap_left {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : E × FG} (h : IsBoundedBilinearMap 𝕜 f) (y : F) :
            IsBoundedLinearMap 𝕜 fun (x : E) => f (x, y)
            theorem IsBoundedBilinearMap.isBoundedLinearMap_right {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : E × FG} (h : IsBoundedBilinearMap 𝕜 f) (x : E) :
            IsBoundedLinearMap 𝕜 fun (y : F) => f (x, y)
            theorem isBoundedBilinearMap_smul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {𝕜' : Type u_5} [NormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {E : Type u_6} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace 𝕜' E] [IsScalarTower 𝕜 𝕜' E] :
            IsBoundedBilinearMap 𝕜 fun (p : 𝕜' × E) => p.1 p.2
            theorem isBoundedBilinearMap_mul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] :
            IsBoundedBilinearMap 𝕜 fun (p : 𝕜 × 𝕜) => p.1 * p.2
            theorem isBoundedBilinearMap_comp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] :
            IsBoundedBilinearMap 𝕜 fun (p : (F →L[𝕜] G) × (E →L[𝕜] F)) => p.1.comp p.2
            theorem ContinuousLinearMap.isBoundedLinearMap_comp_left {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (g : F →L[𝕜] G) :
            IsBoundedLinearMap 𝕜 fun (f : E →L[𝕜] F) => g.comp f
            theorem ContinuousLinearMap.isBoundedLinearMap_comp_right {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (f : E →L[𝕜] F) :
            IsBoundedLinearMap 𝕜 fun (g : F →L[𝕜] G) => g.comp f
            theorem isBoundedBilinearMap_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] :
            IsBoundedBilinearMap 𝕜 fun (p : (E →L[𝕜] F) × E) => p.1 p.2
            theorem isBoundedBilinearMap_smulRight {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] :
            IsBoundedBilinearMap 𝕜 fun (p : (E →L[𝕜] 𝕜) × F) => p.1.smulRight p.2

            The function ContinuousLinearMap.smulRight, associating to a continuous linear map f : E → 𝕜 and a scalar c : F the tensor product f ⊗ c as a continuous linear map from E to F, is a bounded bilinear map.

            theorem isBoundedBilinearMap_compMultilinear {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {ι : Type u_5} {E : ιType u_6} [Fintype ι] [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] :
            IsBoundedBilinearMap 𝕜 fun (p : (F →L[𝕜] G) × ContinuousMultilinearMap 𝕜 E F) => p.1.compContinuousMultilinearMap p.2

            The composition of a continuous linear map with a continuous multilinear map is a bounded bilinear operation.

            def IsBoundedBilinearMap.linearDeriv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : E × FG} (h : IsBoundedBilinearMap 𝕜 f) (p : E × F) :
            E × F →ₗ[𝕜] G

            Definition of the derivative of a bilinear map f, given at a point p by q ↦ f(p.1, q.2) + f(q.1, p.2) as in the standard formula for the derivative of a product. We define this function here as a linear map E × F →ₗ[𝕜] G, then IsBoundedBilinearMap.deriv strengthens it to a continuous linear map E × F →L[𝕜] G.

            Equations
            • h.linearDeriv p = (h.toContinuousLinearMap.deriv₂ p)
            Instances For
              def IsBoundedBilinearMap.deriv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : E × FG} (h : IsBoundedBilinearMap 𝕜 f) (p : E × F) :
              E × F →L[𝕜] G

              The derivative of a bounded bilinear map at a point p : E × F, as a continuous linear map from E × F to G. The statement that this is indeed the derivative of f is IsBoundedBilinearMap.hasFDerivAt in Analysis.Calculus.FDeriv.

              Equations
              • h.deriv p = h.toContinuousLinearMap.deriv₂ p
              Instances For
                @[simp]
                theorem IsBoundedBilinearMap.deriv_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : E × FG} (h : IsBoundedBilinearMap 𝕜 f) (p : E × F) (q : E × F) :
                (h.deriv p) q = f (p.1, q.2) + f (q.1, p.2)
                theorem ContinuousLinearMap.mulLeftRight_isBoundedBilinear (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (𝕜' : Type u_5) [NormedRing 𝕜'] [NormedAlgebra 𝕜 𝕜'] :
                IsBoundedBilinearMap 𝕜 fun (p : 𝕜' × 𝕜') => ((ContinuousLinearMap.mulLeftRight 𝕜 𝕜') p.1) p.2

                The function ContinuousLinearMap.mulLeftRight : 𝕜' × 𝕜' → (𝕜' →L[𝕜] 𝕜') is a bounded bilinear map.

                theorem IsBoundedBilinearMap.isBoundedLinearMap_deriv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : E × FG} (h : IsBoundedBilinearMap 𝕜 f) :
                IsBoundedLinearMap 𝕜 fun (p : E × F) => h.deriv p

                Given a bounded bilinear map f, the map associating to a point p the derivative of f at p is itself a bounded linear map.

                theorem Continuous.clm_comp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {X : Type u_5} [TopologicalSpace X] {g : XF →L[𝕜] G} {f : XE →L[𝕜] F} (hg : Continuous g) (hf : Continuous f) :
                Continuous fun (x : X) => (g x).comp (f x)
                theorem ContinuousOn.clm_comp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {X : Type u_5} [TopologicalSpace X] {g : XF →L[𝕜] G} {f : XE →L[𝕜] F} {s : Set X} (hg : ContinuousOn g s) (hf : ContinuousOn f s) :
                ContinuousOn (fun (x : X) => (g x).comp (f x)) s
                theorem Continuous.clm_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {X : Type u_5} [TopologicalSpace X] {f : XE →L[𝕜] F} {g : XE} (hf : Continuous f) (hg : Continuous g) :
                Continuous fun (x : X) => (f x) (g x)
                theorem ContinuousOn.clm_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {X : Type u_5} [TopologicalSpace X] {f : XE →L[𝕜] F} {g : XE} {s : Set X} (hf : ContinuousOn f s) (hg : ContinuousOn g s) :
                ContinuousOn (fun (x : X) => (f x) (g x)) s

                The set of continuous linear equivalences between two Banach spaces is open #

                In this section we establish that the set of continuous linear equivalences between two Banach spaces is an open subset of the space of linear maps between them.

                theorem ContinuousLinearEquiv.isOpen {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace E] :
                IsOpen (Set.range ContinuousLinearEquiv.toContinuousLinearMap)
                theorem ContinuousLinearEquiv.nhds {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace E] (e : E ≃L[𝕜] F) :
                Set.range ContinuousLinearEquiv.toContinuousLinearMap nhds e