OAI/Combinatorics/ListHadwiger/Fractional.lean

GitHub source file

59 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LinearListHadwiger.Fractional.Stable line 9
  2. lemma OAI.LinearListHadwiger.Fractional.Stable.mono line 12
  3. lemma OAI.LinearListHadwiger.Fractional.stable_empty line 15
  4. lemma OAI.LinearListHadwiger.Fractional.stable_singleton line 16
  5. def OAI.LinearListHadwiger.Fractional.Cover line 19
  6. def OAI.LinearListHadwiger.Fractional.cost line 23
  7. def OAI.LinearListHadwiger.Fractional.number line 25
  8. lemma OAI.LinearListHadwiger.Fractional.cost_nonneg line 28
  9. def OAI.LinearListHadwiger.Fractional.singletonWeights line 31
  10. lemma OAI.LinearListHadwiger.Fractional.singletonWeights_cover line 34
  11. lemma OAI.LinearListHadwiger.Fractional.singletonWeights_cost line 55
  12. lemma OAI.LinearListHadwiger.Fractional.costs_nonempty line 61
  13. lemma OAI.LinearListHadwiger.Fractional.costs_bddBelow line 65
  14. lemma OAI.LinearListHadwiger.Fractional.number_le_cost line 71
  15. lemma OAI.LinearListHadwiger.Fractional.number_nonneg line 74
  16. lemma OAI.LinearListHadwiger.Fractional.number_le_card line 77
  17. lemma OAI.LinearListHadwiger.Fractional.Cover.clamp line 80
  18. lemma OAI.LinearListHadwiger.Fractional.cover_isClosed line 107
  19. lemma OAI.LinearListHadwiger.Fractional.cost_continuous line 134
  20. theorem OAI.LinearListHadwiger.Fractional.optimum_exists line 139
  21. lemma OAI.LinearListHadwiger.Fractional.number_le_iff line 157
  22. def OAI.LinearListHadwiger.Fractional.Dual line 166
  23. lemma OAI.LinearListHadwiger.Fractional.Dual.le_one line 169
  24. lemma OAI.LinearListHadwiger.Fractional.dual_zero line 172
  25. lemma OAI.LinearListHadwiger.Fractional.dual_isClosed line 175
  26. lemma OAI.LinearListHadwiger.Fractional.dual_maximum line 192
  27. lemma OAI.LinearListHadwiger.Fractional.weak_duality line 202
  28. lemma OAI.LinearListHadwiger.Fractional.dual_le_number line 225
  29. def OAI.LinearListHadwiger.Fractional.indicator line 231
  30. lemma OAI.LinearListHadwiger.Fractional.indicator_empty line 233
  31. lemma OAI.LinearListHadwiger.Fractional.constant_mem_hull_cover line 235
  32. lemma OAI.LinearListHadwiger.Fractional.functional_eq_sum line 279
  33. lemma OAI.LinearListHadwiger.Fractional.functional_indicator line 288
  34. lemma OAI.LinearListHadwiger.Fractional.dual_above line 295
  35. theorem OAI.LinearListHadwiger.Fractional.duality line 343
  36. def OAI.LinearListHadwiger.Fractional.transport line 359
  37. lemma OAI.LinearListHadwiger.Fractional.transport_expect line 362
  38. lemma OAI.LinearListHadwiger.Fractional.transport_sum line 373
  39. lemma OAI.LinearListHadwiger.Fractional.transport_nonneg line 377
  40. def OAI.LinearListHadwiger.Fractional.marginal line 381
  41. lemma OAI.LinearListHadwiger.Fractional.marginal_eq_expect line 384
  42. def OAI.LinearListHadwiger.Fractional.prune line 389
  43. lemma OAI.LinearListHadwiger.Fractional.prune_cost line 392
  44. lemma OAI.LinearListHadwiger.Fractional.prune_marginal line 397
  45. lemma OAI.LinearListHadwiger.Fractional.prune_cover line 412
  46. lemma OAI.LinearListHadwiger.Fractional.exact_cover line 439
  47. lemma OAI.LinearListHadwiger.Fractional.marginal_sum line 467
  48. lemma OAI.LinearListHadwiger.Fractional.partition_small line 476
  49. lemma OAI.LinearListHadwiger.Fractional.partition_small_real line 528
  50. def OAI.LinearListHadwiger.Fractional.splitWeights line 540
  51. lemma OAI.LinearListHadwiger.Fractional.splitWeights_sum line 544
  52. lemma OAI.LinearListHadwiger.Fractional.splitWeights_marginal line 553
  53. lemma OAI.LinearListHadwiger.Fractional.bounded_cover line 572
  54. theorem OAI.LinearListHadwiger.Fractional.bounded_sampling line 611
  55. lemma OAI.LinearListHadwiger.Fractional.cover_comap line 658
  56. lemma OAI.LinearListHadwiger.Fractional.number_comap line 686
  57. lemma OAI.LinearListHadwiger.Fractional.number_induce line 692
  58. lemma OAI.LinearListHadwiger.Fractional.Dual.comap line 695
  59. lemma OAI.LinearListHadwiger.Fractional.number_le_induce_add line 709