OAI/Analysis/AffineBernstein/ConstantDetCalculus.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.AffineBernstein.matrixDirDeriv line 19

    Source documentation

    Entrywise derivative of a genuine smooth matrix field.

    def matrixDirDeriv {n m : ℕ} (v : Space n) (A : Space n → Matrix (Fin m) (Fin m) ℝ)
    (x : Space n) : Matrix (Fin m) (Fin m) ℝ := fun i j => dirDeriv v (fun y => A y i j) x

    Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.dirDeriv

  2. lemma OAI.AffineBernstein.dirDeriv_matrix_mul line 22
  3. lemma OAI.AffineBernstein.dirDeriv_matrix_trace line 32
  4. lemma OAI.AffineBernstein.contDiff_inverseHessian_entry line 37
  5. lemma OAI.AffineBernstein.contDiff_hessian_entry_global line 46
  6. lemma OAI.AffineBernstein.matrixDirDeriv_inverseHessian line 51
  7. lemma OAI.AffineBernstein.hessian_dirDeriv_vector line 71
  8. lemma OAI.AffineBernstein.hessian_dirDeriv_twice line 76
  9. lemma OAI.AffineBernstein.constant_det_trace_diff_zero line 81
  10. lemma OAI.AffineBernstein.constant_det_directional_equation line 95
  11. lemma OAI.AffineBernstein.directional_second_gradient line 123