OAI/Computability/DirectedFeedback/Games/QuestionMarginal.lean

GitHub source file

59 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.DFVSGames.Foundations.Repetition.selectedSplit_question_probability line 19
  2. theorem OAI.DFVSGames.Foundations.Repetition.selectedJoint_eventMass line 35
  3. theorem OAI.DFVSGames.Foundations.Repetition.selectedJointLaw_question_probability line 81
  4. theorem OAI.DFVSGames.Foundations.Repetition.selectedJointLaw_questions_pushforward line 119
  5. def OAI.DFVSGames.Foundations.Repetition.selectedTupleLikelihood line 155
  6. theorem OAI.DFVSGames.Foundations.Repetition.selectedTupleLikelihood_nonnegative line 161
  7. theorem OAI.DFVSGames.Foundations.Repetition.selectedTupleLikelihood_le_one line 169
  8. theorem OAI.DFVSGames.Foundations.Repetition.selectedTupleLikelihood_mass line 177
  9. def OAI.DFVSGames.Foundations.Repetition.selectedQuestionMarginal line 190
  10. theorem OAI.DFVSGames.Foundations.Repetition.selectedQuestionMarginal_weight line 197
  11. theorem OAI.DFVSGames.Foundations.Repetition.selectedQuestionMarginal_totalVariation_sq_sum_le_log line 215
  12. theorem OAI.DFVSGames.Foundations.Repetition.unselectedQuestionMarginal_totalVariation_sq_sum_le_log line 233
  13. theorem OAI.DFVSGames.Foundations.Repetition.unselectedQuestionMarginal_totalVariation_sum_le_sqrt line 255
  14. theorem OAI.DFVSGames.Foundations.Repetition.unselectedQuestionMarginal_totalVariation_sum_le_sqrt_sub_card line 283
  15. theorem OAI.DFVSGames.Foundations.Repetition.isProbability_comp_equiv line 307
  16. theorem OAI.DFVSGames.Foundations.Repetition.partialRevealMarginal_isProbability line 316
  17. abbrev OAI.DFVSGames.Foundations.Repetition.SelectedCommonData line 337
  18. theorem OAI.DFVSGames.Foundations.Repetition.selected_fullReveal_isProbability line 342
  19. def OAI.DFVSGames.Foundations.Repetition.selectedCommonLaw line 359
  20. theorem OAI.DFVSGames.Foundations.Repetition.firstMarginal_totalVariation_le line 379
  21. def OAI.DFVSGames.Foundations.Repetition.leftCommonMarginal line 388
  22. def OAI.DFVSGames.Foundations.Repetition.leftCommonProfile line 391
  23. def OAI.DFVSGames.Foundations.Repetition.swapSeedLeft line 394
  24. theorem OAI.DFVSGames.Foundations.Repetition.leftCommonMarginal_isProbability line 400
  25. theorem OAI.DFVSGames.Foundations.Repetition.leftCommonProfile_isProbability line 405
  26. theorem OAI.DFVSGames.Foundations.Repetition.leftCommonProfile_error line 410
  27. def OAI.DFVSGames.Foundations.Repetition.swapQuestionEndpoints line 457
  28. def OAI.DFVSGames.Foundations.Repetition.rightCommonMarginal line 463
  29. def OAI.DFVSGames.Foundations.Repetition.rightCommonProfile line 466
  30. theorem OAI.DFVSGames.Foundations.Repetition.rightCommonProfile_isProbability line 469
  31. theorem OAI.DFVSGames.Foundations.Repetition.swap_question_pushforward_snd line 475
  32. theorem OAI.DFVSGames.Foundations.Repetition.leftRevealModel_swap line 481
  33. theorem OAI.DFVSGames.Foundations.Repetition.rightCommonProfile_error line 491
  34. theorem OAI.DFVSGames.Foundations.Repetition.finiteDistribution_nonempty line 528
  35. def OAI.DFVSGames.Foundations.Repetition.selectedProfileFallback line 538
  36. def OAI.DFVSGames.Foundations.Repetition.selectedLeftProfile line 546
  37. def OAI.DFVSGames.Foundations.Repetition.selectedRightProfile line 559
  38. def OAI.DFVSGames.Foundations.Repetition.selectedLeftProfileError line 572
  39. def OAI.DFVSGames.Foundations.Repetition.selectedRightProfileError line 579
  40. theorem OAI.DFVSGames.Foundations.Repetition.selectedLeftProfileError_le line 586
  41. theorem OAI.DFVSGames.Foundations.Repetition.selectedRightProfileError_le line 600
  42. def OAI.DFVSGames.Foundations.Repetition.selectedSamplingTarget line 614
  43. theorem OAI.DFVSGames.Foundations.Repetition.selectedSamplingTarget_left_error line 622
  44. theorem OAI.DFVSGames.Foundations.Repetition.selectedSamplingTarget_right_error line 635
  45. theorem OAI.DFVSGames.Foundations.Repetition.pushforward_snd_weight_eq_secondMarginal line 658
  46. def OAI.DFVSGames.Foundations.Repetition.revealDataSplitEquiv line 668
  47. theorem OAI.DFVSGames.Foundations.Repetition.partialRevealMarginal_secondMarginal line 685
  48. def OAI.DFVSGames.Foundations.Repetition.selectedObservationDataEquiv line 705
  49. theorem OAI.DFVSGames.Foundations.Repetition.selectedFullReveal_secondMarginal line 714
  50. theorem OAI.DFVSGames.Foundations.Repetition.selectedRawMarginal_secondMarginal line 728
  51. theorem OAI.DFVSGames.Foundations.Repetition.selectedCommonLaw_secondMarginal line 750
  52. theorem OAI.DFVSGames.Foundations.Repetition.selectedCommonLaw_questions_pushforward line 761
  53. theorem OAI.DFVSGames.Foundations.Repetition.selectedQuestionRadius_le_informationRadius line 787
  54. theorem OAI.DFVSGames.Foundations.Repetition.selectedQuestionMarginal_error_sum line 803
  55. def OAI.DFVSGames.Foundations.Repetition.selectedEmbeddingError line 813
  56. theorem OAI.DFVSGames.Foundations.Repetition.selectedEmbeddingError_nonnegative line 820
  57. theorem OAI.DFVSGames.Foundations.Repetition.selectedLeftProfileError_sum line 829
  58. theorem OAI.DFVSGames.Foundations.Repetition.selectedRightProfileError_sum line 847
  59. theorem OAI.DFVSGames.Foundations.Repetition.selectedEmbeddingError_sum_le_fifteen line 865