Operator norm on the space of continuous linear maps

Define the operator norm on the space of continuous (semi)linear maps between normed spaces, and prove its basic properties. In particular, show that this space is itself a normed space.

Since a lot of elementary properties don't require ‖x‖ = 0 → x = 0 we start setting up the theory for SeminormedAddCommGroup and we specialize to NormedAddCommGroup at the end.

Note that most of statements that apply to semilinear maps only hold when the ring homomorphism is isometric, as expressed by the typeclass [RingHomIsometric σ].

theorem norm_image_of_norm_zero {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_6} {𝓕 : Type u_10} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [SemilinearMapClass 𝓕 σ₁₂ E F] (f : 𝓕) (hf : Continuous ↑f) {x : E} (hx : ‖x‖ = 0) : ‖↑f x‖ = 0

If ‖x‖ = 0 and f is continuous then ‖f x‖ = 0.

theorem SemilinearMapClass.bound_of_shell_semi_normed {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_6} {𝓕 : Type u_10} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] [SemilinearMapClass 𝓕 σ₁₂ E F] (f : 𝓕) {ε : ℝ} {C : ℝ} (ε_pos : 0 < ε) {c : 𝕜} (hc : 1 < ‖c‖) (hf : ∀ (x : E), ε / ‖c‖ ≤ ‖x‖ → ‖x‖ < ε → ‖↑f x‖ ≤ C * ‖x‖) {x : E} (hx : ‖x‖ ≠ 0) : ‖↑f x‖ ≤ C * ‖x‖

theorem SemilinearMapClass.bound_of_continuous {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_6} {𝓕 : Type u_10} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] [SemilinearMapClass 𝓕 σ₁₂ E F] (f : 𝓕) (hf : Continuous ↑f) : ∃ C, 0 < C ∧ ∀ (x : E), ‖↑f x‖ ≤ C * ‖x‖

A continuous linear map between seminormed spaces is bounded when the field is nontrivially normed. The continuity ensures boundedness on a ball of some radius ε. The nontriviality of the norm is then used to rescale any element into an element of norm in [ε/C, ε], whose image has a controlled norm. The norm control for the original element follows by rescaling.

theorem ContinuousLinearMap.bound {𝕜 : 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 σ₁₂] (f : E →SL[σ₁₂] F) : ∃ C, 0 < C ∧ ∀ (x : E), ‖↑f x‖ ≤ C * ‖x‖

noncomputable def LinearIsometry.toSpanSingleton (𝕜 : Type u_1) (E : Type u_4) [SeminormedAddCommGroup E] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] {v : E} (hv : ‖v‖ = 1) : 𝕜 →ₗᵢ[𝕜] E

Given a unit-length element x of a normed space E over a field 𝕜, the natural linear isometry map from 𝕜 to E by taking multiples of x.

Equations

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

@[simp]

theorem LinearIsometry.toSpanSingleton_apply {𝕜 : Type u_1} {E : Type u_4} [SeminormedAddCommGroup E] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] {v : E} (hv : ‖v‖ = 1) (a : 𝕜) : ↑(LinearIsometry.toSpanSingleton 𝕜 E hv) a = a • v

@[simp]

theorem LinearIsometry.coe_toSpanSingleton {𝕜 : Type u_1} {E : Type u_4} [SeminormedAddCommGroup E] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] {v : E} (hv : ‖v‖ = 1) : (LinearIsometry.toSpanSingleton 𝕜 E hv).toLinearMap = LinearMap.toSpanSingleton 𝕜 E v

noncomputable def ContinuousLinearMap.opNorm {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_6} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} (f : E →SL[σ₁₂] F) : ℝ

The operator norm of a continuous linear map is the inf of all its bounds.

Equations

• ContinuousLinearMap.opNorm f = sInf {c | 0 ≤ c ∧ ∀ (x : E), ‖↑f x‖ ≤ c * ‖x‖}

noncomputable instance ContinuousLinearMap.hasOpNorm {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_6} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} : Norm (E →SL[σ₁₂] F)

Equations

• ContinuousLinearMap.hasOpNorm = { norm := ContinuousLinearMap.opNorm }

theorem ContinuousLinearMap.norm_def {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_6} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} (f : E →SL[σ₁₂] F) : ‖f‖ = sInf {c | 0 ≤ c ∧ ∀ (x : E), ‖↑f x‖ ≤ c * ‖x‖}

theorem ContinuousLinearMap.bounds_nonempty {𝕜 : 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 σ₁₂] {f : E →SL[σ₁₂] F} : ∃ c, c ∈ {c | 0 ≤ c ∧ ∀ (x : E), ‖↑f x‖ ≤ c * ‖x‖}

theorem ContinuousLinearMap.bounds_bddBelow {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_6} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} {f : E →SL[σ₁₂] F} : BddBelow {c | 0 ≤ c ∧ ∀ (x : E), ‖↑f x‖ ≤ c * ‖x‖}

theorem ContinuousLinearMap.isLeast_op_norm {𝕜 : 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 σ₁₂] (f : E →SL[σ₁₂] F) : IsLeast {c | 0 ≤ c ∧ ∀ (x : E), ‖↑f x‖ ≤ c * ‖x‖} ‖f‖

theorem ContinuousLinearMap.op_norm_le_bound {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_6} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} (f : E →SL[σ₁₂] F) {M : ℝ} (hMp : 0 ≤ M) (hM : ∀ (x : E), ‖↑f x‖ ≤ M * ‖x‖) : ‖f‖ ≤ M

If one controls the norm of every A x, then one controls the norm of A.

theorem ContinuousLinearMap.op_norm_le_bound' {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_6} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} (f : E →SL[σ₁₂] F) {M : ℝ} (hMp : 0 ≤ M) (hM : ∀ (x : E), ‖x‖ ≠ 0 → ‖↑f x‖ ≤ M * ‖x‖) : ‖f‖ ≤ M

If one controls the norm of every A x, ‖x‖ ≠ 0, then one controls the norm of A.

theorem ContinuousLinearMap.op_norm_le_of_lipschitz {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_6} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} {f : E →SL[σ₁₂] F} {K : NNReal} (hf : LipschitzWith K ↑f) : ‖f‖ ≤ ↑K

theorem ContinuousLinearMap.op_norm_eq_of_bounds {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_6} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} {φ : E →SL[σ₁₂] F} {M : ℝ} (M_nonneg : 0 ≤ M) (h_above : ∀ (x : E), ‖↑φ x‖ ≤ M * ‖x‖) (h_below : ∀ (N : ℝ), N ≥ 0 → (∀ (x : E), ‖↑φ x‖ ≤ N * ‖x‖) → M ≤ N) : ‖φ‖ = M

theorem ContinuousLinearMap.op_norm_neg {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_6} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} (f : E →SL[σ₁₂] F) : ‖-f‖ = ‖f‖

theorem ContinuousLinearMap.op_norm_nonneg {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_6} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} (f : E →SL[σ₁₂] F) : 0 ≤ ‖f‖

theorem ContinuousLinearMap.op_norm_zero {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_6} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} : ‖0‖ = 0

The norm of the 0 operator is 0.

theorem ContinuousLinearMap.norm_id_le {𝕜 : Type u_1} {E : Type u_4} [SeminormedAddCommGroup E] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] : ‖ContinuousLinearMap.id 𝕜 E‖ ≤ 1

The norm of the identity is at most 1. It is in fact 1, except when the space is trivial where it is 0. It means that one can not do better than an inequality in general.

theorem ContinuousLinearMap.le_op_norm {𝕜 : 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 σ₁₂] (f : E →SL[σ₁₂] F) (x : E) : ‖↑f x‖ ≤ ‖f‖ * ‖x‖

The fundamental property of the operator norm: ‖f x‖ ≤ ‖f‖ * ‖x‖.

theorem ContinuousLinearMap.dist_le_op_norm {𝕜 : 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 σ₁₂] (f : E →SL[σ₁₂] F) (x : E) (y : E) : dist (↑f x) (↑f y) ≤ ‖f‖ * dist x y

theorem ContinuousLinearMap.le_of_op_norm_le_of_le {𝕜 : 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 σ₁₂] (f : E →SL[σ₁₂] F) {x : E} {a : ℝ} {b : ℝ} (hf : ‖f‖ ≤ a) (hx : ‖x‖ ≤ b) : ‖↑f x‖ ≤ a * b

theorem ContinuousLinearMap.le_op_norm_of_le {𝕜 : 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 σ₁₂] (f : E →SL[σ₁₂] F) {c : ℝ} {x : E} (h : ‖x‖ ≤ c) : ‖↑f x‖ ≤ ‖f‖ * c

theorem ContinuousLinearMap.le_of_op_norm_le {𝕜 : 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 σ₁₂] (f : E →SL[σ₁₂] F) {c : ℝ} (h : ‖f‖ ≤ c) (x : E) : ‖↑f x‖ ≤ c * ‖x‖

theorem ContinuousLinearMap.op_norm_le_iff {𝕜 : 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 σ₁₂] {f : E →SL[σ₁₂] F} {M : ℝ} (hMp : 0 ≤ M) : ‖f‖ ≤ M ↔ ∀ (x : E), ‖↑f x‖ ≤ M * ‖x‖

theorem ContinuousLinearMap.ratio_le_op_norm {𝕜 : 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 σ₁₂] (f : E →SL[σ₁₂] F) (x : E) : ‖↑f x‖ / ‖x‖ ≤ ‖f‖

theorem ContinuousLinearMap.unit_le_op_norm {𝕜 : 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 σ₁₂] (f : E →SL[σ₁₂] F) (x : E) : ‖x‖ ≤ 1 → ‖↑f x‖ ≤ ‖f‖

The image of the unit ball under a continuous linear map is bounded.

theorem ContinuousLinearMap.op_norm_le_of_shell {𝕜 : 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 σ₁₂] {f : E →SL[σ₁₂] F} {ε : ℝ} {C : ℝ} (ε_pos : 0 < ε) (hC : 0 ≤ C) {c : 𝕜} (hc : 1 < ‖c‖) (hf : ∀ (x : E), ε / ‖c‖ ≤ ‖x‖ → ‖x‖ < ε → ‖↑f x‖ ≤ C * ‖x‖) : ‖f‖ ≤ C

theorem ContinuousLinearMap.op_norm_le_of_ball {𝕜 : 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 σ₁₂] {f : E →SL[σ₁₂] F} {ε : ℝ} {C : ℝ} (ε_pos : 0 < ε) (hC : 0 ≤ C) (hf : ∀ (x : E), x ∈ Metric.ball 0 ε → ‖↑f x‖ ≤ C * ‖x‖) : ‖f‖ ≤ C

theorem ContinuousLinearMap.op_norm_le_of_nhds_zero {𝕜 : 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 σ₁₂] {f : E →SL[σ₁₂] F} {C : ℝ} (hC : 0 ≤ C) (hf : ∀ᶠ (x : E) in nhds 0, ‖↑f x‖ ≤ C * ‖x‖) : ‖f‖ ≤ C

theorem ContinuousLinearMap.op_norm_le_of_shell' {𝕜 : 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 σ₁₂] {f : E →SL[σ₁₂] F} {ε : ℝ} {C : ℝ} (ε_pos : 0 < ε) (hC : 0 ≤ C) {c : 𝕜} (hc : ‖c‖ < 1) (hf : ∀ (x : E), ε * ‖c‖ ≤ ‖x‖ → ‖x‖ < ε → ‖↑f x‖ ≤ C * ‖x‖) : ‖f‖ ≤ C

theorem ContinuousLinearMap.op_norm_le_of_unit_norm {E : Type u_4} {F : Type u_6} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace ℝ F] {f : E →L[ℝ] F} {C : ℝ} (hC : 0 ≤ C) (hf : ∀ (x : E), ‖x‖ = 1 → ‖↑f x‖ ≤ C) : ‖f‖ ≤ C

For a continuous real linear map f, if one controls the norm of every f x, ‖x‖ = 1, then one controls the norm of f.

theorem ContinuousLinearMap.op_norm_add_le {𝕜 : 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 σ₁₂] (f : E →SL[σ₁₂] F) (g : E →SL[σ₁₂] F) : ‖f + g‖ ≤ ‖f‖ + ‖g‖

The operator norm satisfies the triangle inequality.

theorem ContinuousLinearMap.norm_id_of_nontrivial_seminorm {𝕜 : Type u_1} {E : Type u_4} [SeminormedAddCommGroup E] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] (h : ∃ x, ‖x‖ ≠ 0) : ‖ContinuousLinearMap.id 𝕜 E‖ = 1

If there is an element with norm different from 0, then the norm of the identity equals 1. (Since we are working with seminorms supposing that the space is non-trivial is not enough.)

