OAI/Combinatorics/UniformKServer/AllocationAnalysis.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.UniformKServer.UniformIntegrals.height line 17
  2. def OAI.UniformKServer.UniformIntegrals.regular line 18
  3. def OAI.UniformKServer.UniformIntegrals.marked line 19
  4. theorem OAI.UniformKServer.UniformIntegrals.height_ge_one line 21
  5. theorem OAI.UniformKServer.UniformIntegrals.regular_deriv line 26
  6. theorem OAI.UniformKServer.UniformIntegrals.regular_tendsto line 32
  7. theorem OAI.UniformKServer.UniformIntegrals.regular_integrable line 36
  8. theorem OAI.UniformKServer.UniformIntegrals.regular_integral line 43
  9. theorem OAI.UniformKServer.UniformIntegrals.marked_pos line 50
  10. theorem OAI.UniformKServer.UniformIntegrals.marked_local line 55
  11. theorem OAI.UniformKServer.UniformIntegrals.tail_deriv line 62
  12. theorem OAI.UniformKServer.UniformIntegrals.tail_tendsto line 66
  13. theorem OAI.UniformKServer.UniformIntegrals.tail_integrable line 69
  14. theorem OAI.UniformKServer.UniformIntegrals.tail_integral line 72
  15. theorem OAI.UniformKServer.UniformIntegrals.marked_tail_bound line 75
  16. theorem OAI.UniformKServer.UniformIntegrals.marked_tail line 84
  17. theorem OAI.UniformKServer.UniformIntegrals.marked_integrable line 95
  18. theorem OAI.UniformKServer.UniformIntegrals.linear_local line 111
  19. theorem OAI.UniformKServer.UniformIntegrals.linear_integral line 120
  20. theorem OAI.UniformKServer.UniformIntegrals.log_bound line 135
  21. theorem OAI.UniformKServer.UniformIntegrals.marked_local_integral line 145
  22. theorem OAI.UniformKServer.UniformIntegrals.marked_tail_integral line 162
  23. theorem OAI.UniformKServer.UniformIntegrals.marked_integral_uniform line 171
  24. theorem OAI.UniformKServer.AlphaBounds.logarithmic_substitution line 198
  25. theorem OAI.UniformKServer.AlphaBounds.weighted_integral_positive line 225
  26. theorem OAI.UniformKServer.AlphaBounds.weighted_integral_closed line 237
  27. theorem OAI.UniformKServer.AlphaBounds.weight_continuous line 247
  28. theorem OAI.UniformKServer.AlphaBounds.regular_weight line 256
  29. theorem OAI.UniformKServer.AlphaBounds.marked_weight line 281
  30. theorem OAI.UniformKServer.AlphaBounds.regular_weight_integrable line 292
  31. theorem OAI.UniformKServer.AlphaBounds.marked_weight_integrable line 299
  32. theorem OAI.UniformKServer.AlphaBounds.regular_ge_one line 305
  33. theorem OAI.UniformKServer.AlphaBounds.regular_component line 313
  34. theorem OAI.UniformKServer.AlphaBounds.marked_component line 350