OAI/Computability/VertexCover/Sampling/ThresholdPartition.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.UniqueGames.Foundations.CorrelatedSampling.ThresholdInterval line 42
  2. def OAI.UniqueGames.Foundations.CorrelatedSampling.splitPoint line 47
  3. def OAI.UniqueGames.Foundations.CorrelatedSampling.splitLeft line 49
  4. def OAI.UniqueGames.Foundations.CorrelatedSampling.splitRight line 52
  5. def OAI.UniqueGames.Foundations.CorrelatedSampling.cutAt line 55
  6. def OAI.UniqueGames.Foundations.CorrelatedSampling.intervalCDF line 57
  7. theorem OAI.UniqueGames.Foundations.CorrelatedSampling.split_cdf line 59
  8. theorem OAI.UniqueGames.Foundations.CorrelatedSampling.accepted_interval_mass line 64
  9. theorem OAI.UniqueGames.Foundations.CorrelatedSampling.splitLeft_cut line 72
  10. theorem OAI.UniqueGames.Foundations.CorrelatedSampling.splitRight_cut line 77
  11. theorem OAI.UniqueGames.Foundations.CorrelatedSampling.splitLeft_preserves_cut line 85
  12. theorem OAI.UniqueGames.Foundations.CorrelatedSampling.splitRight_preserves_cut line 91
  13. def OAI.UniqueGames.Foundations.CorrelatedSampling.splitAll line 97
  14. def OAI.UniqueGames.Foundations.CorrelatedSampling.unitThresholdInterval line 101
  15. def OAI.UniqueGames.Foundations.CorrelatedSampling.thresholdPartition line 103
  16. def OAI.UniqueGames.Foundations.CorrelatedSampling.sumOnIntervals line 107
  17. theorem OAI.UniqueGames.Foundations.CorrelatedSampling.sumOn_splitAll line 111
  18. theorem OAI.UniqueGames.Foundations.CorrelatedSampling.partition_sum line 121
  19. theorem OAI.UniqueGames.Foundations.CorrelatedSampling.partition_total_mass line 130
  20. theorem OAI.UniqueGames.Foundations.CorrelatedSampling.partition_cdf line 136
  21. theorem OAI.UniqueGames.Foundations.CorrelatedSampling.splitAll_new_cuts line 141
  22. theorem OAI.UniqueGames.Foundations.CorrelatedSampling.splitAll_preserves_cuts line 153
  23. theorem OAI.UniqueGames.Foundations.CorrelatedSampling.partition_cuts line 167
  24. theorem OAI.UniqueGames.Foundations.CorrelatedSampling.sumOnIntervals_congr line 177
  25. theorem OAI.UniqueGames.Foundations.CorrelatedSampling.partition_acceptance_mass line 187
  26. theorem OAI.UniqueGames.Foundations.CorrelatedSampling.sum_interval_get line 197