OAI/Probability/EntangledGames/Resampling.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ThresholdParallelRepetition.FiniteProbability.Law.Profile line 14
  2. def OAI.ThresholdParallelRepetition.FiniteProbability.Law.updateLeft line 16
  3. def OAI.ThresholdParallelRepetition.FiniteProbability.Law.updateRight line 18
  4. def OAI.ThresholdParallelRepetition.FiniteProbability.Law.left line 21
  5. def OAI.ThresholdParallelRepetition.FiniteProbability.Law.right line 24
  6. def OAI.ThresholdParallelRepetition.FiniteProbability.Law.IgnoresLeft line 28
  7. def OAI.ThresholdParallelRepetition.FiniteProbability.Law.IgnoresRight line 30
  8. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Law.updateLeft_self line 34
  9. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Law.updateRight_self line 37
  10. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Law.updateLeft_same line 40
  11. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Law.updateRight_same line 44
  12. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Law.updateLeft_comm line 48
  13. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Law.updateRight_comm line 53
  14. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Law.updateLeft_right_comm line 58
  15. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Law.left_ignoresLeft line 67
  16. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Law.right_ignoresRight line 75
  17. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Law.left_ignoresLeft_other line 84
  18. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Law.left_ignoresRight_other line 93
  19. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Law.right_ignoresRight_other line 102
  20. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Law.right_ignoresLeft_other line 111
  21. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Law.left_of_ignores line 121
  22. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Law.right_of_ignores line 127
  23. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Law.pair_avg_left line 134
  24. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Law.pair_avg_right line 139
  25. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Law.pi_avg_left line 145
  26. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Law.pi_avg_right line 161
  27. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Law.left_linear line 180
  28. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Law.right_linear line 184
  29. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Law.pi_left_pairing line 189
  30. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Law.pi_right_pairing line 204
  31. def OAI.ThresholdParallelRepetition.FiniteProbability.Law.lefts line 221
  32. def OAI.ThresholdParallelRepetition.FiniteProbability.Law.rights line 224
  33. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Law.lefts_ignoresLeft_mem line 228
  34. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Law.rights_ignoresRight_mem line 238
  35. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Law.lefts_ignoresRight_notMem line 248
  36. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Law.rights_ignoresLeft_notMem line 258
  37. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Law.pi_lefts_pairing line 269
  38. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Law.pi_rights_pairing line 281
  39. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Law.updateLeft_update line 295
  40. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Law.updateRight_update line 301
  41. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Law.left_update line 308
  42. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Law.right_update line 314
  43. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Law.pi_fixed_left_pairing line 322
  44. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Law.pi_fixed_right_pairing line 334
  45. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Law.pi_fixed_lefts_pairing line 347
  46. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Law.pi_fixed_rights_pairing line 362
  47. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Law.lefts_linear line 381
  48. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Law.rights_linear line 393
  49. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Law.lefts_sum line 405
  50. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Law.rights_sum line 416