OAI/Analysis/AffineBernstein/CofactorCodazzi.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.AffineBernstein.fderiv_adjugate_entries line 14
2. theorem OAI.AffineBernstein.cofactor_divergence_of_codazzi line 51

   Source comment

   Cofactor divergence vanishes for every differentiable Codazzi matrix field, including size one and the empty angular block. No invertibility is required.

   theorem cofactor_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 => (M y).adjugate j i) x (e j)) = 0 := by
   …