theorem ContinuousLinearMap.op_norm_smul_le {𝕜 : 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 σ₁₂] {𝕜' : Type u_11} [NormedField 𝕜'] [NormedSpace 𝕜' F] [SMulCommClass 𝕜₂ 𝕜' F] (c : 𝕜') (f : E →SL[σ₁₂] F) : ‖c • f‖ ≤ ‖c‖ * ‖f‖

noncomputable def ContinuousLinearMap.tmpSeminormedAddCommGroup {𝕜 : 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 σ₁₂] : SeminormedAddCommGroup (E →SL[σ₁₂] F)

Continuous linear maps themselves form a seminormed space with respect to the operator norm. This is only a temporary definition because we want to replace the topology with ContinuousLinearMap.topologicalSpace to avoid diamond issues. See Note [forgetful inheritance]

Equations

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

noncomputable def ContinuousLinearMap.tmpPseudoMetricSpace {𝕜 : 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 σ₁₂] : PseudoMetricSpace (E →SL[σ₁₂] F)

The PseudoMetricSpace structure on E →SL[σ₁₂] F coming from ContinuousLinearMap.tmpSeminormedAddCommGroup. See Note [forgetful inheritance]

Equations

• ContinuousLinearMap.tmpPseudoMetricSpace = SeminormedAddCommGroup.toPseudoMetricSpace

noncomputable def ContinuousLinearMap.tmpUniformSpace {𝕜 : 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 σ₁₂] : UniformSpace (E →SL[σ₁₂] F)

The UniformSpace structure on E →SL[σ₁₂] F coming from ContinuousLinearMap.tmpSeminormedAddCommGroup. See Note [forgetful inheritance]

Equations

• ContinuousLinearMap.tmpUniformSpace = PseudoMetricSpace.toUniformSpace

noncomputable def ContinuousLinearMap.tmpTopologicalSpace {𝕜 : 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 σ₁₂] : TopologicalSpace (E →SL[σ₁₂] F)

The TopologicalSpace structure on E →SL[σ₁₂] F coming from ContinuousLinearMap.tmpSeminormedAddCommGroup. See Note [forgetful inheritance]

Equations

• ContinuousLinearMap.tmpTopologicalSpace = UniformSpace.toTopologicalSpace

theorem ContinuousLinearMap.tmpTopologicalAddGroup {𝕜 : 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 σ₁₂] : TopologicalAddGroup (E →SL[σ₁₂] F)

theorem ContinuousLinearMap.tmp_closedBall_div_subset {𝕜 : 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 σ₁₂] {a : ℝ} {b : ℝ} (ha : 0 < a) (hb : 0 < b) : Metric.closedBall 0 (a / b) ⊆ {f | ∀ (x : E), x ∈ Metric.closedBall 0 b → ↑f x ∈ Metric.closedBall 0 a}

theorem ContinuousLinearMap.tmp_topology_eq {𝕜 : 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 σ₁₂] : ContinuousLinearMap.tmpTopologicalSpace = ContinuousLinearMap.topologicalSpace

theorem ContinuousLinearMap.tmpUniformSpace_eq {𝕜 : 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 σ₁₂] : ContinuousLinearMap.tmpUniformSpace = ContinuousLinearMap.uniformSpace

noncomputable instance ContinuousLinearMap.toPseudoMetricSpace {𝕜 : 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 σ₁₂] : PseudoMetricSpace (E →SL[σ₁₂] F)

Equations

• ContinuousLinearMap.toPseudoMetricSpace = PseudoMetricSpace.replaceUniformity ContinuousLinearMap.tmpPseudoMetricSpace (_ : uniformity (E →SL[σ₁₂] F) = uniformity (E →SL[σ₁₂] F))

noncomputable instance ContinuousLinearMap.toSeminormedAddCommGroup {𝕜 : 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 σ₁₂] : SeminormedAddCommGroup (E →SL[σ₁₂] F)

Continuous linear maps themselves form a seminormed space with respect to the operator norm.

Equations

• ContinuousLinearMap.toSeminormedAddCommGroup = SeminormedAddCommGroup.mk

theorem ContinuousLinearMap.nnnorm_def {𝕜 : 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 σ₁₂] (f : E →SL[σ₁₂] F) : ‖f‖₊ = sInf {c | ∀ (x : E), ‖↑f x‖₊ ≤ c * ‖x‖₊}

theorem ContinuousLinearMap.op_nnnorm_le_bound {𝕜 : 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 σ₁₂] (f : E →SL[σ₁₂] F) (M : NNReal) (hM : ∀ (x : E), ‖↑f x‖₊ ≤ M * ‖x‖₊) : ‖f‖₊ ≤ M

If one controls the norm of every A x, then one controls the norm of A.

theorem ContinuousLinearMap.op_nnnorm_le_bound' {𝕜 : 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 σ₁₂] (f : E →SL[σ₁₂] F) (M : NNReal) (hM : ∀ (x : E), ‖x‖₊ ≠ 0 → ‖↑f x‖₊ ≤ M * ‖x‖₊) : ‖f‖₊ ≤ M

If one controls the norm of every A x, ‖x‖₊ ≠ 0, then one controls the norm of A.

theorem ContinuousLinearMap.op_nnnorm_le_of_unit_nnnorm {E : Type u_4} {F : Type u_6} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace ℝ F] {f : E →L[ℝ] F} {C : NNReal} (hf : ∀ (x : E), ‖x‖₊ = 1 → ‖↑f x‖₊ ≤ C) : ‖f‖₊ ≤ C

For a continuous real linear map f, if one controls the norm of every f x, ‖x‖₊ = 1, then one controls the norm of f.

theorem ContinuousLinearMap.op_nnnorm_le_of_lipschitz {𝕜 : 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 σ₁₂] {f : E →SL[σ₁₂] F} {K : NNReal} (hf : LipschitzWith K ↑f) : ‖f‖₊ ≤ K

theorem ContinuousLinearMap.op_nnnorm_eq_of_bounds {𝕜 : 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 σ₁₂] {φ : E →SL[σ₁₂] F} (M : NNReal) (h_above : ∀ (x : E), ‖↑φ x‖ ≤ ↑M * ‖x‖) (h_below : ∀ (N : NNReal), (∀ (x : E), ‖↑φ x‖₊ ≤ N * ‖x‖₊) → M ≤ N) : ‖φ‖₊ = M

theorem ContinuousLinearMap.op_nnnorm_le_iff {𝕜 : 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 σ₁₂] {f : E →SL[σ₁₂] F} {C : NNReal} : ‖f‖₊ ≤ C ↔ ∀ (x : E), ‖↑f x‖₊ ≤ C * ‖x‖₊

theorem ContinuousLinearMap.isLeast_op_nnnorm {𝕜 : 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 σ₁₂] (f : E →SL[σ₁₂] F) : IsLeast {C | ∀ (x : E), ‖↑f x‖₊ ≤ C * ‖x‖₊} ‖f‖₊

noncomputable instance ContinuousLinearMap.toNormedSpace {𝕜 : 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 σ₁₂] {𝕜' : Type u_11} [NormedField 𝕜'] [NormedSpace 𝕜' F] [SMulCommClass 𝕜₂ 𝕜' F] : NormedSpace 𝕜' (E →SL[σ₁₂] F)

Equations

• ContinuousLinearMap.toNormedSpace = NormedSpace.mk (_ : ∀ (c : 𝕜') (f : E →SL[σ₁₂] F), ‖c • f‖ ≤ ‖c‖ * ‖f‖)

theorem ContinuousLinearMap.op_norm_comp_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 σ₂₃] (h : F →SL[σ₂₃] G) (f : E →SL[σ₁₂] F) : ‖ContinuousLinearMap.comp h f‖ ≤ ‖h‖ * ‖f‖

The operator norm is submultiplicative.

theorem ContinuousLinearMap.op_norm_comp_le' {𝕜 : Type u_1} {E : Type u_4} {Eₗ : Type u_5} {Fₗ : Type u_7} [SeminormedAddCommGroup E] [SeminormedAddCommGroup Eₗ] [SeminormedAddCommGroup Fₗ] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 Eₗ] [NormedSpace 𝕜 Fₗ] (h : Eₗ →L[𝕜] Fₗ) (f : E →L[𝕜] Eₗ) : ‖ContinuousLinearMap.comp h f‖ ≤ ‖h‖ * ‖f‖

The operator norm is submultiplicative.

theorem ContinuousLinearMap.op_nnnorm_comp_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 σ₂₃] (h : F →SL[σ₂₃] G) [RingHomIsometric σ₁₃] (f : E →SL[σ₁₂] F) : ‖ContinuousLinearMap.comp h f‖₊ ≤ ‖h‖₊ * ‖f‖₊

noncomputable instance ContinuousLinearMap.toSemiNormedRing {𝕜 : Type u_1} {E : Type u_4} [SeminormedAddCommGroup E] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] : SeminormedRing (E →L[𝕜] E)

Continuous linear maps form a seminormed ring with respect to the operator norm.

Equations

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

noncomputable instance ContinuousLinearMap.toNormedAlgebra {𝕜 : Type u_1} {E : Type u_4} [SeminormedAddCommGroup E] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] : NormedAlgebra 𝕜 (E →L[𝕜] E)

For a normed space E, continuous linear endomorphisms form a normed algebra with respect to the operator norm.

Equations

• ContinuousLinearMap.toNormedAlgebra = let src := ContinuousLinearMap.algebra; NormedAlgebra.mk (_ : ∀ (c : 𝕜) (f : E →L[𝕜] E), ‖c • f‖ ≤ ‖c‖ * ‖f‖)

theorem ContinuousLinearMap.le_op_nnnorm {𝕜 : 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 σ₁₂] (f : E →SL[σ₁₂] F) (x : E) : ‖↑f x‖₊ ≤ ‖f‖₊ * ‖x‖₊

theorem ContinuousLinearMap.nndist_le_op_nnnorm {𝕜 : 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 σ₁₂] (f : E →SL[σ₁₂] F) (x : E) (y : E) : nndist (↑f x) (↑f y) ≤ ‖f‖₊ * nndist x y

theorem ContinuousLinearMap.lipschitz {𝕜 : 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 σ₁₂] (f : E →SL[σ₁₂] F) : LipschitzWith ‖f‖₊ ↑f

continuous linear maps are Lipschitz continuous.

theorem ContinuousLinearMap.lipschitz_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 σ₁₂] (x : E) : LipschitzWith ‖x‖₊ fun f => ↑f x

Evaluation of a continuous linear map f at a point is Lipschitz continuous in f.

theorem ContinuousLinearMap.exists_mul_lt_apply_of_lt_op_nnnorm {𝕜 : 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 σ₁₂] (f : E →SL[σ₁₂] F) {r : NNReal} (hr : r < ‖f‖₊) : ∃ x, r * ‖x‖₊ < ‖↑f x‖₊

theorem ContinuousLinearMap.exists_mul_lt_of_lt_op_norm {𝕜 : 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 σ₁₂] (f : E →SL[σ₁₂] F) {r : ℝ} (hr₀ : 0 ≤ r) (hr : r < ‖f‖) : ∃ x, r * ‖x‖ < ‖↑f x‖

theorem ContinuousLinearMap.exists_lt_apply_of_lt_op_nnnorm {𝕜 : Type u_11} {𝕜₂ : Type u_12} {E : Type u_13} {F : Type u_14} [NormedAddCommGroup E] [SeminormedAddCommGroup F] [DenselyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] {σ₁₂ : 𝕜 →+* 𝕜₂} [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] [RingHomIsometric σ₁₂] (f : E →SL[σ₁₂] F) {r : NNReal} (hr : r < ‖f‖₊) : ∃ x, ‖x‖₊ < 1 ∧ r < ‖↑f x‖₊

theorem ContinuousLinearMap.exists_lt_apply_of_lt_op_norm {𝕜 : Type u_11} {𝕜₂ : Type u_12} {E : Type u_13} {F : Type u_14} [NormedAddCommGroup E] [SeminormedAddCommGroup F] [DenselyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] {σ₁₂ : 𝕜 →+* 𝕜₂} [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] [RingHomIsometric σ₁₂] (f : E →SL[σ₁₂] F) {r : ℝ} (hr : r < ‖f‖) : ∃ x, ‖x‖ < 1 ∧ r < ‖↑f x‖

theorem ContinuousLinearMap.sSup_unit_ball_eq_nnnorm {𝕜 : Type u_11} {𝕜₂ : Type u_12} {E : Type u_13} {F : Type u_14} [NormedAddCommGroup E] [SeminormedAddCommGroup F] [DenselyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] {σ₁₂ : 𝕜 →+* 𝕜₂} [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] [RingHomIsometric σ₁₂] (f : E →SL[σ₁₂] F) : sSup ((fun x => ‖↑f x‖₊) '' Metric.ball 0 1) = ‖f‖₊

theorem ContinuousLinearMap.sSup_unit_ball_eq_norm {𝕜 : Type u_11} {𝕜₂ : Type u_12} {E : Type u_13} {F : Type u_14} [NormedAddCommGroup E] [SeminormedAddCommGroup F] [DenselyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] {σ₁₂ : 𝕜 →+* 𝕜₂} [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] [RingHomIsometric σ₁₂] (f : E →SL[σ₁₂] F) : sSup ((fun x => ‖↑f x‖) '' Metric.ball 0 1) = ‖f‖

