OAI/Probability/SKRatio/Calculus/Curvature.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SKRatio.Fields.symmetric_row_cost line 15
  2. lemma OAI.SKRatio.Fields.symmetric_row_quadratic line 37
  3. lemma OAI.SKRatio.Fields.quadratic_le_euclideanOpNorm line 51
  4. theorem OAI.SKRatio.Fields.gibbs_cubic_curvature line 71
  5. lemma OAI.SKRatio.Fields.signed_forms_le line 114
  6. theorem OAI.SKRatio.Fields.all_fields_poincare line 154
  7. lemma OAI.SKRatio.Fields.symmetric_abs_row_quad line 169
  8. lemma OAI.SKRatio.Fields.euclideanOpNorm_le_abs_row line 180
  9. lemma OAI.SKRatio.Fields.cubic_row_bound line 209
  10. lemma OAI.SKRatio.Fields.tanh_euclideanOpNorm line 222
  11. lemma OAI.SKRatio.Fields.tanh_square_row line 247
  12. theorem OAI.SKRatio.Fields.poincare_of_matrix_bounds line 254