OAI/Combinatorics/ThinTrees/Sparsification/GraphicNormalization.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Graphic normalization.

  1. def OAI.AlgorithmicThinTrees.Normalization.dropRoot line 15
  2. def OAI.AlgorithmicThinTrees.Normalization.integerColumns line 32
  3. def OAI.AlgorithmicThinTrees.Normalization.graphColumns line 35
  4. lemma OAI.AlgorithmicThinTrees.Normalization.graphColumns_cast line 38
  5. lemma OAI.AlgorithmicThinTrees.Normalization.graphColumns_norm line 50
  6. lemma OAI.AlgorithmicThinTrees.Normalization.integral_det_bound line 63
  7. lemma OAI.AlgorithmicThinTrees.Normalization.integral_containedPacking line 79
  8. lemma OAI.AlgorithmicThinTrees.Normalization.graph_containedPacking line 103
  9. theorem OAI.AlgorithmicThinTrees.Normalization.graphic_normalization line 132