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] : ‖fst 𝕜 E F‖ ≤ 1

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] : ‖snd 𝕜 E F‖ ≤ 1

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) : ‖f.prod g‖ = ‖(f, g)‖

@[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) : ‖f.prod g‖₊ = ‖(f, g)‖₊

noncomputable 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

• ContinuousLinearMap.prodₗᵢ R = { toLinearEquiv := ContinuousLinearMap.prodₗ R, norm_map' := ⋯ }

noncomputable 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.

Equations

• One or more equations did not get rendered due to their size.

@[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₄)) : (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).prodCongr (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).prodCongr (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] : ‖fst 𝕜 E F‖ = 1

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] : ‖snd 𝕜 E F‖ = 1

The operator norm of the second projection E × F → F is exactly 1 if F is nontrivial.