OAI/Probability/SKGap/Matrix/DiscreteMatrixCalculus.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SKGapCutoff.Primary.derivativeMatrix line 18
  2. def OAI.SKGapCutoff.Primary.ShapeBound line 21
  3. lemma OAI.SKGapCutoff.Primary.opNorm_eq line 24
  4. lemma OAI.SKGapCutoff.Primary.opNorm_le_frobenius line 27
  5. lemma OAI.SKGapCutoff.Primary.opNorm_add line 33
  6. lemma OAI.SKGapCutoff.Primary.opNorm_smul line 37
  7. lemma OAI.SKGapCutoff.Primary.ShapeBound.mono line 40
  8. lemma OAI.SKGapCutoff.Primary.ShapeBound.add line 43
  9. lemma OAI.SKGapCutoff.Primary.shapeBound_of_frobenius line 49
  10. lemma OAI.SKGapCutoff.Primary.ShapeBound.perturb line 53
  11. lemma OAI.SKGapCutoff.Primary.fourth_sum line 57
  12. lemma OAI.SKGapCutoff.Primary.fourth_sum_le line 68
  13. lemma OAI.SKGapCutoff.Primary.quadratic_entry_error line 82
  14. lemma OAI.SKGapCutoff.Primary.diagonal_mul_shape line 100
  15. lemma OAI.SKGapCutoff.Primary.tanh_derivative_error line 132
  16. lemma OAI.SKGapCutoff.Primary.tanh_derivative_shape line 141
  17. def OAI.SKGapCutoff.Primary.derivativeVector line 150
  18. def OAI.SKGapCutoff.Primary.siteMean line 153
  19. lemma OAI.SKGapCutoff.Primary.siteMean_derivative line 155
  20. lemma OAI.SKGapCutoff.Primary.euclidean_ones_norm_sq line 165
  21. lemma OAI.SKGapCutoff.Primary.siteMean_derivative_square line 169
  22. lemma OAI.SKGapCutoff.Primary.siteMean_derivative_square_bound line 184
  23. lemma OAI.SKGapCutoff.Primary.derivative_norm_of_mean_square line 190
  24. lemma OAI.SKGapCutoff.Primary.outer_frobenius_bound line 196
  25. lemma OAI.SKGapCutoff.Primary.spin_diagonal_frobenius line 219
  26. lemma OAI.SKGapCutoff.Primary.derivativeMatrix_product line 225
  27. lemma OAI.SKGapCutoff.Primary.product_derivative_error line 234
  28. lemma OAI.SKGapCutoff.Primary.derivativeMatrix_linear line 257
  29. lemma OAI.SKGapCutoff.Primary.derivativeMatrix_sub line 266
  30. lemma OAI.SKGapCutoff.Primary.derivativeMatrix_smul line 271
  31. lemma OAI.SKGapCutoff.Primary.derivativeMatrix_spin line 277
  32. lemma OAI.SKGapCutoff.Primary.variance_derivative_error line 281
  33. lemma OAI.SKGapCutoff.Primary.variance_derivative_opNorm line 300
  34. lemma OAI.SKGapCutoff.Primary.tanh_derivative_formal_error line 316