OAI/Computability/MinUncut/PCP/SelectedInformation.lean

GitHub source file

63 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MinUncutGames.Foundations.Repetition.mergeCoordinates line 12
  2. def OAI.MinUncutGames.Foundations.Repetition.coordinateSplitEquiv line 16
  3. theorem OAI.MinUncutGames.Foundations.Repetition.iid_coordinate_split line 24
  4. abbrev OAI.MinUncutGames.Foundations.Repetition.SelectedLabels line 54
  5. def OAI.MinUncutGames.Foundations.Repetition.selectedQuestionTuple line 57
  6. def OAI.MinUncutGames.Foundations.Repetition.selectedAnswerLabel line 64
  7. def OAI.MinUncutGames.Foundations.Repetition.selectedLikelihood line 70
  8. theorem OAI.MinUncutGames.Foundations.Repetition.selectedLikelihood_nonnegative line 81
  9. theorem OAI.MinUncutGames.Foundations.Repetition.selectedLikelihood_sum line 92
  10. theorem OAI.MinUncutGames.Foundations.Repetition.selectedLikelihood_sum_le_one line 103
  11. def OAI.MinUncutGames.Foundations.Repetition.selectedSplitLaw line 111
  12. theorem OAI.MinUncutGames.Foundations.Repetition.selectedSplit_probability line 118
  13. abbrev OAI.MinUncutGames.Foundations.Repetition.SelectedInput line 134
  14. def OAI.MinUncutGames.Foundations.Repetition.selectedInputLaw line 137
  15. def OAI.MinUncutGames.Foundations.Repetition.selectedInputProfile line 142
  16. def OAI.MinUncutGames.Foundations.Repetition.selectedSideMass line 146
  17. theorem OAI.MinUncutGames.Foundations.Repetition.selectedSideMass_sum line 154
  18. theorem OAI.MinUncutGames.Foundations.Repetition.selectedSideMass_total line 166
  19. def OAI.MinUncutGames.Foundations.Repetition.selectedSideWeight line 188
  20. theorem OAI.MinUncutGames.Foundations.Repetition.selected_information_bound line 195
  21. def OAI.MinUncutGames.Foundations.Repetition.selectedJointWeight line 225
  22. theorem OAI.MinUncutGames.Foundations.Repetition.selectedJointWeight_nonnegative line 236
  23. theorem OAI.MinUncutGames.Foundations.Repetition.selectedJointWeight_firstMarginal line 248
  24. theorem OAI.MinUncutGames.Foundations.Repetition.selectedJointWeight_isProbability line 259
  25. def OAI.MinUncutGames.Foundations.Repetition.selectedJointLaw line 270
  26. theorem OAI.MinUncutGames.Foundations.Repetition.selectedJointWeight_factorization line 276
  27. theorem OAI.MinUncutGames.Foundations.Repetition.totalVariation_triangle line 294
  28. def OAI.MinUncutGames.Foundations.Repetition.conditionWeights line 305
  29. theorem OAI.MinUncutGames.Foundations.Repetition.conditionWeights_isProbability line 308
  30. theorem OAI.MinUncutGames.Foundations.Repetition.totalVariation_condition_le line 325
  31. theorem OAI.MinUncutGames.Foundations.Repetition.totalVariation_condition_half_le line 348
  32. theorem OAI.MinUncutGames.Foundations.Repetition.totalVariation_append_kernel line 354
  33. def OAI.MinUncutGames.Foundations.Repetition.kernelPushforward line 367
  34. theorem OAI.MinUncutGames.Foundations.Repetition.totalVariation_kernelPushforward_le line 370
  35. def OAI.MinUncutGames.Foundations.Repetition.maskedJoint line 391
  36. def OAI.MinUncutGames.Foundations.Repetition.maskedModel line 395
  37. def OAI.MinUncutGames.Foundations.Repetition.leftRevealModel line 399
  38. def OAI.MinUncutGames.Foundations.Repetition.rightRevealModel line 403
  39. theorem OAI.MinUncutGames.Foundations.Repetition.sum_maskedJoint line 407
  40. theorem OAI.MinUncutGames.Foundations.Repetition.maskedJoint_isProbability_iff line 423
  41. theorem OAI.MinUncutGames.Foundations.Repetition.maskedJoint_firstMarginal_inl line 445
  42. theorem OAI.MinUncutGames.Foundations.Repetition.maskedJoint_firstMarginal_inr line 454
  43. theorem OAI.MinUncutGames.Foundations.Repetition.abs_half_sub_half_mul line 460
  44. theorem OAI.MinUncutGames.Foundations.Repetition.abs_masked_inl line 466
  45. theorem OAI.MinUncutGames.Foundations.Repetition.abs_masked_inr line 480
  46. theorem OAI.MinUncutGames.Foundations.Repetition.masked_totalVariation_identity line 493
  47. theorem OAI.MinUncutGames.Foundations.Repetition.leftRevealModel_totalVariation_le line 534
  48. theorem OAI.MinUncutGames.Foundations.Repetition.rightRevealModel_totalVariation_le line 541
  49. def OAI.MinUncutGames.Foundations.Repetition.mergeAt line 551
  50. theorem OAI.MinUncutGames.Foundations.Repetition.mergeAt_self line 555
  51. theorem OAI.MinUncutGames.Foundations.Repetition.mergeAt_other line 559
  52. def OAI.MinUncutGames.Foundations.Repetition.partialRevealWeight line 563
  53. theorem OAI.MinUncutGames.Foundations.Repetition.product_reveal_at line 567
  54. def OAI.MinUncutGames.Foundations.Repetition.partialRevealMarginal line 577
  55. def OAI.MinUncutGames.Foundations.Repetition.fullRevealMarginal line 584
  56. theorem OAI.MinUncutGames.Foundations.Repetition.fullRevealMarginal_merge line 592
  57. def OAI.MinUncutGames.Foundations.Repetition.fullRevealModel line 618
  58. theorem OAI.MinUncutGames.Foundations.Repetition.fullRevealModel_merge line 625
  59. def OAI.MinUncutGames.Foundations.Repetition.revealSplitEquiv line 633
  60. theorem OAI.MinUncutGames.Foundations.Repetition.totalVariation_comp_equiv line 655
  61. theorem OAI.MinUncutGames.Foundations.Repetition.fullReveal_totalVariation line 663
  62. theorem OAI.MinUncutGames.Foundations.Repetition.leftReveal_full_error line 678
  63. theorem OAI.MinUncutGames.Foundations.Repetition.rightReveal_full_error line 687