OAI/Analysis/AffineBernstein/NewtonBasisFurther.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AffineBernstein.bilinearOfMatrix_reconstruct line 18
2. lemma OAI.AffineBernstein.bilinearOfMatrix_change line 33
3. lemma OAI.AffineBernstein.basisHessian_change line 47
4. lemma OAI.AffineBernstein.supportNewtonTensor_change line 53
5. theorem OAI.AffineBernstein.supportNewtonTensor_eq_tangential_cofactor line 63

   Source comment

   In every orthonormal frame adapted to the unit normal, the global tensor is EXACTLY the cofactor of the tangential ambient Hessian. The empty tangential block causes no exception.

   theorem supportNewtonTensor_eq_tangential_cofactor
       (b c : OrthonormalBasis (ι ⊕ Unit) ℝ E) {H : E → ℝ} {e : E}
       (hH : ContDiffAt ℝ ∞ H e) (hc : c (Sum.inr ()) = e)
       (hr : ∀ v, fderiv ℝ (fderiv ℝ H) e v e = 0) (i j : ι) :
       supportNewtonTensor b H e (c (Sum.inl i)) (c (Sum.inl j)) =
         (Matrix.of fun l m : ι => fderiv ℝ (fderiv ℝ H) e
           (c (Sum.inl l)) (c (Sum.inl m))).adjugate i j := by
   …

   Mentions: OAI.AffineBernstein.supportNewtonTensor