OAI/Combinatorics/ThinTrees/Continuation/Interior.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

Continuation interior.

  1. lemma OAI.AlgorithmicThinTrees.MetricTests.qform_transpose line 19
  2. lemma OAI.AlgorithmicThinTrees.MetricTests.qform_responseMatrix line 23
  3. lemma OAI.AlgorithmicThinTrees.MetricTests.qform_sum line 28
  4. lemma OAI.AlgorithmicThinTrees.MetricTests.abs_qform_le_entries line 32
  5. lemma OAI.AlgorithmicThinTrees.MetricTests.difference_outer_centered line 55
  6. lemma OAI.AlgorithmicThinTrees.MetricTests.abs_triangle_energy line 61
  7. lemma OAI.AlgorithmicThinTrees.MetricTests.distinctTriple_card_le line 73
  8. lemma OAI.AlgorithmicThinTrees.MetricTests.abs_triangle_sum line 78
  9. lemma OAI.AlgorithmicThinTrees.MetricTests.lowerPencil_hermitian line 97
  10. lemma OAI.AlgorithmicThinTrees.MetricTests.upperPencil_hermitian line 101
  11. lemma OAI.AlgorithmicThinTrees.MetricTests.edgePencil_hermitian line 110
  12. def OAI.AlgorithmicThinTrees.MetricTests.StepFree.Close line 116
  13. lemma OAI.AlgorithmicThinTrees.MetricTests.StepFree.Close.symm line 121
  14. lemma OAI.AlgorithmicThinTrees.MetricTests.StepFree.Close.mono line 124
  15. lemma OAI.AlgorithmicThinTrees.MetricTests.StepFree.Close.qform_bound line 128
  16. lemma OAI.AlgorithmicThinTrees.MetricTests.StepFree.Close.lower_error line 134
  17. lemma OAI.AlgorithmicThinTrees.MetricTests.StepFree.Close.upper_error line 140
  18. lemma OAI.AlgorithmicThinTrees.MetricTests.StepFree.Close.edge_error line 158
  19. lemma OAI.AlgorithmicThinTrees.MetricTests.scaled_inverse_power line 181
  20. lemma OAI.AlgorithmicThinTrees.MetricTests.inverse_power_mono line 192
  21. lemma OAI.AlgorithmicThinTrees.MetricTests.auxiliary_numbers line 198
  22. def OAI.AlgorithmicThinTrees.MetricTests.auxiliaryPoint line 260
  23. lemma OAI.AlgorithmicThinTrees.MetricTests.auxiliaryPoint_matrix line 264
  24. lemma OAI.AlgorithmicThinTrees.MetricTests.connected_size_five line 269
  25. lemma OAI.AlgorithmicThinTrees.MetricTests.baseline_lower line 284
  26. theorem OAI.AlgorithmicThinTrees.MetricTests.auxiliary_cube line 291