OAI/Computability/DirectedFeedback/Games/SelectedLikelihood.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DFVSGames.Foundations.Repetition.selectedLabelAccepts line 14
  2. def OAI.DFVSGames.Foundations.Repetition.selectedLocalAnswers line 20
  3. def OAI.DFVSGames.Foundations.Repetition.selectedLocalTest line 25
  4. theorem OAI.DFVSGames.Foundations.Repetition.selectedLocalTest_nonnegative line 31
  5. theorem OAI.DFVSGames.Foundations.Repetition.selectedQuestionTuple_left line 40
  6. theorem OAI.DFVSGames.Foundations.Repetition.selectedQuestionTuple_right line 49
  7. theorem OAI.DFVSGames.Foundations.Repetition.selectedWins_of_answerLabel line 58
  8. theorem OAI.DFVSGames.Foundations.Repetition.selectedLikelihood_factorization line 82
  9. def OAI.DFVSGames.Foundations.Repetition.revealLeftFactor line 129
  10. def OAI.DFVSGames.Foundations.Repetition.revealRightFactor line 134
  11. theorem OAI.DFVSGames.Foundations.Repetition.revealLeftFactor_nonnegative line 140
  12. theorem OAI.DFVSGames.Foundations.Repetition.revealRightFactor_nonnegative line 147
  13. theorem OAI.DFVSGames.Foundations.Repetition.revealLaw_factorization line 153
  14. def OAI.DFVSGames.Foundations.Repetition.partialLeftFactor line 168
  15. def OAI.DFVSGames.Foundations.Repetition.partialRightFactor line 172
  16. theorem OAI.DFVSGames.Foundations.Repetition.partialRevealWeight_factorization line 176
  17. def OAI.DFVSGames.Foundations.Repetition.completionTupleEquiv line 204
  18. def OAI.DFVSGames.Foundations.Repetition.updatedTableFallback line 210
  19. theorem OAI.DFVSGames.Foundations.Repetition.updatedTableFallback_zero line 215
  20. theorem OAI.DFVSGames.Foundations.Repetition.normalizeOr_weight_eq_zero_of_zero line 227
  21. def OAI.DFVSGames.Foundations.Repetition.selectedLeftRaw line 244
  22. def OAI.DFVSGames.Foundations.Repetition.selectedRightRaw line 252
  23. theorem OAI.DFVSGames.Foundations.Repetition.selectedLeftRaw_nonnegative line 261
  24. theorem OAI.DFVSGames.Foundations.Repetition.selectedRightRaw_nonnegative line 274
  25. def OAI.DFVSGames.Foundations.Repetition.selectedLeftCompletion line 286
  26. def OAI.DFVSGames.Foundations.Repetition.selectedRightCompletion line 295
  27. theorem OAI.DFVSGames.Foundations.Repetition.selectedLeftCompletion_zero line 305
  28. theorem OAI.DFVSGames.Foundations.Repetition.selectedRightCompletion_zero line 316
  29. theorem OAI.DFVSGames.Foundations.Repetition.selectedLeftCompletion_support line 327
  30. theorem OAI.DFVSGames.Foundations.Repetition.selectedRightCompletion_support line 337
  31. def OAI.DFVSGames.Foundations.Repetition.selectedCompletionScale line 346
  32. theorem OAI.DFVSGames.Foundations.Repetition.selected_completion_factorization line 355
  33. theorem OAI.DFVSGames.Foundations.Repetition.selectedCommonLaw_completion_row_mass line 379
  34. theorem OAI.DFVSGames.Foundations.Repetition.selected_completion_row_recombine line 401
  35. theorem OAI.DFVSGames.Foundations.Repetition.partialRevealWeight_forget line 440
  36. theorem OAI.DFVSGames.Foundations.Repetition.partialReveal_event_forget line 452
  37. theorem OAI.DFVSGames.Foundations.Repetition.selectedOutsideLikelihood_event_sum line 469
  38. theorem OAI.DFVSGames.Foundations.Repetition.selected_partial_event_total line 531
  39. def OAI.DFVSGames.Foundations.Repetition.selectedFullLeftCompletion line 552
  40. def OAI.DFVSGames.Foundations.Repetition.selectedFullRightCompletion line 560
  41. theorem OAI.DFVSGames.Foundations.Repetition.selectedFullLeftCompletion_support line 569
  42. theorem OAI.DFVSGames.Foundations.Repetition.selectedFullRightCompletion_support line 591
  43. theorem OAI.DFVSGames.Foundations.Repetition.selected_full_completion_probability line 612
  44. theorem OAI.DFVSGames.Foundations.Repetition.selected_completion_event_row line 638
  45. def OAI.DFVSGames.Foundations.Repetition.selectedFullCompletionMixture line 682
  46. theorem OAI.DFVSGames.Foundations.Repetition.selectedFullCompletionMixture_probability line 691
  47. theorem OAI.DFVSGames.Foundations.Repetition.selectedFullCompletionMixture_eq_conditionedQuestions line 713