OAI/Computability/MaxCut/PCP/SelectedProfileBudget.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

The selected-success likelihood factors into a fixed verifier check and two separate tests on the local deterministic answers.

  1. theorem OAI.MaxCutGames.Foundations.Repetition.selectedQuestionRadius_le_informationRadius line 16
  2. theorem OAI.MaxCutGames.Foundations.Repetition.selectedQuestionMarginal_error_sum line 32
  3. def OAI.MaxCutGames.Foundations.Repetition.selectedEmbeddingError line 42
  4. theorem OAI.MaxCutGames.Foundations.Repetition.selectedEmbeddingError_nonnegative line 49
  5. theorem OAI.MaxCutGames.Foundations.Repetition.selectedLeftProfileError_sum line 58
  6. theorem OAI.MaxCutGames.Foundations.Repetition.selectedRightProfileError_sum line 76
  7. theorem OAI.MaxCutGames.Foundations.Repetition.selectedEmbeddingError_sum_le_fifteen line 94
  8. def OAI.MaxCutGames.Foundations.Repetition.selectedLabelAccepts line 118
  9. def OAI.MaxCutGames.Foundations.Repetition.selectedLocalAnswers line 124
  10. def OAI.MaxCutGames.Foundations.Repetition.selectedLocalTest line 129
  11. theorem OAI.MaxCutGames.Foundations.Repetition.selectedLocalTest_nonnegative line 135
  12. theorem OAI.MaxCutGames.Foundations.Repetition.selectedQuestionTuple_left line 144
  13. theorem OAI.MaxCutGames.Foundations.Repetition.selectedQuestionTuple_right line 153
  14. theorem OAI.MaxCutGames.Foundations.Repetition.selectedWins_of_answerLabel line 162
  15. theorem OAI.MaxCutGames.Foundations.Repetition.selectedLikelihood_factorization line 186
  16. def OAI.MaxCutGames.Foundations.Repetition.revealLeftFactor line 234
  17. def OAI.MaxCutGames.Foundations.Repetition.revealRightFactor line 239
  18. theorem OAI.MaxCutGames.Foundations.Repetition.revealLeftFactor_nonnegative line 245
  19. theorem OAI.MaxCutGames.Foundations.Repetition.revealRightFactor_nonnegative line 252
  20. theorem OAI.MaxCutGames.Foundations.Repetition.revealLaw_factorization line 258
  21. def OAI.MaxCutGames.Foundations.Repetition.partialLeftFactor line 273
  22. def OAI.MaxCutGames.Foundations.Repetition.partialRightFactor line 277
  23. theorem OAI.MaxCutGames.Foundations.Repetition.partialRevealWeight_factorization line 281
  24. def OAI.MaxCutGames.Foundations.Repetition.completionTupleEquiv line 316
  25. def OAI.MaxCutGames.Foundations.Repetition.updatedTableFallback line 322
  26. theorem OAI.MaxCutGames.Foundations.Repetition.updatedTableFallback_zero line 327
  27. theorem OAI.MaxCutGames.Foundations.Repetition.normalizeOr_weight_eq_zero_of_zero line 339
  28. def OAI.MaxCutGames.Foundations.Repetition.selectedLeftRaw line 356
  29. def OAI.MaxCutGames.Foundations.Repetition.selectedRightRaw line 364
  30. theorem OAI.MaxCutGames.Foundations.Repetition.selectedLeftRaw_nonnegative line 373
  31. theorem OAI.MaxCutGames.Foundations.Repetition.selectedRightRaw_nonnegative line 386
  32. def OAI.MaxCutGames.Foundations.Repetition.selectedLeftCompletion line 398
  33. def OAI.MaxCutGames.Foundations.Repetition.selectedRightCompletion line 407
  34. theorem OAI.MaxCutGames.Foundations.Repetition.selectedLeftCompletion_zero line 417
  35. theorem OAI.MaxCutGames.Foundations.Repetition.selectedRightCompletion_zero line 428
  36. theorem OAI.MaxCutGames.Foundations.Repetition.selectedLeftCompletion_support line 439
  37. theorem OAI.MaxCutGames.Foundations.Repetition.selectedRightCompletion_support line 449
  38. def OAI.MaxCutGames.Foundations.Repetition.selectedCompletionScale line 458
  39. theorem OAI.MaxCutGames.Foundations.Repetition.selected_completion_factorization line 468

    Source documentation

    Pointwise factorization of the actual selected common-data row.

    theorem selected_completion_factorization (G : Game Q₁ Q₂ A₁ A₂)
    (strategy : Strategy (Fin n → Q₁) (Fin n → Q₂) (Fin n → A₁) (Fin n → A₂))
    (selected : Finset (Fin n)) (j : {i : Fin n // i ∉ selected})
    (s : SelectedCommonData (Q₁ := Q₁) (Q₂ := Q₂) (A₁ := A₁) (A₂ := A₂) selected j)
…

    Mentions: OAI.MaxCutGames.Foundations.Repetition.SelectedCommonData

  40. theorem OAI.MaxCutGames.Foundations.Repetition.selectedCommonLaw_completion_row_mass line 492
  41. theorem OAI.MaxCutGames.Foundations.Repetition.selected_completion_row_recombine line 516

    Source documentation

    Actual common-row mass times the two local completion probabilities is the selected partial-reveal weight with its actual coordinate indicator.

    theorem selected_completion_row_recombine (G : Game Q₁ Q₂ A₁ A₂)
    (strategy : Strategy (Fin n → Q₁) (Fin n → Q₂) (Fin n → A₁) (Fin n → A₂))
    (selected : Finset (Fin n)) (positive : 0 < G.selectedSuccess strategy selected)
    (j : {i : Fin n // i ∉ selected})
    (s : SelectedCommonData (Q₁ := Q₁) (Q₂ := Q₂) (A₁ := A₁) (A₂ := A₂) selected j)
…

    Mentions: OAI.MaxCutGames.Foundations.Repetition.SelectedCommonData

  42. theorem OAI.MaxCutGames.Foundations.Repetition.partialRevealWeight_forget line 558
  43. theorem OAI.MaxCutGames.Foundations.Repetition.partialReveal_event_forget line 570
  44. theorem OAI.MaxCutGames.Foundations.Repetition.selectedOutsideLikelihood_event_sum line 587
  45. theorem OAI.MaxCutGames.Foundations.Repetition.selected_partial_event_total line 649
  46. def OAI.MaxCutGames.Foundations.Repetition.selectedFullLeftCompletion line 670
  47. def OAI.MaxCutGames.Foundations.Repetition.selectedFullRightCompletion line 678
  48. theorem OAI.MaxCutGames.Foundations.Repetition.selectedFullLeftCompletion_support line 687
  49. theorem OAI.MaxCutGames.Foundations.Repetition.selectedFullRightCompletion_support line 709
  50. theorem OAI.MaxCutGames.Foundations.Repetition.selected_full_completion_probability line 730
  51. theorem OAI.MaxCutGames.Foundations.Repetition.selected_completion_event_row line 756
  52. def OAI.MaxCutGames.Foundations.Repetition.selectedFullCompletionMixture line 800
  53. theorem OAI.MaxCutGames.Foundations.Repetition.selectedFullCompletionMixture_probability line 809
  54. theorem OAI.MaxCutGames.Foundations.Repetition.selectedFullCompletionMixture_eq_conditionedQuestions line 833

    Source documentation

    Exact equality with the actual repeated-game question law conditioned on the selected wins, derived by summing the local completion rows.

    theorem selectedFullCompletionMixture_eq_conditionedQuestions (G : Game Q₁ Q₂ A₁ A₂)
    (strategy : Strategy (Fin n → Q₁) (Fin n → Q₂) (Fin n → A₁) (Fin n → A₂))
    (selected : Finset (Fin n)) (positive : 0 < G.selectedSuccess strategy selected)
    (j : {i : Fin n // i ∉ selected}) :
    selectedFullCompletionMixture G strategy selected positive j =
      (G.repetition n).questions.condition (G.selectedWins strategy selected) positive := by
…

    Mentions: OAI.MaxCutGames.Foundations.Repetition.selectedFullCompletionMixture