OAI/Combinatorics/ThinTrees/Metric/MatrixBound.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Metric matrix bound.

  1. def OAI.AlgorithmicThinTrees.MetricTests.difference line 17
  2. def OAI.AlgorithmicThinTrees.MetricTests.Test line 19
  3. def OAI.AlgorithmicThinTrees.MetricTests.CenteredTest line 23
  4. lemma OAI.AlgorithmicThinTrees.MetricTests.test_zero line 26
  5. lemma OAI.AlgorithmicThinTrees.MetricTests.test_add line 31
  6. lemma OAI.AlgorithmicThinTrees.MetricTests.test_smul line 38
  7. lemma OAI.AlgorithmicThinTrees.MetricTests.test_sum line 44
  8. lemma OAI.AlgorithmicThinTrees.MetricTests.test_convex line 52
  9. lemma OAI.AlgorithmicThinTrees.MetricTests.test_closed line 56
  10. def OAI.AlgorithmicThinTrees.MetricTests.columnPoints line 61
  11. lemma OAI.AlgorithmicThinTrees.MetricTests.eval_difference line 64
  12. lemma OAI.AlgorithmicThinTrees.MetricTests.gram_distance line 68
  13. lemma OAI.AlgorithmicThinTrees.MetricTests.sqrt_gram line 80
  14. lemma OAI.AlgorithmicThinTrees.MetricTests.sqrt_columns_metric line 85
  15. lemma OAI.AlgorithmicThinTrees.MetricTests.contraction line 90
  16. lemma OAI.AlgorithmicThinTrees.MetricTests.laplacian_pairing line 103
  17. lemma OAI.AlgorithmicThinTrees.MetricTests.column_edge_energy line 107
  18. theorem OAI.AlgorithmicThinTrees.MetricTests.polynomial_nuclear_bound line 115