OAI/Combinatorics/UniformKServer/RankSuperadditivity.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.UniformKServer.RankSuperadditivity.Input line 13
  2. def OAI.UniformKServer.RankSuperadditivity.countRank line 20
  3. def OAI.UniformKServer.RankSuperadditivity.rankSum line 23
  4. def OAI.UniformKServer.RankSuperadditivity.hinge line 27
  5. def OAI.UniformKServer.RankSuperadditivity.interpolate line 29
  6. theorem OAI.UniformKServer.RankSuperadditivity.interpolate_cons line 32
  7. theorem OAI.UniformKServer.RankSuperadditivity.finite_convex_interpolation_aux line 36
  8. theorem OAI.UniformKServer.RankSuperadditivity.finite_convex_interpolation line 104
  9. theorem OAI.UniformKServer.RankSuperadditivity.countRank_bounds line 115
  10. theorem OAI.UniformKServer.RankSuperadditivity.countRank_one line 124
  11. theorem OAI.UniformKServer.RankSuperadditivity.indicator_count line 128
  12. theorem OAI.UniformKServer.RankSuperadditivity.indicator_count_real line 136
  13. def OAI.UniformKServer.RankSuperadditivity.deficit line 147
  14. theorem OAI.UniformKServer.RankSuperadditivity.deficit_eq_sum_rank line 150
  15. theorem OAI.UniformKServer.RankSuperadditivity.selected_count_lower line 155
  16. theorem OAI.UniformKServer.RankSuperadditivity.selected_rank_lower line 172
  17. def OAI.UniformKServer.RankSuperadditivity.activeRanks line 180
  18. theorem OAI.UniformKServer.RankSuperadditivity.hinge_selection line 183
  19. theorem OAI.UniformKServer.RankSuperadditivity.hinge_dual line 197
  20. theorem OAI.UniformKServer.RankSuperadditivity.deficit_subadditive line 218
  21. theorem OAI.UniformKServer.RankSuperadditivity.hinge_superadditivity line 232
  22. def OAI.UniformKServer.RankSuperadditivity.mean line 250
  23. def OAI.UniformKServer.RankSuperadditivity.risk line 251
  24. theorem OAI.UniformKServer.RankSuperadditivity.sum_rank_eq line 254
  25. theorem OAI.UniformKServer.RankSuperadditivity.component_bound line 261
  26. theorem OAI.UniformKServer.RankSuperadditivity.mean_parent line 264
  27. theorem OAI.UniformKServer.RankSuperadditivity.risk_hinge_large line 269
  28. theorem OAI.UniformKServer.RankSuperadditivity.risk_hinge_superadditive line 280
  29. theorem OAI.UniformKServer.RankSuperadditivity.risk_congr line 289
  30. theorem OAI.UniformKServer.RankSuperadditivity.risk_add line 297
  31. theorem OAI.UniformKServer.RankSuperadditivity.risk_smul line 302
  32. theorem OAI.UniformKServer.RankSuperadditivity.risk_affine line 307
  33. theorem OAI.UniformKServer.RankSuperadditivity.interpolation_superadditive line 315
  34. theorem OAI.UniformKServer.RankSuperadditivity.rank_superadditivity line 334