theorem ContinuousLinearMap.sSup_closed_unit_ball_eq_nnnorm {𝕜 : Type u_11} {𝕜₂ : Type u_12} {E : Type u_13} {F : Type u_14} [NormedAddCommGroup E] [SeminormedAddCommGroup F] [DenselyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] {σ₁₂ : 𝕜 →+* 𝕜₂} [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] [RingHomIsometric σ₁₂] (f : E →SL[σ₁₂] F) : sSup ((fun x => ‖↑f x‖₊) '' Metric.closedBall 0 1) = ‖f‖₊

theorem ContinuousLinearMap.sSup_closed_unit_ball_eq_norm {𝕜 : Type u_11} {𝕜₂ : Type u_12} {E : Type u_13} {F : Type u_14} [NormedAddCommGroup E] [SeminormedAddCommGroup F] [DenselyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] {σ₁₂ : 𝕜 →+* 𝕜₂} [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] [RingHomIsometric σ₁₂] (f : E →SL[σ₁₂] F) : sSup ((fun x => ‖↑f x‖) '' Metric.closedBall 0 1) = ‖f‖

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‖) : ‖f‖ = ‖g‖

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‖) : ‖f‖ ≤ C

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) : ‖↑(↑f x) y‖ ≤ ‖f‖ * ‖x‖ * ‖y‖

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) : ‖↑(↑f x) y‖ ≤ a * b * c

@[simp]

theorem ContinuousLinearMap.op_norm_prod {𝕜 : 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ₗ) (g : E →L[𝕜] Gₗ) : ‖ContinuousLinearMap.prod f g‖ = ‖(f, g)‖

@[simp]

theorem ContinuousLinearMap.op_nnnorm_prod {𝕜 : 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ₗ) (g : E →L[𝕜] Gₗ) : ‖ContinuousLinearMap.prod f g‖₊ = ‖(f, g)‖₊

noncomputable def ContinuousLinearMap.prodₗᵢ {𝕜 : 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ₗ] (R : Type u_11) [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' := (_ : ∀ (x : (E →L[𝕜] Fₗ) × (E →L[𝕜] Gₗ)), ‖↑(ContinuousLinearMap.prodₗ R) x‖ = ‖x‖) }

@[simp]

theorem ContinuousLinearMap.op_norm_subsingleton {𝕜 : 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 σ₁₂] (f : E →SL[σ₁₂] F) [Subsingleton E] : ‖f‖ = 0

theorem ContinuousLinearMap.isBigOWith_id {𝕜 : 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 σ₁₂] (f : E →SL[σ₁₂] F) (l : Filter E) : Asymptotics.IsBigOWith ‖f‖ l ↑f fun x => x

theorem ContinuousLinearMap.isBigO_id {𝕜 : 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 σ₁₂] (f : E →SL[σ₁₂] F) (l : Filter E) : ↑f =O[l] fun x => x

theorem ContinuousLinearMap.isBigOWith_comp {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {F : Type u_6} {G : Type u_8} [SeminormedAddCommGroup F] [SeminormedAddCommGroup G] [NontriviallyNormedField 𝕜₂] [NontriviallyNormedField 𝕜₃] [NormedSpace 𝕜₂ F] [NormedSpace 𝕜₃ G] {σ₂₃ : 𝕜₂ →+* 𝕜₃} [RingHomIsometric σ₂₃] {α : Type u_11} (g : F →SL[σ₂₃] G) (f : α → F) (l : Filter α) : Asymptotics.IsBigOWith ‖g‖ l (fun x' => ↑g (f x')) f

theorem ContinuousLinearMap.isBigO_comp {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {F : Type u_6} {G : Type u_8} [SeminormedAddCommGroup F] [SeminormedAddCommGroup G] [NontriviallyNormedField 𝕜₂] [NontriviallyNormedField 𝕜₃] [NormedSpace 𝕜₂ F] [NormedSpace 𝕜₃ G] {σ₂₃ : 𝕜₂ →+* 𝕜₃} [RingHomIsometric σ₂₃] {α : Type u_11} (g : F →SL[σ₂₃] G) (f : α → F) (l : Filter α) : (fun x' => ↑g (f x')) =O[l] f

theorem ContinuousLinearMap.isBigOWith_sub {𝕜 : 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 σ₁₂] (f : E →SL[σ₁₂] F) (l : Filter E) (x : E) : Asymptotics.IsBigOWith ‖f‖ l (fun x' => ↑f (x' - x)) fun x' => x' - x

theorem ContinuousLinearMap.isBigO_sub {𝕜 : 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 σ₁₂] (f : E →SL[σ₁₂] F) (l : Filter E) (x : E) : (fun x' => ↑f (x' - x)) =O[l] fun x' => x' - x

theorem LinearIsometry.norm_toContinuousLinearMap_le {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_6} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} (f : E →ₛₗᵢ[σ₁₂] F) : ‖LinearIsometry.toContinuousLinearMap f‖ ≤ 1

theorem LinearMap.mkContinuous_norm_le {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_6} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} (f : E →ₛₗ[σ₁₂] F) {C : ℝ} (hC : 0 ≤ C) (h : ∀ (x : E), ‖↑f x‖ ≤ C * ‖x‖) : ‖LinearMap.mkContinuous f C h‖ ≤ C

If a continuous linear map is constructed from a linear map via the constructor mkContinuous, then its norm is bounded by the bound given to the constructor if it is nonnegative.

theorem LinearMap.mkContinuous_norm_le' {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_6} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} (f : E →ₛₗ[σ₁₂] F) {C : ℝ} (h : ∀ (x : E), ‖↑f x‖ ≤ C * ‖x‖) : ‖LinearMap.mkContinuous f C h‖ ≤ max C 0

If a continuous linear map is constructed from a linear map via the constructor mkContinuous, then its norm is bounded by the bound or zero if bound is negative.

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) : ‖LinearMap.mkContinuous (↑f x) (C * ‖x‖) (h x)‖ ≤ max C 0 * ‖x‖

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‖) : E →SL[σ₁₃] F →SL[σ₂₃] G

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.

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‖) : E →SL[σ₁₃] F →SL[σ₂₃] G

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

• LinearMap.mkContinuous₂ f C hC = LinearMap.mkContinuousOfExistsBound₂ f (_ : ∃ C, ∀ (x : E) (y : F), ‖↑(↑f x) y‖ ≤ C * ‖x‖ * ‖y‖)

@[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) : F →SL[σ₂₃] E →SL[σ₁₃] G

Flip the order of arguments of a continuous bilinear map. For a version bundled as LinearIsometryEquiv, see ContinuousLinearMap.flipL.

Equations

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

@[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) : ContinuousLinearMap.flip (ContinuousLinearMap.flip f) = f

@[simp]

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) : ‖ContinuousLinearMap.flip f‖ = ‖f‖

@[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) : ContinuousLinearMap.flip (f + g) = ContinuousLinearMap.flip f + ContinuousLinearMap.flip 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 σ₁₃] : (E →SL[σ₁₃] F →SL[σ₂₃] G) ≃ₗᵢ[𝕜₃] F →SL[σ₂₃] E →SL[σ₁₃] 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.

@[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ₗ] : (E →L[𝕜] Fₗ →L[𝕜] Gₗ) ≃ₗᵢ[𝕜] Fₗ →L[𝕜] E →L[𝕜] 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.

@[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 σ₁₂] : E →SL[σ₁₂] (E →SL[σ₁₂] F) →L[𝕜₂] 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 →SL[σ₁₂] F))

@[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ₗ] : E →L[𝕜] (E →L[𝕜] Fₗ) →L[𝕜] 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ₗ))

@[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 σ₁₂] : (F →SL[σ₂₃] G) →L[𝕜₃] (E →SL[σ₁₂] F) →SL[σ₂₃] E →SL[σ₁₃] G

Composition of continuous semilinear maps as a continuous semibilinear map.

Equations

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

noncomputable def ContinuousLinearMap.instNormContinuousLinearMapToSemiringToDivisionSemiringToSemifieldToFieldToNormedFieldIdToNonAssocSemiringContinuousLinearMapToSemiringToDivisionSemiringToSemifieldToFieldToNormedFieldToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceToAddCommMonoidToAddCommGroupToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceToAddCommMonoidToAddCommGroupToModuleToModuleTopologicalSpaceToTopologicalAddGroupAddCommMonoidToContinuousAddToAddGroupToSeminormedAddGroupContinuousLinearMapContinuousLinearMapToSemiringToDivisionSemiringToSemifieldToFieldToNormedFieldToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceToAddCommMonoidToAddCommGroupToModuleTopologicalSpaceToTopologicalAddGroupAddCommMonoidToContinuousAddToAddGroupToSeminormedAddGroupContinuousLinearMapTopologicalSpaceAddCommMonoidModuleSmulCommClass_selfToCommMonoidToCommRingToEuclideanDomainToMulActionToMonoidWithZeroToZeroToNegZeroClassToSubNegZeroMonoidToSubtractionMonoidToDivisionAddCommMonoidToMulActionWithZeroContinuousConstSMulToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceToSeminormedRingToSeminormedCommRingToNormedCommRingToSMulToZeroToAddMonoidToSMulZeroClassToZeroToSMulWithZeroContinuousSMulToZeroToCommMonoidWithZeroToCommGroupWithZeroBoundedSMulModuleSmulCommClass_selfToCommMonoidToCommRingToEuclideanDomainToMulActionToMonoidWithZeroToZeroToNegZeroClassToSubNegZeroMonoidToSubtractionMonoidToDivisionAddCommMonoidToMulActionWithZeroContinuousConstSMulToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceToSeminormedRingToSeminormedCommRingToNormedCommRingToSMulToZeroToAddMonoidToSMulZeroClassToZeroToSMulWithZeroContinuousSMulToZeroToCommMonoidWithZeroToCommGroupWithZeroBoundedSMulTopologicalSpaceAddCommGroupToRingToNormedRingToNormedCommRingToRingToNormedRingAddCommGroupToRingToNormedRingTopologicalAddGroupAddCommMonoidToContinuousAddToAddGroupToSeminormedAddGroupToSeminormedAddCommGroupModuleModuleSmulCommClassToMonoidToDistribMulActionToSMulZeroClassToAddZeroClassToDistribSMulContinuousConstSMulToSMulToZeroToAddMonoidToSMulZeroClassToSMulWithZeroToMulActionWithZeroContinuousSMulToPseudoMetricSpaceZeroBoundedSMulToNormedSpace {𝕜 : 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 σ₁₃] [RingHomIsometric σ₁₂] : Norm ((F →SL[σ₂₃] G) →L[𝕜₃] (E →SL[σ₁₂] F) →SL[σ₂₃] E →SL[σ₁₃] G)

Porting note: Local instance for norm_compSL_le. Should be by inferInstance, and indeed not be needed.

Equations

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

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 => 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 => 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ₗ] : (Fₗ →L[𝕜] Gₗ) →L[𝕜] (E →L[𝕜] Fₗ) →L[𝕜] E →L[𝕜] 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 𝕜)

noncomputable def ContinuousLinearMap.instNormContinuousLinearMapToSemiringToDivisionSemiringToSemifieldToFieldToNormedFieldIdToNonAssocSemiringContinuousLinearMapToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceToAddCommMonoidToAddCommGroupToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceToAddCommMonoidToAddCommGroupToModuleToModuleTopologicalSpaceToTopologicalAddGroupAddCommMonoidToContinuousAddToAddGroupToSeminormedAddGroupContinuousLinearMapContinuousLinearMapToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceToAddCommMonoidToAddCommGroupToModuleTopologicalSpaceToTopologicalAddGroupAddCommMonoidToContinuousAddToAddGroupToSeminormedAddGroupContinuousLinearMapTopologicalSpaceAddCommMonoidModuleSmulCommClass_selfToCommMonoidToCommRingToEuclideanDomainToMulActionToMonoidWithZeroToZeroToNegZeroClassToSubNegZeroMonoidToSubtractionMonoidToDivisionAddCommMonoidToMulActionWithZeroContinuousConstSMulToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceToSeminormedRingToSeminormedCommRingToNormedCommRingToSMulToZeroToAddMonoidToSMulZeroClassToZeroToSMulWithZeroContinuousSMulToZeroToCommMonoidWithZeroToCommGroupWithZeroBoundedSMulModuleSmulCommClass_selfToMulActionToZeroToNegZeroClassToSubNegZeroMonoidToSubtractionMonoidToDivisionAddCommMonoidToMulActionWithZeroContinuousConstSMulToSMulToZeroToAddMonoidToSMulZeroClassToSMulWithZeroContinuousSMulBoundedSMulTopologicalSpaceAddCommGroupToRingToNormedRingAddCommGroupTopologicalAddGroupAddCommMonoidToContinuousAddToAddGroupToSeminormedAddGroupToSeminormedAddCommGroupIdsModuleModuleSmulCommClassToMonoidToDistribMulActionToSMulZeroClassToAddZeroClassToDistribSMulContinuousConstSMulToSMulToZeroToAddMonoidToSMulZeroClassToSMulWithZeroToMulActionWithZeroContinuousSMulIds (𝕜 : 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ₗ] : Norm ((Fₗ →L[𝕜] Gₗ) →L[𝕜] (E →L[𝕜] Fₗ) →L[𝕜] E →L[𝕜] Gₗ)

