OAI/Probability/EntangledGames/FiniteProbability.lean

GitHub source file

66 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.ThresholdParallelRepetition.FiniteProbability.Law line 11
  2. def OAI.ThresholdParallelRepetition.FiniteProbability.Law.avg line 20
  3. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Law.avg_const line 22
  4. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Law.avg_add line 24
  5. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Law.avg_sub line 27
  6. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Law.avg_smul line 31
  7. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Law.avg_sum line 34
  8. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Law.avg_linear line 37
  9. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Law.avg_nonneg line 41
  10. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Law.avg_mono line 43
  11. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Law.avg_le_const line 45
  12. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Law.weight_le_one line 47
  13. def OAI.ThresholdParallelRepetition.FiniteProbability.Law.point line 50
  14. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Law.point_avg line 55
  15. def OAI.ThresholdParallelRepetition.FiniteProbability.Law.bind line 58
  16. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Law.bind_avg line 65
  17. def OAI.ThresholdParallelRepetition.FiniteProbability.Law.map line 70
  18. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Law.map_avg line 71
  19. def OAI.ThresholdParallelRepetition.FiniteProbability.Law.prod line 75
  20. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Law.prod_avg line 80
  21. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Law.avg_comm line 84
  22. def OAI.ThresholdParallelRepetition.FiniteProbability.Law.pi line 92
  23. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Law.pi_avg_prod line 97
  24. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Law.avg_eq_sum line 103
  25. def OAI.ThresholdParallelRepetition.FiniteProbability.Law.normalize line 105
  26. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Law.normalize_weight line 111
  27. def OAI.ThresholdParallelRepetition.FiniteProbability.Law.first line 123
  28. def OAI.ThresholdParallelRepetition.FiniteProbability.Law.second line 128
  29. def OAI.ThresholdParallelRepetition.FiniteProbability.Law.givenFirst line 133
  30. def OAI.ThresholdParallelRepetition.FiniteProbability.Law.givenSecond line 136
  31. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Law.first_given line 140
  32. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Law.second_given line 144
  33. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Law.disintegrate_first line 149
  34. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Law.disintegrate_second line 153
  35. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Law.prod_split line 162
  36. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Law.pi_weight_split line 168
  37. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Law.pi_avg_split line 179
  38. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Law.split_update line 187
  39. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Law.update_split line 194
  40. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Law.pi_avg_update line 201
  41. def OAI.ThresholdParallelRepetition.FiniteProbability.Law.kl line 210
  42. def OAI.ThresholdParallelRepetition.FiniteProbability.Law.Supports line 212
  43. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Law.mul_log_ratio_lower line 214
  44. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Law.kl_nonneg line 228
  45. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Law.kl_log_sub line 233
  46. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Law.map_weight_pos line 243
  47. def OAI.ThresholdParallelRepetition.FiniteProbability.Law.marginal line 254
  48. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Law.marginal_avg line 256
  49. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Law.supports_marginal_pi line 259
  50. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Law.avg_log_pi line 266
  51. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Law.supports_marginal line 280
  52. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Law.kl_tensorization line 294
  53. def OAI.ThresholdParallelRepetition.FiniteProbability.Law.tilt line 305
  54. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Law.tilt_avg line 311
  55. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Law.tilt_supports line 316
  56. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Law.kl_tilt line 322
  57. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Law.kl_tilt_le line 332
  58. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Law.avg_indicator line 346
  59. def OAI.ThresholdParallelRepetition.FiniteProbability.Law.coordDensity line 350
  60. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Law.coordDensity_eq line 354
  61. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Law.marginal_density_avg line 360
  62. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Law.marginal_density_weight line 371
  63. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Law.coordDensity_nonneg line 379
  64. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Law.coordDensity_total line 383
  65. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Law.marginal_tilt_eq line 390
  66. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Law.coord_entropy_sum_le line 400