OAI/Combinatorics/ThinTrees/Continuation/SpectralSize.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Spectral size.

  1. lemma OAI.AlgorithmicThinTrees.MetricTests.laplacian_centered_energy line 17
  2. lemma OAI.AlgorithmicThinTrees.MetricTests.range_le_edge_variation line 21
  3. theorem OAI.AlgorithmicThinTrees.MetricTests.laplacian_poincare line 31
  4. def OAI.AlgorithmicThinTrees.MetricTests.graphSize line 64
  5. lemma OAI.AlgorithmicThinTrees.MetricTests.graphSize_pos line 66
  6. lemma OAI.AlgorithmicThinTrees.MetricTests.vertex_edge_le_size_cube line 70
  7. theorem OAI.AlgorithmicThinTrees.MetricTests.laplacian_spectral_gap line 82
  8. lemma OAI.AlgorithmicThinTrees.MetricTests.qform_one_sum_sq line 92
  9. lemma OAI.AlgorithmicThinTrees.MetricTests.centering_idempotent line 96
  10. lemma OAI.AlgorithmicThinTrees.MetricTests.qform_centering_sum_sq line 99
  11. lemma OAI.AlgorithmicThinTrees.MetricTests.centering_psd line 104
  12. theorem OAI.AlgorithmicThinTrees.MetricTests.laplacian_lower_order line 108
  13. lemma OAI.AlgorithmicThinTrees.MetricTests.qform_outer line 121
  14. lemma OAI.AlgorithmicThinTrees.MetricTests.qform_outer_le line 125
  15. lemma OAI.AlgorithmicThinTrees.MetricTests.difference_outer_le line 129
  16. theorem OAI.AlgorithmicThinTrees.MetricTests.laplacian_upper_energy line 133
  17. theorem OAI.AlgorithmicThinTrees.MetricTests.laplacian_upper_order line 145