OAI/Combinatorics/UniformKServer/Denominators.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Source companion 04, Lemma denominators: the exact logarithmic denominator family and its dimension-free simplex sum estimate. This is required to instantiate the compact proportion tracker, not a new main theorem.

  1. def OAI.UniformKServer.Denominators.regular line 12
  2. def OAI.UniformKServer.Denominators.height line 13
  3. def OAI.UniformKServer.Denominators.marked line 14
  4. def OAI.UniformKServer.Denominators.family line 15
  5. theorem OAI.UniformKServer.Denominators.log_nonneg line 21
  6. theorem OAI.UniformKServer.Denominators.height_ge_one line 26
  7. theorem OAI.UniformKServer.Denominators.regular_pos line 30
  8. theorem OAI.UniformKServer.Denominators.marked_pos line 35
  9. theorem OAI.UniformKServer.Denominators.exp_sq_bound line 43
  10. theorem OAI.UniformKServer.Denominators.regular_scalar line 47
  11. theorem OAI.UniformKServer.Denominators.marked_scalar line 83
  12. theorem OAI.UniformKServer.Denominators.total_ge_one line 100
  13. theorem OAI.UniformKServer.Denominators.regular_simplex line 106
  14. theorem OAI.UniformKServer.Denominators.marked_simplex line 120