ノルム空間

一般の微分では，実数直線だけでなくノルム空間を扱います． NormedAddCommGroup E はノルムを持つ加法可換群， NormedSpace ℝ E は実ノルムベクトル空間です．

#check NormedAddCommGroup
#check NormedSpace
#check norm_nonneg
#check norm_add_le

section NormedSpaces

variable {E : Type*} [NormedAddCommGroup E]

example (x : E) : 0 ≤ ‖x‖ := by
  exact norm_nonneg x

example {x : E} : ‖x‖ = 0 ↔ x = 0 := by
  exact norm_eq_zero

example (x y : E) : ‖x + y‖ ≤ ‖x‖ + ‖y‖ := by
  exact norm_add_le x y

example : PseudoMetricSpace E := by
  infer_instance

variable [NormedSpace ℝ E]

example (a : ℝ) (x : E) : ‖a • x‖ = |a| * ‖x‖ := by
  exact norm_smul a x

example [FiniteDimensional ℝ E] : CompleteSpace E := by
  infer_instance

end NormedSpaces

有限次元ノルム空間が完備であることなど，解析の標準的な背景定理も型クラス探索で得られることがあります． infer_instance は，必要な型クラスインスタンスを Lean に探させるコマンドです．