OAI/NumberTheory/Ostmann/Arithmetic/HistoryHeightBudgetFixed.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Ostmann.Arithmetic.HistoryHeightBudgetFixed.product_fixedBound line 12
  2. theorem OAI.Ostmann.Arithmetic.HistoryHeightBudgetFixed.product_ofFn_fixedBound line 20
  3. theorem OAI.Ostmann.Arithmetic.HistoryHeightBudgetFixed.pivot_fixedBound line 27
  4. def OAI.Ostmann.Arithmetic.HistoryHeightBudgetFixed.StateFixedBound line 40
  5. theorem OAI.Ostmann.Arithmetic.HistoryHeightBudgetFixed.append_fixedBound line 43
  6. theorem OAI.Ostmann.Arithmetic.HistoryHeightBudgetFixed.child_fixedBound line 56
  7. def OAI.Ostmann.Arithmetic.HistoryHeightBudgetFixed.TreeFixedBound line 76
  8. theorem OAI.Ostmann.Arithmetic.HistoryHeightBudgetFixed.root_frequency_mem line 81
  9. theorem OAI.Ostmann.Arithmetic.HistoryHeightBudgetFixed.encode_fixedBound line 84
  10. def OAI.Ostmann.Arithmetic.HistoryHeightBudgetFixed.frequencyBound line 104
  11. theorem OAI.Ostmann.Arithmetic.HistoryHeightBudgetFixed.one_le_frequencyBound line 107
  12. theorem OAI.Ostmann.Arithmetic.HistoryHeightBudgetFixed.supported_frequencyBound line 109
  13. theorem OAI.Ostmann.Arithmetic.HistoryHeightBudgetFixed.symbolicHistory_fixedBound line 121
  14. theorem OAI.Ostmann.Arithmetic.HistoryHeightBudgetFixed.coefficientHistory_fixedBound line 129