OAI/Probability/EntangledGames/RepeatedModel.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.ThresholdParallelRepetition.RepeatedModel line 13
  2. abbrev OAI.ThresholdParallelRepetition.RepeatedModel.Result line 26
  3. def OAI.ThresholdParallelRepetition.RepeatedModel.answers line 27
  4. def OAI.ThresholdParallelRepetition.RepeatedModel.joint line 29
  5. lemma OAI.ThresholdParallelRepetition.RepeatedModel.joint_avg line 33
  6. def OAI.ThresholdParallelRepetition.RepeatedModel.winsAt line 36
  7. def OAI.ThresholdParallelRepetition.RepeatedModel.indicator line 38
  8. def OAI.ThresholdParallelRepetition.RepeatedModel.mass line 40
  9. lemma OAI.ThresholdParallelRepetition.RepeatedModel.indicator_nonneg line 41
  10. lemma OAI.ThresholdParallelRepetition.RepeatedModel.indicator_le_one line 43
  11. lemma OAI.ThresholdParallelRepetition.RepeatedModel.mass_nonneg line 45
  12. lemma OAI.ThresholdParallelRepetition.RepeatedModel.mass_le_one line 46
  13. lemma OAI.ThresholdParallelRepetition.RepeatedModel.mass_empty line 47
  14. lemma OAI.ThresholdParallelRepetition.RepeatedModel.indicator_insert line 50
  15. lemma OAI.ThresholdParallelRepetition.RepeatedModel.mass_insert_le line 54
  16. abbrev OAI.ThresholdParallelRepetition.RepeatedModel.Records line 60
  17. def OAI.ThresholdParallelRepetition.RepeatedModel.restrictA line 61
  18. def OAI.ThresholdParallelRepetition.RepeatedModel.restrictB line 62
  19. def OAI.ThresholdParallelRepetition.RepeatedModel.mask line 63
  20. def OAI.ThresholdParallelRepetition.RepeatedModel.coarseA line 65
  21. def OAI.ThresholdParallelRepetition.RepeatedModel.coarseB line 67
  22. lemma OAI.ThresholdParallelRepetition.RepeatedModel.mask_restrict line 69
  23. lemma OAI.ThresholdParallelRepetition.RepeatedModel.coarse_event line 74
  24. lemma OAI.ThresholdParallelRepetition.RepeatedModel.mask_nonneg line 79
  25. lemma OAI.ThresholdParallelRepetition.RepeatedModel.mask_le_one line 81
  26. lemma OAI.ThresholdParallelRepetition.RepeatedModel.coarse_event_le_one line 83
  27. lemma OAI.ThresholdParallelRepetition.RepeatedModel.mass_coarse line 87
  28. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Law.firsts_updateRight line 105
  29. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Law.seconds_updateLeft line 111
  30. lemma OAI.ThresholdParallelRepetition.RepeatedModel.coarseA_local line 126
  31. lemma OAI.ThresholdParallelRepetition.RepeatedModel.coarseB_local line 130
  32. lemma OAI.ThresholdParallelRepetition.RepeatedModel.mask_congr line 134
  33. lemma OAI.ThresholdParallelRepetition.RepeatedModel.mask_local_left line 141
  34. lemma OAI.ThresholdParallelRepetition.RepeatedModel.mask_local_right line 147
  35. def OAI.ThresholdParallelRepetition.RepeatedModel.exposure line 153
  36. def OAI.ThresholdParallelRepetition.RepeatedModel.fineA line 179
  37. def OAI.ThresholdParallelRepetition.RepeatedModel.fineB line 181
  38. def OAI.ThresholdParallelRepetition.RepeatedModel.refinement line 184
  39. lemma OAI.ThresholdParallelRepetition.RepeatedModel.fine_event line 211
  40. lemma OAI.ThresholdParallelRepetition.RepeatedModel.score_eq_mass_ratio line 232
  41. lemma OAI.ThresholdParallelRepetition.RepeatedModel.card_records line 247