OAI/Analysis/AffineBernstein/JetCalculus.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.AffineBernstein.second_fderiv_comp line 15
2. theorem OAI.AffineBernstein.graphMap_fderiv line 41
3. theorem OAI.AffineBernstein.graphMap_second line 48
4. theorem OAI.AffineBernstein.second_fderiv_clm_comp line 66

   Source comment

   Second derivative under a fixed continuous linear functional.

   theorem second_fderiv_clm_comp (L : F →L[ℝ] G) {Y : E → F} {x : E}
       (hY : ContDiffAt ℝ ∞ Y x) (v w : E) :
       fderiv ℝ (fderiv ℝ (fun q => L (Y q))) x v w =
         L (fderiv ℝ (fderiv ℝ Y) x v w) := by
   …