OAI/NumberTheory/Ostmann/Characters/HistoryFrequencyBudgetBasic.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Ostmann.Characters.HistoryFrequencyBudget.exponent line 9
  2. def OAI.Ostmann.Characters.HistoryFrequencyBudget.bound line 12
  3. def OAI.Ostmann.Characters.HistoryFrequencyBudget.signedRange line 14
  4. def OAI.Ostmann.Characters.HistoryFrequencyBudget.ranges line 16
  5. theorem OAI.Ostmann.Characters.HistoryFrequencyBudget.mem_signedRange line 19
  6. theorem OAI.Ostmann.Characters.HistoryFrequencyBudget.signedRange_card line 32
  7. theorem OAI.Ostmann.Characters.HistoryFrequencyBudget.exponent_nonneg line 37
  8. theorem OAI.Ostmann.Characters.HistoryFrequencyBudget.bound_pos line 40
  9. theorem OAI.Ostmann.Characters.HistoryFrequencyBudget.bound_le_exp line 45
  10. def OAI.Ostmann.Characters.HistoryFrequencyBudget.linearEnvelope line 48
  11. theorem OAI.Ostmann.Characters.HistoryFrequencyBudget.linearEnvelope_pos line 50
  12. theorem OAI.Ostmann.Characters.HistoryFrequencyBudget.exponent_le_linear line 53
  13. theorem OAI.Ostmann.Characters.HistoryFrequencyBudget.budget_exp_bound line 63