Porting note: Local instance for norm_compL_le. Should be by inferInstance, and indeed not be needed.

Equations

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

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ₗ) : E →L[𝕜] (Eₗ →L[𝕜] Fₗ) →L[𝕜] Eₗ →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

@[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ₗ) : (Eₗ →L[𝕜] E) →L[𝕜] Fₗ →L[𝕜] Eₗ →L[𝕜] Gₗ

Apply L(-,y) pointwise to bilinear maps, as a continuous bilinear map

Equations

• ContinuousLinearMap.precompL Eₗ L = ContinuousLinearMap.flip (ContinuousLinearMap.precompR Eₗ (ContinuousLinearMap.flip L))

noncomputable def ContinuousLinearMap.instSeminormedAddCommGroupContinuousLinearMapToSemiringToDivisionSemiringToSemifieldToFieldToNormedFieldIdToNonAssocSemiringContinuousLinearMapToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceToAddCommMonoidToAddCommGroupToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceToAddCommMonoidToAddCommGroupToModuleToModuleTopologicalSpaceToTopologicalAddGroupAddCommMonoidToContinuousAddToAddGroupToSeminormedAddGroupContinuousLinearMapToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceToAddCommMonoidToAddCommGroupToModuleTopologicalSpaceToTopologicalAddGroupAddCommMonoidToContinuousAddToAddGroupToSeminormedAddGroupModuleSmulCommClass_selfToCommMonoidToCommRingToEuclideanDomainToMulActionToMonoidWithZeroToZeroToNegZeroClassToSubNegZeroMonoidToSubtractionMonoidToDivisionAddCommMonoidToMulActionWithZeroContinuousConstSMulToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceToSeminormedRingToSeminormedCommRingToNormedCommRingToSMulToZeroToAddMonoidToSMulZeroClassToZeroToSMulWithZeroContinuousSMulToZeroToCommMonoidWithZeroToCommGroupWithZeroBoundedSMulModuleSmulCommClass_selfToMulActionToZeroToNegZeroClassToSubNegZeroMonoidToSubtractionMonoidToDivisionAddCommMonoidToMulActionWithZeroContinuousConstSMulToSMulToZeroToAddMonoidToSMulZeroClassToSMulWithZeroContinuousSMulBoundedSMul {𝕜 : Type u_1} (Eₗ : Type u_5) {Fₗ : Type u_7} {Gₗ : Type u_9} [SeminormedAddCommGroup Eₗ] [SeminormedAddCommGroup Fₗ] [SeminormedAddCommGroup Gₗ] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 Eₗ] [NormedSpace 𝕜 Fₗ] [NormedSpace 𝕜 Gₗ] : SeminormedAddCommGroup ((Eₗ →L[𝕜] Fₗ) →L[𝕜] Eₗ →L[𝕜] Gₗ)

Porting note: Local instances for norm_precompR_le. Should be by inferInstance, and indeed not be needed.

Equations

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

noncomputable def ContinuousLinearMap.instNormedSpaceContinuousLinearMapToSemiringToDivisionSemiringToSemifieldToFieldToNormedFieldIdToNonAssocSemiringContinuousLinearMapToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceToAddCommMonoidToAddCommGroupToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceToAddCommMonoidToAddCommGroupToModuleToModuleTopologicalSpaceToTopologicalAddGroupAddCommMonoidToContinuousAddToAddGroupToSeminormedAddGroupContinuousLinearMapToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceToAddCommMonoidToAddCommGroupToModuleTopologicalSpaceToTopologicalAddGroupAddCommMonoidToContinuousAddToAddGroupToSeminormedAddGroupModuleSmulCommClass_selfToCommMonoidToCommRingToEuclideanDomainToMulActionToMonoidWithZeroToZeroToNegZeroClassToSubNegZeroMonoidToSubtractionMonoidToDivisionAddCommMonoidToMulActionWithZeroContinuousConstSMulToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceToSeminormedRingToSeminormedCommRingToNormedCommRingToSMulToZeroToAddMonoidToSMulZeroClassToZeroToSMulWithZeroContinuousSMulToZeroToCommMonoidWithZeroToCommGroupWithZeroBoundedSMulModuleSmulCommClass_selfToMulActionToZeroToNegZeroClassToSubNegZeroMonoidToSubtractionMonoidToDivisionAddCommMonoidToMulActionWithZeroContinuousConstSMulToSMulToZeroToAddMonoidToSMulZeroClassToSMulWithZeroContinuousSMulBoundedSMulInstSeminormedAddCommGroupContinuousLinearMapToSemiringToDivisionSemiringToSemifieldToFieldToNormedFieldIdToNonAssocSemiringContinuousLinearMapToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceToAddCommMonoidToAddCommGroupToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceToAddCommMonoidToAddCommGroupToModuleToModuleTopologicalSpaceToTopologicalAddGroupAddCommMonoidToContinuousAddToAddGroupToSeminormedAddGroupContinuousLinearMapToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceToAddCommMonoidToAddCommGroupToModuleTopologicalSpaceToTopologicalAddGroupAddCommMonoidToContinuousAddToAddGroupToSeminormedAddGroupModuleSmulCommClass_selfToCommMonoidToCommRingToEuclideanDomainToMulActionToMonoidWithZeroToZeroToNegZeroClassToSubNegZeroMonoidToSubtractionMonoidToDivisionAddCommMonoidToMulActionWithZeroContinuousConstSMulToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceToSeminormedRingToSeminormedCommRingToNormedCommRingToSMulToZeroToAddMonoidToSMulZeroClassToZeroToSMulWithZeroContinuousSMulToZeroToCommMonoidWithZeroToCommGroupWithZeroBoundedSMulModuleSmulCommClass_selfToMulActionToZeroToNegZeroClassToSubNegZeroMonoidToSubtractionMonoidToDivisionAddCommMonoidToMulActionWithZeroContinuousConstSMulToSMulToZeroToAddMonoidToSMulZeroClassToSMulWithZeroContinuousSMulBoundedSMul {𝕜 : Type u_1} (Eₗ : Type u_5) {Fₗ : Type u_7} {Gₗ : Type u_9} [SeminormedAddCommGroup Eₗ] [SeminormedAddCommGroup Fₗ] [SeminormedAddCommGroup Gₗ] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 Eₗ] [NormedSpace 𝕜 Fₗ] [NormedSpace 𝕜 Gₗ] : NormedSpace 𝕜 ((Eₗ →L[𝕜] Fₗ) →L[𝕜] Eₗ →L[𝕜] Gₗ)

Equations

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

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ₗ) : ‖ContinuousLinearMap.precompR Eₗ L‖ ≤ ‖L‖

noncomputable def ContinuousLinearMap.instNormContinuousLinearMapToSemiringToDivisionSemiringToSemifieldToFieldToNormedFieldIdToNonAssocSemiringContinuousLinearMapToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceToAddCommMonoidToAddCommGroupToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceToAddCommMonoidToAddCommGroupToModuleToModuleTopologicalSpaceToTopologicalAddGroupAddCommMonoidToContinuousAddToAddGroupToSeminormedAddGroupContinuousLinearMapToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceToAddCommMonoidToAddCommGroupContinuousLinearMapToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceToAddCommMonoidToAddCommGroupToModuleTopologicalSpaceToTopologicalAddGroupAddCommMonoidToContinuousAddToAddGroupToSeminormedAddGroupToModuleModuleSmulCommClass_selfToCommMonoidToCommRingToEuclideanDomainToMulActionToMonoidWithZeroToZeroToNegZeroClassToSubNegZeroMonoidToSubtractionMonoidToDivisionAddCommMonoidToMulActionWithZeroContinuousConstSMulToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceToSeminormedRingToSeminormedCommRingToNormedCommRingToSMulToZeroToAddMonoidToSMulZeroClassToZeroToSMulWithZeroContinuousSMulToZeroToCommMonoidWithZeroToCommGroupWithZeroBoundedSMulTopologicalSpaceAddCommGroupToRingToNormedRingTopologicalAddGroupAddCommMonoidToContinuousAddToAddGroupToSeminormedAddGroupToSeminormedAddCommGroupIdsModuleSmulCommClass_selfToMulActionToZeroToNegZeroClassToSubNegZeroMonoidToSubtractionMonoidToDivisionAddCommMonoidToMulActionWithZeroContinuousConstSMulToSMulToZeroToAddMonoidToSMulZeroClassToSMulWithZeroContinuousSMulBoundedSMulModuleSmulCommClassToMonoidToDistribMulActionToSMulZeroClassToAddZeroClassToDistribSMulContinuousConstSMulToSMulToZeroToAddMonoidToSMulZeroClassToSMulWithZeroToMulActionWithZeroContinuousSMulIds {𝕜 : 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ₗ] : Norm ((Eₗ →L[𝕜] E) →L[𝕜] Fₗ →L[𝕜] Eₗ →L[𝕜] Gₗ)

Porting note: Local instance for norm_precompL_le. Should be by inferInstance, and indeed not be needed.

Equations

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

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ₗ) : ‖ContinuousLinearMap.precompL Eₗ L‖ ≤ ‖L‖

