Physlib.Mathematics.InnerProductSpace.Basic

The notation $\|x\|_2$ denotes the $L_2$ norm of an element $x$ in a space equipped with an inner product, which is defined as the square root of the inner product of $x$ with itself, i.e., $\|x\|_2 = \sqrt{\langle x, x \rangle}$.

Given a generalized inner product space $E$ over a field $\mathbb{k}$ (where $\mathbb{k}$ is typically $\mathbb{R}$ or $\mathbb{C}$), this definition extracts the underlying core structure required for an inner product space. This core structure includes the definition of the inner product $\langle \cdot, \cdot \rangle$ and the fundamental axioms it satisfies, such as linearity in the first argument, conjugate symmetry, and positive definiteness. This is used in cases where the space's default norm $\|\cdot\|$ does not necessarily coincide with the $L_2$ norm $\sqrt{\langle \cdot, \cdot \rangle}$.

Given a generalized inner product space $E$ over a field $\mathbb{k}$ (where $\mathbb{k}$ is typically $\mathbb{R}$ or $\mathbb{C}$), this instance provides the inner product $\langle \cdot, \cdot \rangle$ on $E$. It extracts the inner product operation from the underlying core structure of the `InnerProductSpace' 𝕜 E` typeclass, which generalizes standard inner product spaces by allowing the space's default norm to differ from the $L_2$ norm $\sqrt{\langle x, x \rangle}$.

Given a standard inner product space $E$ over a field $\mathbb{k}$ (where $\mathbb{k}$ is $\mathbb{R}$ or $\mathbb{C}$), this instance defines a generalized inner product space structure `InnerProductSpace' 𝕜 E` on $E$. In this construction, the $L_2$ norm $\|x\|_2$ is identified with the standard norm $\|x\|$ of the space, and the underlying inner product core is inherited directly. The requirement for the equivalence between the norm and the inner product is satisfied with constants $c = 1$ and $d = 1$, as the identity $\|x\|^2 = \text{Re} \langle x, x \rangle$ holds for all $x \in E$.

For a generalized inner product space $E$ over a field $\mathbb{k}$ (typically $\mathbb{R}$ or $\mathbb{C}$), this definition equips the type synonym $\text{WithLp } 2 E$ with a norm. For any element $x \in \text{WithLp } 2 E$, its norm is defined as $\|x\|_2 = \sqrt{\text{Re} \langle x, x \rangle}$, where $\langle \cdot, \cdot \rangle$ is the inner product provided by the generalized inner product space structure on $E$. This definition ensures that the space $\text{WithLp } 2 E$ is specifically endowed with the $L_2$ norm derived from its inner product.

Given a generalized inner product space $E$ over a field $\mathbb{k}$ (typically $\mathbb{R}$ or $\mathbb{C}$), this definition equips the type synonym $\text{WithLp } 2 E$ with an inner product $\langle \cdot, \cdot \rangle$. For any elements $x, y \in \text{WithLp } 2 E$, their inner product is defined as $\langle x, y \rangle := \langle \phi(x), \phi(y) \rangle_E$, where $\phi : \text{WithLp } 2 E \to E$ is the canonical identity equivalence and $\langle \cdot, \cdot \rangle_E$ is the inner product provided by the generalized inner product space structure on $E$.

Given a generalized inner product space $E$ over a field $\mathbb{k}$ (where $\mathbb{k}$ is $\mathbb{R}$ or $\mathbb{C}$), this definition endows the type synonym $\text{WithLp } 2 E$ with the structure of a normed additive commutative group. The underlying additive group structure is inherited from $E$, and the norm used is the $L_2$ norm, $\|x\|_2 = \sqrt{\text{Re} \langle x, x \rangle}$. This ensures that $\text{WithLp } 2 E$ satisfies the axioms of a normed group, specifically defining the distance between elements $x$ and $y$ as $d(x, y) = \|x - y\|_2$.

Let $E$ be a generalized inner product space. For any element $x$ in the space $\text{WithLp } 2 E$, the norm $\|x\|$ (the default norm of the type synonym) is equal to the absolute value of the $L_2$ norm of the underlying element in $E$, denoted by $\|x\|_2$.

