OAI/Analysis/AffineBernstein/NewtonField.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.AffineBernstein.fderiv_newtonTensor_entry line 15
2. theorem OAI.AffineBernstein.newtonTensor_divergence_of_codazzi line 34

   Source comment

   Newton divergence for a genuine differentiable Codazzi field in constant coordinates. Its sole tensor hypothesis is the third derivative symmetry.

   theorem newtonTensor_divergence_of_codazzi (M : E → Matrix ι ι ℝ) (x : E) (e : ι → E)
       (hM : ∀ l m, DifferentiableAt ℝ (fun y => M y l m) x)
       (hCodazzi : ∀ l j m, fderiv ℝ (fun y => M y l m) x (e j) =
         fderiv ℝ (fun y => M y l j) x (e m)) (i : ι) :
       (∑ j, fderiv ℝ (fun y => newtonTensor (M y) j i) x (e j)) = 0 := by
   …

   Mentions: OAI.AffineBernstein.newtonTensor