Mathlib.Analysis.Normed.Module.Span

LinearMap.toSpanSingleton_homothety theorem

(x : E) (c : 𝕜) : ‖LinearMap.toSpanSingleton 𝕜 E x c‖ = ‖x‖ * ‖c‖

Full source

theorem toSpanSingleton_homothety (x : E) (c : 𝕜) :
    ‖LinearMap.toSpanSingleton 𝕜 E x c‖ = ‖x‖ * ‖c‖ := by
  rw [mul_comm]
  exact norm_smul _ _

Homothety Property of Scalar Multiplication: $\|c \cdot x\| = \|x\| \cdot \|c\|$

Informal description

For any vector $x$ in a normed space $E$ over a normed division ring $\mathbb{K}$ and any scalar $c \in \mathbb{K}$, the norm of the vector obtained by scaling $x$ by $c$ (i.e., $c \cdot x$) is equal to the product of the norms of $x$ and $c$, i.e., $\|c \cdot x\| = \|x\| \cdot \|c\|$.

LinearEquiv.toSpanNonzeroSingleton_homothety theorem

(x : E) (h : x ≠ 0) (c : 𝕜) : ‖LinearEquiv.toSpanNonzeroSingleton 𝕜 E x h c‖ = ‖x‖ * ‖c‖

Full source

theorem _root_.LinearEquiv.toSpanNonzeroSingleton_homothety (x : E) (h : x ≠ 0) (c : 𝕜) :
    ‖LinearEquiv.toSpanNonzeroSingleton 𝕜 E x h c‖ = ‖x‖ * ‖c‖ :=
  LinearMap.toSpanSingleton_homothety _ _ _

Homothety Property of Linear Equivalence to Span of Nonzero Vector: $\|L(c)\| = \|x\| \cdot \|c\|$

Informal description

For any nonzero vector $x$ in a normed space $E$ over a normed division ring $\mathbb{K}$ and any scalar $c \in \mathbb{K}$, the norm of the image of $c$ under the linear equivalence from $\mathbb{K}$ to the span of $x$ is equal to the product of the norms of $x$ and $c$, i.e., $\|L(c)\| = \|x\| \cdot \|c\|$, where $L \colon \mathbb{K} \to \mathbb{K} \cdot x$ is the linear equivalence map.

ContinuousLinearEquiv.toSpanNonzeroSingleton definition

(x : E) (h : x ≠ 0) : 𝕜 ≃L[𝕜] 𝕜 ∙ x

Full source

/-- Given a nonzero element `x` of a normed space `E₁` over a field `𝕜`, the natural
    continuous linear equivalence from `E₁` to the span of `x`. -/
noncomputable def toSpanNonzeroSingleton (x : E) (h : x ≠ 0) : 𝕜 ≃L[𝕜] 𝕜 ∙ x :=
  ofHomothety (LinearEquiv.toSpanNonzeroSingleton 𝕜 E x h) ‖x‖ (norm_pos_iff.mpr h)
    (LinearEquiv.toSpanNonzeroSingleton_homothety 𝕜 x h)

Continuous linear equivalence between a field and the span of a nonzero vector

Informal description

Given a nonzero element $x$ in a normed space $E$ over a field $\mathbb{K}$, the natural continuous linear equivalence from $\mathbb{K}$ to the span of $x$ (denoted $\mathbb{K} \cdot x$) is defined. This equivalence is constructed using a homothety condition, ensuring that for any scalar $c \in \mathbb{K}$, the norm of the image $c \cdot x$ is equal to $\|x\| \cdot \|c\|$.

ContinuousLinearEquiv.coord definition

(x : E) (h : x ≠ 0) : (𝕜 ∙ x) →L[𝕜] 𝕜

Full source

/-- Given a nonzero element `x` of a normed space `E₁` over a field `𝕜`, the natural continuous
    linear map from the span of `x` to `𝕜`. -/