Given a generalized inner product space $E$ over a field $\mathbb{k}$ (where $\mathbb{k}$ is $\mathbb{R}$ or $\mathbb{C}$), this definition endows the type synonym $\text{WithLp } 2 E$ with the structure of a normed space over $\mathbb{k}$. This construction uses the $L_2$ norm derived from the inner product, $\|x\|_2 = \sqrt{\text{Re} \langle x, x \rangle}$, and ensures that the scalar multiplication satisfies the homogeneity property $\|\alpha \cdot x\| = |\alpha| \cdot \|x\|$ for all $\alpha \in \mathbb{k}$ and $x \in \text{WithLp } 2 E$.

Given a generalized inner product space $E$ over a field $\mathbb{k}$ (where $\mathbb{k}$ is $\mathbb{R}$ or $\mathbb{C}$), this definition endows the type synonym $\text{WithLp } 2 E$ with the structure of a standard inner product space. The inner product $\langle \cdot, \cdot \rangle$ is inherited from the underlying space $E$, and the norm is the $L_2$ norm defined by $\|x\|_2 = \sqrt{\text{Re} \langle x, x \rangle}$. This construction ensures that the compatibility condition $\|x\|_2^2 = \text{Re} \langle x, x \rangle$ holds for all $x \in \text{WithLp } 2 E$.

Given a generalized inner product space $E$ over a field $\mathbb{k}$ (where $\mathbb{k}$ is $\mathbb{R}$ or $\mathbb{C}$), let $\|\cdot\|$ be the default norm on $E$. This definition defines a continuous linear map from $E$ to $\text{WithLp } 2 E$, where $\text{WithLp } 2 E$ denotes the same underlying vector space but equipped with the $L_2$ norm $\|x\|_2 = \sqrt{\text{Re} \langle x, x \rangle}$. The map is the identity function on the elements of the space, and it is continuous because the generalized inner product space structure requires the default norm $\|\cdot\|$ and the $L_2$ norm to be topologically equivalent.

Let $E$ be a generalized inner product space over a field $\mathbb{k}$ (where $\mathbb{k}$ is $\mathbb{R}$ or $\mathbb{C}$). The map `fromL2` is the continuous linear map from $\text{WithLp } 2 E$ to $E$ that acts as the identity on the underlying elements. Here, $\text{WithLp } 2 E$ denotes the space $E$ equipped with the $L_2$ norm $\|x\|_2 = \sqrt{\text{Re} \langle x, x \rangle}$, while $E$ carries its original norm $\|\cdot\|$. The continuity of this map is guaranteed by the requirement in a generalized inner product space that the original norm and the $L_2$ norm are topologically equivalent.

Let $E$ be a generalized inner product space over a field $\mathbb{k}$ (where $\mathbb{k}$ is $\mathbb{R}$ or $\mathbb{C}$). Let $\text{WithLp } 2 E$ denote the space $E$ equipped with the $L_2$ norm $\|x\|_2 = \sqrt{\text{Re} \langle x, x \rangle}$. Let $\text{fromL2} : \text{WithLp } 2 E \to E$ and $\text{toL2} : E \to \text{WithLp } 2 E$ be the canonical continuous linear maps that act as the identity on the underlying elements. For any $x \in \text{WithLp } 2 E$ and $y \in E$, the following identity holds: $$\langle \text{fromL2}(x), y \rangle = \langle x, \text{toL2}(y) \rangle$$ where the left inner product is the one provided by the structure on $E$ and the right inner product is the one provided by the structure on $\text{WithLp } 2 E$.

Let $E$ be a generalized inner product space over a field $\mathbb{k}$ (where $\mathbb{k}$ is $\mathbb{R}$ or $\mathbb{C}$). Let $\text{WithLp } 2 E$ denote the space $E$ equipped with the $L_2$ norm $\|x\|_2 = \sqrt{\text{Re} \langle x, x \rangle}$ and its induced inner product. Let $\text{WithLp.ofLp} : \text{WithLp } 2 E \to E$ and $\text{WithLp.toLp } 2 : E \to \text{WithLp } 2 E$ be the canonical identity maps between the space $E$ and its $L_2$ type synonym. For any $x \in E$ and $y \in \text{WithLp } 2 E$, the following identity holds: $$\langle \text{WithLp.ofLp } y, x \rangle = \langle y, \text{WithLp.toLp } 2 x \rangle$$ where the inner product on the left is the one defined on $E$, and the inner product on the right is the one defined on $\text{WithLp } 2 E$.