noncomputable def ContinuousLinearMap.prodMapL (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (M₁ : Type u₁) [SeminormedAddCommGroup M₁] [NormedSpace 𝕜 M₁] (M₂ : Type u₂) [SeminormedAddCommGroup M₂] [NormedSpace 𝕜 M₂] (M₃ : Type u₃) [SeminormedAddCommGroup M₃] [NormedSpace 𝕜 M₃] (M₄ : Type u₄) [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₁} [SeminormedAddCommGroup M₁] [NormedSpace 𝕜 M₁] {M₂ : Type u₂} [SeminormedAddCommGroup M₂] [NormedSpace 𝕜 M₂] {M₃ : Type u₃} [SeminormedAddCommGroup M₃] [NormedSpace 𝕜 M₃] {M₄ : Type u₄} [SeminormedAddCommGroup M₄] [NormedSpace 𝕜 M₄] (p : (M₁ →L[𝕜] M₂) × (M₃ →L[𝕜] M₄)) : ↑(ContinuousLinearMap.prodMapL 𝕜 M₁ M₂ M₃ M₄) p = ContinuousLinearMap.prodMap p.fst p.snd

theorem Continuous.prod_mapL (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {M₁ : Type u₁} [SeminormedAddCommGroup M₁] [NormedSpace 𝕜 M₁] {M₂ : Type u₂} [SeminormedAddCommGroup M₂] [NormedSpace 𝕜 M₂] {M₃ : Type u₃} [SeminormedAddCommGroup M₃] [NormedSpace 𝕜 M₃] {M₄ : Type u₄} [SeminormedAddCommGroup M₄] [NormedSpace 𝕜 M₄] {X : Type u_11} [TopologicalSpace X] {f : X → M₁ →L[𝕜] M₂} {g : X → M₃ →L[𝕜] M₄} (hf : Continuous f) (hg : Continuous g) : Continuous fun x => ContinuousLinearMap.prodMap (f x) (g x)

theorem Continuous.prod_map_equivL (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {M₁ : Type u₁} [SeminormedAddCommGroup M₁] [NormedSpace 𝕜 M₁] {M₂ : Type u₂} [SeminormedAddCommGroup M₂] [NormedSpace 𝕜 M₂] {M₃ : Type u₃} [SeminormedAddCommGroup M₃] [NormedSpace 𝕜 M₃] {M₄ : Type u₄} [SeminormedAddCommGroup M₄] [NormedSpace 𝕜 M₄] {X : Type u_11} [TopologicalSpace X] {f : X → M₁ ≃L[𝕜] M₂} {g : X → M₃ ≃L[𝕜] M₄} (hf : Continuous fun x => ↑(f x)) (hg : Continuous fun x => ↑(g x)) : Continuous fun x => ↑(ContinuousLinearEquiv.prod (f x) (g x))

theorem ContinuousOn.prod_mapL (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {M₁ : Type u₁} [SeminormedAddCommGroup M₁] [NormedSpace 𝕜 M₁] {M₂ : Type u₂} [SeminormedAddCommGroup M₂] [NormedSpace 𝕜 M₂] {M₃ : Type u₃} [SeminormedAddCommGroup M₃] [NormedSpace 𝕜 M₃] {M₄ : Type u₄} [SeminormedAddCommGroup M₄] [NormedSpace 𝕜 M₄] {X : Type u_11} [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 => ContinuousLinearMap.prodMap (f x) (g x)) s

theorem ContinuousOn.prod_map_equivL (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {M₁ : Type u₁} [SeminormedAddCommGroup M₁] [NormedSpace 𝕜 M₁] {M₂ : Type u₂} [SeminormedAddCommGroup M₂] [NormedSpace 𝕜 M₂] {M₃ : Type u₃} [SeminormedAddCommGroup M₃] [NormedSpace 𝕜 M₃] {M₄ : Type u₄} [SeminormedAddCommGroup M₄] [NormedSpace 𝕜 M₄] {X : Type u_11} [TopologicalSpace X] {f : X → M₁ ≃L[𝕜] M₂} {g : X → M₃ ≃L[𝕜] M₄} {s : Set X} (hf : ContinuousOn (fun x => ↑(f x)) s) (hg : ContinuousOn (fun x => ↑(g x)) s) : ContinuousOn (fun x => ↑(ContinuousLinearEquiv.prod (f x) (g x))) s

noncomputable def ContinuousLinearMap.mul (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (𝕜' : Type u_11) [NonUnitalSeminormedRing 𝕜'] [NormedSpace 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' 𝕜'] [SMulCommClass 𝕜 𝕜' 𝕜'] : 𝕜' →L[𝕜] 𝕜' →L[𝕜] 𝕜'

Multiplication in a non-unital normed algebra as a continuous bilinear map.

Equations

• ContinuousLinearMap.mul 𝕜 𝕜' = LinearMap.mkContinuous₂ (LinearMap.mul 𝕜 𝕜') 1 (_ : ∀ (x y : 𝕜'), ‖↑(↑(LinearMap.mul 𝕜 𝕜') x) y‖ ≤ 1 * ‖x‖ * ‖y‖)

@[simp]

theorem ContinuousLinearMap.mul_apply' (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (𝕜' : Type u_11) [NonUnitalSeminormedRing 𝕜'] [NormedSpace 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' 𝕜'] [SMulCommClass 𝕜 𝕜' 𝕜'] (x : 𝕜') (y : 𝕜') : ↑(↑(ContinuousLinearMap.mul 𝕜 𝕜') x) y = x * y

@[simp]

theorem ContinuousLinearMap.op_norm_mul_apply_le (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (𝕜' : Type u_11) [NonUnitalSeminormedRing 𝕜'] [NormedSpace 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' 𝕜'] [SMulCommClass 𝕜 𝕜' 𝕜'] (x : 𝕜') : ‖↑(ContinuousLinearMap.mul 𝕜 𝕜') x‖ ≤ ‖x‖

theorem ContinuousLinearMap.op_norm_mul_le (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (𝕜' : Type u_11) [NonUnitalSeminormedRing 𝕜'] [NormedSpace 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' 𝕜'] [SMulCommClass 𝕜 𝕜' 𝕜'] : ‖ContinuousLinearMap.mul 𝕜 𝕜'‖ ≤ 1

noncomputable def NonUnitalAlgHom.Lmul (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (𝕜' : Type u_11) [NonUnitalSeminormedRing 𝕜'] [NormedSpace 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' 𝕜'] [SMulCommClass 𝕜 𝕜' 𝕜'] : 𝕜' →ₙₐ[𝕜] 𝕜' →L[𝕜] 𝕜'

Multiplication on the left in a non-unital normed algebra 𝕜' as a non-unital algebra homomorphism into the algebra of continuous linear maps. This is the left regular representation of A acting on itself.

This has more algebraic structure than ContinuousLinearMap.mul, but there is no longer continuity bundled in the first coordinate. An alternative viewpoint is that this upgrades NonUnitalAlgHom.lmul from a homomorphism into linear maps to a homomorphism into continuous linear maps.

Equations

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

@[simp]

theorem NonUnitalAlgHom.coe_Lmul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {𝕜' : Type u_11} [NonUnitalSeminormedRing 𝕜'] [NormedSpace 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' 𝕜'] [SMulCommClass 𝕜 𝕜' 𝕜'] : ↑(NonUnitalAlgHom.Lmul 𝕜 𝕜') = ↑(ContinuousLinearMap.mul 𝕜 𝕜')

noncomputable def ContinuousLinearMap.mulLeftRight (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (𝕜' : Type u_11) [NonUnitalSeminormedRing 𝕜'] [NormedSpace 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' 𝕜'] [SMulCommClass 𝕜 𝕜' 𝕜'] : 𝕜' →L[𝕜] 𝕜' →L[𝕜] 𝕜' →L[𝕜] 𝕜'

Simultaneous left- and right-multiplication in a non-unital normed algebra, considered as a continuous trilinear map. This is akin to its non-continuous version LinearMap.mulLeftRight, but there is a minor difference: LinearMap.mulLeftRight is uncurried.

Equations

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

@[simp]

theorem ContinuousLinearMap.mulLeftRight_apply (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (𝕜' : Type u_11) [NonUnitalSeminormedRing 𝕜'] [NormedSpace 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' 𝕜'] [SMulCommClass 𝕜 𝕜' 𝕜'] (x : 𝕜') (y : 𝕜') (z : 𝕜') : ↑(↑(↑(ContinuousLinearMap.mulLeftRight 𝕜 𝕜') x) y) z = x * z * y

theorem ContinuousLinearMap.op_norm_mulLeftRight_apply_apply_le (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (𝕜' : Type u_11) [NonUnitalSeminormedRing 𝕜'] [NormedSpace 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' 𝕜'] [SMulCommClass 𝕜 𝕜' 𝕜'] (x : 𝕜') (y : 𝕜') : ‖↑(↑(ContinuousLinearMap.mulLeftRight 𝕜 𝕜') x) y‖ ≤ ‖x‖ * ‖y‖

theorem ContinuousLinearMap.op_norm_mulLeftRight_apply_le (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (𝕜' : Type u_11) [NonUnitalSeminormedRing 𝕜'] [NormedSpace 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' 𝕜'] [SMulCommClass 𝕜 𝕜' 𝕜'] (x : 𝕜') : ‖↑(ContinuousLinearMap.mulLeftRight 𝕜 𝕜') x‖ ≤ ‖x‖

noncomputable def ContinuousLinearMap.instNormContinuousLinearMapToSemiringToDivisionSemiringToSemifieldToFieldToNormedFieldIdToNonAssocSemiringToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceToAddCommMonoidToNonUnitalNonAssocSemiringToNonUnitalNonAssocRingToNonUnitalRingToModuleToSeminormedAddCommGroupTopologicalSpaceToAddCommGroupToTopologicalAddGroupAddCommMonoidToContinuousAddToTopologicalSemiringSemi_normed_top_ringModuleSmulCommClass_selfToCommMonoidToCommRingToEuclideanDomainToMulActionToMonoidWithZeroToZeroToSemigroupWithZeroToNonUnitalSemiringToMulActionWithZeroContinuousConstSMulToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceToSeminormedRingToSeminormedCommRingToNormedCommRingToSMulToZeroToAddMonoidToSMulZeroClassToZeroToSMulWithZeroContinuousSMulToZeroToCommMonoidWithZeroToCommGroupWithZeroBoundedSMulAddCommGroupToRingToNormedRingTopologicalAddGroupToNonUnitalNonAssocRingToNonAssocRingRingToNonUnitalSeminormedRingToSemiNormedRingSmulCommClassToMonoidToDistribMulActionToSMulZeroClassToAddZeroClassToDistribSMulContinuousConstSMulToMonoidMonoidWithZeroSmulCommClassToDistribMulActionSemiringApplyModuleApplySMulCommClassContinuousConstSMulToContinuousMul (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (𝕜' : Type u_11) [NonUnitalSeminormedRing 𝕜'] [NormedSpace 𝕜 𝕜'] : Norm (𝕜' →L[𝕜] 𝕜' →L[𝕜] 𝕜' →L[𝕜] 𝕜')

Porting note: Local instance for op_norm_mulLeftRight_le. Should be by inferInstance, and indeed not be needed.

Equations

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

theorem ContinuousLinearMap.op_norm_mulLeftRight_le (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (𝕜' : Type u_11) [NonUnitalSeminormedRing 𝕜'] [NormedSpace 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' 𝕜'] [SMulCommClass 𝕜 𝕜' 𝕜'] : ‖ContinuousLinearMap.mulLeftRight 𝕜 𝕜'‖ ≤ 1

class RegularNormedAlgebra (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (𝕜' : Type u_11) [NonUnitalSeminormedRing 𝕜'] [NormedSpace 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' 𝕜'] [SMulCommClass 𝕜 𝕜' 𝕜'] : Prop

• isometry_mul' : Isometry ↑(ContinuousLinearMap.mul 𝕜 𝕜')

  The left regular representation of the algebra on itself is an isometry.

This is a mixin class for non-unital normed algebras which states that the left-regular representation of the algebra on itself is isometric. Every unital normed algebra with ‖1‖ = 1 is a regular normed algebra (see NormedAlgebra.instRegularNormedAlgebra). In addition, so is every C⋆-algebra, non-unital included (see CstarRing.instRegularNormedAlgebra), but there are yet other examples. Any algebra with an approximate identity (e.g., $$L^1$$) is also regular.

This is a useful class because it gives rise to a nice norm on the unitization; in particular it is a C⋆-norm when the norm on A is a C⋆-norm.

noncomputable instance NormedAlgebra.instRegularNormedAlgebra {𝕜 : Type u_12} {𝕜' : Type u_13} [NontriviallyNormedField 𝕜] [SeminormedRing 𝕜'] [NormedAlgebra 𝕜 𝕜'] [NormOneClass 𝕜'] : RegularNormedAlgebra 𝕜 𝕜'

Every (unital) normed algebra such that ‖1‖ = 1 is a RegularNormedAlgebra.

Equations

• @NormedAlgebra.instRegularNormedAlgebra = @NormedAlgebra.instRegularNormedAlgebra.proof_1

theorem ContinuousLinearMap.isometry_mul (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (𝕜' : Type u_11) [NonUnitalSeminormedRing 𝕜'] [NormedSpace 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' 𝕜'] [SMulCommClass 𝕜 𝕜' 𝕜'] [RegularNormedAlgebra 𝕜 𝕜'] : Isometry ↑(ContinuousLinearMap.mul 𝕜 𝕜')

@[simp]

theorem ContinuousLinearMap.op_norm_mul_apply (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (𝕜' : Type u_11) [NonUnitalSeminormedRing 𝕜'] [NormedSpace 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' 𝕜'] [SMulCommClass 𝕜 𝕜' 𝕜'] [RegularNormedAlgebra 𝕜 𝕜'] (x : 𝕜') : ‖↑(ContinuousLinearMap.mul 𝕜 𝕜') x‖ = ‖x‖

@[simp]

theorem ContinuousLinearMap.op_nnnorm_mul_apply (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (𝕜' : Type u_11) [NonUnitalSeminormedRing 𝕜'] [NormedSpace 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' 𝕜'] [SMulCommClass 𝕜 𝕜' 𝕜'] [RegularNormedAlgebra 𝕜 𝕜'] (x : 𝕜') : ‖↑(ContinuousLinearMap.mul 𝕜 𝕜') x‖₊ = ‖x‖₊

noncomputable def ContinuousLinearMap.mulₗᵢ (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (𝕜' : Type u_11) [NonUnitalSeminormedRing 𝕜'] [NormedSpace 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' 𝕜'] [SMulCommClass 𝕜 𝕜' 𝕜'] [RegularNormedAlgebra 𝕜 𝕜'] : 𝕜' →ₗᵢ[𝕜] 𝕜' →L[𝕜] 𝕜'

Multiplication in a normed algebra as a linear isometry to the space of continuous linear maps.

Equations

• ContinuousLinearMap.mulₗᵢ 𝕜 𝕜' = { toLinearMap := ↑(ContinuousLinearMap.mul 𝕜 𝕜'), norm_map' := (_ : ∀ (x : 𝕜'), ‖↑(ContinuousLinearMap.mul 𝕜 𝕜') x‖ = ‖x‖) }

@[simp]

theorem ContinuousLinearMap.coe_mulₗᵢ (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (𝕜' : Type u_11) [NonUnitalSeminormedRing 𝕜'] [NormedSpace 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' 𝕜'] [SMulCommClass 𝕜 𝕜' 𝕜'] [RegularNormedAlgebra 𝕜 𝕜'] : ↑(ContinuousLinearMap.mulₗᵢ 𝕜 𝕜') = ↑(ContinuousLinearMap.mul 𝕜 𝕜')

noncomputable def ContinuousLinearMap.lsmul (𝕜 : Type u_1) {E : Type u_4} [SeminormedAddCommGroup E] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] (𝕜' : Type u_11) [NormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] [NormedSpace 𝕜' E] [IsScalarTower 𝕜 𝕜' E] : 𝕜' →L[𝕜] E →L[𝕜] E

Scalar multiplication as a continuous bilinear map.

Equations

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

@[simp]

theorem ContinuousLinearMap.lsmul_apply (𝕜 : Type u_1) {E : Type u_4} [SeminormedAddCommGroup E] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] (𝕜' : Type u_11) [NormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] [NormedSpace 𝕜' E] [IsScalarTower 𝕜 𝕜' E] (c : 𝕜') (x : E) : ↑(↑(ContinuousLinearMap.lsmul 𝕜 𝕜') c) x = c • x

theorem ContinuousLinearMap.norm_toSpanSingleton (𝕜 : Type u_1) {E : Type u_4} [SeminormedAddCommGroup E] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] (x : E) : ‖ContinuousLinearMap.toSpanSingleton 𝕜 x‖ = ‖x‖

theorem ContinuousLinearMap.op_norm_lsmul_apply_le {𝕜 : Type u_1} {E : Type u_4} [SeminormedAddCommGroup E] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] {𝕜' : Type u_11} [NormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] [NormedSpace 𝕜' E] [IsScalarTower 𝕜 𝕜' E] (x : 𝕜') : ‖↑(ContinuousLinearMap.lsmul 𝕜 𝕜') x‖ ≤ ‖x‖

theorem ContinuousLinearMap.op_norm_lsmul_le {𝕜 : Type u_1} {E : Type u_4} [SeminormedAddCommGroup E] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] {𝕜' : Type u_11} [NormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] [NormedSpace 𝕜' E] [IsScalarTower 𝕜 𝕜' E] : ‖ContinuousLinearMap.lsmul 𝕜 𝕜'‖ ≤ 1

The norm of lsmul is at most 1 in any semi-normed group.

@[simp]

theorem ContinuousLinearMap.norm_restrictScalars {𝕜 : Type u_1} {E : Type u_4} {Fₗ : Type u_7} [SeminormedAddCommGroup E] [SeminormedAddCommGroup Fₗ] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 Fₗ] {𝕜' : Type u_11} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜' 𝕜] [NormedSpace 𝕜' E] [IsScalarTower 𝕜' 𝕜 E] [NormedSpace 𝕜' Fₗ] [IsScalarTower 𝕜' 𝕜 Fₗ] (f : E →L[𝕜] Fₗ) : ‖ContinuousLinearMap.restrictScalars 𝕜' f‖ = ‖f‖

noncomputable def ContinuousLinearMap.restrictScalarsIsometry (𝕜 : Type u_1) (E : Type u_4) (Fₗ : Type u_7) [SeminormedAddCommGroup E] [SeminormedAddCommGroup Fₗ] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 Fₗ] (𝕜' : Type u_11) [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜' 𝕜] [NormedSpace 𝕜' E] [IsScalarTower 𝕜' 𝕜 E] [NormedSpace 𝕜' Fₗ] [IsScalarTower 𝕜' 𝕜 Fₗ] (𝕜'' : Type u_12) [Ring 𝕜''] [Module 𝕜'' Fₗ] [ContinuousConstSMul 𝕜'' Fₗ] [SMulCommClass 𝕜 𝕜'' Fₗ] [SMulCommClass 𝕜' 𝕜'' Fₗ] : (E →L[𝕜] Fₗ) →ₗᵢ[𝕜''] E →L[𝕜'] Fₗ

ContinuousLinearMap.restrictScalars as a LinearIsometry.

Equations

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

@[simp]

theorem ContinuousLinearMap.coe_restrictScalarsIsometry (𝕜 : Type u_1) (E : Type u_4) (Fₗ : Type u_7) [SeminormedAddCommGroup E] [SeminormedAddCommGroup Fₗ] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 Fₗ] (𝕜' : Type u_11) [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜' 𝕜] [NormedSpace 𝕜' E] [IsScalarTower 𝕜' 𝕜 E] [NormedSpace 𝕜' Fₗ] [IsScalarTower 𝕜' 𝕜 Fₗ] {𝕜'' : Type u_12} [Ring 𝕜''] [Module 𝕜'' Fₗ] [ContinuousConstSMul 𝕜'' Fₗ] [SMulCommClass 𝕜 𝕜'' Fₗ] [SMulCommClass 𝕜' 𝕜'' Fₗ] : ↑(ContinuousLinearMap.restrictScalarsIsometry 𝕜 E Fₗ 𝕜' 𝕜'') = ContinuousLinearMap.restrictScalars 𝕜'

@[simp]

theorem ContinuousLinearMap.restrictScalarsIsometry_toLinearMap (𝕜 : Type u_1) (E : Type u_4) (Fₗ : Type u_7) [SeminormedAddCommGroup E] [SeminormedAddCommGroup Fₗ] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 Fₗ] (𝕜' : Type u_11) [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜' 𝕜] [NormedSpace 𝕜' E] [IsScalarTower 𝕜' 𝕜 E] [NormedSpace 𝕜' Fₗ] [IsScalarTower 𝕜' 𝕜 Fₗ] {𝕜'' : Type u_12} [Ring 𝕜''] [Module 𝕜'' Fₗ] [ContinuousConstSMul 𝕜'' Fₗ] [SMulCommClass 𝕜 𝕜'' Fₗ] [SMulCommClass 𝕜' 𝕜'' Fₗ] : (ContinuousLinearMap.restrictScalarsIsometry 𝕜 E Fₗ 𝕜' 𝕜'').toLinearMap = ContinuousLinearMap.restrictScalarsₗ 𝕜 E Fₗ 𝕜' 𝕜''

noncomputable def ContinuousLinearMap.restrictScalarsL (𝕜 : Type u_1) (E : Type u_4) (Fₗ : Type u_7) [SeminormedAddCommGroup E] [SeminormedAddCommGroup Fₗ] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 Fₗ] (𝕜' : Type u_11) [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜' 𝕜] [NormedSpace 𝕜' E] [IsScalarTower 𝕜' 𝕜 E] [NormedSpace 𝕜' Fₗ] [IsScalarTower 𝕜' 𝕜 Fₗ] (𝕜'' : Type u_12) [Ring 𝕜''] [Module 𝕜'' Fₗ] [ContinuousConstSMul 𝕜'' Fₗ] [SMulCommClass 𝕜 𝕜'' Fₗ] [SMulCommClass 𝕜' 𝕜'' Fₗ] : (E →L[𝕜] Fₗ) →L[𝕜''] E →L[𝕜'] Fₗ

ContinuousLinearMap.restrictScalars as a ContinuousLinearMap.

Equations

• ContinuousLinearMap.restrictScalarsL 𝕜 E Fₗ 𝕜' 𝕜'' = LinearIsometry.toContinuousLinearMap (ContinuousLinearMap.restrictScalarsIsometry 𝕜 E Fₗ 𝕜' 𝕜'')

@[simp]

theorem ContinuousLinearMap.coe_restrictScalarsL {𝕜 : Type u_1} {E : Type u_4} {Fₗ : Type u_7} [SeminormedAddCommGroup E] [SeminormedAddCommGroup Fₗ] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 Fₗ] {𝕜' : Type u_11} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜' 𝕜] [NormedSpace 𝕜' E] [IsScalarTower 𝕜' 𝕜 E] [NormedSpace 𝕜' Fₗ] [IsScalarTower 𝕜' 𝕜 Fₗ] {𝕜'' : Type u_12} [Ring 𝕜''] [Module 𝕜'' Fₗ] [ContinuousConstSMul 𝕜'' Fₗ] [SMulCommClass 𝕜 𝕜'' Fₗ] [SMulCommClass 𝕜' 𝕜'' Fₗ] : ↑(ContinuousLinearMap.restrictScalarsL 𝕜 E Fₗ 𝕜' 𝕜'') = ContinuousLinearMap.restrictScalarsₗ 𝕜 E Fₗ 𝕜' 𝕜''

@[simp]

theorem ContinuousLinearMap.coe_restrict_scalarsL' {𝕜 : Type u_1} {E : Type u_4} {Fₗ : Type u_7} [SeminormedAddCommGroup E] [SeminormedAddCommGroup Fₗ] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 Fₗ] {𝕜' : Type u_11} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜' 𝕜] [NormedSpace 𝕜' E] [IsScalarTower 𝕜' 𝕜 E] [NormedSpace 𝕜' Fₗ] [IsScalarTower 𝕜' 𝕜 Fₗ] {𝕜'' : Type u_12} [Ring 𝕜''] [Module 𝕜'' Fₗ] [ContinuousConstSMul 𝕜'' Fₗ] [SMulCommClass 𝕜 𝕜'' Fₗ] [SMulCommClass 𝕜' 𝕜'' Fₗ] : ↑(ContinuousLinearMap.restrictScalarsL 𝕜 E Fₗ 𝕜' 𝕜'') = ContinuousLinearMap.restrictScalars 𝕜'

theorem Submodule.norm_subtypeL_le {𝕜 : Type u_1} {E : Type u_4} [SeminormedAddCommGroup E] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] (K : Submodule 𝕜 E) : ‖Submodule.subtypeL K‖ ≤ 1

theorem ContinuousLinearEquiv.lipschitz {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_6} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₁ : 𝕜₂ →+* 𝕜} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [RingHomIsometric σ₁₂] (e : E ≃SL[σ₁₂] F) : LipschitzWith ‖↑e‖₊ ↑e

theorem ContinuousLinearEquiv.isBigO_comp {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_6} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₁ : 𝕜₂ →+* 𝕜} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [RingHomIsometric σ₁₂] (e : E ≃SL[σ₁₂] F) {α : Type u_11} (f : α → E) (l : Filter α) : (fun x' => ↑e (f x')) =O[l] f

theorem ContinuousLinearEquiv.isBigO_sub {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_6} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₁ : 𝕜₂ →+* 𝕜} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [RingHomIsometric σ₁₂] (e : E ≃SL[σ₁₂] F) (l : Filter E) (x : E) : (fun x' => ↑e (x' - x)) =O[l] fun x' => x' - x

theorem ContinuousLinearEquiv.isBigO_comp_rev {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_6} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₁ : 𝕜₂ →+* 𝕜} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [RingHomIsometric σ₂₁] (e : E ≃SL[σ₁₂] F) {α : Type u_11} (f : α → E) (l : Filter α) : f =O[l] fun x' => ↑e (f x')

theorem ContinuousLinearEquiv.isBigO_sub_rev {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_6} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₁ : 𝕜₂ →+* 𝕜} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [RingHomIsometric σ₂₁] (e : E ≃SL[σ₁₂] F) (l : Filter E) (x : E) : (fun x' => x' - x) =O[l] fun x' => ↑e (x' - x)

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) : E' →SL[σ₁₃'] F' →SL[σ₂₃'] G

