OAI/Combinatorics/ThinTrees/Normalization/Algorithm.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

Normalization algorithm.

  1. def OAI.AlgorithmicThinTrees.Normalization.realColumns line 16
  2. def OAI.AlgorithmicThinTrees.Normalization.weights line 17
  3. def OAI.AlgorithmicThinTrees.Normalization.realWeights line 18
  4. def OAI.AlgorithmicThinTrees.Normalization.decrement line 20
  5. def OAI.AlgorithmicThinTrees.Normalization.threshold line 21
  6. def OAI.AlgorithmicThinTrees.Normalization.testMatrix line 23
  7. def OAI.AlgorithmicThinTrees.Normalization.heavy line 27
  8. def OAI.AlgorithmicThinTrees.Normalization.advance line 31
  9. def OAI.AlgorithmicThinTrees.Normalization.scalesAt line 35
  10. lemma OAI.AlgorithmicThinTrees.Normalization.scalesAt_zero line 38
  11. lemma OAI.AlgorithmicThinTrees.Normalization.realWeights_one line 41
  12. lemma OAI.AlgorithmicThinTrees.Normalization.testMatrix_symm line 45
  13. lemma OAI.AlgorithmicThinTrees.Normalization.testMatrix_cast line 51
  14. lemma OAI.AlgorithmicThinTrees.Normalization.heavy_none line 61
  15. lemma OAI.AlgorithmicThinTrees.Normalization.heavy_some line 74
  16. lemma OAI.AlgorithmicThinTrees.Normalization.update_realWeights line 85
  17. lemma OAI.AlgorithmicThinTrees.Normalization.advance_box line 94
  18. lemma OAI.AlgorithmicThinTrees.Normalization.scalesAt_box line 109
  19. lemma OAI.AlgorithmicThinTrees.Normalization.realWeights_box line 119
  20. lemma OAI.AlgorithmicThinTrees.Normalization.scalesAt_terminates line 126
  21. lemma OAI.AlgorithmicThinTrees.Normalization.scalesAt_parts line 180
  22. def OAI.AlgorithmicThinTrees.Normalization.multiplier line 200
  23. def OAI.AlgorithmicThinTrees.Normalization.normalizationLength line 201
  24. def OAI.AlgorithmicThinTrees.Normalization.normalizedScales line 202