Let $E$ be a generalized inner product space over a field $\mathbb{k}$ (where $\mathbb{k}$ is $\mathbb{R}$ or $\mathbb{C}$). Let $\text{toL2} : E \to \text{WithLp } 2 E$ and $\text{fromL2} : \text{WithLp } 2 E \to E$ be the continuous linear identity maps between $E$ and the space equipped with the $L_2$ norm $\|x\|_2 = \sqrt{\text{Re} \langle x, x \rangle}$. For any $x \in E$ and $y \in \text{WithLp } 2 E$, the inner product satisfies: $$\langle \text{toL2 } x, y \rangle = \langle x, \text{fromL2 } y \rangle$$ where the left-hand side uses the inner product on $\text{WithLp } 2 E$ and the right-hand side uses the inner product on $E$.

Let $E$ be a generalized inner product space over a field $\mathbb{k}$ (where $\mathbb{k}$ is $\mathbb{R}$ or $\mathbb{C}$). Let $\text{WithLp } 2 E$ denote the space $E$ equipped with the $L_2$ norm $\|x\|_2 = \sqrt{\text{Re} \langle x, x \rangle}$. Let $\text{WithLp.toLp } 2 : E \to \text{WithLp } 2 E$ and $\text{WithLp.ofLp} : \text{WithLp } 2 E \to E$ be the identity maps between the underlying vector spaces. For any $y \in E$ and $x \in \text{WithLp } 2 E$, the inner product satisfies: $$\langle \text{WithLp.toLp } 2 \, y, x \rangle = \langle y, \text{WithLp.ofLp } x \rangle$$ where the left-hand side uses the inner product on $\text{WithLp } 2 E$ and the right-hand side uses the inner product on $E$.

Let $E$ be a generalized inner product space over a field $\mathbb{k}$ (where $\mathbb{k}$ is $\mathbb{R}$ or $\mathbb{C}$). Let $\text{WithLp } 2 E$ denote the space $E$ equipped with the $L_2$ norm $\|x\|_2 = \sqrt{\text{Re} \langle x, x \rangle}$. Let $\text{fromL2} : \text{WithLp } 2 E \to E$ and $\text{toL2} : E \to \text{WithLp } 2 E$ be the continuous linear maps that act as the identity on the underlying elements. For any $x \in \text{WithLp } 2 E$, it holds that $\text{toL2}(\text{fromL2}(x)) = x$.

Let $E$ be a generalized inner product space over a field $\mathbb{k}$ (where $\mathbb{k}$ is $\mathbb{R}$ or $\mathbb{C}$). Let $\text{toL2} : E \to \text{WithLp } 2 E$ be the continuous linear map that acts as the identity on the underlying elements of the vector space, and let $\text{fromL2} : \text{WithLp } 2 E \to E$ be the corresponding continuous linear map in the opposite direction. For any $x \in E$, it holds that $\text{fromL2}(\text{toL2 } x) = x$.

Let $E$ be a generalized inner product space over a field $\mathbb{k}$ (where $\mathbb{k}$ is $\mathbb{R}$ or $\mathbb{C}$). By definition, such a space is equipped with a default norm $\|\cdot\|$ and an inner product $\langle \cdot, \cdot \rangle$ that induces an $L_2$ norm $\|x\|_2 = \sqrt{\text{Re} \langle x, x \rangle}$ equivalent to $\|\cdot\|$. The term `equivL2` is the continuous linear equivalence (isomorphism of topological vector spaces) between $\text{WithLp } 2 E$, which denotes the space $E$ equipped with the $L_2$ norm, and the space $E$ carrying its original norm. The map is defined as the identity on the underlying elements of the vector space.

Let $E$ be a generalized inner product space over a field $\mathbb{k}$ (where $\mathbb{k}$ is $\mathbb{R}$ or $\mathbb{C}$). If $E$ is complete with respect to its original norm $\|\cdot\|$, then it is also a complete space when equipped with the $L_2$ norm $\|x\|_2 = \sqrt{\text{Re} \langle x, x \rangle}$ (denoted as $\text{WithLp } 2 E$).

Let $E$ be a generalized inner product space. For any vectors $x, y \in E$, if $\langle v, x \rangle = \langle v, y \rangle$ for all $v \in E$, then $x = y$.