noncomputable def coord (x : E) (h : x ≠ 0) : (𝕜 ∙ x) →L[𝕜] 𝕜 :=
  (toSpanNonzeroSingleton 𝕜 x h).symm

Coordinate map from the span of a nonzero vector to the base field

Informal description

Given a nonzero element $x$ in a normed space $E$ over a field $\mathbb{K}$, the continuous linear map $\text{coord}_{\mathbb{K}, x, h}$ from the span of $x$ (denoted $\mathbb{K} \cdot x$) back to $\mathbb{K}$ is defined as the inverse of the natural continuous linear equivalence between $\mathbb{K}$ and $\mathbb{K} \cdot x$.

ContinuousLinearEquiv.coe_toSpanNonzeroSingleton_symm theorem

{x : E} (h : x ≠ 0) : ⇑(toSpanNonzeroSingleton 𝕜 x h).symm = coord 𝕜 x h

Full source

@[simp]
theorem coe_toSpanNonzeroSingleton_symm {x : E} (h : x ≠ 0) :
    ⇑(toSpanNonzeroSingleton 𝕜 x h).symm = coord 𝕜 x h :=
  rfl

Inverse of Span Equivalence Equals Coordinate Map for Nonzero Vectors

Informal description

For any nonzero element $x$ in a normed space $E$ over a field $\mathbb{K}$, the inverse of the continuous linear equivalence $\text{toSpanNonzeroSingleton}_{\mathbb{K}, x, h}$ from $\mathbb{K}$ to the span of $x$ (denoted $\mathbb{K} \cdot x$) is equal to the coordinate map $\text{coord}_{\mathbb{K}, x, h}$ from $\mathbb{K} \cdot x$ back to $\mathbb{K}$.

ContinuousLinearEquiv.coord_toSpanNonzeroSingleton theorem

{x : E} (h : x ≠ 0) (c : 𝕜) : coord 𝕜 x h (toSpanNonzeroSingleton 𝕜 x h c) = c

Full source

@[simp]
theorem coord_toSpanNonzeroSingleton {x : E} (h : x ≠ 0) (c : 𝕜) :
    coord 𝕜 x h (toSpanNonzeroSingleton 𝕜 x h c) = c :=
  (toSpanNonzeroSingleton 𝕜 x h).symm_apply_apply c

Inverse Property of Coordinate Map and Span Equivalence

Informal description

Let $\mathbb{K}$ be a normed field and $E$ be a normed space over $\mathbb{K}$. For any nonzero vector $x \in E$ and any scalar $c \in \mathbb{K}$, the coordinate map $\text{coord}_{\mathbb{K}, x, h}$ evaluated at the image of $c$ under the continuous linear equivalence $\text{toSpanNonzeroSingleton}_{\mathbb{K}, x, h}$ equals $c$, i.e., \[ \text{coord}_{\mathbb{K}, x, h}(\text{toSpanNonzeroSingleton}_{\mathbb{K}, x, h}(c)) = c. \]

ContinuousLinearEquiv.toSpanNonzeroSingleton_coord theorem

{x : E} (h : x ≠ 0) (y : 𝕜 ∙ x) : toSpanNonzeroSingleton 𝕜 x h (coord 𝕜 x h y) = y

Full source

@[simp]
theorem toSpanNonzeroSingleton_coord {x : E} (h : x ≠ 0) (y : 𝕜 ∙ x) :
    toSpanNonzeroSingleton 𝕜 x h (coord 𝕜 x h y) = y :=
  (toSpanNonzeroSingleton 𝕜 x h).apply_symm_apply y

Span Equivalence and Coordinate Map are Inverses for Nonzero Vectors

Informal description

Let $\mathbb{K}$ be a normed field and $E$ be a normed space over $\mathbb{K}$. For any nonzero vector $x \in E$ (i.e., $x \neq 0$) and any element $y$ in the span of $x$ (i.e., $y \in \mathbb{K} \cdot x$), applying the continuous linear equivalence $\text{toSpanNonzeroSingleton}_{\mathbb{K}, x, h}$ to the coordinate $\text{coord}_{\mathbb{K}, x, h}(y)$ of $y$ recovers $y$ itself. In other words, the composition of the coordinate map with the span equivalence is the identity on $\mathbb{K} \cdot x$.