Compose a bilinear map E →SL[σ₁₃] F →SL[σ₂₃] G with two linear maps E' →SL[σ₁'] E and F' →SL[σ₂'] F.

Equations

• ContinuousLinearMap.bilinearComp f gE gF = ContinuousLinearMap.flip (ContinuousLinearMap.comp (ContinuousLinearMap.flip (ContinuousLinearMap.comp f gE)) gF)

@[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ₗ) : E × Fₗ →L[𝕜] E × 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.

@[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 => ↑(↑f p.fst) q.snd + ↑(↑f q.fst) p.snd

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ₗ) : ↑(↑f (x + x')) (y + y') = ↑(↑f x) y + ↑(↑(ContinuousLinearMap.deriv₂ f) (x, y)) (x', y') + ↑(↑f x') y'

theorem LinearMap.bound_of_shell {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_6} [NormedAddCommGroup E] [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] (f : E →ₛₗ[σ₁₂] F) {ε : ℝ} {C : ℝ} (ε_pos : 0 < ε) {c : 𝕜} (hc : 1 < ‖c‖) (hf : ∀ (x : E), ε / ‖c‖ ≤ ‖x‖ → ‖x‖ < ε → ‖↑f x‖ ≤ C * ‖x‖) (x : E) : ‖↑f x‖ ≤ C * ‖x‖

theorem LinearMap.bound_of_ball_bound {𝕜 : Type u_1} {E : Type u_4} {Fₗ : Type u_7} [NormedAddCommGroup E] [NormedAddCommGroup Fₗ] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 Fₗ] {r : ℝ} (r_pos : 0 < r) (c : ℝ) (f : E →ₗ[𝕜] Fₗ) (h : ∀ (z : E), z ∈ Metric.ball 0 r → ‖↑f z‖ ≤ c) : ∃ C, ∀ (z : E), ‖↑f z‖ ≤ C * ‖z‖

LinearMap.bound_of_ball_bound' is a version of this lemma over a field satisfying IsROrC that produces a concrete bound.

theorem LinearMap.antilipschitz_of_comap_nhds_le {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_6} [NormedAddCommGroup E] [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [h : RingHomIsometric σ₁₂] (f : E →ₛₗ[σ₁₂] F) (hf : Filter.comap (↑f) (nhds 0) ≤ nhds 0) : ∃ K, AntilipschitzWith K ↑f

theorem ContinuousLinearMap.op_norm_zero_iff {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_6} [NormedAddCommGroup E] [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} (f : E →SL[σ₁₂] F) [RingHomIsometric σ₁₂] : ‖f‖ = 0 ↔ f = 0

An operator is zero iff its norm vanishes.

@[simp]

theorem ContinuousLinearMap.norm_id {𝕜 : Type u_1} {E : Type u_4} [NormedAddCommGroup E] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [Nontrivial E] : ‖ContinuousLinearMap.id 𝕜 E‖ = 1

If a normed space is non-trivial, then the norm of the identity equals 1.

noncomputable instance ContinuousLinearMap.normOneClass {𝕜 : Type u_1} {E : Type u_4} [NormedAddCommGroup E] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [Nontrivial E] : NormOneClass (E →L[𝕜] E)

Equations

• @ContinuousLinearMap.normOneClass = @ContinuousLinearMap.normOneClass.proof_1

noncomputable instance ContinuousLinearMap.toNormedAddCommGroup {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_6} [NormedAddCommGroup E] [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] : NormedAddCommGroup (E →SL[σ₁₂] F)

Continuous linear maps themselves form a normed space with respect to the operator norm.

Equations

• ContinuousLinearMap.toNormedAddCommGroup = NormedAddCommGroup.ofSeparation (_ : ∀ (f : E →SL[σ₁₂] F), ‖f‖ = 0 → f = 0)

noncomputable instance ContinuousLinearMap.toNormedRing {𝕜 : Type u_1} {E : Type u_4} [NormedAddCommGroup E] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] : NormedRing (E →L[𝕜] E)

Continuous linear maps form a normed ring with respect to the operator norm.

Equations

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

theorem ContinuousLinearMap.homothety_norm {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_6} [NormedAddCommGroup E] [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] [Nontrivial E] (f : E →SL[σ₁₂] F) {a : ℝ} (hf : ∀ (x : E), ‖↑f x‖ = a * ‖x‖) : ‖f‖ = a

theorem ContinuousLinearMap.antilipschitz_of_embedding {𝕜 : Type u_1} {E : Type u_4} {Fₗ : Type u_7} [NormedAddCommGroup E] [NormedAddCommGroup Fₗ] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 Fₗ] (f : E →L[𝕜] Fₗ) (hf : Embedding ↑f) : ∃ K, AntilipschitzWith K ↑f

