Operator norm: bilinear maps #
This file contains lemmas concerning operator norm as applied to bilinear maps E × F → G,
interpreted as linear maps E → F → G as usual (and similarly for semilinear variants).
theorem
ContinuousLinearMap.opNorm_ext
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{𝕜₃ : Type u_3}
{E : Type u_4}
{F : Type u_6}
{G : Type u_8}
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup F]
[SeminormedAddCommGroup G]
[NontriviallyNormedField 𝕜]
[NontriviallyNormedField 𝕜₂]
[NontriviallyNormedField 𝕜₃]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜₂ F]
[NormedSpace 𝕜₃ G]
{σ₁₂ : 𝕜 →+* 𝕜₂}
{σ₁₃ : 𝕜 →+* 𝕜₃}
[RingHomIsometric σ₁₃]
(f : E →SL[σ₁₂] F)
(g : E →SL[σ₁₃] G)
(h : ∀ (x : E), ‖f x‖ = ‖g x‖)
:
@[deprecated ContinuousLinearMap.opNorm_ext]
theorem
ContinuousLinearMap.op_norm_ext
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{𝕜₃ : Type u_3}
{E : Type u_4}
{F : Type u_6}
{G : Type u_8}
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup F]
[SeminormedAddCommGroup G]
[NontriviallyNormedField 𝕜]
[NontriviallyNormedField 𝕜₂]
[NontriviallyNormedField 𝕜₃]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜₂ F]
[NormedSpace 𝕜₃ G]
{σ₁₂ : 𝕜 →+* 𝕜₂}
{σ₁₃ : 𝕜 →+* 𝕜₃}
[RingHomIsometric σ₁₃]
(f : E →SL[σ₁₂] F)
(g : E →SL[σ₁₃] G)
(h : ∀ (x : E), ‖f x‖ = ‖g x‖)
:
Alias of ContinuousLinearMap.opNorm_ext.
theorem
ContinuousLinearMap.opNorm_le_bound₂
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{𝕜₃ : Type u_3}
{E : Type u_4}
{F : Type u_6}
{G : Type u_8}
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup F]
[SeminormedAddCommGroup G]
[NontriviallyNormedField 𝕜]
[NontriviallyNormedField 𝕜₂]
[NontriviallyNormedField 𝕜₃]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜₂ F]
[NormedSpace 𝕜₃ G]
{σ₂₃ : 𝕜₂ →+* 𝕜₃}
{σ₁₃ : 𝕜 →+* 𝕜₃}
[RingHomIsometric σ₂₃]
(f : E →SL[σ₁₃] F →SL[σ₂₃] G)
{C : ℝ}
(h0 : 0 ≤ C)
(hC : ∀ (x : E) (y : F), ‖(f x) y‖ ≤ C * ‖x‖ * ‖y‖)
:
@[deprecated ContinuousLinearMap.opNorm_le_bound₂]
theorem
ContinuousLinearMap.op_norm_le_bound₂
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{𝕜₃ : Type u_3}
{E : Type u_4}
{F : Type u_6}
{G : Type u_8}
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup F]
[SeminormedAddCommGroup G]
[NontriviallyNormedField 𝕜]
[NontriviallyNormedField 𝕜₂]
[NontriviallyNormedField 𝕜₃]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜₂ F]
[NormedSpace 𝕜₃ G]
{σ₂₃ : 𝕜₂ →+* 𝕜₃}
{σ₁₃ : 𝕜 →+* 𝕜₃}
[RingHomIsometric σ₂₃]
(f : E →SL[σ₁₃] F →SL[σ₂₃] G)
{C : ℝ}
(h0 : 0 ≤ C)
(hC : ∀ (x : E) (y : F), ‖(f x) y‖ ≤ C * ‖x‖ * ‖y‖)
:
Alias of ContinuousLinearMap.opNorm_le_bound₂.
theorem
ContinuousLinearMap.le_opNorm₂
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{𝕜₃ : Type u_3}
{E : Type u_4}
{F : Type u_6}
{G : Type u_8}
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup F]
[SeminormedAddCommGroup G]
[NontriviallyNormedField 𝕜]
[NontriviallyNormedField 𝕜₂]
[NontriviallyNormedField 𝕜₃]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜₂ F]
[NormedSpace 𝕜₃ G]
{σ₂₃ : 𝕜₂ →+* 𝕜₃}
{σ₁₃ : 𝕜 →+* 𝕜₃}
[RingHomIsometric σ₂₃]
[RingHomIsometric σ₁₃]
(f : E →SL[σ₁₃] F →SL[σ₂₃] G)
(x : E)
(y : F)
:
@[deprecated ContinuousLinearMap.le_opNorm₂]
theorem
ContinuousLinearMap.le_op_norm₂
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{𝕜₃ : Type u_3}
{E : Type u_4}
{F : Type u_6}
{G : Type u_8}
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup F]
[SeminormedAddCommGroup G]
[NontriviallyNormedField 𝕜]
[NontriviallyNormedField 𝕜₂]
[NontriviallyNormedField 𝕜₃]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜₂ F]
[NormedSpace 𝕜₃ G]
{σ₂₃ : 𝕜₂ →+* 𝕜₃}
{σ₁₃ : 𝕜 →+* 𝕜₃}
[RingHomIsometric σ₂₃]
[RingHomIsometric σ₁₃]
(f : E →SL[σ₁₃] F →SL[σ₂₃] G)
(x : E)
(y : F)
:
Alias of ContinuousLinearMap.le_opNorm₂.
theorem
ContinuousLinearMap.le_of_opNorm₂_le_of_le
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{𝕜₃ : Type u_3}
{E : Type u_4}
{F : Type u_6}
{G : Type u_8}
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup F]
[SeminormedAddCommGroup G]
[NontriviallyNormedField 𝕜]
[NontriviallyNormedField 𝕜₂]
[NontriviallyNormedField 𝕜₃]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜₂ F]
[NormedSpace 𝕜₃ G]
{σ₂₃ : 𝕜₂ →+* 𝕜₃}
{σ₁₃ : 𝕜 →+* 𝕜₃}
[RingHomIsometric σ₂₃]
[RingHomIsometric σ₁₃]
(f : E →SL[σ₁₃] F →SL[σ₂₃] G)
{x : E}
{y : F}
{a : ℝ}
{b : ℝ}
{c : ℝ}
(hf : ‖f‖ ≤ a)
(hx : ‖x‖ ≤ b)
(hy : ‖y‖ ≤ c)
:
@[deprecated ContinuousLinearMap.le_of_opNorm₂_le_of_le]
theorem
ContinuousLinearMap.le_of_op_norm₂_le_of_le
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{𝕜₃ : Type u_3}
{E : Type u_4}
{F : Type u_6}
{G : Type u_8}
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup F]
[SeminormedAddCommGroup G]
[NontriviallyNormedField 𝕜]
[NontriviallyNormedField 𝕜₂]
[NontriviallyNormedField 𝕜₃]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜₂ F]
[NormedSpace 𝕜₃ G]
{σ₂₃ : 𝕜₂ →+* 𝕜₃}
{σ₁₃ : 𝕜 →+* 𝕜₃}
[RingHomIsometric σ₂₃]
[RingHomIsometric σ₁₃]
(f : E →SL[σ₁₃] F →SL[σ₂₃] G)
{x : E}
{y : F}
{a : ℝ}
{b : ℝ}
{c : ℝ}
(hf : ‖f‖ ≤ a)
(hx : ‖x‖ ≤ b)
(hy : ‖y‖ ≤ c)
:
theorem
LinearMap.norm_mkContinuous₂_aux
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{𝕜₃ : Type u_3}
{E : Type u_4}
{F : Type u_6}
{G : Type u_8}
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup F]
[SeminormedAddCommGroup G]
[NontriviallyNormedField 𝕜]
[NontriviallyNormedField 𝕜₂]
[NontriviallyNormedField 𝕜₃]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜₂ F]
[NormedSpace 𝕜₃ G]
{σ₂₃ : 𝕜₂ →+* 𝕜₃}
{σ₁₃ : 𝕜 →+* 𝕜₃}
(f : E →ₛₗ[σ₁₃] F →ₛₗ[σ₂₃] G)
(C : ℝ)
(h : ∀ (x : E) (y : F), ‖(f x) y‖ ≤ C * ‖x‖ * ‖y‖)
(x : E)
:
noncomputable def
LinearMap.mkContinuousOfExistsBound₂
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{𝕜₃ : Type u_3}
{E : Type u_4}
{F : Type u_6}
{G : Type u_8}
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup F]
[SeminormedAddCommGroup G]
[NontriviallyNormedField 𝕜]
[NontriviallyNormedField 𝕜₂]
[NontriviallyNormedField 𝕜₃]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜₂ F]
[NormedSpace 𝕜₃ G]
{σ₂₃ : 𝕜₂ →+* 𝕜₃}
{σ₁₃ : 𝕜 →+* 𝕜₃}
[RingHomIsometric σ₂₃]
(f : E →ₛₗ[σ₁₃] F →ₛₗ[σ₂₃] G)
(h : ∃ (C : ℝ), ∀ (x : E) (y : F), ‖(f x) y‖ ≤ C * ‖x‖ * ‖y‖)
:
Create a bilinear map (represented as a map E →L[𝕜] F →L[𝕜] G) from the corresponding linear
map and existence of a bound on the norm of the image. The linear map can be constructed using
LinearMap.mk₂.
If you have an explicit bound, use LinearMap.mkContinuous₂ instead, as a norm estimate will
follow automatically in LinearMap.mkContinuous₂_norm_le.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
LinearMap.mkContinuous₂
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{𝕜₃ : Type u_3}
{E : Type u_4}
{F : Type u_6}
{G : Type u_8}
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup F]
[SeminormedAddCommGroup G]
[NontriviallyNormedField 𝕜]
[NontriviallyNormedField 𝕜₂]
[NontriviallyNormedField 𝕜₃]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜₂ F]
[NormedSpace 𝕜₃ G]
{σ₂₃ : 𝕜₂ →+* 𝕜₃}
{σ₁₃ : 𝕜 →+* 𝕜₃}
[RingHomIsometric σ₂₃]
(f : E →ₛₗ[σ₁₃] F →ₛₗ[σ₂₃] G)
(C : ℝ)
(hC : ∀ (x : E) (y : F), ‖(f x) y‖ ≤ C * ‖x‖ * ‖y‖)
:
Create a bilinear map (represented as a map E →L[𝕜] F →L[𝕜] G) from the corresponding linear
map and a bound on the norm of the image. The linear map can be constructed using
LinearMap.mk₂. Lemmas LinearMap.mkContinuous₂_norm_le' and LinearMap.mkContinuous₂_norm_le
provide estimates on the norm of an operator constructed using this function.
Equations
Instances For
@[simp]
theorem
LinearMap.mkContinuous₂_apply
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{𝕜₃ : Type u_3}
{E : Type u_4}
{F : Type u_6}
{G : Type u_8}
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup F]
[SeminormedAddCommGroup G]
[NontriviallyNormedField 𝕜]
[NontriviallyNormedField 𝕜₂]
[NontriviallyNormedField 𝕜₃]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜₂ F]
[NormedSpace 𝕜₃ G]
{σ₂₃ : 𝕜₂ →+* 𝕜₃}
{σ₁₃ : 𝕜 →+* 𝕜₃}
[RingHomIsometric σ₂₃]
(f : E →ₛₗ[σ₁₃] F →ₛₗ[σ₂₃] G)
{C : ℝ}
(hC : ∀ (x : E) (y : F), ‖(f x) y‖ ≤ C * ‖x‖ * ‖y‖)
(x : E)
(y : F)
:
((LinearMap.mkContinuous₂ f C hC) x) y = (f x) y
theorem
LinearMap.mkContinuous₂_norm_le'
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{𝕜₃ : Type u_3}
{E : Type u_4}
{F : Type u_6}
{G : Type u_8}
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup F]
[SeminormedAddCommGroup G]
[NontriviallyNormedField 𝕜]
[NontriviallyNormedField 𝕜₂]
[NontriviallyNormedField 𝕜₃]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜₂ F]
[NormedSpace 𝕜₃ G]
{σ₂₃ : 𝕜₂ →+* 𝕜₃}
{σ₁₃ : 𝕜 →+* 𝕜₃}
[RingHomIsometric σ₂₃]
(f : E →ₛₗ[σ₁₃] F →ₛₗ[σ₂₃] G)
{C : ℝ}
(hC : ∀ (x : E) (y : F), ‖(f x) y‖ ≤ C * ‖x‖ * ‖y‖)
:
‖LinearMap.mkContinuous₂ f C hC‖ ≤ max C 0
theorem
LinearMap.mkContinuous₂_norm_le
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{𝕜₃ : Type u_3}
{E : Type u_4}
{F : Type u_6}
{G : Type u_8}
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup F]
[SeminormedAddCommGroup G]
[NontriviallyNormedField 𝕜]
[NontriviallyNormedField 𝕜₂]
[NontriviallyNormedField 𝕜₃]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜₂ F]
[NormedSpace 𝕜₃ G]
{σ₂₃ : 𝕜₂ →+* 𝕜₃}
{σ₁₃ : 𝕜 →+* 𝕜₃}
[RingHomIsometric σ₂₃]
(f : E →ₛₗ[σ₁₃] F →ₛₗ[σ₂₃] G)
{C : ℝ}
(h0 : 0 ≤ C)
(hC : ∀ (x : E) (y : F), ‖(f x) y‖ ≤ C * ‖x‖ * ‖y‖)
:
‖LinearMap.mkContinuous₂ f C hC‖ ≤ C
noncomputable def
ContinuousLinearMap.flip
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{𝕜₃ : Type u_3}
{E : Type u_4}
{F : Type u_6}
{G : Type u_8}
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup F]
[SeminormedAddCommGroup G]
[NontriviallyNormedField 𝕜]
[NontriviallyNormedField 𝕜₂]
[NontriviallyNormedField 𝕜₃]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜₂ F]
[NormedSpace 𝕜₃ G]
{σ₂₃ : 𝕜₂ →+* 𝕜₃}
{σ₁₃ : 𝕜 →+* 𝕜₃}
[RingHomIsometric σ₂₃]
[RingHomIsometric σ₁₃]
(f : E →SL[σ₁₃] F →SL[σ₂₃] G)
:
Flip the order of arguments of a continuous bilinear map.
For a version bundled as LinearIsometryEquiv, see
ContinuousLinearMap.flipL.
Equations
- ContinuousLinearMap.flip f = LinearMap.mkContinuous₂ (LinearMap.mk₂'ₛₗ σ₂₃ σ₁₃ (fun (y : F) (x : E) => (f x) y) ⋯ ⋯ ⋯ ⋯) ‖f‖ ⋯
Instances For
@[simp]
theorem
ContinuousLinearMap.flip_apply
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{𝕜₃ : Type u_3}
{E : Type u_4}
{F : Type u_6}
{G : Type u_8}
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup F]
[SeminormedAddCommGroup G]
[NontriviallyNormedField 𝕜]
[NontriviallyNormedField 𝕜₂]
[NontriviallyNormedField 𝕜₃]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜₂ F]
[NormedSpace 𝕜₃ G]
{σ₂₃ : 𝕜₂ →+* 𝕜₃}
{σ₁₃ : 𝕜 →+* 𝕜₃}
[RingHomIsometric σ₂₃]
[RingHomIsometric σ₁₃]
(f : E →SL[σ₁₃] F →SL[σ₂₃] G)
(x : E)
(y : F)
:
((ContinuousLinearMap.flip f) y) x = (f x) y
@[simp]
theorem
ContinuousLinearMap.flip_flip
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{𝕜₃ : Type u_3}
{E : Type u_4}
{F : Type u_6}
{G : Type u_8}
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup F]
[SeminormedAddCommGroup G]
[NontriviallyNormedField 𝕜]
[NontriviallyNormedField 𝕜₂]
[NontriviallyNormedField 𝕜₃]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜₂ F]
[NormedSpace 𝕜₃ G]
{σ₂₃ : 𝕜₂ →+* 𝕜₃}
{σ₁₃ : 𝕜 →+* 𝕜₃}
[RingHomIsometric σ₂₃]
[RingHomIsometric σ₁₃]
(f : E →SL[σ₁₃] F →SL[σ₂₃] G)
:
@[simp]
theorem
ContinuousLinearMap.opNorm_flip
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{𝕜₃ : Type u_3}
{E : Type u_4}
{F : Type u_6}
{G : Type u_8}
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup F]
[SeminormedAddCommGroup G]
[NontriviallyNormedField 𝕜]
[NontriviallyNormedField 𝕜₂]
[NontriviallyNormedField 𝕜₃]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜₂ F]
[NormedSpace 𝕜₃ G]
{σ₂₃ : 𝕜₂ →+* 𝕜₃}
{σ₁₃ : 𝕜 →+* 𝕜₃}
[RingHomIsometric σ₂₃]
[RingHomIsometric σ₁₃]
(f : E →SL[σ₁₃] F →SL[σ₂₃] G)
:
@[deprecated ContinuousLinearMap.opNorm_flip]
theorem
ContinuousLinearMap.op_norm_flip
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{𝕜₃ : Type u_3}
{E : Type u_4}
{F : Type u_6}
{G : Type u_8}
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup F]
[SeminormedAddCommGroup G]
[NontriviallyNormedField 𝕜]
[NontriviallyNormedField 𝕜₂]
[NontriviallyNormedField 𝕜₃]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜₂ F]
[NormedSpace 𝕜₃ G]
{σ₂₃ : 𝕜₂ →+* 𝕜₃}
{σ₁₃ : 𝕜 →+* 𝕜₃}
[RingHomIsometric σ₂₃]
[RingHomIsometric σ₁₃]
(f : E →SL[σ₁₃] F →SL[σ₂₃] G)
:
Alias of ContinuousLinearMap.opNorm_flip.
@[simp]
theorem
ContinuousLinearMap.flip_add
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{𝕜₃ : Type u_3}
{E : Type u_4}
{F : Type u_6}
{G : Type u_8}
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup F]
[SeminormedAddCommGroup G]
[NontriviallyNormedField 𝕜]
[NontriviallyNormedField 𝕜₂]
[NontriviallyNormedField 𝕜₃]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜₂ F]
[NormedSpace 𝕜₃ G]
{σ₂₃ : 𝕜₂ →+* 𝕜₃}
{σ₁₃ : 𝕜 →+* 𝕜₃}
[RingHomIsometric σ₂₃]
[RingHomIsometric σ₁₃]
(f : E →SL[σ₁₃] F →SL[σ₂₃] G)
(g : E →SL[σ₁₃] F →SL[σ₂₃] G)
:
@[simp]
theorem
ContinuousLinearMap.flip_smul
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{𝕜₃ : Type u_3}
{E : Type u_4}
{F : Type u_6}
{G : Type u_8}
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup F]
[SeminormedAddCommGroup G]
[NontriviallyNormedField 𝕜]
[NontriviallyNormedField 𝕜₂]
[NontriviallyNormedField 𝕜₃]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜₂ F]
[NormedSpace 𝕜₃ G]
{σ₂₃ : 𝕜₂ →+* 𝕜₃}
{σ₁₃ : 𝕜 →+* 𝕜₃}
[RingHomIsometric σ₂₃]
[RingHomIsometric σ₁₃]
(c : 𝕜₃)
(f : E →SL[σ₁₃] F →SL[σ₂₃] G)
:
ContinuousLinearMap.flip (c • f) = c • ContinuousLinearMap.flip f
noncomputable def
ContinuousLinearMap.flipₗᵢ'
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{𝕜₃ : Type u_3}
(E : Type u_4)
(F : Type u_6)
(G : Type u_8)
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup F]
[SeminormedAddCommGroup G]
[NontriviallyNormedField 𝕜]
[NontriviallyNormedField 𝕜₂]
[NontriviallyNormedField 𝕜₃]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜₂ F]
[NormedSpace 𝕜₃ G]
(σ₂₃ : 𝕜₂ →+* 𝕜₃)
(σ₁₃ : 𝕜 →+* 𝕜₃)
[RingHomIsometric σ₂₃]
[RingHomIsometric σ₁₃]
:
Flip the order of arguments of a continuous bilinear map.
This is a version bundled as a LinearIsometryEquiv.
For an unbundled version see ContinuousLinearMap.flip.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
ContinuousLinearMap.flipₗᵢ'_symm
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{𝕜₃ : Type u_3}
{E : Type u_4}
{F : Type u_6}
{G : Type u_8}
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup F]
[SeminormedAddCommGroup G]
[NontriviallyNormedField 𝕜]
[NontriviallyNormedField 𝕜₂]
[NontriviallyNormedField 𝕜₃]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜₂ F]
[NormedSpace 𝕜₃ G]
{σ₂₃ : 𝕜₂ →+* 𝕜₃}
{σ₁₃ : 𝕜 →+* 𝕜₃}
[RingHomIsometric σ₂₃]
[RingHomIsometric σ₁₃]
:
LinearIsometryEquiv.symm (ContinuousLinearMap.flipₗᵢ' E F G σ₂₃ σ₁₃) = ContinuousLinearMap.flipₗᵢ' F E G σ₁₃ σ₂₃
@[simp]
theorem
ContinuousLinearMap.coe_flipₗᵢ'
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{𝕜₃ : Type u_3}
{E : Type u_4}
{F : Type u_6}
{G : Type u_8}
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup F]
[SeminormedAddCommGroup G]
[NontriviallyNormedField 𝕜]
[NontriviallyNormedField 𝕜₂]
[NontriviallyNormedField 𝕜₃]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜₂ F]
[NormedSpace 𝕜₃ G]
{σ₂₃ : 𝕜₂ →+* 𝕜₃}
{σ₁₃ : 𝕜 →+* 𝕜₃}
[RingHomIsometric σ₂₃]
[RingHomIsometric σ₁₃]
:
⇑(ContinuousLinearMap.flipₗᵢ' E F G σ₂₃ σ₁₃) = ContinuousLinearMap.flip
noncomputable def
ContinuousLinearMap.flipₗᵢ
(𝕜 : Type u_1)
(E : Type u_4)
(Fₗ : Type u_7)
(Gₗ : Type u_9)
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup Fₗ]
[SeminormedAddCommGroup Gₗ]
[NontriviallyNormedField 𝕜]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜 Fₗ]
[NormedSpace 𝕜 Gₗ]
:
Flip the order of arguments of a continuous bilinear map.
This is a version bundled as a LinearIsometryEquiv.
For an unbundled version see ContinuousLinearMap.flip.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
ContinuousLinearMap.flipₗᵢ_symm
{𝕜 : Type u_1}
{E : Type u_4}
{Fₗ : Type u_7}
{Gₗ : Type u_9}
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup Fₗ]
[SeminormedAddCommGroup Gₗ]
[NontriviallyNormedField 𝕜]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜 Fₗ]
[NormedSpace 𝕜 Gₗ]
:
LinearIsometryEquiv.symm (ContinuousLinearMap.flipₗᵢ 𝕜 E Fₗ Gₗ) = ContinuousLinearMap.flipₗᵢ 𝕜 Fₗ E Gₗ
@[simp]
theorem
ContinuousLinearMap.coe_flipₗᵢ
{𝕜 : Type u_1}
{E : Type u_4}
{Fₗ : Type u_7}
{Gₗ : Type u_9}
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup Fₗ]
[SeminormedAddCommGroup Gₗ]
[NontriviallyNormedField 𝕜]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜 Fₗ]
[NormedSpace 𝕜 Gₗ]
:
⇑(ContinuousLinearMap.flipₗᵢ 𝕜 E Fₗ Gₗ) = ContinuousLinearMap.flip
noncomputable def
ContinuousLinearMap.apply'
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
(F : Type u_6)
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup F]
[NontriviallyNormedField 𝕜]
[NontriviallyNormedField 𝕜₂]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜₂ F]
(σ₁₂ : 𝕜 →+* 𝕜₂)
[RingHomIsometric σ₁₂]
:
The continuous semilinear map obtained by applying a continuous semilinear map at a given vector.
This is the continuous version of LinearMap.applyₗ.
Equations
- ContinuousLinearMap.apply' F σ₁₂ = ContinuousLinearMap.flip (ContinuousLinearMap.id 𝕜₂ (E →SL[σ₁₂] F))
Instances For
@[simp]
theorem
ContinuousLinearMap.apply_apply'
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup F]
[NontriviallyNormedField 𝕜]
[NontriviallyNormedField 𝕜₂]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
[RingHomIsometric σ₁₂]
(v : E)
(f : E →SL[σ₁₂] F)
:
((ContinuousLinearMap.apply' F σ₁₂) v) f = f v
noncomputable def
ContinuousLinearMap.apply
(𝕜 : Type u_1)
{E : Type u_4}
(Fₗ : Type u_7)
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup Fₗ]
[NontriviallyNormedField 𝕜]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜 Fₗ]
:
The continuous semilinear map obtained by applying a continuous semilinear map at a given vector.
This is the continuous version of LinearMap.applyₗ.
Equations
- ContinuousLinearMap.apply 𝕜 Fₗ = ContinuousLinearMap.flip (ContinuousLinearMap.id 𝕜 (E →L[𝕜] Fₗ))
Instances For
@[simp]
theorem
ContinuousLinearMap.apply_apply
{𝕜 : Type u_1}
{E : Type u_4}
{Fₗ : Type u_7}
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup Fₗ]
[NontriviallyNormedField 𝕜]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜 Fₗ]
(v : E)
(f : E →L[𝕜] Fₗ)
:
((ContinuousLinearMap.apply 𝕜 Fₗ) v) f = f v
noncomputable def
ContinuousLinearMap.compSL
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{𝕜₃ : Type u_3}
(E : Type u_4)
(F : Type u_6)
(G : Type u_8)
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup F]
[SeminormedAddCommGroup G]
[NontriviallyNormedField 𝕜]
[NontriviallyNormedField 𝕜₂]
[NontriviallyNormedField 𝕜₃]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜₂ F]
[NormedSpace 𝕜₃ G]
(σ₁₂ : 𝕜 →+* 𝕜₂)
(σ₂₃ : 𝕜₂ →+* 𝕜₃)
{σ₁₃ : 𝕜 →+* 𝕜₃}
[RingHomCompTriple σ₁₂ σ₂₃ σ₁₃]
[RingHomIsometric σ₂₃]
[RingHomIsometric σ₁₃]
[RingHomIsometric σ₁₂]
:
Composition of continuous semilinear maps as a continuous semibilinear map.
Equations
- ContinuousLinearMap.compSL E F G σ₁₂ σ₂₃ = LinearMap.mkContinuous₂ (LinearMap.mk₂'ₛₗ (RingHom.id 𝕜₃) σ₂₃ ContinuousLinearMap.comp ⋯ ⋯ ⋯ ⋯) 1 ⋯
Instances For
theorem
ContinuousLinearMap.norm_compSL_le
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{𝕜₃ : Type u_3}
(E : Type u_4)
(F : Type u_6)
(G : Type u_8)
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup F]
[SeminormedAddCommGroup G]
[NontriviallyNormedField 𝕜]
[NontriviallyNormedField 𝕜₂]
[NontriviallyNormedField 𝕜₃]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜₂ F]
[NormedSpace 𝕜₃ G]
(σ₁₂ : 𝕜 →+* 𝕜₂)
(σ₂₃ : 𝕜₂ →+* 𝕜₃)
{σ₁₃ : 𝕜 →+* 𝕜₃}
[RingHomCompTriple σ₁₂ σ₂₃ σ₁₃]
[RingHomIsometric σ₂₃]
[RingHomIsometric σ₁₃]
[RingHomIsometric σ₁₂]
:
‖ContinuousLinearMap.compSL E F G σ₁₂ σ₂₃‖ ≤ 1
@[simp]
theorem
ContinuousLinearMap.compSL_apply
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{𝕜₃ : Type u_3}
{E : Type u_4}
{F : Type u_6}
{G : Type u_8}
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup F]
[SeminormedAddCommGroup G]
[NontriviallyNormedField 𝕜]
[NontriviallyNormedField 𝕜₂]
[NontriviallyNormedField 𝕜₃]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜₂ F]
[NormedSpace 𝕜₃ G]
{σ₁₂ : 𝕜 →+* 𝕜₂}
{σ₂₃ : 𝕜₂ →+* 𝕜₃}
{σ₁₃ : 𝕜 →+* 𝕜₃}
[RingHomCompTriple σ₁₂ σ₂₃ σ₁₃]
[RingHomIsometric σ₂₃]
[RingHomIsometric σ₁₃]
[RingHomIsometric σ₁₂]
(f : F →SL[σ₂₃] G)
(g : E →SL[σ₁₂] F)
:
((ContinuousLinearMap.compSL E F G σ₁₂ σ₂₃) f) g = ContinuousLinearMap.comp f g
theorem
Continuous.const_clm_comp
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{𝕜₃ : Type u_3}
{E : Type u_4}
{F : Type u_6}
{G : Type u_8}
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup F]
[SeminormedAddCommGroup G]
[NontriviallyNormedField 𝕜]
[NontriviallyNormedField 𝕜₂]
[NontriviallyNormedField 𝕜₃]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜₂ F]
[NormedSpace 𝕜₃ G]
{σ₁₂ : 𝕜 →+* 𝕜₂}
{σ₂₃ : 𝕜₂ →+* 𝕜₃}
{σ₁₃ : 𝕜 →+* 𝕜₃}
[RingHomCompTriple σ₁₂ σ₂₃ σ₁₃]
[RingHomIsometric σ₂₃]
[RingHomIsometric σ₁₃]
[RingHomIsometric σ₁₂]
{X : Type u_11}
[TopologicalSpace X]
{f : X → E →SL[σ₁₂] F}
(hf : Continuous f)
(g : F →SL[σ₂₃] G)
:
Continuous fun (x : X) => ContinuousLinearMap.comp g (f x)
theorem
Continuous.clm_comp_const
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{𝕜₃ : Type u_3}
{E : Type u_4}
{F : Type u_6}
{G : Type u_8}
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup F]
[SeminormedAddCommGroup G]
[NontriviallyNormedField 𝕜]
[NontriviallyNormedField 𝕜₂]
[NontriviallyNormedField 𝕜₃]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜₂ F]
[NormedSpace 𝕜₃ G]
{σ₁₂ : 𝕜 →+* 𝕜₂}
{σ₂₃ : 𝕜₂ →+* 𝕜₃}
{σ₁₃ : 𝕜 →+* 𝕜₃}
[RingHomCompTriple σ₁₂ σ₂₃ σ₁₃]
[RingHomIsometric σ₂₃]
[RingHomIsometric σ₁₃]
[RingHomIsometric σ₁₂]
{X : Type u_11}
[TopologicalSpace X]
{g : X → F →SL[σ₂₃] G}
(hg : Continuous g)
(f : E →SL[σ₁₂] F)
:
Continuous fun (x : X) => ContinuousLinearMap.comp (g x) f
noncomputable def
ContinuousLinearMap.compL
(𝕜 : Type u_1)
(E : Type u_4)
(Fₗ : Type u_7)
(Gₗ : Type u_9)
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup Fₗ]
[SeminormedAddCommGroup Gₗ]
[NontriviallyNormedField 𝕜]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜 Fₗ]
[NormedSpace 𝕜 Gₗ]
:
Composition of continuous linear maps as a continuous bilinear map.
Equations
- ContinuousLinearMap.compL 𝕜 E Fₗ Gₗ = ContinuousLinearMap.compSL E Fₗ Gₗ (RingHom.id 𝕜) (RingHom.id 𝕜)
Instances For
theorem
ContinuousLinearMap.norm_compL_le
(𝕜 : Type u_1)
(E : Type u_4)
(Fₗ : Type u_7)
(Gₗ : Type u_9)
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup Fₗ]
[SeminormedAddCommGroup Gₗ]
[NontriviallyNormedField 𝕜]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜 Fₗ]
[NormedSpace 𝕜 Gₗ]
:
‖ContinuousLinearMap.compL 𝕜 E Fₗ Gₗ‖ ≤ 1
@[simp]
theorem
ContinuousLinearMap.compL_apply
(𝕜 : Type u_1)
(E : Type u_4)
(Fₗ : Type u_7)
(Gₗ : Type u_9)
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup Fₗ]
[SeminormedAddCommGroup Gₗ]
[NontriviallyNormedField 𝕜]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜 Fₗ]
[NormedSpace 𝕜 Gₗ]
(f : Fₗ →L[𝕜] Gₗ)
(g : E →L[𝕜] Fₗ)
:
((ContinuousLinearMap.compL 𝕜 E Fₗ Gₗ) f) g = ContinuousLinearMap.comp f g
noncomputable def
ContinuousLinearMap.precompR
{𝕜 : Type u_1}
{E : Type u_4}
(Eₗ : Type u_5)
{Fₗ : Type u_7}
{Gₗ : Type u_9}
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup Eₗ]
[SeminormedAddCommGroup Fₗ]
[SeminormedAddCommGroup Gₗ]
[NontriviallyNormedField 𝕜]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜 Eₗ]
[NormedSpace 𝕜 Fₗ]
[NormedSpace 𝕜 Gₗ]
(L : E →L[𝕜] Fₗ →L[𝕜] Gₗ)
:
Apply L(x,-) pointwise to bilinear maps, as a continuous bilinear map
Equations
- ContinuousLinearMap.precompR Eₗ L = ContinuousLinearMap.comp (ContinuousLinearMap.compL 𝕜 Eₗ Fₗ Gₗ) L
Instances For
@[simp]
theorem
ContinuousLinearMap.precompR_apply
{𝕜 : Type u_1}
{E : Type u_4}
(Eₗ : Type u_5)
{Fₗ : Type u_7}
{Gₗ : Type u_9}
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup Eₗ]
[SeminormedAddCommGroup Fₗ]
[SeminormedAddCommGroup Gₗ]
[NontriviallyNormedField 𝕜]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜 Eₗ]
[NormedSpace 𝕜 Fₗ]
[NormedSpace 𝕜 Gₗ]
(L : E →L[𝕜] Fₗ →L[𝕜] Gₗ)
:
∀ (a : E), (ContinuousLinearMap.precompR Eₗ L) a = (ContinuousLinearMap.compL 𝕜 Eₗ Fₗ Gₗ) (L a)
noncomputable def
ContinuousLinearMap.precompL
{𝕜 : Type u_1}
{E : Type u_4}
(Eₗ : Type u_5)
{Fₗ : Type u_7}
{Gₗ : Type u_9}
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup Eₗ]
[SeminormedAddCommGroup Fₗ]
[SeminormedAddCommGroup Gₗ]
[NontriviallyNormedField 𝕜]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜 Eₗ]
[NormedSpace 𝕜 Fₗ]
[NormedSpace 𝕜 Gₗ]
(L : E →L[𝕜] Fₗ →L[𝕜] Gₗ)
:
Apply L(-,y) pointwise to bilinear maps, as a continuous bilinear map
Equations
Instances For
@[simp]
theorem
ContinuousLinearMap.precompL_apply
{𝕜 : Type u_1}
{E : Type u_4}
(Eₗ : Type u_5)
{Fₗ : Type u_7}
{Gₗ : Type u_9}
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup Eₗ]
[SeminormedAddCommGroup Fₗ]
[SeminormedAddCommGroup Gₗ]
[NontriviallyNormedField 𝕜]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜 Eₗ]
[NormedSpace 𝕜 Fₗ]
[NormedSpace 𝕜 Gₗ]
(L : E →L[𝕜] Fₗ →L[𝕜] Gₗ)
(u : Eₗ →L[𝕜] E)
(f : Fₗ)
(g : Eₗ)
:
(((ContinuousLinearMap.precompL Eₗ L) u) f) g = (L (u g)) f
theorem
ContinuousLinearMap.norm_precompR_le
{𝕜 : Type u_1}
{E : Type u_4}
(Eₗ : Type u_5)
{Fₗ : Type u_7}
{Gₗ : Type u_9}
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup Eₗ]
[SeminormedAddCommGroup Fₗ]
[SeminormedAddCommGroup Gₗ]
[NontriviallyNormedField 𝕜]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜 Eₗ]
[NormedSpace 𝕜 Fₗ]
[NormedSpace 𝕜 Gₗ]
(L : E →L[𝕜] Fₗ →L[𝕜] Gₗ)
:
theorem
ContinuousLinearMap.norm_precompL_le
{𝕜 : Type u_1}
{E : Type u_4}
(Eₗ : Type u_5)
{Fₗ : Type u_7}
{Gₗ : Type u_9}
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup Eₗ]
[SeminormedAddCommGroup Fₗ]
[SeminormedAddCommGroup Gₗ]
[NontriviallyNormedField 𝕜]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜 Eₗ]
[NormedSpace 𝕜 Fₗ]
[NormedSpace 𝕜 Gₗ]
(L : E →L[𝕜] Fₗ →L[𝕜] Gₗ)
:
noncomputable def
ContinuousLinearMap.bilinearComp
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{𝕜₃ : Type u_3}
{E : Type u_4}
{F : Type u_6}
{G : Type u_8}
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup F]
[SeminormedAddCommGroup G]
[NontriviallyNormedField 𝕜]
[NontriviallyNormedField 𝕜₂]
[NontriviallyNormedField 𝕜₃]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜₂ F]
[NormedSpace 𝕜₃ G]
{σ₂₃ : 𝕜₂ →+* 𝕜₃}
{σ₁₃ : 𝕜 →+* 𝕜₃}
{E' : Type u_11}
{F' : Type u_12}
[SeminormedAddCommGroup E']
[SeminormedAddCommGroup F']
{𝕜₁' : Type u_13}
{𝕜₂' : Type u_14}
[NontriviallyNormedField 𝕜₁']
[NontriviallyNormedField 𝕜₂']
[NormedSpace 𝕜₁' E']
[NormedSpace 𝕜₂' F']
{σ₁' : 𝕜₁' →+* 𝕜}
{σ₁₃' : 𝕜₁' →+* 𝕜₃}
{σ₂' : 𝕜₂' →+* 𝕜₂}
{σ₂₃' : 𝕜₂' →+* 𝕜₃}
[RingHomCompTriple σ₁' σ₁₃ σ₁₃']
[RingHomCompTriple σ₂' σ₂₃ σ₂₃']
[RingHomIsometric σ₂₃]
[RingHomIsometric σ₁₃']
[RingHomIsometric σ₂₃']
(f : E →SL[σ₁₃] F →SL[σ₂₃] G)
(gE : E' →SL[σ₁'] E)
(gF : F' →SL[σ₂'] F)
:
Compose a bilinear map E →SL[σ₁₃] F →SL[σ₂₃] G with two linear maps
E' →SL[σ₁'] E and F' →SL[σ₂'] F.
Equations
Instances For
@[simp]
theorem
ContinuousLinearMap.bilinearComp_apply
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{𝕜₃ : Type u_3}
{E : Type u_4}
{F : Type u_6}
{G : Type u_8}
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup F]
[SeminormedAddCommGroup G]
[NontriviallyNormedField 𝕜]
[NontriviallyNormedField 𝕜₂]
[NontriviallyNormedField 𝕜₃]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜₂ F]
[NormedSpace 𝕜₃ G]
{σ₂₃ : 𝕜₂ →+* 𝕜₃}
{σ₁₃ : 𝕜 →+* 𝕜₃}
{E' : Type u_11}
{F' : Type u_12}
[SeminormedAddCommGroup E']
[SeminormedAddCommGroup F']
{𝕜₁' : Type u_13}
{𝕜₂' : Type u_14}
[NontriviallyNormedField 𝕜₁']
[NontriviallyNormedField 𝕜₂']
[NormedSpace 𝕜₁' E']
[NormedSpace 𝕜₂' F']
{σ₁' : 𝕜₁' →+* 𝕜}
{σ₁₃' : 𝕜₁' →+* 𝕜₃}
{σ₂' : 𝕜₂' →+* 𝕜₂}
{σ₂₃' : 𝕜₂' →+* 𝕜₃}
[RingHomCompTriple σ₁' σ₁₃ σ₁₃']
[RingHomCompTriple σ₂' σ₂₃ σ₂₃']
[RingHomIsometric σ₂₃]
[RingHomIsometric σ₁₃']
[RingHomIsometric σ₂₃']
(f : E →SL[σ₁₃] F →SL[σ₂₃] G)
(gE : E' →SL[σ₁'] E)
(gF : F' →SL[σ₂'] F)
(x : E')
(y : F')
:
((ContinuousLinearMap.bilinearComp f gE gF) x) y = (f (gE x)) (gF y)
noncomputable def
ContinuousLinearMap.deriv₂
{𝕜 : Type u_1}
{E : Type u_4}
{Fₗ : Type u_7}
{Gₗ : Type u_9}
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup Fₗ]
[SeminormedAddCommGroup Gₗ]
[NontriviallyNormedField 𝕜]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜 Fₗ]
[NormedSpace 𝕜 Gₗ]
(f : E →L[𝕜] Fₗ →L[𝕜] Gₗ)
:
Derivative of a continuous bilinear map f : E →L[𝕜] F →L[𝕜] G interpreted as a map E × F → G
at point p : E × F evaluated at q : E × F, as a continuous bilinear map.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
ContinuousLinearMap.coe_deriv₂
{𝕜 : Type u_1}
{E : Type u_4}
{Fₗ : Type u_7}
{Gₗ : Type u_9}
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup Fₗ]
[SeminormedAddCommGroup Gₗ]
[NontriviallyNormedField 𝕜]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜 Fₗ]
[NormedSpace 𝕜 Gₗ]
(f : E →L[𝕜] Fₗ →L[𝕜] Gₗ)
(p : E × Fₗ)
:
⇑((ContinuousLinearMap.deriv₂ f) p) = fun (q : E × Fₗ) => (f p.1) q.2 + (f q.1) p.2
theorem
ContinuousLinearMap.map_add_add
{𝕜 : Type u_1}
{E : Type u_4}
{Fₗ : Type u_7}
{Gₗ : Type u_9}
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup Fₗ]
[SeminormedAddCommGroup Gₗ]
[NontriviallyNormedField 𝕜]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜 Fₗ]
[NormedSpace 𝕜 Gₗ]
(f : E →L[𝕜] Fₗ →L[𝕜] Gₗ)
(x : E)
(x' : E)
(y : Fₗ)
(y' : Fₗ)
: