OAI/Analysis/KLS/Spectral/BrascampLiebCurvature.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.LeanBlast.KLS.bl_contDiff_gradient line 16
  2. theorem OAI.LeanBlast.KLS.bl_contDiff_hessianMatrix line 20
  3. theorem OAI.LeanBlast.KLS.contDiff_matrix_det line 35
  4. theorem OAI.LeanBlast.KLS.contDiff_matrix_adjugate line 40
  5. theorem OAI.LeanBlast.KLS.contDiff_matrix_inv line 59
  6. theorem OAI.LeanBlast.KLS.steinGamma_self_eq_dotProduct line 66
  7. theorem OAI.LeanBlast.KLS.steinGamma_self_nonneg line 71
  8. theorem OAI.LeanBlast.KLS.contDiff_steinGamma_self line 77
  9. theorem OAI.LeanBlast.KLS.hasCompactSupport_steinGamma_self line 87
  10. theorem OAI.LeanBlast.KLS.sum_standardBasisVector line 94
  11. theorem OAI.LeanBlast.KLS.second_fderiv_eq_hessianMatrix line 99
  12. theorem OAI.LeanBlast.KLS.fderiv_eq_gradient_dotProduct line 110
  13. theorem OAI.LeanBlast.KLS.quadratic_schur_positive line 116