Norm (ノルム) (Section III.6)

• Norm (ノルム) (Section III.6) #Card
  • A norm on a real vector space $X$ is a map $|\cdot| : X \to \mathbb{R}_+$ such that $|x| = 0 \implies x = 0$; $|\lambda x| = |\lambda| |x|$; $|x + y| \leq |x| + |y|$.

Back

A norm in a real vector space $X$ is a map $|\cdot| : X \to \mathbb{R}_+$ such that for each $x, y \in X$ and $\lambda \in \mathbb{R}$: $$|x| = 0 \implies x = 0, \qquad |\lambda \cdot x| = |\lambda| |x|, \qquad |x + y| \leq |x| + |y|.$$

• Each norm defines a metric by $d(x,y) := |x - y|$。
• $\mathbb{R}^m$ の 3 つの基本ノルム: $|x|_2 = \sqrt{\sum |x_k|^2}$, $|x|1 = \sum |x_k|$, $|x|\infty = \max |x_k|$。それぞれ $d, s, t$ に対応（$d(x,y) = |x-y|_2$ など）。

Lean

NormedAddCommGroup X + NormedSpace ℝ X（‖x‖; dist_eq_norm）