Let $E$ be a generalized inner product space over a field $\mathbb{k}$. For any vectors $x, y \in E$, if the inner product $\langle x, v \rangle$ equals $\langle y, v \rangle$ for every vector $v \in E$, then $x = y$.

Let $E$ be a generalized inner product space over a field $\mathbb{k}$ (typically $\mathbb{R}$ or $\mathbb{C}$). For any vectors $x, y \in E$, the inner product satisfies conjugate symmetry: $\overline{\langle y, x \rangle} = \langle x, y \rangle$, where $\overline{z}$ denotes the conjugate of the scalar $z$.

Let $E$ be a generalized inner product space over a field $\mathbb{k}$ (where $\mathbb{k}$ is either $\mathbb{R}$ or $\mathbb{C}$). For any vectors $x, y \in E$ and any scalar $r \in \mathbb{k}$, the inner product of $r \cdot x$ with $y$ satisfies $\langle r \cdot x, y \rangle = \bar{r} \langle x, y \rangle$, where $\bar{r}$ denotes the conjugate of the scalar $r$.

Let $E$ be a generalized inner product space over the field $\mathbb{k}$ (where $\mathbb{k}$ is $\mathbb{R}$ or $\mathbb{C}$). For any vectors $x, y \in E$ and any scalar $r \in \mathbb{k}$, the inner product $\langle \cdot, \cdot \rangle$ is linear in its second argument, satisfying the identity $\langle x, r \cdot y \rangle = r \langle x, y \rangle$.

In a generalized inner product space $E$ over a field $\mathbb{k}$, for any vector $x \in E$, the inner product of the zero vector with $x$ is zero, denoted as $\langle 0, x \rangle = 0$.

Let $E$ be a generalized inner product space over a field $\mathbb{k}$. For any vector $x \in E$, the inner product of $x$ with the zero vector on the right is zero, i.e., $\langle x, 0 \rangle = 0$.

In a generalized inner product space $E$ over a field $\mathbb{k}$, for any vectors $x, y, z \in E$, the inner product satisfies the left-additivity property: $\langle x + y, z \rangle = \langle x, z \rangle + \langle y, z \rangle$.

In a generalized inner product space $E$, for any vectors $x, y, z \in E$, the inner product is additive in the second argument, meaning $\langle x, y + z \rangle = \langle x, y \rangle + \langle x, z \rangle$.

In a generalized inner product space $E$ over a field $\mathbb{k}$, for any elements $x, y, z \in E$, the inner product $\langle \cdot, \cdot \rangle$ satisfies the identity $\langle x - y, z \rangle = \langle x, z \rangle - \langle y, z \rangle$.

Let $E$ be a generalized inner product space over a field $\mathbb{k}$. For any vectors $x, y, z \in E$, the inner product satisfies the distributivity property over subtraction in the second argument: $$\langle x, y - z \rangle = \langle x, y \rangle - \langle x, z \rangle$$ where $\langle \cdot, \cdot \rangle$ denotes the inner product provided by the space $E$.

Let $E$ be a generalized inner product space over a field $\mathbb{k}$. For any vectors $x, y \in E$, the inner product satisfies the identity $\langle -x, y \rangle = -\langle x, y \rangle$.

Let $E$ be a generalized inner product space. For any vectors $x, y \in E$, the inner product satisfies the identity $\langle x, -y \rangle = -\langle x, y \rangle$.

Let $E$ be a generalized inner product space over a field $\mathbb{k}$. For any $x \in E$, the inner product of $x$ with itself is zero if and only if $x$ is the zero vector, i.e., $\langle x, x \rangle = 0 \iff x = 0$.

Let $E$ be a generalized inner product space. For any vector $x \in E$ and any finite family of vectors $\{g_i\}_{i \in I}$ in $E$, the inner product of $x$ with the sum of the vectors $g_i$ is equal to the sum of the inner products of $x$ with each vector $g_i$: $$\left\langle x, \sum_{i \in I} g_i \right\rangle = \sum_{i \in I} \langle x, g_i \rangle$$

Let $\alpha$ be a topological space and $E$ be a generalized inner product space over a field $\mathbb{k}$. If $f : \alpha \to E$ and $g : \alpha \to E$ are continuous functions, then the function mapping each $a \in \alpha$ to the inner product $\langle f(a), g(a) \rangle$ is continuous.

