OAI/Analysis/AffineBernstein/NewtonPiola.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AffineBernstein.fderiv_piMatrix_entry line 15
2. lemma OAI.AffineBernstein.adjugate_linear_piola line 21
3. lemma OAI.AffineBernstein.piMatrix_shift_hasDerivAt line 30
4. lemma OAI.AffineBernstein.newton_linear_piola line 42

   Source comment

   The linearized Piola cancellation is the divergence identity for the penultimate Newton tensor.

   lemma newton_linear_piola (A : ι → ι → ℝ) (V : ι → ι → ι → ℝ)
       (hV : ∀ l j m, V j l m = V m l j) (i : ι) :
       (∑ j, fderiv ℝ (fderiv ℝ (fun B : ι → ι → ℝ => (Matrix.of B).adjugate j i)) A
         (V j) (fun l m => (1 : Matrix ι ι ℝ) l m)) = 0 := by
   …