ContinuousLinearEquiv.coord_self theorem

(x : E) (h : x ≠ 0) : (coord 𝕜 x h) (⟨x, Submodule.mem_span_singleton_self x⟩ : 𝕜 ∙ x) = 1

Full source

@[simp]
theorem coord_self (x : E) (h : x ≠ 0) :
    (coord 𝕜 x h) (⟨x, Submodule.mem_span_singleton_self x⟩ : 𝕜 ∙ x) = 1 :=
  LinearEquiv.coord_self 𝕜 E x h

Coordinate Map Evaluates to One on the Spanning Vector

Informal description

Let $E$ be a normed space over a normed field $\mathbb{K}$, and let $x \in E$ be a nonzero vector. The coordinate map $\text{coord}_{\mathbb{K}, x, h}$ evaluated at the vector $x$ (considered as an element of the span $\mathbb{K} \cdot x$) is equal to $1$, i.e., \[ \text{coord}_{\mathbb{K}, x, h}(x) = 1. \]

LinearIsometryEquiv.toSpanUnitSingleton definition

(x : E) (hx : ‖x‖ = 1) : 𝕜 ≃ₗᵢ[𝕜] 𝕜 ∙ x

Full source

/-- Given a unit element `x` of a normed space `E` over a field `𝕜`, the natural
    linear isometry equivalence from `E` to the span of `x`. -/
noncomputable def toSpanUnitSingleton (x : E) (hx : ‖x‖ = 1) :
    𝕜 ≃ₗᵢ[𝕜] 𝕜 ∙ x where
  toLinearEquiv := LinearEquiv.toSpanNonzeroSingleton 𝕜 E x (by aesop)
  norm_map' := by
    intro
    rw [LinearEquiv.toSpanNonzeroSingleton_homothety, hx, one_mul]

Linear isometric equivalence between a field and the span of a unit vector

Informal description

Given a unit vector $x$ in a normed space $E$ over a field $\mathbb{K}$ (i.e., $\|x\| = 1$), the map $\mathbb{K} \to \mathbb{K} \cdot x$ defined by $r \mapsto r \cdot x$ is a linear isometric equivalence between $\mathbb{K}$ and the span of $x$. This means it is a bijective linear map that preserves the norm, i.e., $\|r \cdot x\| = |r| \cdot \|x\| = |r|$ for all $r \in \mathbb{K}$.

LinearIsometryEquiv.toSpanUnitSingleton_apply theorem

(x : E) (hx : ‖x‖ = 1) (r : 𝕜) : toSpanUnitSingleton x hx r = (⟨r • x, by aesop⟩ : 𝕜 ∙ x)

Full source

@[simp] theorem toSpanUnitSingleton_apply (x : E) (hx : ‖x‖ = 1) (r : 𝕜) :
    toSpanUnitSingleton x hx r = (⟨r • x, by aesop⟩ : 𝕜 ∙ x) := by
  rfl

Action of Linear Isometric Equivalence on Scalar Multiplication: $\text{toSpanUnitSingleton}(x, hx)(r) = r \cdot x$

Informal description

For a unit vector $x$ in a normed space $E$ over a field $\mathbb{K}$ (i.e., $\|x\| = 1$), the linear isometric equivalence $\mathbb{K} \simeq \mathbb{K} \cdot x$ maps any scalar $r \in \mathbb{K}$ to the vector $r \cdot x$ in the span of $x$. That is, the equivalence $\text{toSpanUnitSingleton}(x, hx)$ satisfies $\text{toSpanUnitSingleton}(x, hx)(r) = r \cdot x$ for all $r \in \mathbb{K}$.

Main definitions