OAI/Probability/SKGap/Localization/DiagonalHessianJoined.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SKGap.sqrt_half_holder line 13
  2. def OAI.SKGap.diagonalRoot line 25
  3. def OAI.SKGap.diagonalHessian line 26
  4. lemma OAI.SKGap.diagonalRoot_norm line 29
  5. lemma OAI.SKGap.diagonalRoot_half_holder line 35
  6. theorem OAI.SKGap.diagonalHessian_half_holder line 42
  7. lemma OAI.SKGap.diagonalHessian_hermitian line 66
  8. lemma OAI.SKGap.matrix_quadratic_op_bound line 73
  9. theorem OAI.SKGap.hermitian_margin_transfer line 90
  10. def OAI.SKGap.empiricalConditionalMiddle line 115
  11. lemma OAI.SKGap.empirical_columns_one line 128
  12. lemma OAI.SKGap.empirical_columns_two line 136
  13. lemma OAI.SKGap.empirical_columns_matrix line 141
  14. lemma OAI.SKGap.pathDiagonal_one_eq_sqrt line 153
  15. lemma OAI.SKGap.pathDiagonal_sq line 156
  16. theorem OAI.SKGap.conditionalEmpiricalCore_eq_hessian line 163