Documentation

Mathlib.Analysis.NormedSpace.OperatorNorm.Prod

Operator norm: Cartesian products #

Interaction of operator norm with Cartesian products.

theorem ContinuousLinearMap.norm_fst_le (π•œ : Type u_1) (E : Type u_2) (F : Type u_3) [NontriviallyNormedField π•œ] [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NormedSpace π•œ E] [NormedSpace π•œ F] :

The operator norm of the first projection E Γ— F β†’ E is at most 1. (It is 0 if E is zero, so the inequality cannot be improved without further assumptions.)

theorem ContinuousLinearMap.norm_snd_le (π•œ : Type u_1) (E : Type u_2) (F : Type u_3) [NontriviallyNormedField π•œ] [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NormedSpace π•œ E] [NormedSpace π•œ F] :

The operator norm of the second projection E Γ— F β†’ F is at most 1. (It is 0 if F is zero, so the inequality cannot be improved without further assumptions.)

@[simp]
theorem ContinuousLinearMap.opNorm_prod {π•œ : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField π•œ] [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [SeminormedAddCommGroup G] [NormedSpace π•œ E] [NormedSpace π•œ F] [NormedSpace π•œ G] (f : E β†’L[π•œ] F) (g : E β†’L[π•œ] G) :
@[deprecated ContinuousLinearMap.opNorm_prod]
theorem ContinuousLinearMap.op_norm_prod {π•œ : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField π•œ] [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [SeminormedAddCommGroup G] [NormedSpace π•œ E] [NormedSpace π•œ F] [NormedSpace π•œ G] (f : E β†’L[π•œ] F) (g : E β†’L[π•œ] G) :

Alias of ContinuousLinearMap.opNorm_prod.

@[simp]
theorem ContinuousLinearMap.opNNNorm_prod {π•œ : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField π•œ] [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [SeminormedAddCommGroup G] [NormedSpace π•œ E] [NormedSpace π•œ F] [NormedSpace π•œ G] (f : E β†’L[π•œ] F) (g : E β†’L[π•œ] G) :
@[deprecated ContinuousLinearMap.opNNNorm_prod]
theorem ContinuousLinearMap.op_nnnorm_prod {π•œ : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField π•œ] [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [SeminormedAddCommGroup G] [NormedSpace π•œ E] [NormedSpace π•œ F] [NormedSpace π•œ G] (f : E β†’L[π•œ] F) (g : E β†’L[π•œ] G) :

Alias of ContinuousLinearMap.opNNNorm_prod.

def ContinuousLinearMap.prodβ‚—α΅’ {π•œ : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField π•œ] [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [SeminormedAddCommGroup G] [NormedSpace π•œ E] [NormedSpace π•œ F] [NormedSpace π•œ G] (R : Type u_5) [Semiring R] [Module R F] [Module R G] [ContinuousConstSMul R F] [ContinuousConstSMul R G] [SMulCommClass π•œ R F] [SMulCommClass π•œ R G] :
(E β†’L[π•œ] F) Γ— (E β†’L[π•œ] G) ≃ₗᡒ[R] E β†’L[π•œ] F Γ— G

ContinuousLinearMap.prod as a LinearIsometryEquiv.

Equations
Instances For
    def ContinuousLinearMap.prodMapL (π•œ : Type u_1) [NontriviallyNormedField π•œ] (M₁ : Type u_5) (Mβ‚‚ : Type u_6) (M₃ : Type u_7) (Mβ‚„ : Type u_8) [SeminormedAddCommGroup M₁] [NormedSpace π•œ M₁] [SeminormedAddCommGroup Mβ‚‚] [NormedSpace π•œ Mβ‚‚] [SeminormedAddCommGroup M₃] [NormedSpace π•œ M₃] [SeminormedAddCommGroup Mβ‚„] [NormedSpace π•œ Mβ‚„] :
    (M₁ β†’L[π•œ] Mβ‚‚) Γ— (M₃ β†’L[π•œ] Mβ‚„) β†’L[π•œ] M₁ Γ— M₃ β†’L[π•œ] Mβ‚‚ Γ— Mβ‚„

    ContinuousLinearMap.prodMap as a continuous linear map.

    Instances For
      @[simp]
      theorem ContinuousLinearMap.prodMapL_apply (π•œ : Type u_1) [NontriviallyNormedField π•œ] {M₁ : Type u_5} {Mβ‚‚ : Type u_6} {M₃ : Type u_7} {Mβ‚„ : Type u_8} [SeminormedAddCommGroup M₁] [NormedSpace π•œ M₁] [SeminormedAddCommGroup Mβ‚‚] [NormedSpace π•œ Mβ‚‚] [SeminormedAddCommGroup M₃] [NormedSpace π•œ M₃] [SeminormedAddCommGroup Mβ‚„] [NormedSpace π•œ Mβ‚„] (p : (M₁ β†’L[π•œ] Mβ‚‚) Γ— (M₃ β†’L[π•œ] Mβ‚„)) :
      (ContinuousLinearMap.prodMapL π•œ M₁ Mβ‚‚ M₃ Mβ‚„) p = p.1.prodMap p.2
      theorem Continuous.prod_mapL (π•œ : Type u_1) [NontriviallyNormedField π•œ] {M₁ : Type u_5} {Mβ‚‚ : Type u_6} {M₃ : Type u_7} {Mβ‚„ : Type u_8} [SeminormedAddCommGroup M₁] [NormedSpace π•œ M₁] [SeminormedAddCommGroup Mβ‚‚] [NormedSpace π•œ Mβ‚‚] [SeminormedAddCommGroup M₃] [NormedSpace π•œ M₃] [SeminormedAddCommGroup Mβ‚„] [NormedSpace π•œ Mβ‚„] {X : Type u_9} [TopologicalSpace X] {f : X β†’ M₁ β†’L[π•œ] Mβ‚‚} {g : X β†’ M₃ β†’L[π•œ] Mβ‚„} (hf : Continuous f) (hg : Continuous g) :
      Continuous fun (x : X) => (f x).prodMap (g x)
      theorem Continuous.prod_map_equivL (π•œ : Type u_1) [NontriviallyNormedField π•œ] {M₁ : Type u_5} {Mβ‚‚ : Type u_6} {M₃ : Type u_7} {Mβ‚„ : Type u_8} [SeminormedAddCommGroup M₁] [NormedSpace π•œ M₁] [SeminormedAddCommGroup Mβ‚‚] [NormedSpace π•œ Mβ‚‚] [SeminormedAddCommGroup M₃] [NormedSpace π•œ M₃] [SeminormedAddCommGroup Mβ‚„] [NormedSpace π•œ Mβ‚„] {X : Type u_9} [TopologicalSpace X] {f : X β†’ M₁ ≃L[π•œ] Mβ‚‚} {g : X β†’ M₃ ≃L[π•œ] Mβ‚„} (hf : Continuous fun (x : X) => ↑(f x)) (hg : Continuous fun (x : X) => ↑(g x)) :
      Continuous fun (x : X) => ↑((f x).prod (g x))
      theorem ContinuousOn.prod_mapL (π•œ : Type u_1) [NontriviallyNormedField π•œ] {M₁ : Type u_5} {Mβ‚‚ : Type u_6} {M₃ : Type u_7} {Mβ‚„ : Type u_8} [SeminormedAddCommGroup M₁] [NormedSpace π•œ M₁] [SeminormedAddCommGroup Mβ‚‚] [NormedSpace π•œ Mβ‚‚] [SeminormedAddCommGroup M₃] [NormedSpace π•œ M₃] [SeminormedAddCommGroup Mβ‚„] [NormedSpace π•œ Mβ‚„] {X : Type u_9} [TopologicalSpace X] {f : X β†’ M₁ β†’L[π•œ] Mβ‚‚} {g : X β†’ M₃ β†’L[π•œ] Mβ‚„} {s : Set X} (hf : ContinuousOn f s) (hg : ContinuousOn g s) :
      ContinuousOn (fun (x : X) => (f x).prodMap (g x)) s
      theorem ContinuousOn.prod_map_equivL (π•œ : Type u_1) [NontriviallyNormedField π•œ] {M₁ : Type u_5} {Mβ‚‚ : Type u_6} {M₃ : Type u_7} {Mβ‚„ : Type u_8} [SeminormedAddCommGroup M₁] [NormedSpace π•œ M₁] [SeminormedAddCommGroup Mβ‚‚] [NormedSpace π•œ Mβ‚‚] [SeminormedAddCommGroup M₃] [NormedSpace π•œ M₃] [SeminormedAddCommGroup Mβ‚„] [NormedSpace π•œ Mβ‚„] {X : Type u_9} [TopologicalSpace X] {f : X β†’ M₁ ≃L[π•œ] Mβ‚‚} {g : X β†’ M₃ ≃L[π•œ] Mβ‚„} {s : Set X} (hf : ContinuousOn (fun (x : X) => ↑(f x)) s) (hg : ContinuousOn (fun (x : X) => ↑(g x)) s) :
      ContinuousOn (fun (x : X) => ↑((f x).prod (g x))) s
      @[simp]
      theorem ContinuousLinearMap.norm_fst (π•œ : Type u_1) (E : Type u_2) (F : Type u_3) [NontriviallyNormedField π•œ] [NormedAddCommGroup E] [NormedSpace π•œ E] [SeminormedAddCommGroup F] [NormedSpace π•œ F] [Nontrivial E] :

      The operator norm of the first projection E Γ— F β†’ E is exactly 1 if E is nontrivial.

      @[simp]
      theorem ContinuousLinearMap.norm_snd (π•œ : Type u_1) (E : Type u_2) (F : Type u_3) [NontriviallyNormedField π•œ] [SeminormedAddCommGroup E] [NormedSpace π•œ E] [NormedAddCommGroup F] [NormedSpace π•œ F] [Nontrivial F] :

      The operator norm of the second projection E Γ— F β†’ F is exactly 1 if F is nontrivial.