OAI/NumberTheory/Ostmann/Arithmetic/FrequencyTreeNodes.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Preorder frequency data and its exact product of split costs

  1. def OAI.Ostmann.pairedNodeFrequencies line 13
  2. theorem OAI.Ostmann.pairedNodeFrequencies_bound line 17
  3. def OAI.Ostmann.frequencySplitList line 23
  4. theorem OAI.Ostmann.frequencySplitList_length line 29
  5. def OAI.Ostmann.frequencyLeafWeight line 39
  6. theorem OAI.Ostmann.frequencyLeafWeight_nonneg line 44
  7. theorem OAI.Ostmann.frequencyTreeWeight_eq_splitList line 50
  8. theorem OAI.Ostmann.prod_range_list_getD line 63
  9. def OAI.Ostmann.emptyNodeFrequencies line 73
  10. def OAI.Ostmann.treeNodeFrequencies line 75
  11. theorem OAI.Ostmann.pairedNodeFrequencies_moduli_bounds line 79
  12. theorem OAI.Ostmann.frequencySplitList_moduli_bounds line 91
  13. theorem OAI.Ostmann.treeNodeFrequencies_divisor_bound line 104