OAI/Computability/MinUncut/PCP/SelectedLikelihood.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MinUncutGames.Foundations.Repetition.selectedLabelAccepts line 13
  2. def OAI.MinUncutGames.Foundations.Repetition.selectedLocalAnswers line 19
  3. def OAI.MinUncutGames.Foundations.Repetition.selectedLocalTest line 24
  4. theorem OAI.MinUncutGames.Foundations.Repetition.selectedLocalTest_nonnegative line 30
  5. theorem OAI.MinUncutGames.Foundations.Repetition.selectedQuestionTuple_left line 39
  6. theorem OAI.MinUncutGames.Foundations.Repetition.selectedQuestionTuple_right line 48
  7. theorem OAI.MinUncutGames.Foundations.Repetition.selectedWins_of_answerLabel line 57
  8. theorem OAI.MinUncutGames.Foundations.Repetition.selectedLikelihood_factorization line 81
  9. def OAI.MinUncutGames.Foundations.Repetition.revealLeftFactor line 122
  10. def OAI.MinUncutGames.Foundations.Repetition.revealRightFactor line 127
  11. theorem OAI.MinUncutGames.Foundations.Repetition.revealLeftFactor_nonnegative line 133
  12. theorem OAI.MinUncutGames.Foundations.Repetition.revealRightFactor_nonnegative line 140
  13. theorem OAI.MinUncutGames.Foundations.Repetition.revealLaw_factorization line 146
  14. def OAI.MinUncutGames.Foundations.Repetition.partialLeftFactor line 161
  15. def OAI.MinUncutGames.Foundations.Repetition.partialRightFactor line 165
  16. theorem OAI.MinUncutGames.Foundations.Repetition.partialRevealWeight_factorization line 169
  17. def OAI.MinUncutGames.Foundations.Repetition.completionTupleEquiv line 187
  18. def OAI.MinUncutGames.Foundations.Repetition.updatedTableFallback line 193
  19. theorem OAI.MinUncutGames.Foundations.Repetition.updatedTableFallback_zero line 198
  20. theorem OAI.MinUncutGames.Foundations.Repetition.normalizeOr_weight_eq_zero_of_zero line 210
  21. def OAI.MinUncutGames.Foundations.Repetition.selectedLeftRaw line 227
  22. def OAI.MinUncutGames.Foundations.Repetition.selectedRightRaw line 235
  23. theorem OAI.MinUncutGames.Foundations.Repetition.selectedLeftRaw_nonnegative line 244
  24. theorem OAI.MinUncutGames.Foundations.Repetition.selectedRightRaw_nonnegative line 257
  25. def OAI.MinUncutGames.Foundations.Repetition.selectedLeftCompletion line 269
  26. def OAI.MinUncutGames.Foundations.Repetition.selectedRightCompletion line 278
  27. theorem OAI.MinUncutGames.Foundations.Repetition.selectedLeftCompletion_zero line 288
  28. theorem OAI.MinUncutGames.Foundations.Repetition.selectedRightCompletion_zero line 299
  29. theorem OAI.MinUncutGames.Foundations.Repetition.selectedLeftCompletion_support line 310
  30. theorem OAI.MinUncutGames.Foundations.Repetition.selectedRightCompletion_support line 320
  31. def OAI.MinUncutGames.Foundations.Repetition.selectedCompletionScale line 329
  32. theorem OAI.MinUncutGames.Foundations.Repetition.selected_completion_factorization line 338
  33. theorem OAI.MinUncutGames.Foundations.Repetition.selectedCommonLaw_completion_row_mass line 362
  34. theorem OAI.MinUncutGames.Foundations.Repetition.selected_completion_row_recombine line 384
  35. theorem OAI.MinUncutGames.Foundations.Repetition.partialRevealWeight_forget line 414
  36. theorem OAI.MinUncutGames.Foundations.Repetition.partialReveal_event_forget line 426
  37. theorem OAI.MinUncutGames.Foundations.Repetition.selectedOutsideLikelihood_event_sum line 443
  38. theorem OAI.MinUncutGames.Foundations.Repetition.selected_partial_event_total line 505
  39. def OAI.MinUncutGames.Foundations.Repetition.selectedFullLeftCompletion line 526
  40. def OAI.MinUncutGames.Foundations.Repetition.selectedFullRightCompletion line 534
  41. theorem OAI.MinUncutGames.Foundations.Repetition.selectedFullLeftCompletion_support line 543
  42. theorem OAI.MinUncutGames.Foundations.Repetition.selectedFullRightCompletion_support line 565
  43. theorem OAI.MinUncutGames.Foundations.Repetition.selected_full_completion_probability line 586
  44. theorem OAI.MinUncutGames.Foundations.Repetition.selected_completion_event_row line 612
  45. def OAI.MinUncutGames.Foundations.Repetition.selectedFullCompletionMixture line 656
  46. theorem OAI.MinUncutGames.Foundations.Repetition.selectedFullCompletionMixture_probability line 665
  47. theorem OAI.MinUncutGames.Foundations.Repetition.selectedFullCompletionMixture_eq_conditionedQuestions line 687