OAI/Analysis/AffineBernstein/ParametricChangeOfCoordinates.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AffineBernstein.second_comp_of_critical line 18

   Source comment

   At a critical point the Hessian chain rule has no second derivative of the coordinate change. Here it is proved for the actual Fréchet derivatives.

   lemma second_comp_of_critical {f : F → ℝ} {φ : E → F} {x : E}
       (hf : ContDiffAt ℝ ∞ f (φ x)) (hφ : ContDiffAt ℝ ∞ φ x)
       (hz : fderiv ℝ f (φ x) = 0) (v w : E) :
       fderiv ℝ (fderiv ℝ (f ∘ φ)) x v w =
         fderiv ℝ (fderiv ℝ f) (φ x) (fderiv ℝ φ x v) (fderiv ℝ φ x w) := by
   …

2. def OAI.AffineBernstein.parametricJacobian line 40
3. lemma OAI.AffineBernstein.hessian_comp_of_critical line 43
4. lemma OAI.AffineBernstein.parametricSecondForm_comp line 66
5. lemma OAI.AffineBernstein.parametricFrame_comp_matrix line 75
6. lemma OAI.AffineBernstein.parametricFrame_comp_det line 93