If a continuous linear map is a topology embedding, then it is expands the distances by a positive factor.

noncomputable def ContinuousLinearMap.ofMemClosureImageCoeBounded {𝕜 : Type u_1} {𝕜₂ : Type u_2} {F : Type u_6} [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} {E' : Type u_11} [SeminormedAddCommGroup E'] [NormedSpace 𝕜 E'] [RingHomIsometric σ₁₂] (f : E' → F) {s : Set (E' →SL[σ₁₂] F)} (hs : Bornology.IsBounded s) (hf : f ∈ closure (FunLike.coe '' s)) : E' →SL[σ₁₂] F

Construct a bundled continuous (semi)linear map from a map f : E → F and a proof of the fact that it belongs to the closure of the image of a bounded set s : Set (E →SL[σ₁₂] F) under coercion to function. Coercion to function of the result is definitionally equal to f.

Equations

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

@[simp]

theorem ContinuousLinearMap.ofMemClosureImageCoeBounded_apply {𝕜 : Type u_1} {𝕜₂ : Type u_2} {F : Type u_6} [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} {E' : Type u_11} [SeminormedAddCommGroup E'] [NormedSpace 𝕜 E'] [RingHomIsometric σ₁₂] (f : E' → F) {s : Set (E' →SL[σ₁₂] F)} (hs : Bornology.IsBounded s) (hf : f ∈ closure (FunLike.coe '' s)) : ↑(ContinuousLinearMap.ofMemClosureImageCoeBounded f hs hf) = f

noncomputable def ContinuousLinearMap.ofTendstoOfBoundedRange {𝕜 : Type u_1} {𝕜₂ : Type u_2} {F : Type u_6} [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} {E' : Type u_11} [SeminormedAddCommGroup E'] [NormedSpace 𝕜 E'] [RingHomIsometric σ₁₂] {α : Type u_12} {l : Filter α} [Filter.NeBot l] (f : E' → F) (g : α → E' →SL[σ₁₂] F) (hf : Filter.Tendsto (fun a x => ↑(g a) x) l (nhds f)) (hg : Bornology.IsBounded (Set.range g)) : E' →SL[σ₁₂] F

Let f : E → F be a map, let g : α → E →SL[σ₁₂] F be a family of continuous (semi)linear maps that takes values in a bounded set and converges to f pointwise along a nontrivial filter. Then f is a continuous (semi)linear map.

Equations

• ContinuousLinearMap.ofTendstoOfBoundedRange f g hf hg = ContinuousLinearMap.ofMemClosureImageCoeBounded f hg (_ : f ∈ closure (FunLike.coe '' Set.range g))

@[simp]

theorem ContinuousLinearMap.ofTendstoOfBoundedRange_apply {𝕜 : Type u_1} {𝕜₂ : Type u_2} {F : Type u_6} [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} {E' : Type u_11} [SeminormedAddCommGroup E'] [NormedSpace 𝕜 E'] [RingHomIsometric σ₁₂] {α : Type u_12} {l : Filter α} [Filter.NeBot l] (f : E' → F) (g : α → E' →SL[σ₁₂] F) (hf : Filter.Tendsto (fun a x => ↑(g a) x) l (nhds f)) (hg : Bornology.IsBounded (Set.range g)) : ↑(ContinuousLinearMap.ofTendstoOfBoundedRange f g hf hg) = f

theorem ContinuousLinearMap.tendsto_of_tendsto_pointwise_of_cauchySeq {𝕜 : Type u_1} {𝕜₂ : Type u_2} {F : Type u_6} [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} {E' : Type u_11} [SeminormedAddCommGroup E'] [NormedSpace 𝕜 E'] [RingHomIsometric σ₁₂] {f : ℕ → E' →SL[σ₁₂] F} {g : E' →SL[σ₁₂] F} (hg : Filter.Tendsto (fun n x => ↑(f n) x) Filter.atTop (nhds ↑g)) (hf : CauchySeq f) : Filter.Tendsto f Filter.atTop (nhds g)

If a Cauchy sequence of continuous linear map converges to a continuous linear map pointwise, then it converges to the same map in norm. This lemma is used to prove that the space of continuous linear maps is complete provided that the codomain is a complete space.

noncomputable instance ContinuousLinearMap.instCompleteSpaceContinuousLinearMapToSemiringToDivisionSemiringToSemifieldToFieldToNormedFieldToSemiringToDivisionSemiringToSemifieldToFieldToNormedFieldToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceToAddCommMonoidToAddCommGroupToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceToSeminormedAddCommGroupToAddCommMonoidToAddCommGroupToModuleToModuleUniformSpaceToAddCommGroupTo_uniformAddGroup {𝕜 : Type u_1} {𝕜₂ : Type u_2} {F : Type u_6} [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} {E' : Type u_11} [SeminormedAddCommGroup E'] [NormedSpace 𝕜 E'] [RingHomIsometric σ₁₂] [CompleteSpace F] : CompleteSpace (E' →SL[σ₁₂] F)

If the target space is complete, the space of continuous linear maps with its norm is also complete. This works also if the source space is seminormed.

Equations

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

theorem ContinuousLinearMap.isCompact_closure_image_coe_of_bounded {𝕜 : Type u_1} {𝕜₂ : Type u_2} {F : Type u_6} [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} {E' : Type u_11} [SeminormedAddCommGroup E'] [NormedSpace 𝕜 E'] [RingHomIsometric σ₁₂] [ProperSpace F] {s : Set (E' →SL[σ₁₂] F)} (hb : Bornology.IsBounded s) : IsCompact (closure (FunLike.coe '' s))

Let s be a bounded set in the space of continuous (semi)linear maps E →SL[σ] F taking values in a proper space. Then s interpreted as a set in the space of maps E → F with topology of pointwise convergence is precompact: its closure is a compact set.

theorem ContinuousLinearMap.isCompact_image_coe_of_bounded_of_closed_image {𝕜 : Type u_1} {𝕜₂ : Type u_2} {F : Type u_6} [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} {E' : Type u_11} [SeminormedAddCommGroup E'] [NormedSpace 𝕜 E'] [RingHomIsometric σ₁₂] [ProperSpace F] {s : Set (E' →SL[σ₁₂] F)} (hb : Bornology.IsBounded s) (hc : IsClosed (FunLike.coe '' s)) : IsCompact (FunLike.coe '' s)

Let s be a bounded set in the space of continuous (semi)linear maps E →SL[σ] F taking values in a proper space. If s interpreted as a set in the space of maps E → F with topology of pointwise convergence is closed, then it is compact.

TODO: reformulate this in terms of a type synonym with the right topology.

theorem ContinuousLinearMap.isClosed_image_coe_of_bounded_of_weak_closed {𝕜 : Type u_1} {𝕜₂ : Type u_2} {F : Type u_6} [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} {E' : Type u_11} [SeminormedAddCommGroup E'] [NormedSpace 𝕜 E'] [RingHomIsometric σ₁₂] {s : Set (E' →SL[σ₁₂] F)} (hb : Bornology.IsBounded s) (hc : ∀ (f : E' →SL[σ₁₂] F), ↑f ∈ closure (FunLike.coe '' s) → f ∈ s) : IsClosed (FunLike.coe '' s)

If a set s of semilinear functions is bounded and is closed in the weak-* topology, then its image under coercion to functions E → F is a closed set. We don't have a name for E →SL[σ] F with weak-* topology in mathlib, so we use an equivalent condition (see isClosed_induced_iff').

TODO: reformulate this in terms of a type synonym with the right topology.

theorem ContinuousLinearMap.isCompact_image_coe_of_bounded_of_weak_closed {𝕜 : Type u_1} {𝕜₂ : Type u_2} {F : Type u_6} [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} {E' : Type u_11} [SeminormedAddCommGroup E'] [NormedSpace 𝕜 E'] [RingHomIsometric σ₁₂] [ProperSpace F] {s : Set (E' →SL[σ₁₂] F)} (hb : Bornology.IsBounded s) (hc : ∀ (f : E' →SL[σ₁₂] F), ↑f ∈ closure (FunLike.coe '' s) → f ∈ s) : IsCompact (FunLike.coe '' s)

If a set s of semilinear functions is bounded and is closed in the weak-* topology, then its image under coercion to functions E → F is a compact set. We don't have a name for E →SL[σ] F with weak-* topology in mathlib, so we use an equivalent condition (see isClosed_induced_iff').

theorem ContinuousLinearMap.is_weak_closed_closedBall {𝕜 : Type u_1} {𝕜₂ : Type u_2} {F : Type u_6} [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} {E' : Type u_11} [SeminormedAddCommGroup E'] [NormedSpace 𝕜 E'] [RingHomIsometric σ₁₂] (f₀ : E' →SL[σ₁₂] F) (r : ℝ) ⦃f : E' →SL[σ₁₂] F⦄ (hf : ↑f ∈ closure (FunLike.coe '' Metric.closedBall f₀ r)) : f ∈ Metric.closedBall f₀ r

A closed ball is closed in the weak-* topology. We don't have a name for E →SL[σ] F with weak-* topology in mathlib, so we use an equivalent condition (see isClosed_induced_iff').

theorem ContinuousLinearMap.isClosed_image_coe_closedBall {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_6} [NormedAddCommGroup E] [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] (f₀ : E →SL[σ₁₂] F) (r : ℝ) : IsClosed (FunLike.coe '' Metric.closedBall f₀ r)

The set of functions f : E → F that represent continuous linear maps f : E →SL[σ₁₂] F at distance ≤ r from f₀ : E →SL[σ₁₂] F is closed in the topology of pointwise convergence. This is one of the key steps in the proof of the Banach-Alaoglu theorem.

theorem ContinuousLinearMap.isCompact_image_coe_closedBall {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_6} [NormedAddCommGroup E] [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] [ProperSpace F] (f₀ : E →SL[σ₁₂] F) (r : ℝ) : IsCompact (FunLike.coe '' Metric.closedBall f₀ r)

Banach-Alaoglu theorem. The set of functions f : E → F that represent continuous linear maps f : E →SL[σ₁₂] F at distance ≤ r from f₀ : E →SL[σ₁₂] F is compact in the topology of pointwise convergence. Other versions of this theorem can be found in Analysis.NormedSpace.WeakDual.

noncomputable def ContinuousLinearMap.extend {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_6} {Fₗ : Type u_7} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup Fₗ] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] [NormedSpace 𝕜 Fₗ] {σ₁₂ : 𝕜 →+* 𝕜₂} (f : E →SL[σ₁₂] F) [CompleteSpace F] (e : E →L[𝕜] Fₗ) (h_dense : DenseRange ↑e) (h_e : UniformInducing ↑e) : Fₗ →SL[σ₁₂] F

Extension of a continuous linear map f : E →SL[σ₁₂] F, with E a normed space and F a complete normed space, along a uniform and dense embedding e : E →L[𝕜] Fₗ.

Equations

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

@[simp]

theorem ContinuousLinearMap.extend_eq {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_6} {Fₗ : Type u_7} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup Fₗ] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] [NormedSpace 𝕜 Fₗ] {σ₁₂ : 𝕜 →+* 𝕜₂} (f : E →SL[σ₁₂] F) [CompleteSpace F] (e : E →L[𝕜] Fₗ) (h_dense : DenseRange ↑e) (h_e : UniformInducing ↑e) (x : E) : ↑(ContinuousLinearMap.extend f e h_dense h_e) (↑e x) = ↑f x

