OAI/Combinatorics/ThinTrees/Sparsification/GraphicHalf.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Graphic half.

  1. def OAI.AlgorithmicThinTrees.GraphicHalf.fullColumns line 16
  2. lemma OAI.AlgorithmicThinTrees.GraphicHalf.fullColumns_cast line 19
  3. lemma OAI.AlgorithmicThinTrees.GraphicHalf.fullColumns_gram line 26
  4. def OAI.AlgorithmicThinTrees.GraphicHalf.positiveForm line 36
  5. lemma OAI.AlgorithmicThinTrees.GraphicHalf.positiveForm_cast line 39
  6. def OAI.AlgorithmicThinTrees.GraphicHalf.scaledColumns line 45
  7. def OAI.AlgorithmicThinTrees.GraphicHalf.scaledForm line 48
  8. lemma OAI.AlgorithmicThinTrees.GraphicHalf.scaledColumns_cast line 51
  9. lemma OAI.AlgorithmicThinTrees.GraphicHalf.scaledForm_cast line 57
  10. lemma OAI.AlgorithmicThinTrees.GraphicHalf.scaledColumns_gram line 64
  11. lemma OAI.AlgorithmicThinTrees.GraphicHalf.scaledColumns_zero line 75
  12. lemma OAI.AlgorithmicThinTrees.GraphicHalf.scaledColumns_leverage line 79
  13. def OAI.AlgorithmicThinTrees.GraphicHalf.halfEdges line 88
  14. lemma OAI.AlgorithmicThinTrees.GraphicHalf.laplacian_mono line 93
  15. lemma OAI.AlgorithmicThinTrees.GraphicHalf.fullColumns_covariance line 99
  16. theorem OAI.AlgorithmicThinTrees.GraphicHalf.half_bounds line 107