Mathlib.Analysis.NormedSpace.OperatorNorm.NormedSpace

LinearMap.bound_of_shell theorem

 [RingHomIsometric σ₁₂] (f : E →ₛₗ[σ₁₂] F) {ε C : ℝ} (ε_pos : 0 < ε) {c : 𝕜} (hc : 1 < ‖c‖)
  (hf : ∀ x, ε / ‖c‖ ≤ ‖x‖ → ‖x‖ < ε → ‖f x‖ ≤ C * ‖x‖) (x : E) : ‖f x‖ ≤ C * ‖x‖

Full source

theorem bound_of_shell [RingHomIsometric σ₁₂] (f : E →ₛₗ[σ₁₂] F) {ε C : ℝ} (ε_pos : 0 < ε) {c : 𝕜}
    (hc : 1 < ‖c‖) (hf : ∀ x, ε / ‖c‖ ≤ ‖x‖ → ‖x‖ < ε → ‖f x‖ ≤ C * ‖x‖) (x : E) :
    ‖f x‖ ≤ C * ‖x‖ := by
  by_cases hx : x = 0; · simp [hx]
  exact SemilinearMapClass.bound_of_shell_semi_normed f ε_pos hc hf (norm_ne_zero_iff.2 hx)

Bound on Linear Map via Shell Condition

Informal description

Let $E$ and $F$ be normed spaces over a normed field $\mathbb{K}$, and let $\sigma_{12} : \mathbb{K} \to \mathbb{K}$ be a ring homomorphism that is isometric. Given a $\sigma_{12}$-linear map $f : E \to F$, suppose there exist positive real numbers $\varepsilon$ and $C$ such that $0 < \varepsilon$, and an element $c \in \mathbb{K}$ with $\|c\| > 1$. If for all $x \in E$ satisfying $\varepsilon / \|c\| \leq \|x\| < \varepsilon$, the inequality $\|f(x)\| \leq C \|x\|$ holds, then for all $x \in E$, we have $\|f(x)\| \leq C \|x\|$.

LinearMap.bound_of_ball_bound theorem

 {r : ℝ} (r_pos : 0 < r) (c : ℝ) (f : E →ₗ[𝕜] Fₗ) (h : ∀ z ∈ Metric.ball (0 : E) r, ‖f z‖ ≤ c) :
  ∃ C, ∀ z : E, ‖f z‖ ≤ C * ‖z‖

Full source

/-- `LinearMap.bound_of_ball_bound'` is a version of this lemma over a field satisfying `RCLike`
that produces a concrete bound.
-/
theorem bound_of_ball_bound {r : ℝ} (r_pos : 0 < r) (c : ℝ) (f : E →ₗ[𝕜] Fₗ)
    (h : ∀ z ∈ Metric.ball (0 : E) r, ‖f z‖ ≤ c) : ∃ C, ∀ z : E, ‖f z‖ ≤ C * ‖z‖ := by
  obtain ⟨k, hk⟩ := @NontriviallyNormedField.non_trivial 𝕜 _
  use c * (‖k‖ / r)
  intro z
  refine bound_of_shell _ r_pos hk (fun x hko hxo => ?_) _
  calc
    ‖f x‖ ≤ c := h _ (mem_ball_zero_iff.mpr hxo)
    _ ≤ c * (‖x‖ * ‖k‖ / r) := le_mul_of_one_le_right ?_ ?_
    _ = _ := by ring
  · exact le_trans (norm_nonneg _) (h 0 (by simp [r_pos]))
  · rw [div_le_iff₀ (zero_lt_one.trans hk)] at hko
    exact (one_le_div r_pos).mpr hko

Existence of Linear Bound from Ball Condition in Normed Spaces

Informal description

Let $E$ and $F$ be normed spaces over a normed field $\mathbb{K}$. Given a linear map $f : E \to F$, a positive real number $r > 0$, and a constant $c \in \mathbb{R}$, if for all $z$ in the open ball of radius $r$ centered at $0$ in $E$ we have $\|f(z)\| \leq c$, then there exists a constant $C$ such that for all $z \in E$, $\|f(z)\| \leq C \|z\|$.

LinearMap.antilipschitz_of_comap_nhds_le theorem

 [h : RingHomIsometric σ₁₂] (f : E →ₛₗ[σ₁₂] F) (hf : (𝓝 0).comap f ≤ 𝓝 0) : ∃ K, AntilipschitzWith K f

