OAI/Combinatorics/UniformKServer/RankFunctions.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.UniformKServer.RankFunctions.pstar line 13
  2. def OAI.UniformKServer.RankFunctions.sstar line 14
  3. def OAI.UniformKServer.RankFunctions.rank line 15
  4. def OAI.UniformKServer.RankFunctions.gap line 21
  5. def OAI.UniformKServer.RankFunctions.allowed line 26
  6. def OAI.UniformKServer.RankFunctions.A line 28
  7. def OAI.UniformKServer.RankFunctions.B line 29
  8. def OAI.UniformKServer.RankFunctions.h line 30
  9. def OAI.UniformKServer.RankFunctions.middle line 31
  10. theorem OAI.UniformKServer.RankFunctions.coeff_bounds line 33
  11. theorem OAI.UniformKServer.RankFunctions.h_nonneg line 48
  12. theorem OAI.UniformKServer.RankFunctions.h_antitone line 49
  13. theorem OAI.UniformKServer.RankFunctions.h_diff line 53
  14. theorem OAI.UniformKServer.RankFunctions.h_bound line 63
  15. theorem OAI.UniformKServer.RankFunctions.middle_match line 67
  16. theorem OAI.UniformKServer.RankFunctions.rank_middle line 71
  17. theorem OAI.UniformKServer.RankFunctions.middle_antitone line 87
  18. theorem OAI.UniformKServer.RankFunctions.middle_drop line 99
  19. theorem OAI.UniformKServer.RankFunctions.h_convex line 127
  20. theorem OAI.UniformKServer.RankFunctions.middle_convex line 135
  21. theorem OAI.UniformKServer.RankFunctions.rank_convex line 143
  22. theorem OAI.UniformKServer.RankFunctions.rank_antitone line 182
  23. theorem OAI.UniformKServer.RankFunctions.rank_zero line 197
  24. theorem OAI.UniformKServer.RankFunctions.rank_cutoff line 198
  25. theorem OAI.UniformKServer.RankFunctions.rank_beyond line 199
  26. theorem OAI.UniformKServer.RankFunctions.rank_nonneg line 203
  27. theorem OAI.UniformKServer.RankFunctions.rank_le_one line 217
  28. theorem OAI.UniformKServer.RankFunctions.rank_positive line 220
  29. theorem OAI.UniformKServer.RankFunctions.rank_affine line 234
  30. theorem OAI.UniformKServer.RankFunctions.gap_nonneg line 238
  31. theorem OAI.UniformKServer.RankFunctions.rank_parameter_antitone line 246
  32. theorem OAI.UniformKServer.RankFunctions.gap_comparison line 251
  33. theorem OAI.UniformKServer.RankFunctions.sqrt_diff_aux line 279
  34. theorem OAI.UniformKServer.RankFunctions.left_bound line 289
  35. theorem OAI.UniformKServer.RankFunctions.sqrt_left line 296
  36. theorem OAI.UniformKServer.RankFunctions.coeff_at line 314
  37. theorem OAI.UniformKServer.RankFunctions.sqrt_middle_eq line 321
  38. theorem OAI.UniformKServer.RankFunctions.sqrt_middle_ordered line 326
  39. theorem OAI.UniformKServer.RankFunctions.sqrt_rank_lipschitz line 365
  40. theorem OAI.UniformKServer.RankFunctions.rank_properties line 384