# 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) [] [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) [] [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} [] [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} [] [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} [] [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} [] [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} [] [NormedSpace π E] [NormedSpace π F] [NormedSpace π G] (R : Type u_5) [] [Module R F] [Module 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
• = { toLinearEquiv := , norm_map' := β― }
Instances For
def ContinuousLinearMap.prodMapL (π : Type u_1) [] (Mβ : Type u_5) (Mβ : Type u_6) (Mβ : Type u_7) (Mβ : Type u_8) [] [NormedSpace π Mβ] [] [NormedSpace π Mβ] [] [NormedSpace π Mβ] [] [NormedSpace π Mβ] :
(Mβ βL[π] Mβ) Γ (Mβ βL[π] Mβ) βL[π] Mβ Γ Mβ βL[π] Mβ Γ Mβ

ContinuousLinearMap.prodMap as a continuous linear map.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem ContinuousLinearMap.prodMapL_apply (π : Type u_1) [] {Mβ : Type u_5} {Mβ : Type u_6} {Mβ : Type u_7} {Mβ : Type u_8} [] [NormedSpace π Mβ] [] [NormedSpace π Mβ] [] [NormedSpace π 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) [] {Mβ : Type u_5} {Mβ : Type u_6} {Mβ : Type u_7} {Mβ : Type u_8} [] [NormedSpace π Mβ] [] [NormedSpace π Mβ] [] [NormedSpace π Mβ] [] [NormedSpace π Mβ] {X : Type u_9} [] {f : X β Mβ βL[π] Mβ} {g : X β Mβ βL[π] Mβ} (hf : ) (hg : ) :
Continuous fun (x : X) => (f x).prodMap (g x)
theorem Continuous.prod_map_equivL (π : Type u_1) [] {Mβ : Type u_5} {Mβ : Type u_6} {Mβ : Type u_7} {Mβ : Type u_8} [] [NormedSpace π Mβ] [] [NormedSpace π Mβ] [] [NormedSpace π Mβ] [] [NormedSpace π Mβ] {X : Type u_9} [] {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) [] {Mβ : Type u_5} {Mβ : Type u_6} {Mβ : Type u_7} {Mβ : Type u_8} [] [NormedSpace π Mβ] [] [NormedSpace π Mβ] [] [NormedSpace π Mβ] [] [NormedSpace π Mβ] {X : Type u_9} [] {f : X β Mβ βL[π] Mβ} {g : X β Mβ βL[π] Mβ} {s : Set X} (hf : ) (hg : ) :
ContinuousOn (fun (x : X) => (f x).prodMap (g x)) s
theorem ContinuousOn.prod_map_equivL (π : Type u_1) [] {Mβ : Type u_5} {Mβ : Type u_6} {Mβ : Type u_7} {Mβ : Type u_8} [] [NormedSpace π Mβ] [] [NormedSpace π Mβ] [] [NormedSpace π Mβ] [] [NormedSpace π Mβ] {X : Type u_9} [] {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) [] [NormedSpace π E] [NormedSpace π F] [] :

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) [] [NormedSpace π E] [NormedSpace π F] [] :

The operator norm of the second projection E Γ F β F is exactly 1 if F is nontrivial.