Full source

theorem antilipschitz_of_comap_nhds_le [h : RingHomIsometric σ₁₂] (f : E →ₛₗ[σ₁₂] F)
    (hf : (𝓝 0).comap f ≤ 𝓝 0) : ∃ K, AntilipschitzWith K f := by
  rcases ((nhds_basis_ball.comap _).le_basis_iff nhds_basis_ball).1 hf 1 one_pos with ⟨ε, ε0, hε⟩
  simp only [Set.subset_def, Set.mem_preimage, mem_ball_zero_iff] at hε
  lift ε to ℝ≥0 using ε0.le
  rcases NormedField.exists_one_lt_norm 𝕜 with ⟨c, hc⟩
  refine ⟨ε⁻¹ * ‖c‖₊, AddMonoidHomClass.antilipschitz_of_bound f fun x => ?_⟩
  by_cases hx : f x = 0
  · rw [← hx] at hf
    obtain rfl : x = 0 := Specializes.eq (specializes_iff_pure.2 <|
      ((Filter.tendsto_pure_pure _ _).mono_right (pure_le_nhds _)).le_comap.trans hf)
    exact norm_zero.trans_le (mul_nonneg (NNReal.coe_nonneg _) (norm_nonneg _))
  have hc₀ : c ≠ 0 := norm_pos_iff.1 (one_pos.trans hc)
  rw [← h.1] at hc
  rcases rescale_to_shell_zpow hc ε0 hx with ⟨n, -, hlt, -, hle⟩
  simp only [← map_zpow₀, h.1, ← map_smulₛₗ] at hlt hle
  calc
    ‖x‖ = ‖c ^ n‖‖c ^ n‖⁻¹ * ‖c ^ n • x‖ := by
      rwa [← norm_inv, ← norm_smul, inv_smul_smul₀ (zpow_ne_zero _ _)]
    _ ≤ ‖c ^ n‖‖c ^ n‖⁻¹ * 1 := (mul_le_mul_of_nonneg_left (hε _ hlt).le (inv_nonneg.2 (norm_nonneg _)))
    _ ≤ ε⁻¹ * ‖c‖ * ‖f x‖ := by rwa [mul_one]

Existence of Antilipschitz Constant for Linear Maps with Filter Condition

Informal description

Let $E$ and $F$ be normed spaces over a normed field $\mathbb{K}$, and let $\sigma_{12} : \mathbb{K} \to \mathbb{K}$ be an isometric ring homomorphism. Given a $\sigma_{12}$-linear map $f : E \to F$, if the preimage of the neighborhood filter of $0$ under $f$ is contained in the neighborhood filter of $0$ in $E$, then there exists a constant $K$ such that $f$ is $K$-antilipschitz.

ContinuousLinearMap.opNorm_zero_iff theorem

[RingHomIsometric σ₁₂] : ‖f‖ = 0 ↔ f = 0

Full source

/-- An operator is zero iff its norm vanishes. -/
theorem opNorm_zero_iff [RingHomIsometric σ₁₂] : ‖f‖‖f‖ = 0 ↔ f = 0 :=
  Iff.intro
    (fun hn => ContinuousLinearMap.ext fun x => norm_le_zero_iff.1
      (calc
        _ ≤ ‖f‖ * ‖x‖ := le_opNorm _ _
        _ = _ := by rw [hn, zero_mul]))
    (by
      rintro rfl
      exact opNorm_zero)

Operator Norm Vanishes if and only if Map is Zero

Informal description

For a continuous linear map $f$ between normed spaces, the operator norm $\|f\|$ is zero if and only if $f$ is the zero map.

ContinuousLinearMap.norm_id theorem

[Nontrivial E] : ‖id 𝕜 E‖ = 1

Full source

/-- If a normed space is non-trivial, then the norm of the identity equals `1`. -/
@[simp]
theorem norm_id [Nontrivial E] : ‖id 𝕜 E‖ = 1 := by
  refine norm_id_of_nontrivial_seminorm ?_
  obtain ⟨x, hx⟩ := exists_ne (0 : E)
  exact ⟨x, ne_of_gt (norm_pos_iff.2 hx)⟩

Operator Norm of Identity Map in Nontrivial Normed Space is 1

Informal description

