OAI/Combinatorics/IndependentSets/Repetition/TraceLaw.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.IndependentSetsGames.Foundations.CorrelatedSampling.traceAverage line 15
  2. theorem OAI.IndependentSetsGames.Foundations.CorrelatedSampling.traceAverage_const line 19
  3. theorem OAI.IndependentSetsGames.Foundations.CorrelatedSampling.traceAverage_mono line 25
  4. theorem OAI.IndependentSetsGames.Foundations.CorrelatedSampling.traceAverage_sum line 37
  5. theorem OAI.IndependentSetsGames.Foundations.CorrelatedSampling.firstAccepted_law line 49
  6. def OAI.IndependentSetsGames.Foundations.CorrelatedSampling.goodFirstIndicator line 95
  7. theorem OAI.IndependentSetsGames.Foundations.CorrelatedSampling.goodFirstIndicator_expansion line 100
  8. theorem OAI.IndependentSetsGames.Foundations.CorrelatedSampling.goodFirstIndicator_law line 116
  9. structure OAI.IndependentSetsGames.Foundations.CorrelatedSampling.ThresholdInterval line 132
  10. def OAI.IndependentSetsGames.Foundations.CorrelatedSampling.splitPoint line 137
  11. def OAI.IndependentSetsGames.Foundations.CorrelatedSampling.splitLeft line 139
  12. def OAI.IndependentSetsGames.Foundations.CorrelatedSampling.splitRight line 142
  13. def OAI.IndependentSetsGames.Foundations.CorrelatedSampling.cutAt line 145
  14. def OAI.IndependentSetsGames.Foundations.CorrelatedSampling.intervalCDF line 147
  15. theorem OAI.IndependentSetsGames.Foundations.CorrelatedSampling.split_cdf line 149
  16. theorem OAI.IndependentSetsGames.Foundations.CorrelatedSampling.accepted_interval_mass line 154
  17. theorem OAI.IndependentSetsGames.Foundations.CorrelatedSampling.splitLeft_cut line 162
  18. theorem OAI.IndependentSetsGames.Foundations.CorrelatedSampling.splitRight_cut line 167
  19. theorem OAI.IndependentSetsGames.Foundations.CorrelatedSampling.splitLeft_preserves_cut line 175
  20. theorem OAI.IndependentSetsGames.Foundations.CorrelatedSampling.splitRight_preserves_cut line 181
  21. def OAI.IndependentSetsGames.Foundations.CorrelatedSampling.splitAll line 187
  22. def OAI.IndependentSetsGames.Foundations.CorrelatedSampling.unitThresholdInterval line 191
  23. def OAI.IndependentSetsGames.Foundations.CorrelatedSampling.thresholdPartition line 193
  24. def OAI.IndependentSetsGames.Foundations.CorrelatedSampling.sumOnIntervals line 197
  25. theorem OAI.IndependentSetsGames.Foundations.CorrelatedSampling.sumOn_splitAll line 201
  26. theorem OAI.IndependentSetsGames.Foundations.CorrelatedSampling.partition_sum line 211
  27. theorem OAI.IndependentSetsGames.Foundations.CorrelatedSampling.partition_total_mass line 220
  28. theorem OAI.IndependentSetsGames.Foundations.CorrelatedSampling.partition_cdf line 226
  29. theorem OAI.IndependentSetsGames.Foundations.CorrelatedSampling.splitAll_new_cuts line 231
  30. theorem OAI.IndependentSetsGames.Foundations.CorrelatedSampling.splitAll_preserves_cuts line 243
  31. theorem OAI.IndependentSetsGames.Foundations.CorrelatedSampling.partition_cuts line 257
  32. theorem OAI.IndependentSetsGames.Foundations.CorrelatedSampling.sumOnIntervals_congr line 267
  33. theorem OAI.IndependentSetsGames.Foundations.CorrelatedSampling.partition_acceptance_mass line 277
  34. theorem OAI.IndependentSetsGames.Foundations.CorrelatedSampling.sum_interval_get line 287