OAI/Combinatorics/ThinTrees/Metric/CenteredMatrices.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

Centered matrices.

  1. def OAI.AlgorithmicThinTrees.MetricTests.ones line 17
  2. def OAI.AlgorithmicThinTrees.MetricTests.constantProjection line 19
  3. def OAI.AlgorithmicThinTrees.MetricTests.centering line 22
  4. lemma OAI.AlgorithmicThinTrees.MetricTests.ones_dot line 24
  5. lemma OAI.AlgorithmicThinTrees.MetricTests.constantProjection_psd line 27
  6. lemma OAI.AlgorithmicThinTrees.MetricTests.constantProjection_symmetric line 31
  7. lemma OAI.AlgorithmicThinTrees.MetricTests.centering_symmetric line 34
  8. lemma OAI.AlgorithmicThinTrees.MetricTests.constantProjection_mulVec line 37
  9. lemma OAI.AlgorithmicThinTrees.MetricTests.qform_constantProjection line 42
  10. lemma OAI.AlgorithmicThinTrees.MetricTests.centering_mulVec line 48
  11. lemma OAI.AlgorithmicThinTrees.MetricTests.centering_mulVec_of_sum_zero line 52
  12. lemma OAI.AlgorithmicThinTrees.MetricTests.centering_mulVec_sum line 56
  13. lemma OAI.AlgorithmicThinTrees.MetricTests.constantProjection_ones line 64
  14. lemma OAI.AlgorithmicThinTrees.MetricTests.centering_ones line 69
  15. lemma OAI.AlgorithmicThinTrees.MetricTests.centered_dot line 72
  16. def OAI.AlgorithmicThinTrees.MetricTests.centered line 76
  17. lemma OAI.AlgorithmicThinTrees.MetricTests.centered_psd line 79
  18. lemma OAI.AlgorithmicThinTrees.MetricTests.centered_ones line 83
  19. lemma OAI.AlgorithmicThinTrees.MetricTests.qform_centered line 86
  20. def OAI.AlgorithmicThinTrees.MetricTests.CenteredPositive line 91
  21. def OAI.AlgorithmicThinTrees.MetricTests.regularize line 94
  22. def OAI.AlgorithmicThinTrees.MetricTests.inverseOnZeroSum line 97
  23. lemma OAI.AlgorithmicThinTrees.MetricTests.centered_positive line 100
  24. lemma OAI.AlgorithmicThinTrees.MetricTests.regularize_centered_pd line 107
  25. lemma OAI.AlgorithmicThinTrees.MetricTests.inverseOnZeroSum_solves line 127
  26. lemma OAI.AlgorithmicThinTrees.MetricTests.inverse_centered_le line 143
  27. lemma OAI.AlgorithmicThinTrees.MetricTests.centeredTest_mul_constant line 161
  28. lemma OAI.AlgorithmicThinTrees.MetricTests.centeredTest_constant_mul line 166
  29. lemma OAI.AlgorithmicThinTrees.MetricTests.centeredTest_mul_centering line 172
  30. lemma OAI.AlgorithmicThinTrees.MetricTests.centeredTest_centering_mul line 176
  31. lemma OAI.AlgorithmicThinTrees.MetricTests.centered_trace line 180
  32. lemma OAI.AlgorithmicThinTrees.MetricTests.regularize_trace line 186
  33. lemma OAI.AlgorithmicThinTrees.MetricTests.laplacian_zeroSum_pos line 191
  34. lemma OAI.AlgorithmicThinTrees.MetricTests.laplacian_ones line 215
  35. lemma OAI.AlgorithmicThinTrees.MetricTests.laplacian_centered_positive line 224
  36. lemma OAI.AlgorithmicThinTrees.MetricTests.laplacian_regularize_pd line 228