OAI/Computability/MaxCut/Games/RawPartnerTarget.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

A partner target whose coordinates depend only on the displayed full/single positions. It does not contain hidden occurrence identities or right-hand sides.

  1. abbrev OAI.MaxCutGames.Soundness.RawPartnerTarget.RawPoint line 19
  2. def OAI.MaxCutGames.Soundness.RawPartnerTarget.rawProjection line 23
  3. def OAI.MaxCutGames.Soundness.RawPartnerTarget.gammaOfRawMap line 29
  4. theorem OAI.MaxCutGames.Soundness.RawPartnerTarget.rawPoint_decomposition line 32
  5. theorem OAI.MaxCutGames.Soundness.RawPartnerTarget.rawMap_expansion line 37
  6. theorem OAI.MaxCutGames.Soundness.RawPartnerTarget.rawMap_on_partner line 44
  7. theorem OAI.MaxCutGames.Soundness.RawPartnerTarget.rawMap_pullback line 50
  8. instance OAI.MaxCutGames.Soundness.ConditionalIncidences.zeroBits line 80
  9. def OAI.MaxCutGames.Soundness.ConditionalIncidences.membershipBool line 83
  10. def OAI.MaxCutGames.Soundness.ConditionalIncidences.fullCoefficient line 86
  11. def OAI.MaxCutGames.Soundness.ConditionalIncidences.singleCoefficient line 91
  12. def OAI.MaxCutGames.Soundness.ConditionalIncidences.fillHidden line 95
  13. theorem OAI.MaxCutGames.Soundness.ConditionalIncidences.singleCoefficient_zero line 99
  14. theorem OAI.MaxCutGames.Soundness.ConditionalIncidences.zeroSet_subset line 107
  15. def OAI.MaxCutGames.Soundness.ConditionalIncidences.actualFirst line 117
  16. def OAI.MaxCutGames.Soundness.ConditionalIncidences.actualSecond line 122
  17. def OAI.MaxCutGames.Soundness.ConditionalIncidences.localFirstFromH line 127
  18. def OAI.MaxCutGames.Soundness.ConditionalIncidences.localSecondFromH line 138
  19. theorem OAI.MaxCutGames.Soundness.ConditionalIncidences.localFirstFromH_question_inside line 150
  20. theorem OAI.MaxCutGames.Soundness.ConditionalIncidences.localSecondFromH_question_inside line 160
  21. theorem OAI.MaxCutGames.Soundness.ConditionalIncidences.outside_pair_agree line 172
  22. theorem OAI.MaxCutGames.Soundness.ConditionalIncidences.fillHidden_occurrences line 178
  23. theorem OAI.MaxCutGames.Soundness.ConditionalIncidences.fillHidden_names line 190
  24. theorem OAI.MaxCutGames.Soundness.ConditionalIncidences.localFirstFromH_correct line 202

    Source documentation

    Equality of the entire first private input, including its row map.

    theorem localFirstFromH_correct
    (distinct : ∀ o i i', name o i = name o i' → i = i')
    (reference sample : RawObservationFibre J name gamma observed) :
    localFirstFromH J name gamma observed reference (fun j => (sample.val.2 j.val).1) =
      actualFirst J gamma sample.val.2 := by
…

    Mentions: OAI.MaxCutGames.Soundness.ConditionalIncidences.RawObservationFibre, OAI.MaxCutGames.Soundness.ConditionalIncidences.localFirstFromH, OAI.MaxCutGames.Soundness.ConditionalIncidences.actualFirst

  25. theorem OAI.MaxCutGames.Soundness.ConditionalIncidences.localSecondFromH_correct line 224

    Source documentation

    Equality of the entire second private input. The constructor requires no occurrence, equation rhs, or slot from any position in K.

    theorem localSecondFromH_correct (reference sample : RawObservationFibre J name gamma observed) :
    localSecondFromH J name gamma observed reference
        (fun j => name (sample.val.2 j.val).1 (sample.val.2 j.val).2) =
      actualSecond J name gamma sample.val.2 := by
…

    Mentions: OAI.MaxCutGames.Soundness.ConditionalIncidences.RawObservationFibre, OAI.MaxCutGames.Soundness.ConditionalIncidences.localSecondFromH, OAI.MaxCutGames.Soundness.ConditionalIncidences.actualSecond