OAI/Analysis/AffineBernstein/NewtonTensor.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.AffineBernstein.newtonTensor line 15

   Source comment

   The penultimate Newton tensor, defined polynomially, not using an inverse.

   def newtonTensor (A : Matrix ι ι ℝ) : Matrix ι ι ℝ := fun i j =>
   …

2. theorem OAI.AffineBernstein.contDiff_newtonTensor_entry line 19
3. theorem OAI.AffineBernstein.newtonTensor_eq_deriv line 23
4. theorem OAI.AffineBernstein.newtonTensor_isSymm line 45