For any vector $x$ in a generalized inner product space $F$, the real part of the inner product of $x$ with itself is non-negative, that is, $0 \le \text{Re} \langle x, x \rangle$.

For any elements $x$ and $y$ in a real inner product space $F$, the inner product is symmetric, satisfying $\langle y, x \rangle = \langle x, y \rangle$.

Let $E$ be a normed space and $F$ be a generalized inner product space. If $f: E \to F$ and $g: E \to F$ are $n$-times continuously differentiable at a point $x \in E$ with respect to the field $\mathbb{R}$, then the scalar-valued function mapping $x$ to the inner product $\langle f(x), g(x) \rangle$ is also $n$-times continuously differentiable at $x$ with respect to $\mathbb{R}$.

Let $E$ be a normed space and $F$ be a generalized inner product space. If $f: E \to F$ and $g: E \to F$ are $n$-times continuously differentiable functions ($C^n$ functions) over $\mathbb{R}$, then the scalar-valued function mapping $x$ to the inner product $\langle f(x), g(x) \rangle$ is also $n$-times continuously differentiable over $\mathbb{R}$.

For any two elements $(x, y)$ and $(x', y')$ in the product space $E \times F$, where $E$ and $F$ are inner product spaces over a field $\mathbb{k}$, the inner product is defined as the sum of the inner products of their components: $$\langle (x, y), (x', y') \rangle = \langle x, x' \rangle + \langle y, y' \rangle$$

Let $E$ and $F$ be generalized inner product spaces over a field $\mathbb{k}$. For any two elements $x, y$ in the product space $E \times F$, the inner product $\langle x, y \rangle$ is equal to the sum of the inner products of their components: $$\langle x, y \rangle = \langle x_1, y_1 \rangle + \langle x_2, y_2 \rangle$$ where $x = (x_1, x_2)$ and $y = (y_1, y_2)$, with $x_1, y_1 \in E$ and $x_2, y_2 \in F$.

For generalized inner product spaces $E$ and $F$ over a field $\mathbb{k}$ (where $\mathbb{k}$ is $\mathbb{R}$ or $\mathbb{C}$), the product space $E \times F$ is endowed with a generalized inner product space structure. The inner product is defined component-wise as: $$\langle (x_1, y_1), (x_2, y_2) \rangle = \langle x_1, x_2 \rangle_E + \langle y_1, y_2 \rangle_F$$ The associated $L_2$ norm on the product space is given by $\|(x, y)\|_2 = \sqrt{\|x\|_2^2 + \|y\|_2^2}$, where $\| \cdot \|_2$ denotes the $L_2$ norms of the respective spaces. This construction satisfies the required equivalence condition with the standard product norm $\|(x, y)\| = \max(\|x\|, \|y\|)$, meaning there exist constants $c, d > 0$ such that $c \|(x, y)\|^2 \le \text{Re} \langle (x, y), (x, y) \rangle \le d \|(x, y)\|^2$ for all $(x, y) \in E \times F$.

Let $\iota$ be a finite index set and $E$ be a generalized inner product space over a field $\mathbb{k}$ (where $\mathbb{k}$ is $\mathbb{R}$ or $\mathbb{C}$). The space of functions $\iota \to E$ (the product space $\prod_{i \in \iota} E$) is itself a generalized inner product space. The inner product of two elements $x, y \in \iota \to E$ is defined as the sum of the inner products of their components: $$\langle x, y \rangle = \sum_{i \in \iota} \langle x_i, y_i \rangle$$ The associated $L_2$ norm for this space is given by $$\|x\|_2 = \sqrt{\sum_{i \in \iota} \|x_i\|_2^2}$$ where $\|x_i\|_2 = \sqrt{\text{Re} \langle x_i, x_i \rangle}$ is the $L_2$ norm on $E$. This structure satisfies the requirement that the inner product is equivalent to the standard product norm (supremum norm) on $\iota \to E$.

In a generalized inner product space $E$ over a field $\mathbb{k}$ (where $\mathbb{k}$ is $\mathbb{R}$ or $\mathbb{C}$), the inner product operation $(x, y) \mapsto \langle x, y \rangle$ is a bounded bilinear map over $\mathbb{R}$.