OAI/Combinatorics/ThinTrees/Continuation/CenteredDomain.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

Centered domain.

  1. lemma OAI.AlgorithmicThinTrees.MetricTests.mul_constant_of_ones line 17
  2. lemma OAI.AlgorithmicThinTrees.MetricTests.constant_mul_of_ones line 21
  3. lemma OAI.AlgorithmicThinTrees.MetricTests.mul_centering_of_ones line 27
  4. lemma OAI.AlgorithmicThinTrees.MetricTests.centering_mul_of_ones line 31
  5. lemma OAI.AlgorithmicThinTrees.MetricTests.centered_eq line 35
  6. lemma OAI.AlgorithmicThinTrees.MetricTests.centeredPositive_psd line 39
  7. lemma OAI.AlgorithmicThinTrees.MetricTests.regularize_pd line 49
  8. lemma OAI.AlgorithmicThinTrees.MetricTests.centeredPositive_add_psd line 69
  9. lemma OAI.AlgorithmicThinTrees.MetricTests.centered_rankOne line 78
  10. lemma OAI.AlgorithmicThinTrees.MetricTests.centered_regularize line 84
  11. lemma OAI.AlgorithmicThinTrees.MetricTests.centered_resistance_nonneg line 91
  12. lemma OAI.AlgorithmicThinTrees.MetricTests.centered_inverse_antitone line 95
  13. lemma OAI.AlgorithmicThinTrees.MetricTests.centered_resistance_order line 103
  14. def OAI.AlgorithmicThinTrees.MetricTests.metricDomain line 137
  15. lemma OAI.AlgorithmicThinTrees.MetricTests.laplacian_mem_domain line 141
  16. lemma OAI.AlgorithmicThinTrees.MetricTests.domain_psd line 147
  17. lemma OAI.AlgorithmicThinTrees.MetricTests.domain_positive line 151
  18. lemma OAI.AlgorithmicThinTrees.MetricTests.domain_closed line 157
  19. lemma OAI.AlgorithmicThinTrees.MetricTests.domain_convex line 170
  20. lemma OAI.AlgorithmicThinTrees.MetricTests.difference_sum line 189
  21. lemma OAI.AlgorithmicThinTrees.MetricTests.test_centered line 192
  22. lemma OAI.AlgorithmicThinTrees.MetricTests.centered_one line 198
  23. lemma OAI.AlgorithmicThinTrees.MetricTests.centering_test line 201
  24. lemma OAI.AlgorithmicThinTrees.MetricTests.domain_trace_bound line 204
  25. lemma OAI.AlgorithmicThinTrees.MetricTests.domain_bounded line 209
  26. lemma OAI.AlgorithmicThinTrees.MetricTests.domain_compact line 223
  27. lemma OAI.AlgorithmicThinTrees.MetricTests.shortcut_add_mem_domain line 226