OAI/Computability/MaxCut/PCP/ProfileCorrection.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

Replacing the input marginal of an actual conditional profile.

  1. def OAI.MaxCutGames.Foundations.Repetition.ProfileCorrection.seedQuestionMarginal line 16
  2. theorem OAI.MaxCutGames.Foundations.Repetition.ProfileCorrection.seedQuestionMarginal_isProbability line 19
  3. theorem OAI.MaxCutGames.Foundations.Repetition.ProfileCorrection.seedQuestionMarginal_first line 30
  4. theorem OAI.MaxCutGames.Foundations.Repetition.ProfileCorrection.totalVariation_triangle line 35
  5. theorem OAI.MaxCutGames.Foundations.Repetition.ProfileCorrection.left_profile_correction line 44
  6. def OAI.MaxCutGames.Foundations.Repetition.revealEndpoint line 99
  7. def OAI.MaxCutGames.Foundations.Repetition.revealLaw line 103

    Source documentation

    Independently reveal either endpoint with probability one half.

    def revealLaw (μ : FiniteDistribution (X × Y)) :
    FiniteDistribution ((X × Y) × (X ⊕ Y)) :=
…
  8. theorem OAI.MaxCutGames.Foundations.Repetition.revealLaw_weight line 108
  9. def OAI.MaxCutGames.Foundations.Repetition.revealFirstLaw line 118
  10. theorem OAI.MaxCutGames.Foundations.Repetition.revealFirstLaw_weight line 123
  11. def OAI.MaxCutGames.Foundations.Repetition.revealFallback line 129

    Source documentation

    The default row still preserves the displayed endpoint if that endpoint has zero probability in the base question law.

    def revealFallback (μ : FiniteDistribution (X × Y)) (r : X ⊕ Y) :
    FiniteDistribution (X × Y) :=
…
  12. def OAI.MaxCutGames.Foundations.Repetition.revealProfile line 135
  13. theorem OAI.MaxCutGames.Foundations.Repetition.revealProfile_inl_support line 139
  14. theorem OAI.MaxCutGames.Foundations.Repetition.revealProfile_inr_support line 151
  15. def OAI.MaxCutGames.Foundations.Repetition.revealInputLaw line 163
  16. theorem OAI.MaxCutGames.Foundations.Repetition.revealInputLaw_weight line 166
  17. theorem OAI.MaxCutGames.Foundations.Repetition.reveal_profile_recombination line 174

    Source documentation

    The conditional product representation is proved from the sampled law, including reveal values with zero probability.

    theorem reveal_profile_recombination (μ : FiniteDistribution (X × Y))
    (r : X ⊕ Y) (q : X × Y) :
    (revealInputLaw μ).weight r * (revealProfile μ r).weight q =
      (revealLaw μ).weight (q,r) := by
…

    Mentions: OAI.MaxCutGames.Foundations.Repetition.revealInputLaw, OAI.MaxCutGames.Foundations.Repetition.revealProfile, OAI.MaxCutGames.Foundations.Repetition.revealLaw

  18. theorem OAI.MaxCutGames.Foundations.Repetition.reveal_profile_inl_recombination line 181
  19. theorem OAI.MaxCutGames.Foundations.Repetition.reveal_profile_inr_recombination line 188
  20. theorem OAI.MaxCutGames.Foundations.Repetition.revealInputLaw_inl line 195
  21. theorem OAI.MaxCutGames.Foundations.Repetition.revealInputLaw_inr line 204
  22. theorem OAI.MaxCutGames.Foundations.Repetition.revealProfile_inl_diagonal line 211
  23. theorem OAI.MaxCutGames.Foundations.Repetition.revealProfile_inr_diagonal line 233
  24. theorem OAI.MaxCutGames.Foundations.Repetition.revealLaw_sum_left line 259
  25. theorem OAI.MaxCutGames.Foundations.Repetition.revealLaw_sum_right line 264
  26. theorem OAI.MaxCutGames.Foundations.Repetition.revealLaw_forget line 269
  27. theorem OAI.MaxCutGames.Foundations.Repetition.reveal_product_factorization line 281

    Source documentation

    A conditional product of independently revealed coordinates has its exact point weight. This is the product identity used by the information bound, derived from the single-coordinate sampled distribution.

    theorem reveal_product_factorization {ι : Type*} [Fintype ι]
    (μ : FiniteDistribution (X × Y)) (r : ι → X ⊕ Y) (q : ι → X × Y) :
    (∏ i, (revealInputLaw μ).weight (r i)) *
      (∏ i, (revealProfile μ (r i)).weight (q i)) =
        ∏ i, (revealLaw μ).weight (q i,r i) := by
…

    Mentions: OAI.MaxCutGames.Foundations.Repetition.revealInputLaw, OAI.MaxCutGames.Foundations.Repetition.revealProfile, OAI.MaxCutGames.Foundations.Repetition.revealLaw

  28. theorem OAI.MaxCutGames.Foundations.Repetition.reveal_product_forget line 291
  29. theorem OAI.MaxCutGames.Foundations.Repetition.reveal_product_expectation line 310

    Source documentation

    Marginalizing the reveal «variables» restores the original independent question law for every observable, including the selected-win likelihood.

    theorem reveal_product_expectation {ι : Type*} [Fintype ι] [DecidableEq ι]
    (μ : FiniteDistribution (X × Y)) (f : (ι → X × Y) → ℝ) :
    (∑ r : ι → X ⊕ Y,
      (∏ i, (revealInputLaw μ).weight (r i)) *
        ∑ q : ι → X × Y, (∏ i, (revealProfile μ (r i)).weight (q i)) * f q) =
      ∑ q : ι → X × Y, (∏ i, μ.weight (q i)) * f q := by
…

    Mentions: OAI.MaxCutGames.Foundations.Repetition.revealInputLaw, OAI.MaxCutGames.Foundations.Repetition.revealProfile