連続線形写像と Frechet 微分

ノルム空間の間の連続線形写像は E →L[𝕜] F です． Frechet 微分では，導関数の値は連続線形写像になります．

#check ContinuousLinearMap
#check HasFDerivAt
#check fderiv

section Frechet

variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
variable {E F : Type*}
variable [NormedAddCommGroup E] [NormedSpace 𝕜 E]
variable [NormedAddCommGroup F] [NormedSpace 𝕜 F]

example : E →L[𝕜] E :=
  ContinuousLinearMap.id 𝕜 E

example (f : E →L[𝕜] F) : E → F :=
  f

example (f : E →L[𝕜] F) : Continuous f := by
  exact f.cont

example (f : E →L[𝕜] F) (x y : E) : f (x + y) = f x + f y := by
  exact f.map_add x y

example (f : E →L[𝕜] F) (a : 𝕜) (x : E) : f (a • x) = a • f x := by
  exact f.map_smul a x

example (f : E →L[𝕜] F) (x : E) : HasFDerivAt f f x := by
  exact f.hasFDerivAt

end Frechet

HasFDerivAt f f' x は，「点 x での f の一次近似が連続線形写像 f' である」という意味です． 実数値関数の HasDerivAt は，この一般論の特殊な形として扱えます．

演習問題

1. E →L[ℝ] F の元が連続関数として使えることを確認してください．

   example {E F : Type*}
       [NormedAddCommGroup E] [NormedSpace ℝ E]
       [NormedAddCommGroup F] [NormedSpace ℝ F]
       (L : E →L[ℝ] F) :
       Continuous L := by
     -- ヒント: `exact L.cont`
     -- 解答例: exact L.cont
     sorry
   

2. HasFDerivAt の statement を #check で表示し，実数 1 変数の HasDerivAt と何が違うか説明してください．

   -- 解答例: `HasFDerivAt` は連続線形写像を微分として指定し，
   -- `HasDerivAt` は 1 変数の微分係数を指定します．
   #check HasFDerivAt
   #check HasDerivAt
   

3. ContinuousLinearMap.id が任意の点で Frechet 微分として自分自身を持つことを確認してください．

   example {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] (x : E) :
       HasFDerivAt (ContinuousLinearMap.id ℝ E) (ContinuousLinearMap.id ℝ E) x := by
     -- ヒント: `exact (ContinuousLinearMap.id ℝ E).hasFDerivAt`
     -- 解答例: exact (ContinuousLinearMap.id ℝ E).hasFDerivAt
     sorry