Documentation

Mathlib.Analysis.NormedSpace.OperatorNorm.NormedSpace

Operator norm for maps on normed spaces #

This file contains statements about operator norm for which it really matters that the underlying space has a norm (rather than just a seminorm).

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) :
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 โˆˆ 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 RCLike 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 : NNReal), AntilipschitzWith K โ‡‘f
theorem ContinuousLinearMap.opNorm_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 ฯƒโ‚โ‚‚] :

An operator is zero iff its norm vanishes.

@[deprecated ContinuousLinearMap.opNorm_zero_iff]
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 ฯƒโ‚โ‚‚] :

Alias of ContinuousLinearMap.opNorm_zero_iff.


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] :

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

@[simp]
noncomputable instance ContinuousLinearMap.normOneClass {๐•œ : Type u_1} {E : Type u_4} [NormedAddCommGroup E] [NontriviallyNormedField ๐•œ] [NormedSpace ๐•œ E] [Nontrivial E] :
NormOneClass (E โ†’L[๐•œ] E)
Equations
  • โ‹ฏ = โ‹ฏ
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
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
  • ContinuousLinearMap.toNormedRing = let __src := ContinuousLinearMap.toNormedAddCommGroup; let __src_1 := ContinuousLinearMap.toSemiNormedRing; NormedRing.mk โ‹ฏ โ‹ฏ
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โ€–) :
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 : NNReal), AntilipschitzWith K โ‡‘f

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

@[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) :
โ€–f.toContinuousLinearMapโ€– = 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} :
โ€–f.toContinuousLinearMap.comp gโ€– = โ€–gโ€–

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

theorem ContinuousLinearMap.opNorm_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) :
โ€–f.comp g.toLinearIsometry.toContinuousLinearMapโ€– = โ€–fโ€–

Precomposition with a linear isometry preserves the operator norm.

@[deprecated ContinuousLinearMap.opNorm_comp_linearIsometryEquiv]
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) :
โ€–f.comp g.toLinearIsometry.toContinuousLinearMapโ€– = โ€–fโ€–

Alias of ContinuousLinearMap.opNorm_comp_linearIsometryEquiv.


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โ‚—) :

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โ‚—) :

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
  • ContinuousLinearMap.smulRightL ๐•œ E Fโ‚— = { toFun := ContinuousLinearMap.smulRightโ‚—, map_add' := โ‹ฏ, map_smul' := โ‹ฏ }.mkContinuousโ‚‚ 1 โ‹ฏ
Instances For
    @[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โ‚—) :
    @[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โ‚—] :
    theorem ContinuousLinearMap.norm_smulRightL_le {๐•œ : Type u_1} {E : Type u_4} {Fโ‚— : Type u_7} [NormedAddCommGroup E] [NormedAddCommGroup Fโ‚—] [NontriviallyNormedField ๐•œ] [NormedSpace ๐•œ E] [NormedSpace ๐•œ Fโ‚—] :
    theorem Submodule.norm_subtypeL {๐•œ : Type u_1} {E : Type u_4} [NormedAddCommGroup E] [NontriviallyNormedField ๐•œ] [NormedSpace ๐•œ E] (K : Submodule ๐•œ E) [Nontrivial โ†ฅK] :
    โ€–K.subtypeLโ€– = 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) :
    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โ€– * โ€–โ†‘e.symmโ€–
    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 < โ€–โ†‘e.symmโ€–
    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 < โ€–โ†‘e.symmโ€–โ‚Š
    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) :
    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) :
    @[simp]

    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
    Instances For
      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) :
      [EquicontinuousAt (DFunLike.coe โˆ˜ f) 0, Equicontinuous (DFunLike.coe โˆ˜ f), UniformEquicontinuous (DFunLike.coe โˆ˜ f), โˆƒ (C : โ„), โˆ€ (i : ฮน) (x : E), โ€–(f i) xโ€– โ‰ค C * โ€–xโ€–, โˆƒ C โ‰ฅ 0, โˆ€ (i : ฮน) (x : E), โ€–(f i) xโ€– โ‰ค C * โ€–xโ€–, โˆƒ (C : โ„), โˆ€ (i : ฮน), โ€–f iโ€– โ‰ค C, โˆƒ C โ‰ฅ 0, โˆ€ (i : ฮน), โ€–f iโ€– โ‰ค C, BddAbove (Set.range fun (x : ฮน) => โ€–f xโ€–), โจ† (i : ฮน), โ†‘โ€–f iโ€–โ‚Š < โŠค].TFAE

      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.