The function space $\mathbf{F}^S$ (LADR 1.24, 1.25)

• The function space $\mathbf{F}^S$ (LADR 1.24, 1.25) #Card
  • $\mathbf{F}^S$ とは何で、なぜベクトル空間になるか？

Back

$S$ が集合のとき、$\mathbf{F}^S$ は $S$ から $\mathbf{F}$ への関数全体。 $f,g\in\mathbf{F}^S$, $\lambda\in\mathbf{F}$ に対し、和・スカラー倍を点ごとに定義： $$(f+g)(x)=f(x)+g(x),\qquad (\lambda f)(x)=\lambda f(x).$$ これで $\mathbf{F}^S$ はベクトル空間（$S\neq\varnothing$）。加法単位元は零関数 $0(x)=0$、$f$ の逆元は $(-f)(x)=-f(x)$。 $\mathbf{F}^n$ は $\mathbf{F}^{{1,\dots,n}}$、$\mathbf{F}^\infty$ は $\mathbf{F}^{{1,2,\dots}}$ とみなせる特別な場合。

Back-extra

確率統計への接続: 関数空間こそ $L^2(\Omega,\mathcal F,\mu)$（自乗可積分な確率変数の空間）の代数的原型。

Lean

S → F は Pi.addCommGroup / Pi.module によりベクトル空間。点ごと演算は Pi.add_apply 等。