Exact source: Mathlib/Analysis/Normed/Operator/Bilinear.lean
Pinned GitHub source · Raw UTF-8 source
Back to A volume-normalized linear contraction obtained by a limit
1/-2Copyright (c) 2019 Jan-David Salchow. All rights reserved.3Released under Apache 2.0 license as described in the file LICENSE.4Authors: Jan-David Salchow, Sébastien Gouëzel, Jean Lo5-/6module78public import Mathlib.Analysis.Normed.Operator.Basic9public import Mathlib.Analysis.Normed.Operator.LinearIsometry10public import Mathlib.Analysis.Normed.Operator.ContinuousLinearMap1112/-!13# Operator norm: bilinear maps1415This file contains lemmas concerning operator norm as applied to bilinear maps `E × F → G`,16interpreted as linear maps `E → F → G` as usual (and similarly for semilinear variants).1718-/1920@[expose] public section2122suppress_compilation2324open Bornology25open Filter hiding map_smul26open scoped NNReal Topology Uniformity2728-- the `ₗ` subscript variables are for special cases about linear (as opposed to semilinear) maps29variable {𝕜 𝕜₂ 𝕜₃ E Eₗ F Fₗ G Gₗ 𝓕 : Type*}3031section SemiNormed3233open Metric ContinuousLinearMap3435variable [SeminormedAddCommGroup E] [SeminormedAddCommGroup Eₗ] [SeminormedAddCommGroup F]36 [SeminormedAddCommGroup Fₗ] [SeminormedAddCommGroup G] [SeminormedAddCommGroup Gₗ]3738variable [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NontriviallyNormedField 𝕜₃]39 [NormedSpace 𝕜 E] [NormedSpace 𝕜 Eₗ] [NormedSpace 𝕜₂ F] [NormedSpace 𝕜 Fₗ] [NormedSpace 𝕜₃ G]40 [NormedSpace 𝕜 Gₗ] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃}41 [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃]4243variable [FunLike 𝓕 E F]4445namespace ContinuousLinearMap4647section OpNorm4849open Set Real5051theorem opNorm_ext [RingHomIsometric σ₁₃] (f : E →SL[σ₁₂] F) (g : E →SL[σ₁₃] G)52 (h : ∀ x, ‖f x‖ = ‖g x‖) : ‖f‖ = ‖g‖ :=53 opNorm_eq_of_bounds (norm_nonneg _)54 (fun x => by55 rw [h x]56 exact le_opNorm _ _)57 fun c hc h₂ =>58 opNorm_le_bound _ hc fun z => by59 rw [← h z]60 exact h₂ z616263variable [RingHomIsometric σ₂₃]6465theorem opNorm_le_bound₂ (f : E →SL[σ₁₃] F →SL[σ₂₃] G) {C : ℝ} (h0 : 0 ≤ C)66 (hC : ∀ x y, ‖f x y‖ ≤ C * ‖x‖ * ‖y‖) : ‖f‖ ≤ C :=67 f.opNorm_le_bound h0 fun x => (f x).opNorm_le_bound (by positivity) <| hC x686970theorem le_opNorm₂ [RingHomIsometric σ₁₃] (f : E →SL[σ₁₃] F →SL[σ₂₃] G) (x : E) (y : F) :71 ‖f x y‖ ≤ ‖f‖ * ‖x‖ * ‖y‖ :=72 (f x).le_of_opNorm_le (f.le_opNorm x) y737475theorem le_of_opNorm₂_le_of_le [RingHomIsometric σ₁₃] (f : E →SL[σ₁₃] F →SL[σ₂₃] G) {x : E} {y : F}76 {a b c : ℝ} (hf : ‖f‖ ≤ a) (hx : ‖x‖ ≤ b) (hy : ‖y‖ ≤ c) :77 ‖f x y‖ ≤ a * b * c :=78 (f x).le_of_opNorm_le_of_le (f.le_of_opNorm_le_of_le hf hx) hy798081end OpNorm8283end ContinuousLinearMap8485namespace LinearMap8687lemma norm_mkContinuous₂_aux (f : E →ₛₗ[σ₁₃] F →ₛₗ[σ₂₃] G) (C : ℝ)88 (h : ∀ x y, ‖f x y‖ ≤ C * ‖x‖ * ‖y‖) (x : E) :89 ‖(f x).mkContinuous (C * ‖x‖) (h x)‖ ≤ max C 0 * ‖x‖ :=90 (mkContinuous_norm_le' (f x) (h x)).trans_eq <| by91 rw [max_mul_of_nonneg _ _ (norm_nonneg x), zero_mul]9293variable [RingHomIsometric σ₂₃]9495/-- Create a bilinear map (represented as a map `E →L[𝕜] F →L[𝕜] G`) from the corresponding linear96map and existence of a bound on the norm of the image. The linear map can be constructed using97`LinearMap.mk₂`.9899If you have an explicit bound, use `LinearMap.mkContinuous₂` instead, as a norm estimate will100follow automatically in `LinearMap.mkContinuous₂_norm_le`. -/101def mkContinuousOfExistsBound₂ (f : E →ₛₗ[σ₁₃] F →ₛₗ[σ₂₃] G)102 (h : ∃ C, ∀ x y, ‖f x y‖ ≤ C * ‖x‖ * ‖y‖) : E →SL[σ₁₃] F →SL[σ₂₃] G :=103 LinearMap.mkContinuousOfExistsBound104 { toFun := fun x => (f x).mkContinuousOfExistsBound <| let ⟨C, hC⟩ := h; ⟨C * ‖x‖, hC x⟩105 map_add' := fun x y => by106 ext z107 simp108 map_smul' := fun c x => by109 ext z110 simp } <|111 let ⟨C, hC⟩ := h; ⟨max C 0, norm_mkContinuous₂_aux f C hC⟩112113/-- Create a bilinear map (represented as a map `E →L[𝕜] F →L[𝕜] G`) from the corresponding linear114map and a bound on the norm of the image. The linear map can be constructed using115`LinearMap.mk₂`. Lemmas `LinearMap.mkContinuous₂_norm_le'` and `LinearMap.mkContinuous₂_norm_le`116provide estimates on the norm of an operator constructed using this function. -/117def mkContinuous₂ (f : E →ₛₗ[σ₁₃] F →ₛₗ[σ₂₃] G) (C : ℝ) (hC : ∀ x y, ‖f x y‖ ≤ C * ‖x‖ * ‖y‖) :118 E →SL[σ₁₃] F →SL[σ₂₃] G :=119 mkContinuousOfExistsBound₂ f ⟨C, hC⟩120121@[simp]122theorem mkContinuous₂_apply (f : E →ₛₗ[σ₁₃] F →ₛₗ[σ₂₃] G) {C : ℝ}123 (hC : ∀ x y, ‖f x y‖ ≤ C * ‖x‖ * ‖y‖) (x : E) (y : F) : f.mkContinuous₂ C hC x y = f x y :=124 rfl125126theorem mkContinuous₂_norm_le' (f : E →ₛₗ[σ₁₃] F →ₛₗ[σ₂₃] G) {C : ℝ}127 (hC : ∀ x y, ‖f x y‖ ≤ C * ‖x‖ * ‖y‖) : ‖f.mkContinuous₂ C hC‖ ≤ max C 0 :=128 mkContinuous_norm_le _ (le_max_iff.2 <| Or.inr le_rfl) (norm_mkContinuous₂_aux f C hC)129130theorem mkContinuous₂_norm_le (f : E →ₛₗ[σ₁₃] F →ₛₗ[σ₂₃] G) {C : ℝ} (h0 : 0 ≤ C)131 (hC : ∀ x y, ‖f x y‖ ≤ C * ‖x‖ * ‖y‖) : ‖f.mkContinuous₂ C hC‖ ≤ C :=132 (f.mkContinuous₂_norm_le' hC).trans_eq <| max_eq_left h0133134end LinearMap135136namespace ContinuousLinearMap137138variable [RingHomIsometric σ₂₃] [RingHomIsometric σ₁₃]139140/-- Flip the order of arguments of a continuous bilinear map.141For a version bundled as `LinearIsometryEquiv`, see142`ContinuousLinearMap.flipL`. -/143def flip (f : E →SL[σ₁₃] F →SL[σ₂₃] G) : F →SL[σ₂₃] E →SL[σ₁₃] G :=144 LinearMap.mkContinuous₂145 (LinearMap.mk₂'ₛₗ σ₂₃ σ₁₃ (fun y x => f x y) (fun x y z => (f z).map_add x y)146 (fun c y x => (f x).map_smulₛₗ c y) (fun z x y => by simp only [f.map_add, add_apply])147 (fun c y x => by simp only [f.map_smulₛₗ, smul_apply]))148 ‖f‖ fun y x => (f.le_opNorm₂ x y).trans_eq <| by simp only [mul_right_comm]149150private theorem le_norm_flip (f : E →SL[σ₁₃] F →SL[σ₂₃] G) : ‖f‖ ≤ ‖flip f‖ :=151 f.opNorm_le_bound₂ (norm_nonneg f.flip) fun x y => by152 rw [mul_right_comm]153 exact (flip f).le_opNorm₂ y x154155@[simp]156theorem flip_apply (f : E →SL[σ₁₃] F →SL[σ₂₃] G) (x : E) (y : F) : f.flip y x = f x y :=157 rfl158159@[simp]160theorem flip_flip (f : E →SL[σ₁₃] F →SL[σ₂₃] G) : f.flip.flip = f := by161 ext162 rfl163164@[simp]165theorem opNorm_flip (f : E →SL[σ₁₃] F →SL[σ₂₃] G) : ‖f.flip‖ = ‖f‖ :=166 le_antisymm (by simpa only [flip_flip] using le_norm_flip f.flip) (le_norm_flip f)167168@[simp]169lemma flip_zero : flip (0 : E →SL[σ₁₃] F →SL[σ₂₃] G) = 0 := rfl170171@[simp]172theorem flip_add (f g : E →SL[σ₁₃] F →SL[σ₂₃] G) : (f + g).flip = f.flip + g.flip :=173 rfl174175@[simp]176theorem flip_smul (c : 𝕜₃) (f : E →SL[σ₁₃] F →SL[σ₂₃] G) : (c • f).flip = c • f.flip :=177 rfl178179variable (E F G σ₁₃ σ₂₃)180181/-- Flip the order of arguments of a continuous bilinear map.182This is a version bundled as a `LinearIsometryEquiv`.183For an unbundled version see `ContinuousLinearMap.flip`. -/184def flipₗᵢ' : (E →SL[σ₁₃] F →SL[σ₂₃] G) ≃ₗᵢ[𝕜₃] F →SL[σ₂₃] E →SL[σ₁₃] G where185 toFun := flip186 invFun := flip187 map_add' := flip_add188 map_smul' := flip_smul189 left_inv := flip_flip190 right_inv := flip_flip191 norm_map' := opNorm_flip192193variable {E F G σ₁₃ σ₂₃}194195@[simp]196theorem flipₗᵢ'_symm : (flipₗᵢ' E F G σ₂₃ σ₁₃).symm = flipₗᵢ' F E G σ₁₃ σ₂₃ :=197 rfl198199@[simp]200theorem coe_flipₗᵢ' : ⇑(flipₗᵢ' E F G σ₂₃ σ₁₃) = flip :=201 rfl202203variable (𝕜 E Fₗ Gₗ)204205/-- Flip the order of arguments of a continuous bilinear map.206This is a version bundled as a `LinearIsometryEquiv`.207For an unbundled version see `ContinuousLinearMap.flip`. -/208def flipₗᵢ : (E →L[𝕜] Fₗ →L[𝕜] Gₗ) ≃ₗᵢ[𝕜] Fₗ →L[𝕜] E →L[𝕜] Gₗ where209 toFun := flip210 invFun := flip211 map_add' := flip_add212 map_smul' := flip_smul213 left_inv := flip_flip214 right_inv := flip_flip215 norm_map' := opNorm_flip216217variable {𝕜 E Fₗ Gₗ}218219@[simp]220theorem flipₗᵢ_symm : (flipₗᵢ 𝕜 E Fₗ Gₗ).symm = flipₗᵢ 𝕜 Fₗ E Gₗ :=221 rfl222223@[simp]224theorem coe_flipₗᵢ : ⇑(flipₗᵢ 𝕜 E Fₗ Gₗ) = flip :=225 rfl226227variable (F σ₁₂)228variable [RingHomIsometric σ₁₂]229230/-- The continuous semilinear map obtained by applying a continuous semilinear map at a given231vector.232233This is the continuous version of `LinearMap.applyₗ`. -/234def apply' : E →SL[σ₁₂] (E →SL[σ₁₂] F) →L[𝕜₂] F :=235 flip (.id 𝕜₂ (E →SL[σ₁₂] F))236237variable {F σ₁₂}238239@[simp]240theorem apply_apply' (v : E) (f : E →SL[σ₁₂] F) : apply' F σ₁₂ v f = f v :=241 rfl242243variable (𝕜 Fₗ)244245/-- The continuous semilinear map obtained by applying a continuous semilinear map at a given246vector.247248This is the continuous version of `LinearMap.applyₗ`. -/249def apply : E →L[𝕜] (E →L[𝕜] Fₗ) →L[𝕜] Fₗ :=250 flip (.id 𝕜 (E →L[𝕜] Fₗ))251252variable {𝕜 Fₗ}253254@[simp]255theorem apply_apply (v : E) (f : E →L[𝕜] Fₗ) : apply 𝕜 Fₗ v f = f v :=256 rfl257258variable (σ₁₂ σ₂₃ E F G)259260261/-- Composition of continuous semilinear maps as a continuous semibilinear map. -/262def compSL : (F →SL[σ₂₃] G) →L[𝕜₃] (E →SL[σ₁₂] F) →SL[σ₂₃] E →SL[σ₁₃] G :=263 LinearMap.mkContinuous₂264 (LinearMap.mk₂'ₛₗ (RingHom.id 𝕜₃) σ₂₃ comp add_comp smul_comp comp_add fun c f g => by265 ext266 simp only [map_smulₛₗ, comp_apply, smul_apply])267 1 fun f g => by simpa only [one_mul] using! opNorm_comp_le f g268269theorem norm_compSL_le : ‖compSL E F G σ₁₂ σ₂₃‖ ≤ 1 :=270 LinearMap.mkContinuous₂_norm_le _ zero_le_one _271272variable {σ₁₂ σ₂₃ E F G}273274@[simp]275theorem compSL_apply (f : F →SL[σ₂₃] G) (g : E →SL[σ₁₂] F) : compSL E F G σ₁₂ σ₂₃ f g = f.comp g :=276 rfl277278theorem _root_.Continuous.const_clm_comp {X} [TopologicalSpace X] {f : X → E →SL[σ₁₂] F}279 (hf : Continuous f) (g : F →SL[σ₂₃] G) :280 Continuous (fun x => g.comp (f x) : X → E →SL[σ₁₃] G) :=281 (compSL E F G σ₁₂ σ₂₃ g).continuous.comp hf282283-- Giving the implicit argument speeds up elaboration significantly284theorem _root_.Continuous.clm_comp_const {X} [TopologicalSpace X] {g : X → F →SL[σ₂₃] G}285 (hg : Continuous g) (f : E →SL[σ₁₂] F) :286 Continuous (fun x => (g x).comp f : X → E →SL[σ₁₃] G) :=287 (@ContinuousLinearMap.flip _ _ _ _ _ (E →SL[σ₁₃] G) _ _ _ _ _ _ _ _ _ _ _ _ _288 (compSL E F G σ₁₂ σ₂₃) f).continuous.comp hg289290variable (𝕜 σ₁₂ σ₂₃ E Fₗ Gₗ)291292/-- Composition of continuous linear maps as a continuous bilinear map. -/293def compL : (Fₗ →L[𝕜] Gₗ) →L[𝕜] (E →L[𝕜] Fₗ) →L[𝕜] E →L[𝕜] Gₗ :=294 compSL E Fₗ Gₗ (RingHom.id 𝕜) (RingHom.id 𝕜)295296theorem norm_compL_le : ‖compL 𝕜 E Fₗ Gₗ‖ ≤ 1 :=297 norm_compSL_le _ _ _ _ _298299@[simp]300theorem compL_apply (f : Fₗ →L[𝕜] Gₗ) (g : E →L[𝕜] Fₗ) : compL 𝕜 E Fₗ Gₗ f g = f.comp g :=301 rfl302303variable (Eₗ) {𝕜 E Fₗ Gₗ}304305/-- Apply `L(x,-)` pointwise to bilinear maps, as a continuous bilinear map -/306@[simps! apply]307def precompR (L : E →L[𝕜] Fₗ →L[𝕜] Gₗ) : E →L[𝕜] (Eₗ →L[𝕜] Fₗ) →L[𝕜] Eₗ →L[𝕜] Gₗ :=308 compL 𝕜 Eₗ Fₗ Gₗ ∘L L309310/-- Apply `L(-,y)` pointwise to bilinear maps, as a continuous bilinear map -/311def precompL (L : E →L[𝕜] Fₗ →L[𝕜] Gₗ) : (Eₗ →L[𝕜] E) →L[𝕜] Fₗ →L[𝕜] Eₗ →L[𝕜] Gₗ :=312 (precompR Eₗ (flip L)).flip313314@[simp] lemma precompL_apply (L : E →L[𝕜] Fₗ →L[𝕜] Gₗ) (u : Eₗ →L[𝕜] E) (f : Fₗ) (g : Eₗ) :315 precompL Eₗ L u f g = L (u g) f := rfl316317theorem norm_precompR_le (L : E →L[𝕜] Fₗ →L[𝕜] Gₗ) : ‖precompR Eₗ L‖ ≤ ‖L‖ :=318 calc319 ‖precompR Eₗ L‖ ≤ ‖compL 𝕜 Eₗ Fₗ Gₗ‖ * ‖L‖ := opNorm_comp_le _ _320 _ ≤ 1 * ‖L‖ := by gcongr; apply norm_compL_le321 _ = ‖L‖ := by rw [one_mul]322323theorem norm_precompL_le (L : E →L[𝕜] Fₗ →L[𝕜] Gₗ) : ‖precompL Eₗ L‖ ≤ ‖L‖ := by324 rw [precompL, opNorm_flip, ← opNorm_flip L]325 exact norm_precompR_le _ L.flip326327end ContinuousLinearMap328329variable {σ₂₁ : 𝕜₂ →+* 𝕜} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂]330331namespace ContinuousLinearMap332333variable {E' F' : Type*} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F']334variable {𝕜₁' : Type*} {𝕜₂' : Type*} [NontriviallyNormedField 𝕜₁'] [NontriviallyNormedField 𝕜₂']335 [NormedSpace 𝕜₁' E'] [NormedSpace 𝕜₂' F'] {σ₁' : 𝕜₁' →+* 𝕜} {σ₁₃' : 𝕜₁' →+* 𝕜₃} {σ₂' : 𝕜₂' →+* 𝕜₂}336 {σ₂₃' : 𝕜₂' →+* 𝕜₃} [RingHomCompTriple σ₁' σ₁₃ σ₁₃'] [RingHomCompTriple σ₂' σ₂₃ σ₂₃']337 [RingHomIsometric σ₂₃] [RingHomIsometric σ₁₃'] [RingHomIsometric σ₂₃']338339/-- Compose a bilinear map `E →SL[σ₁₃] F →SL[σ₂₃] G` with two linear maps340`E' →SL[σ₁'] E` and `F' →SL[σ₂'] F`. -/341def bilinearComp (f : E →SL[σ₁₃] F →SL[σ₂₃] G) (gE : E' →SL[σ₁'] E) (gF : F' →SL[σ₂'] F) :342 E' →SL[σ₁₃'] F' →SL[σ₂₃'] G :=343 ((f.comp gE).flip.comp gF).flip344345@[simp]346theorem bilinearComp_apply (f : E →SL[σ₁₃] F →SL[σ₂₃] G) (gE : E' →SL[σ₁'] E) (gF : F' →SL[σ₂'] F)347 (x : E') (y : F') : f.bilinearComp gE gF x y = f (gE x) (gF y) :=348 rfl349350@[simp]351lemma bilinearComp_zero {gE : E' →SL[σ₁'] E} {gF : F' →SL[σ₂'] F} :352 bilinearComp (0 : E →SL[σ₁₃] F →SL[σ₂₃] G) gE gF = 0 := rfl353354@[simp]355lemma bilinearComp_zero_left {f : E →SL[σ₁₃] F →SL[σ₂₃] G} {gF : F' →SL[σ₂'] F} :356 bilinearComp f (0 : E' →SL[σ₁'] E) gF = 0 := by ext; simp357358@[simp]359lemma bilinearComp_zero_right {f : E →SL[σ₁₃] F →SL[σ₂₃] G} {gE : E' →SL[σ₁'] E} :360 bilinearComp f gE (0 : F' →SL[σ₂'] F) = 0 := by ext; simp361362variable [RingHomIsometric σ₁₃] [RingHomIsometric σ₁'] [RingHomIsometric σ₂']363364/-- Derivative of a continuous bilinear map `f : E →L[𝕜] F →L[𝕜] G` interpreted as a map `E × F → G`365at point `p : E × F` evaluated at `q : E × F`, as a continuous bilinear map. -/366def deriv₂ (f : E →L[𝕜] Fₗ →L[𝕜] Gₗ) : E × Fₗ →L[𝕜] E × Fₗ →L[𝕜] Gₗ :=367 f.bilinearComp (fst _ _ _) (snd _ _ _) + f.flip.bilinearComp (snd _ _ _) (fst _ _ _)368369@[simp]370theorem coe_deriv₂ (f : E →L[𝕜] Fₗ →L[𝕜] Gₗ) (p : E × Fₗ) :371 ⇑(f.deriv₂ p) = fun q : E × Fₗ => f p.1 q.2 + f q.1 p.2 :=372 rfl373374theorem map_add_add (f : E →L[𝕜] Fₗ →L[𝕜] Gₗ) (x x' : E) (y y' : Fₗ) :375 f (x + x') (y + y') = f x y + f.deriv₂ (x, y) (x', y') + f x' y' := by376 simp only [map_add, add_apply, coe_deriv₂, add_assoc]377 abel378379/-- The norm of the tensor product of a scalar linear map and of an element of a normed space380is the product of the norms. -/381@[simp]382theorem norm_smulRight_apply (c : StrongDual 𝕜 E) (f : Fₗ) : ‖smulRight c f‖ = ‖c‖ * ‖f‖ := by383 refine le_antisymm ?_ ?_384 · refine opNorm_le_bound _ (by positivity) fun x => ?_385 calc386 ‖c x • f‖ = ‖c x‖ * ‖f‖ := norm_smul _ _387 _ ≤ ‖c‖ * ‖x‖ * ‖f‖ := by gcongr; apply le_opNorm388 _ = ‖c‖ * ‖f‖ * ‖x‖ := by ring389 · obtain hf | hf := (norm_nonneg f).eq_or_lt'390 · simp [hf]391 · rw [← le_div_iff₀ hf]392 refine opNorm_le_bound _ (by positivity) fun x => ?_393 rw [div_mul_eq_mul_div, le_div_iff₀ hf]394 calc395 ‖c x‖ * ‖f‖ = ‖c x • f‖ := (norm_smul _ _).symm396 _ = ‖smulRight c f x‖ := rfl397 _ ≤ ‖smulRight c f‖ * ‖x‖ := le_opNorm _ _398399/-- The non-negative norm of the tensor product of a scalar linear map and of an element of a normed400space is the product of the non-negative norms. -/401@[simp]402theorem nnnorm_smulRight_apply (c : StrongDual 𝕜 E) (f : Fₗ) : ‖smulRight c f‖₊ = ‖c‖₊ * ‖f‖₊ :=403 NNReal.eq <| c.norm_smulRight_apply f404405@[simp] theorem norm_toSpanSingleton (x : E) : ‖toSpanSingleton 𝕜 x‖ = ‖x‖ := by406 simp [← smulRight_id, norm_id]407408@[simp] theorem nnnorm_toSpanSingleton (x : E) : ‖toSpanSingleton 𝕜 x‖₊ = ‖x‖₊ :=409 NNReal.eq <| norm_toSpanSingleton _410411variable (𝕜 E Fₗ) in412/-- `ContinuousLinearMap.smulRight` as a continuous trilinear map:413`smulRightL (c : StrongDual 𝕜 E) (f : F) (x : E) = c x • f`.414415This is also known as a rank-one operator.416See also `InnerProductSpace.rankOne` for the rank-one operator on Hilbert spaces. -/417@[simps! apply_apply]418def smulRightL : StrongDual 𝕜 E →L[𝕜] Fₗ →L[𝕜] E →L[𝕜] Fₗ :=419 LinearMap.mkContinuous₂420 { toFun := smulRightₗ421 map_add' := fun c₁ c₂ => by422 ext x423 simp only [add_smul, coe_smulRightₗ, add_apply, smulRight_apply, LinearMap.add_apply]424 map_smul' := fun m c => by425 ext x426 simp [smul_smul] }427 1 fun c x => by428 simp only [coe_smulRightₗ, one_mul, norm_smulRight_apply, LinearMap.coe_mk, AddHom.coe_mk,429 le_refl]430431end ContinuousLinearMap432433end SemiNormed434435section Restrict436437namespace ContinuousLinearMap438439variable {𝕜' : Type*} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜']440 [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace 𝕜' E] [IsScalarTower 𝕜 𝕜' E]441 [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F]442 [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [NormedSpace 𝕜' G] [IsScalarTower 𝕜 𝕜' G]443444variable (𝕜) in445/-- Convenience function for restricting the linearity of a bilinear map. -/446def bilinearRestrictScalars (B : E →L[𝕜'] F →L[𝕜'] G) : E →L[𝕜] F →L[𝕜] G :=447 (restrictScalarsL 𝕜' F G 𝕜 𝕜).comp (B.restrictScalars 𝕜)448449variable (B : E →L[𝕜'] F →L[𝕜'] G) (x : E) (y : F)450451theorem bilinearRestrictScalars_eq_restrictScalarsL_comp_restrictScalars :452 B.bilinearRestrictScalars 𝕜 = (restrictScalarsL 𝕜' F G 𝕜 𝕜).comp (B.restrictScalars 𝕜) := rfl453454theorem bilinearRestrictScalars_eq_restrictScalars_restrictScalarsL_comp :455 B.bilinearRestrictScalars 𝕜 = restrictScalars 𝕜 ((restrictScalarsL 𝕜' F G 𝕜 𝕜').comp B) := rfl456457variable (𝕜) in458@[simp]459theorem bilinearRestrictScalars_apply_apply : (B.bilinearRestrictScalars 𝕜) x y = B x y := rfl460461@[simp]462theorem norm_bilinearRestrictScalars : ‖B.bilinearRestrictScalars 𝕜‖ = ‖B‖ := rfl463464end ContinuousLinearMap465466end Restrict