In a nontrivial normed space $E$ over the field $\mathbb{K}$, the operator norm of the identity map $\text{id}_{\mathbb{K} E}$ is equal to $1$.

ContinuousLinearMap.nnnorm_id theorem

[Nontrivial E] : ‖id 𝕜 E‖₊ = 1

Full source

@[simp]
lemma nnnorm_id [Nontrivial E] : ‖id 𝕜 E‖₊ = 1 := NNReal.eq norm_id

Operator Seminorm of Identity Map in Nontrivial Normed Space is 1

Informal description

In a nontrivial normed space $E$ over the field $\mathbb{K}$, the operator seminorm (with the $\mathbb{N}$-valued norm) of the identity map $\text{id}_{\mathbb{K} E}$ is equal to $1$.

ContinuousLinearMap.homothety_norm theorem

 [RingHomIsometric σ₁₂] [Nontrivial E] (f : E →SL[σ₁₂] F) {a : ℝ} (hf : ∀ x, ‖f x‖ = a * ‖x‖) : ‖f‖ = a

Full source

theorem homothety_norm [RingHomIsometric σ₁₂] [Nontrivial E] (f : E →SL[σ₁₂] F) {a : ℝ}
    (hf : ∀ x, ‖f x‖ = a * ‖x‖) : ‖f‖ = a := by
  obtain ⟨x, hx⟩ : ∃ x : E, x ≠ 0 := exists_ne 0
  rw [← norm_pos_iff] at hx
  have ha : 0 ≤ a := by simpa only [hf, hx, mul_nonneg_iff_of_pos_right] using norm_nonneg (f x)
  apply le_antisymm (f.opNorm_le_bound ha fun y => le_of_eq (hf y))
  simpa only [hf, hx, mul_le_mul_right] using f.le_opNorm x

Operator Norm of Homothety Equals Scaling Factor

Informal description

Let $E$ and $F$ be normed spaces over fields $\mathbb{K}_1$ and $\mathbb{K}_2$ respectively, with a ring homomorphism $\sigma_{12} \colon \mathbb{K}_1 \to \mathbb{K}_2$ that is isometric. Suppose $E$ is nontrivial and let $f \colon E \to F$ be a continuous linear map. If there exists a real number $a$ such that $\|f(x)\| = a \|x\|$ for all $x \in E$, then the operator norm of $f$ is equal to $a$.

ContinuousLinearMap.antilipschitz_of_isEmbedding theorem

(f : E →L[𝕜] Fₗ) (hf : IsEmbedding f) : ∃ K, AntilipschitzWith K f

Full source

/-- If a continuous linear map is a topology embedding, then it is expands the distances
by a positive factor. -/
theorem antilipschitz_of_isEmbedding (f : E →L[𝕜] Fₗ) (hf : IsEmbedding f) :
    ∃ K, AntilipschitzWith K f :=
  f.toLinearMap.antilipschitz_of_comap_nhds_le <| map_zero f ▸ (hf.nhds_eq_comap 0).ge

Existence of Antilipschitz Constant for Topologically Embedding Continuous Linear Maps

Informal description

Let $E$ and $F$ be normed spaces over the field $\mathbb{K}$, and let $f \colon E \to F$ be a continuous linear map. If $f$ is a topological embedding, then there exists a constant $K$ such that $f$ is $K$-antilipschitz, meaning that for all $x, y \in E$, we have $\|x - y\| \leq K \|f(x) - f(y)\|$.

LinearIsometry.norm_toContinuousLinearMap theorem

[Nontrivial E] [RingHomIsometric σ₁₂] (f : E →ₛₗᵢ[σ₁₂] F) : ‖f.toContinuousLinearMap‖ = 1

Full source

@[simp]
theorem norm_toContinuousLinearMap [Nontrivial E] [RingHomIsometric σ₁₂] (f : E →ₛₗᵢ[σ₁₂] F) :
    ‖f.toContinuousLinearMap‖ = 1 :=
  f.toContinuousLinearMap.homothety_norm <| by simp

Operator Norm of Linear Isometry is One

Informal description

Let $E$ and $F$ be normed spaces over fields $\mathbb{K}_1$ and $\mathbb{K}_2$ respectively, with a ring homomorphism $\sigma_{12} \colon \mathbb{K}_1 \to \mathbb{K}_2$ that is isometric. Suppose $E$ is nontrivial and let $f \colon E \to F$ be a linear isometry. Then the operator norm of the continuous linear map associated to $f$ is equal to $1$.

