OAI/Probability/SKRatio/Quantization/BinCoefficients.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SKRatio.Bins.matrixInner line 12
  2. lemma OAI.SKRatio.Bins.matrixInner_symm line 14
  3. lemma OAI.SKRatio.Bins.matrixInner_add_left line 17
  4. lemma OAI.SKRatio.Bins.matrixInner_add_right line 21
  5. lemma OAI.SKRatio.Bins.matrixInner_transpose line 25
  6. lemma OAI.SKRatio.Bins.matrixInner_transpose_left line 30
  7. lemma OAI.SKRatio.Bins.matrixInner_sq_sub line 34
  8. def OAI.SKRatio.Bins.linearMatrix line 43
  9. def OAI.SKRatio.Bins.quadraticMatrix line 46
  10. def OAI.SKRatio.Bins.binVariance line 49
  11. lemma OAI.SKRatio.Bins.binVariance_nonneg line 53
  12. lemma OAI.SKRatio.Bins.linearMatrix_inner line 56
  13. lemma OAI.SKRatio.Bins.linearMatrix_cross_zero line 65
  14. lemma OAI.SKRatio.Bins.quadraticMatrix_transpose line 78
  15. lemma OAI.SKRatio.Bins.linear_quadratic_inner_zero line 84
  16. lemma OAI.SKRatio.Bins.quadraticMatrix_inner line 95
  17. def OAI.SKRatio.Bins.residualMatrix line 110
  18. lemma OAI.SKRatio.Bins.residualMatrix_inner line 113
  19. lemma OAI.SKRatio.Bins.residualMatrix_increment line 129