OAI/Analysis/AffineBernstein/DirectionalJacobi.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AffineBernstein.constant_det_directional_jacobi line 18
2. lemma OAI.AffineBernstein.inverseHessianTrace_expMul line 50
3. lemma OAI.AffineBernstein.inverseHessianPair_log_positive line 61
4. lemma OAI.AffineBernstein.inverseHessianTrace_log_positive line 73
5. def OAI.AffineBernstein.inverseNthRoot line 99

   Source documentation

   A convenient exact representation of the reciprocal n-th root, always used on a strictly positive directional Hessian.

   def inverseNthRoot (n : ℕ) (f : Space n → ℝ) (x : Space n) : ℝ :=
   …

   Mentions: OAI.AffineBernstein.Space

6. lemma OAI.AffineBernstein.inverseNthRoot_pos line 102
7. lemma OAI.AffineBernstein.contDiff_inverseNthRoot line 105
8. lemma OAI.AffineBernstein.inverseNthRoot_pow line 109
9. lemma OAI.AffineBernstein.inverseNthRoot_supersolution_of_jacobi line 116
10. lemma OAI.AffineBernstein.constant_det_directional_inverse_root_supersolution line 134