LinearIsometry.norm_toContinuousLinearMap_comp theorem

 [RingHomIsometric σ₁₂] (f : F →ₛₗᵢ[σ₂₃] G) {g : E →SL[σ₁₂] F} : ‖f.toContinuousLinearMap.comp g‖ = ‖g‖

Full source

/-- Postcomposition of a continuous linear map with a linear isometry preserves
the operator norm. -/
theorem norm_toContinuousLinearMap_comp [RingHomIsometric σ₁₂] (f : F →ₛₗᵢ[σ₂₃] G)
    {g : E →SL[σ₁₂] F} : ‖f.toContinuousLinearMap.comp g‖ = ‖g‖ :=
  opNorm_ext (f.toContinuousLinearMap.comp g) g fun x => by
    simp only [norm_map, coe_toContinuousLinearMap, coe_comp', Function.comp_apply]

Operator Norm Preservation under Postcomposition with Linear Isometry

Informal description

Let $E$, $F$, and $G$ be normed spaces over the respective fields, and let $\sigma_{12} : \mathbb{K}_1 \to \mathbb{K}_2$ and $\sigma_{23} : \mathbb{K}_2 \to \mathbb{K}_3$ be ring homomorphisms. Suppose $\sigma_{12}$ is isometric. For any linear isometry $f : F \to_{\sigma_{23}} G$ and any continuous linear map $g : E \to_{\sigma_{12}} F$, the operator norm of the composition $f \circ g$ equals the operator norm of $g$, i.e., $\|f \circ g\| = \|g\|$.

ContinuousLinearMap.opNorm_comp_linearIsometryEquiv theorem

 (f : F →SL[σ₂₃] G) (g : F' ≃ₛₗᵢ[σ₂'] F) : ‖f.comp g.toLinearIsometry.toContinuousLinearMap‖ = ‖f‖

Full source

/-- Precomposition with a linear isometry preserves the operator norm. -/
theorem opNorm_comp_linearIsometryEquiv (f : F →SL[σ₂₃] G) (g : F' ≃ₛₗᵢ[σ₂'] F) :
    ‖f.comp g.toLinearIsometry.toContinuousLinearMap‖ = ‖f‖ := by
  cases subsingleton_or_nontrivial F'
  · haveI := g.symm.toLinearEquiv.toEquiv.subsingleton
    simp
  refine le_antisymm ?_ ?_
  · convert f.opNorm_comp_le g.toLinearIsometry.toContinuousLinearMap
    simp [g.toLinearIsometry.norm_toContinuousLinearMap]
  · convert (f.comp g.toLinearIsometry.toContinuousLinearMap).opNorm_comp_le
        g.symm.toLinearIsometry.toContinuousLinearMap
    · ext
      simp
    haveI := g.symm.surjective.nontrivial
    simp [g.symm.toLinearIsometry.norm_toContinuousLinearMap]

Operator Norm Preservation under Precomposition with Linear Isometric Equivalence

Informal description