theorem ContinuousLinearMap.extend_unique {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_6} {Fₗ : Type u_7} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup Fₗ] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] [NormedSpace 𝕜 Fₗ] {σ₁₂ : 𝕜 →+* 𝕜₂} (f : E →SL[σ₁₂] F) [CompleteSpace F] (e : E →L[𝕜] Fₗ) (h_dense : DenseRange ↑e) (h_e : UniformInducing ↑e) (g : Fₗ →SL[σ₁₂] F) (H : ContinuousLinearMap.comp g e = f) : ContinuousLinearMap.extend f e h_dense h_e = g

@[simp]

theorem ContinuousLinearMap.extend_zero {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_6} {Fₗ : Type u_7} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup Fₗ] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] [NormedSpace 𝕜 Fₗ] {σ₁₂ : 𝕜 →+* 𝕜₂} [CompleteSpace F] (e : E →L[𝕜] Fₗ) (h_dense : DenseRange ↑e) (h_e : UniformInducing ↑e) : ContinuousLinearMap.extend 0 e h_dense h_e = 0

theorem ContinuousLinearMap.op_norm_extend_le {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_6} {Fₗ : Type u_7} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup Fₗ] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] [NormedSpace 𝕜 Fₗ] {σ₁₂ : 𝕜 →+* 𝕜₂} (f : E →SL[σ₁₂] F) [CompleteSpace F] (e : E →L[𝕜] Fₗ) (h_dense : DenseRange ↑e) {N : NNReal} (h_e : ∀ (x : E), ‖x‖ ≤ ↑N * ‖↑e x‖) [RingHomIsometric σ₁₂] : ‖ContinuousLinearMap.extend f e h_dense (_ : UniformInducing ↑e)‖ ≤ ↑N * ‖f‖

If a dense embedding e : E →L[𝕜] G expands the norm by a constant factor N⁻¹, then the norm of the extension of f along e is bounded by N * ‖f‖.

@[simp]

theorem LinearIsometry.norm_toContinuousLinearMap {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_6} [NormedAddCommGroup E] [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [Nontrivial E] [RingHomIsometric σ₁₂] (f : E →ₛₗᵢ[σ₁₂] F) : ‖LinearIsometry.toContinuousLinearMap f‖ = 1

theorem LinearIsometry.norm_toContinuousLinearMap_comp {𝕜 : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {E : Type u_4} {F : Type u_6} {G : Type u_8} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup G] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NontriviallyNormedField 𝕜₃] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] [NormedSpace 𝕜₃ G] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomIsometric σ₁₂] (f : F →ₛₗᵢ[σ₂₃] G) {g : E →SL[σ₁₂] F} : ‖ContinuousLinearMap.comp (LinearIsometry.toContinuousLinearMap f) g‖ = ‖g‖

Postcomposition of a continuous linear map with a linear isometry preserves the operator norm.

theorem ContinuousLinearMap.op_norm_comp_linearIsometryEquiv {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {F : Type u_6} {G : Type u_8} [NormedAddCommGroup F] [NormedAddCommGroup G] [NontriviallyNormedField 𝕜₂] [NontriviallyNormedField 𝕜₃] [NormedSpace 𝕜₂ F] [NormedSpace 𝕜₃ G] {σ₂₃ : 𝕜₂ →+* 𝕜₃} {𝕜₂' : Type u_11} [NontriviallyNormedField 𝕜₂'] {F' : Type u_12} [NormedAddCommGroup F'] [NormedSpace 𝕜₂' F'] {σ₂' : 𝕜₂' →+* 𝕜₂} {σ₂'' : 𝕜₂ →+* 𝕜₂'} {σ₂₃' : 𝕜₂' →+* 𝕜₃} [RingHomInvPair σ₂' σ₂''] [RingHomInvPair σ₂'' σ₂'] [RingHomCompTriple σ₂' σ₂₃ σ₂₃'] [RingHomCompTriple σ₂'' σ₂₃' σ₂₃] [RingHomIsometric σ₂₃] [RingHomIsometric σ₂'] [RingHomIsometric σ₂''] [RingHomIsometric σ₂₃'] (f : F →SL[σ₂₃] G) (g : F' ≃ₛₗᵢ[σ₂'] F) : ‖ContinuousLinearMap.comp f (LinearIsometry.toContinuousLinearMap (LinearIsometryEquiv.toLinearIsometry g))‖ = ‖f‖

Precomposition with a linear isometry preserves the operator norm.

@[simp]

theorem ContinuousLinearMap.norm_smulRight_apply {𝕜 : Type u_1} {E : Type u_4} {Fₗ : Type u_7} [NormedAddCommGroup E] [NormedAddCommGroup Fₗ] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 Fₗ] (c : E →L[𝕜] 𝕜) (f : Fₗ) : ‖ContinuousLinearMap.smulRight c f‖ = ‖c‖ * ‖f‖

The norm of the tensor product of a scalar linear map and of an element of a normed space is the product of the norms.

@[simp]

theorem ContinuousLinearMap.nnnorm_smulRight_apply {𝕜 : Type u_1} {E : Type u_4} {Fₗ : Type u_7} [NormedAddCommGroup E] [NormedAddCommGroup Fₗ] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 Fₗ] (c : E →L[𝕜] 𝕜) (f : Fₗ) : ‖ContinuousLinearMap.smulRight c f‖₊ = ‖c‖₊ * ‖f‖₊

The non-negative norm of the tensor product of a scalar linear map and of an element of a normed space is the product of the non-negative norms.

noncomputable def ContinuousLinearMap.smulRightL (𝕜 : Type u_1) (E : Type u_4) (Fₗ : Type u_7) [NormedAddCommGroup E] [NormedAddCommGroup Fₗ] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 Fₗ] : (E →L[𝕜] 𝕜) →L[𝕜] Fₗ →L[𝕜] E →L[𝕜] Fₗ

ContinuousLinearMap.smulRight as a continuous trilinear map: smulRightL (c : E →L[𝕜] 𝕜) (f : F) (x : E) = c x • f.

Equations

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

@[simp]

theorem ContinuousLinearMap.norm_smulRightL_apply {𝕜 : Type u_1} {E : Type u_4} {Fₗ : Type u_7} [NormedAddCommGroup E] [NormedAddCommGroup Fₗ] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 Fₗ] (c : E →L[𝕜] 𝕜) (f : Fₗ) : ‖↑(↑(ContinuousLinearMap.smulRightL 𝕜 E Fₗ) c) f‖ = ‖c‖ * ‖f‖

@[simp]

theorem ContinuousLinearMap.norm_smulRightL {𝕜 : Type u_1} {E : Type u_4} {Fₗ : Type u_7} [NormedAddCommGroup E] [NormedAddCommGroup Fₗ] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 Fₗ] (c : E →L[𝕜] 𝕜) [Nontrivial Fₗ] : ‖↑(ContinuousLinearMap.smulRightL 𝕜 E Fₗ) c‖ = ‖c‖

@[simp]

theorem ContinuousLinearMap.op_norm_mul (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (𝕜' : Type u_13) [NonUnitalNormedRing 𝕜'] [NormedSpace 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' 𝕜'] [SMulCommClass 𝕜 𝕜' 𝕜'] [RegularNormedAlgebra 𝕜 𝕜'] [Nontrivial 𝕜'] : ‖ContinuousLinearMap.mul 𝕜 𝕜'‖ = 1

@[simp]

theorem ContinuousLinearMap.op_nnnorm_mul (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (𝕜' : Type u_13) [NonUnitalNormedRing 𝕜'] [NormedSpace 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' 𝕜'] [SMulCommClass 𝕜 𝕜' 𝕜'] [RegularNormedAlgebra 𝕜 𝕜'] [Nontrivial 𝕜'] : ‖ContinuousLinearMap.mul 𝕜 𝕜'‖₊ = 1

@[simp]

theorem ContinuousLinearMap.op_norm_lsmul (𝕜 : Type u_1) {E : Type u_4} [NormedAddCommGroup E] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] (𝕜' : Type u_13) [NormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] [NormedSpace 𝕜' E] [IsScalarTower 𝕜 𝕜' E] [Nontrivial E] : ‖ContinuousLinearMap.lsmul 𝕜 𝕜'‖ = 1

The norm of lsmul equals 1 in any nontrivial normed group.

This is ContinuousLinearMap.op_norm_lsmul_le as an equality.

theorem Submodule.norm_subtypeL {𝕜 : Type u_1} {E : Type u_4} [NormedAddCommGroup E] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] (K : Submodule 𝕜 E) [Nontrivial { x // x ∈ K }] : ‖Submodule.subtypeL K‖ = 1

theorem ContinuousLinearEquiv.antilipschitz {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_6} [NormedAddCommGroup E] [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₁ : 𝕜₂ →+* 𝕜} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [RingHomIsometric σ₂₁] (e : E ≃SL[σ₁₂] F) : AntilipschitzWith ‖↑(ContinuousLinearEquiv.symm e)‖₊ ↑e

theorem ContinuousLinearEquiv.one_le_norm_mul_norm_symm {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_6} [NormedAddCommGroup E] [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₁ : 𝕜₂ →+* 𝕜} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [RingHomIsometric σ₂₁] [RingHomIsometric σ₁₂] [Nontrivial E] (e : E ≃SL[σ₁₂] F) : 1 ≤ ‖↑e‖ * ‖↑(ContinuousLinearEquiv.symm e)‖

theorem ContinuousLinearEquiv.norm_pos {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_6} [NormedAddCommGroup E] [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₁ : 𝕜₂ →+* 𝕜} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [RingHomIsometric σ₂₁] [RingHomIsometric σ₁₂] [Nontrivial E] (e : E ≃SL[σ₁₂] F) : 0 < ‖↑e‖

theorem ContinuousLinearEquiv.norm_symm_pos {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_6} [NormedAddCommGroup E] [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₁ : 𝕜₂ →+* 𝕜} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [RingHomIsometric σ₂₁] [RingHomIsometric σ₁₂] [Nontrivial E] (e : E ≃SL[σ₁₂] F) : 0 < ‖↑(ContinuousLinearEquiv.symm e)‖

theorem ContinuousLinearEquiv.nnnorm_symm_pos {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_6} [NormedAddCommGroup E] [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₁ : 𝕜₂ →+* 𝕜} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [RingHomIsometric σ₂₁] [RingHomIsometric σ₁₂] [Nontrivial E] (e : E ≃SL[σ₁₂] F) : 0 < ‖↑(ContinuousLinearEquiv.symm e)‖₊

theorem ContinuousLinearEquiv.subsingleton_or_norm_symm_pos {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_6} [NormedAddCommGroup E] [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₁ : 𝕜₂ →+* 𝕜} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [RingHomIsometric σ₂₁] [RingHomIsometric σ₁₂] (e : E ≃SL[σ₁₂] F) : Subsingleton E ∨ 0 < ‖↑(ContinuousLinearEquiv.symm e)‖

theorem ContinuousLinearEquiv.subsingleton_or_nnnorm_symm_pos {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_6} [NormedAddCommGroup E] [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₁ : 𝕜₂ →+* 𝕜} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [RingHomIsometric σ₂₁] [RingHomIsometric σ₁₂] (e : E ≃SL[σ₁₂] F) : Subsingleton E ∨ 0 < ‖↑(ContinuousLinearEquiv.symm e)‖₊

@[simp]

theorem ContinuousLinearEquiv.coord_norm (𝕜 : Type u_1) {E : Type u_4} [NormedAddCommGroup E] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] (x : E) (h : x ≠ 0) : ‖ContinuousLinearEquiv.coord 𝕜 x h‖ = ‖x‖⁻¹

noncomputable def IsCoercive {E : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] (B : E →L[ℝ] E →L[ℝ] ℝ) : Prop

A bounded bilinear form B in a real normed space is coercive if there is some positive constant C such that C * ‖u‖ * ‖u‖ ≤ B u u.

Equations

• IsCoercive B = ∃ C, 0 < C ∧ ∀ (u : E), C * ‖u‖ * ‖u‖ ≤ ↑(↑B u) u

theorem NormedSpace.equicontinuous_TFAE {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_6} {ι : Type u_11} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] (f : ι → E →SL[σ₁₂] F) : List.TFAE [EquicontinuousAt (FunLike.coe ∘ f) 0, Equicontinuous (FunLike.coe ∘ f), UniformEquicontinuous (FunLike.coe ∘ f), ∃ C, ∀ (i : ι) (x : E), ‖↑(f i) x‖ ≤ C * ‖x‖, ∃ C, C ≥ 0 ∧ ∀ (i : ι) (x : E), ‖↑(f i) x‖ ≤ C * ‖x‖, ∃ C, ∀ (i : ι), ‖f i‖ ≤ C, ∃ C, C ≥ 0 ∧ ∀ (i : ι), ‖f i‖ ≤ C, BddAbove (Set.range fun x => ‖f x‖), ⨆ (i : ι), ↑‖f i‖₊ < ⊤]

Equivalent characterizations for equicontinuity of a family of continuous linear maps between normed spaces. See also WithSeminorms.equicontinuous_TFAE for similar characterizations between spaces satisfying WithSeminorms.