OAI/Combinatorics/ThinTrees/Metric/ConeRepresentation.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

Metric cone representation.

  1. def OAI.AlgorithmicThinTrees.MetricTests.coneImage line 19
  2. lemma OAI.AlgorithmicThinTrees.MetricTests.continuous_trace line 23
  3. lemma OAI.AlgorithmicThinTrees.MetricTests.psd_trace_compact line 26
  4. lemma OAI.AlgorithmicThinTrees.MetricTests.coneImage_trace_bound line 40
  5. lemma OAI.AlgorithmicThinTrees.MetricTests.coneImage_closed line 53
  6. lemma OAI.AlgorithmicThinTrees.MetricTests.coneImage_zero line 82
  7. lemma OAI.AlgorithmicThinTrees.MetricTests.coneImage_add line 85
  8. lemma OAI.AlgorithmicThinTrees.MetricTests.coneImage_smul line 94
  9. def OAI.AlgorithmicThinTrees.MetricTests.representedCone line 101
  10. lemma OAI.AlgorithmicThinTrees.MetricTests.psd_mem_coneImage line 109
  11. lemma OAI.AlgorithmicThinTrees.MetricTests.generator_mem_coneImage line 113
  12. def OAI.AlgorithmicThinTrees.MetricTests.linearTraceMatrix line 125
  13. lemma OAI.AlgorithmicThinTrees.MetricTests.linearTraceMatrix_pairing line 128
  14. lemma OAI.AlgorithmicThinTrees.MetricTests.trace_pairing_transpose_right line 142
  15. def OAI.AlgorithmicThinTrees.MetricTests.symmetricTraceMatrix line 148
  16. lemma OAI.AlgorithmicThinTrees.MetricTests.symmetricTraceMatrix_hermitian line 151
  17. lemma OAI.AlgorithmicThinTrees.MetricTests.symmetricTraceMatrix_pairing line 157
  18. lemma OAI.AlgorithmicThinTrees.MetricTests.symmetricTraceMatrix_psd line 165
  19. abbrev OAI.AlgorithmicThinTrees.MetricTests.DistinctTriple line 174
  20. def OAI.AlgorithmicThinTrees.MetricTests.triangleMatrix line 177
  21. def OAI.AlgorithmicThinTrees.MetricTests.triangleGenerator line 182
  22. lemma OAI.AlgorithmicThinTrees.MetricTests.triangleMatrix_hermitian line 185
  23. lemma OAI.AlgorithmicThinTrees.MetricTests.difference_norm_sq line 189
  24. lemma OAI.AlgorithmicThinTrees.MetricTests.triangleGenerator_trace line 193
  25. lemma OAI.AlgorithmicThinTrees.MetricTests.triangleMatrix_ones line 199
  26. lemma OAI.AlgorithmicThinTrees.MetricTests.triangleMatrix_pairing line 204
  27. lemma OAI.AlgorithmicThinTrees.MetricTests.test_iff_generators line 209
  28. theorem OAI.AlgorithmicThinTrees.MetricTests.metric_dual_representation line 226
  29. lemma OAI.AlgorithmicThinTrees.MetricTests.trace_centered_right line 253
  30. theorem OAI.AlgorithmicThinTrees.MetricTests.centered_metric_dual_representation line 263
  31. theorem OAI.AlgorithmicThinTrees.MetricTests.metricDomain_iff_lmi line 282
  32. lemma OAI.AlgorithmicThinTrees.MetricTests.laplacian_trace line 306
  33. lemma OAI.AlgorithmicThinTrees.MetricTests.domain_trace_size line 312
  34. lemma OAI.AlgorithmicThinTrees.MetricTests.domain_multiplier_bound line 318