Let $F$, $G$, and $F'$ be normed spaces over their respective fields, with ring homomorphisms $\sigma_{23} \colon \mathbb{K}_2 \to \mathbb{K}_3$ and $\sigma_2' \colon \mathbb{K}_2' \to \mathbb{K}_2$. For any continuous linear map $f \colon F \to_{\sigma_{23}} G$ and any linear isometric equivalence $g \colon F' \to_{\sigma_2'} F$, the operator norm of the composition $f \circ g$ equals the operator norm of $f$, i.e., $\|f \circ g\| = \|f\|$.

ContinuousLinearMap.norm_smulRightL theorem

(c : E →L[𝕜] 𝕜) [Nontrivial Fₗ] : ‖smulRightL 𝕜 E Fₗ c‖ = ‖c‖

Full source

@[simp]
theorem norm_smulRightL (c : E →L[𝕜] 𝕜) [Nontrivial Fₗ] : ‖smulRightL 𝕜 E Fₗ c‖ = ‖c‖ :=
  ContinuousLinearMap.homothety_norm _ c.norm_smulRight_apply

Operator Norm of Scalar Multiplication Map Equals Norm of Functional

Informal description

Let $E$ and $F_\lambda$ be normed spaces over a field $\mathbb{K}$, with $F_\lambda$ being nontrivial. For any continuous linear functional $c \colon E \to \mathbb{K}$, the operator norm of the scalar multiplication map $\text{smulRightL}_{\mathbb{K}} E F_\lambda c$ is equal to the norm of $c$, i.e., $\|\text{smulRightL}_{\mathbb{K}} E F_\lambda c\| = \|c\|$.

ContinuousLinearMap.norm_smulRightL_le theorem

: ‖smulRightL 𝕜 E Fₗ‖ ≤ 1

Full source

lemma norm_smulRightL_le : ‖smulRightL 𝕜 E Fₗ‖ ≤ 1 :=
  LinearMap.mkContinuous₂_norm_le _ zero_le_one _

Operator Norm Bound for Scalar Multiplication Map: $\|\text{smulRightL}_{\mathbb{K}} E F_\lambda\| \leq 1$

Informal description

For any normed spaces $E$ and $F_\lambda$ over a field $\mathbb{K}$, the operator norm of the scalar multiplication map $\text{smulRightL}_{\mathbb{K}} E F_\lambda$ is bounded above by $1$, i.e., $\|\text{smulRightL}_{\mathbb{K}} E F_\lambda\| \leq 1$.

Submodule.norm_subtypeL theorem

(K : Submodule 𝕜 E) [Nontrivial K] : ‖K.subtypeL‖ = 1

Full source

theorem norm_subtypeL (K : Submodule 𝕜 E) [Nontrivial K] : ‖K.subtypeL‖ = 1 :=
  K.subtypeₗᵢ.norm_toContinuousLinearMap

Operator Norm of Submodule Inclusion is One

Informal description

Let $E$ be a normed space over the field $\mathbb{K}$ and let $K$ be a nontrivial submodule of $E$. The operator norm of the continuous linear inclusion map from $K$ to $E$ is equal to $1$, i.e., $\|K.\text{subtypeL}\| = 1$.

ContinuousLinearEquiv.antilipschitz theorem

(e : E ≃SL[σ₁₂] F) : AntilipschitzWith ‖(e.symm : F →SL[σ₂₁] E)‖₊ e

Full source

protected theorem antilipschitz (e : E ≃SL[σ₁₂] F) :
    AntilipschitzWith ‖(e.symm : F →SL[σ₂₁] E)‖₊ e :=
  e.symm.lipschitz.to_rightInverse e.left_inv

Antilipschitz Property of Continuous Linear Equivalences with Operator Norm Constant

Informal description

Let $E$ and $F$ be normed spaces over fields $\mathbb{K}_1$ and $\mathbb{K}_2$ respectively, and let $\sigma_{12}: \mathbb{K}_1 \to \mathbb{K}_2$ be a ring homomorphism. For any continuous linear equivalence $e: E \simeq_{\text{SL}[\sigma_{12}]} F$, the map $e$ is antilipschitz with constant $\|e^{-1}\|$, where $\|e^{-1}\|$ denotes the operator norm of the inverse map $e^{-1}: F \to E$.

ContinuousLinearEquiv.one_le_norm_mul_norm_symm theorem

 [RingHomIsometric σ₁₂] [Nontrivial E] (e : E ≃SL[σ₁₂] F) : 1 ≤ ‖(e : E →SL[σ₁₂] F)‖ * ‖(e.symm : F →SL[σ₂₁] E)‖

Full source

theorem one_le_norm_mul_norm_symm [RingHomIsometric σ₁₂] [Nontrivial E] (e : E ≃SL[σ₁₂] F) :
    1 ≤ ‖(e : E →SL[σ₁₂] F)‖ * ‖(e.symm : F →SL[σ₂₁] E)‖ := by
  rw [mul_comm]
  convert (e.symm : F →SL[σ₂₁] E).opNorm_comp_le (e : E →SL[σ₁₂] F)
  rw [e.coe_symm_comp_coe, ContinuousLinearMap.norm_id]

Lower Bound on Product of Operator Norms for Continuous Linear Equivalences

Informal description

Let $E$ and $F$ be normed spaces over fields $\mathbb{K}_1$ and $\mathbb{K}_2$ respectively, with $E$ being nontrivial. Let $\sigma_{12}: \mathbb{K}_1 \to \mathbb{K}_2$ be a ring homomorphism that is isometric. For any continuous linear equivalence $e: E \simeq_{\text{SL}[\sigma_{12}]} F$, the product of the operator norms satisfies $1 \leq \|e\| \cdot \|e^{-1}\|$, where $\|e\|$ is the operator norm of $e$ and $\|e^{-1}\|$ is the operator norm of its inverse.

ContinuousLinearEquiv.norm_pos theorem

[RingHomIsometric σ₁₂] [Nontrivial E] (e : E ≃SL[σ₁₂] F) : 0 < ‖(e : E →SL[σ₁₂] F)‖

Full source

theorem norm_pos [RingHomIsometric σ₁₂] [Nontrivial E] (e : E ≃SL[σ₁₂] F) :
    0 < ‖(e : E →SL[σ₁₂] F)‖ :=
  pos_of_mul_pos_left (lt_of_lt_of_le zero_lt_one e.one_le_norm_mul_norm_symm) (norm_nonneg _)

Positivity of Operator Norm for Continuous Linear Equivalences

Informal description

Let $E$ and $F$ be normed spaces over fields $\mathbb{K}_1$ and $\mathbb{K}_2$ respectively, with $E$ being nontrivial. Let $\sigma_{12}: \mathbb{K}_1 \to \mathbb{K}_2$ be a ring homomorphism that is isometric. For any continuous linear equivalence $e: E \simeq_{\text{SL}[\sigma_{12}]} F$, the operator norm of $e$ is strictly positive, i.e., $\|e\| > 0$.

ContinuousLinearEquiv.norm_symm_pos theorem

[RingHomIsometric σ₁₂] [Nontrivial E] (e : E ≃SL[σ₁₂] F) : 0 < ‖(e.symm : F →SL[σ₂₁] E)‖

Full source

theorem norm_symm_pos [RingHomIsometric σ₁₂] [Nontrivial E] (e : E ≃SL[σ₁₂] F) :
    0 < ‖(e.symm : F →SL[σ₂₁] E)‖ :=
  pos_of_mul_pos_right (zero_lt_one.trans_le e.one_le_norm_mul_norm_symm) (norm_nonneg _)

Positivity of Operator Norm for Inverse of Continuous Linear Equivalence

Informal description

Let $E$ and $F$ be normed spaces over fields $\mathbb{K}_1$ and $\mathbb{K}_2$ respectively, with $E$ being nontrivial. Let $\sigma_{12}: \mathbb{K}_1 \to \mathbb{K}_2$ be a ring homomorphism that is isometric. For any continuous linear equivalence $e: E \simeq_{\text{SL}[\sigma_{12}]} F$, the operator norm of its inverse $e^{-1}: F \to E$ is strictly positive, i.e., $\|e^{-1}\| > 0$.

ContinuousLinearEquiv.nnnorm_symm_pos theorem

[RingHomIsometric σ₁₂] [Nontrivial E] (e : E ≃SL[σ₁₂] F) : 0 < ‖(e.symm : F →SL[σ₂₁] E)‖₊

Full source

theorem nnnorm_symm_pos [RingHomIsometric σ₁₂] [Nontrivial E] (e : E ≃SL[σ₁₂] F) :
    0 < ‖(e.symm : F →SL[σ₂₁] E)‖₊ :=
  e.norm_symm_pos

Positivity of Operator Seminorm for Inverse of Continuous Linear Equivalence

Informal description

Let $E$ and $F$ be normed spaces over fields $\mathbb{K}_1$ and $\mathbb{K}_2$ respectively, with $E$ being nontrivial. Let $\sigma_{12}: \mathbb{K}_1 \to \mathbb{K}_2$ be a ring homomorphism that is isometric. For any continuous linear equivalence $e: E \simeq_{\text{SL}[\sigma_{12}]} F$, the operator seminorm of its inverse $e^{-1}: F \to E$ is strictly positive, i.e., $\|e^{-1}\|_+ > 0$.

ContinuousLinearEquiv.subsingleton_or_norm_symm_pos theorem

[RingHomIsometric σ₁₂] (e : E ≃SL[σ₁₂] F) : Subsingleton E ∨ 0 < ‖(e.symm : F →SL[σ₂₁] E)‖

Full source

theorem subsingleton_or_norm_symm_pos [RingHomIsometric σ₁₂] (e : E ≃SL[σ₁₂] F) :
    SubsingletonSubsingleton E ∨ 0 < ‖(e.symm : F →SL[σ₂₁] E)‖ := by
  rcases subsingleton_or_nontrivial E with (_i | _i)
  · left
    infer_instance
  · right
    exact e.norm_symm_pos

Inverse Operator Norm Positivity or Subsingleton Condition for Continuous Linear Equivalence

Informal description

Let $E$ and $F$ be normed spaces over fields $\mathbb{K}_1$ and $\mathbb{K}_2$ respectively, with a ring homomorphism $\sigma_{12}: \mathbb{K}_1 \to \mathbb{K}_2$ that is isometric. For any continuous linear equivalence $e: E \simeq_{\text{SL}[\sigma_{12}]} F$, either $E$ is a subsingleton (i.e., has at most one element) or the operator norm of the inverse $e^{-1}: F \to E$ is strictly positive, i.e., $\|e^{-1}\| > 0$.

ContinuousLinearEquiv.subsingleton_or_nnnorm_symm_pos theorem

[RingHomIsometric σ₁₂] (e : E ≃SL[σ₁₂] F) : Subsingleton E ∨ 0 < ‖(e.symm : F →SL[σ₂₁] E)‖₊

Full source

theorem subsingleton_or_nnnorm_symm_pos [RingHomIsometric σ₁₂] (e : E ≃SL[σ₁₂] F) :
    SubsingletonSubsingleton E ∨ 0 < ‖(e.symm : F →SL[σ₂₁] E)‖₊ :=
  subsingleton_or_norm_symm_pos e

Positivity of Inverse Operator Seminorm or Subsingleton Condition for Continuous Linear Equivalence

Informal description

Let $E$ and $F$ be normed spaces over fields $\mathbb{K}_1$ and $\mathbb{K}_2$ respectively, with a ring homomorphism $\sigma_{12}: \mathbb{K}_1 \to \mathbb{K}_2$ that is isometric. For any continuous linear equivalence $e: E \simeq_{\text{SL}[\sigma_{12}]} F$, either $E$ is a subsingleton (i.e., has at most one element) or the operator seminorm of the inverse $e^{-1}: F \to E$ is strictly positive, i.e., $\|e^{-1}\|_+ > 0$.

ContinuousLinearEquiv.coord_norm theorem

(x : E) (h : x ≠ 0) : ‖coord 𝕜 x h‖ = ‖x‖⁻¹

Full source

@[simp]
theorem coord_norm (x : E) (h : x ≠ 0) : ‖coord 𝕜 x h‖ = ‖x‖‖x‖⁻¹ := by
  have hx : 0 < ‖x‖ := norm_pos_iff.mpr h
  haveI : Nontrivial (𝕜 ∙ x) := Submodule.nontrivial_span_singleton h
  exact ContinuousLinearMap.homothety_norm _ fun y =>
    homothety_inverse _ hx _ (LinearEquiv.toSpanNonzeroSingleton_homothety 𝕜 x h) _

Operator Norm of Coordinate Functional Equals Reciprocal of Norm

Informal description

For any nonzero element $x$ in a normed space $E$ over a field $\mathbb{K}$, the operator norm of the continuous linear functional $\text{coord}_{\mathbb{K}}(x, h)$ (where $h$ is a proof that $x \neq 0$) is equal to the reciprocal of the norm of $x$, i.e., $\|\text{coord}_{\mathbb{K}}(x, h)\| = \|x\|^{-1}$.

NormedSpace.equicontinuous_TFAE theorem

 :
  List.TFAE
    [EquicontinuousAt ((↑) ∘ f) 0, Equicontinuous ((↑) ∘ f), UniformEquicontinuous ((↑) ∘ f),
      ∃ C, ∀ i x, ‖f i x‖ ≤ C * ‖x‖, ∃ C ≥ 0, ∀ i x, ‖f i x‖ ≤ C * ‖x‖, ∃ C, ∀ i, ‖f i‖ ≤ C, ∃ C ≥ 0, ∀ i, ‖f i‖ ≤ C,
      BddAbove (Set.range (‖f ·‖)), (⨆ i, (‖f i‖₊ : ENNReal)) < ⊤]

Full source

/-- 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`. -/
protected theorem NormedSpace.equicontinuous_TFAE : List.TFAE
    [ EquicontinuousAt ((↑) ∘ f) 0,
      Equicontinuous ((↑) ∘ f),
      UniformEquicontinuous ((↑) ∘ f),
      ∃ C, ∀ i x, ‖f i x‖ ≤ C * ‖x‖,
      ∃ C ≥ 0, ∀ i x, ‖f i x‖ ≤ C * ‖x‖,
      ∃ C, ∀ i, ‖f i‖ ≤ C,
      ∃ C ≥ 0, ∀ i, ‖f i‖ ≤ C,
      BddAbove (Set.range (‖f ·‖)),
      (⨆ i, (‖f i‖₊ : ENNReal)) < ⊤ ] := by
  -- `1 ↔ 2 ↔ 3` follows from `uniformEquicontinuous_of_equicontinuousAt_zero`
  tfae_have 1 → 3 := uniformEquicontinuous_of_equicontinuousAt_zero f
  tfae_have 3 → 2 := UniformEquicontinuous.equicontinuous
  tfae_have 2 → 1 := fun H ↦ H 0
  -- `4 ↔ 5 ↔ 6 ↔ 7 ↔ 8 ↔ 9` is morally trivial, we just have to use a lot of rewriting
  -- and `congr` lemmas
  tfae_have 4 ↔ 5 := by
    rw [exists_ge_and_iff_exists]
    exact fun C₁ C₂ hC ↦ forall₂_imp fun i x ↦ le_trans' <| by gcongr
  tfae_have 5 ↔ 7 := by
    refine exists_congr (fun C ↦ and_congr_right fun hC ↦ forall_congr' fun i ↦ ?_)
    rw [ContinuousLinearMap.opNorm_le_iff hC]
  tfae_have 7 ↔ 8 := by
    simp_rw [bddAbove_iff_exists_ge (0 : ℝ), Set.forall_mem_range]
  tfae_have 6 ↔ 8 := by
    simp_rw [bddAbove_def, Set.forall_mem_range]
  tfae_have 8 ↔ 9 := by
    rw [ENNReal.iSup_coe_lt_top, ← NNReal.bddAbove_coe, ← Set.range_comp]
    rfl
  -- `3 ↔ 4` is the interesting part of the result. It is essentially a combination of
  -- `WithSeminorms.uniformEquicontinuous_iff_exists_continuous_seminorm` which turns
  -- equicontinuity into existence of some continuous seminorm and
  -- `Seminorm.bound_of_continuous_normedSpace` which characterize such seminorms.
  tfae_have 3 ↔ 4 := by
    refine ((norm_withSeminorms 𝕜₂ F).uniformEquicontinuous_iff_exists_continuous_seminorm _).trans
      ?_
    rw [forall_const]
    constructor
    · intro ⟨p, hp, hpf⟩
      rcases p.bound_of_continuous_normedSpace hp with ⟨C, -, hC⟩
      exact ⟨C, fun i x ↦ (hpf i x).trans (hC x)⟩
    · intro ⟨C, hC⟩
      refine ⟨C.toNNReal • normSeminorm 𝕜 E,
        ((norm_withSeminorms 𝕜 E).continuous_seminorm 0).const_smul C.toNNReal, fun i x ↦ ?_⟩
      exact (hC i x).trans (mul_le_mul_of_nonneg_right (C.le_coe_toNNReal) (norm_nonneg x))
  tfae_finish

Equivalent Characterizations of Equicontinuity for Continuous Linear Maps Between Normed Spaces

Informal description

Let $E$ and $F$ be normed spaces, and let $(f_i)_{i \in I}$ be a family of continuous linear maps $f_i : E \to F$. The following statements are equivalent: 1. The family $(f_i)$ is equicontinuous at $0$. 2. The family $(f_i)$ is equicontinuous. 3. The family $(f_i)$ is uniformly equicontinuous. 4. There exists a constant $C$ such that for all $i \in I$ and $x \in E$, $\|f_i x\| \leq C \|x\|$. 5. There exists a constant $C \geq 0$ such that for all $i \in I$ and $x \in E$, $\|f_i x\| \leq C \|x\|$. 6. There exists a constant $C$ such that for all $i \in I$, $\|f_i\| \leq C$. 7. There exists a constant $C \geq 0$ such that for all $i \in I$, $\|f_i\| \leq C$. 8. The set $\{\|f_i\| \mid i \in I\}$ is bounded above. 9. The supremum $\sup_{i \in I} \|f_i\|$ is finite (as an extended real number).