OAI/Combinatorics/UniformKServer/DyadicTiers.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

The source's dyadic tiers, including the minimal last tier and the sharp prefix/unqualified sums. These coefficients are summed before summing scales.

  1. def OAI.UniformKServer.DyadicTiers.value line 16
  2. theorem OAI.UniformKServer.DyadicTiers.one_le_value line 18
  3. theorem OAI.UniformKServer.DyadicTiers.value_pos line 19
  4. theorem OAI.UniformKServer.DyadicTiers.unbounded line 21
  5. def OAI.UniformKServer.DyadicTiers.last line 28
  6. theorem OAI.UniformKServer.DyadicTiers.last_ge line 30
  7. theorem OAI.UniformKServer.DyadicTiers.before_last line 32
  8. theorem OAI.UniformKServer.DyadicTiers.last_mono line 35
  9. theorem OAI.UniformKServer.DyadicTiers.last_bound line 38
  10. theorem OAI.UniformKServer.DyadicTiers.sum_exact line 46
  11. theorem OAI.UniformKServer.DyadicTiers.prefix_sum line 51
  12. theorem OAI.UniformKServer.DyadicTiers.value_mono line 57
  13. theorem OAI.UniformKServer.DyadicTiers.unqualified_sum line 61
  14. theorem OAI.UniformKServer.DyadicTiers.inverse_cutoff line 78
  15. theorem OAI.UniformKServer.DyadicTiers.inverse_sum line 89
  16. theorem OAI.UniformKServer.DyadicTiers.exponential_sum line 93