OAI/Computability/UniqueGames/Soundness/ActualCanonicalPullbackLemmas.lean

GitHub source file

55 declarations, 0 contain sorry, 0 declared as axioms

Canonical-row descent for every actual partner linear map.

  1. def OAI.UniqueGamesTheorem.Soundness.ActualCanonicalPullback.selectedFree line 27
  2. def OAI.UniqueGamesTheorem.Soundness.ActualCanonicalPullback.ambientCoefficients line 34
  3. def OAI.UniqueGamesTheorem.Soundness.ActualCanonicalPullback.freePullback line 41
  4. theorem OAI.UniqueGamesTheorem.Soundness.ActualCanonicalPullback.ofBit_and line 47
  5. theorem OAI.UniqueGamesTheorem.Soundness.ActualCanonicalPullback.inverse_homogeneous line 50
  6. theorem OAI.UniqueGamesTheorem.Soundness.ActualCanonicalPullback.inverse_first line 54
  7. theorem OAI.UniqueGamesTheorem.Soundness.ActualCanonicalPullback.inverse_second line 58
  8. theorem OAI.UniqueGamesTheorem.Soundness.ActualCanonicalPullback.inverse_retained_free line 62
  9. theorem OAI.UniqueGamesTheorem.Soundness.ActualCanonicalPullback.freePullback_expansion line 76
  10. def OAI.UniqueGamesTheorem.Soundness.ActualCanonicalPullback.outsideInsideEquiv line 90
  11. theorem OAI.UniqueGamesTheorem.Soundness.ActualCanonicalPullback.sum_outside_inside line 101
  12. theorem OAI.UniqueGamesTheorem.Soundness.ActualCanonicalPullback.raw_represents line 112
  13. theorem OAI.UniqueGamesTheorem.Soundness.ActualCanonicalPullback.canonical_raw_pullback line 140
  14. theorem OAI.UniqueGamesTheorem.Soundness.ActualCanonicalPullback.ambientCoefficients_single line 150
  15. theorem OAI.UniqueGamesTheorem.Soundness.ActualCanonicalPullback.ambientCoefficients_full_eq line 159
  16. theorem OAI.UniqueGamesTheorem.Soundness.ActualCanonicalPullback.raw_data_locality line 167

    Source documentation

    Raw canonical data is determined by the full displayed occurrences and retained variable names. Hidden single occurrences and slot indices vanish.

    theorem raw_data_locality [DecidableEq R] {Id Name : Type}
    (names : Id → Fin 3 → Name) (rhs : Id → F2)
    (occ occ' : Fin k → Id) (slot slot' : Fin k → Slot)
    (gamma : RawCoefficients J R)
    (hfull : ∀ j, j ∉ J → occ j = occ' j)
    (hsingle : ∀ j, j ∈ J → names (occ j) (ConcreteExtraction.slotIndex (slot j)) =
      names (occ' j) (ConcreteExtraction.slotIndex (slot' j))) :
    ActualCanonical.data occ names rhs (gamma none) (ambientCoefficients J R gamma slot) =
      ActualCanonical.data occ' names rhs (gamma none) (ambientCoefficients J R gamma slot') := by
…

    Mentions: OAI.UniqueGamesTheorem.Soundness.ConcreteExtraction.slotIndex, OAI.UniqueGamesTheorem.Soundness.ActualCanonicalPullback.ambientCoefficients

  17. theorem OAI.UniqueGamesTheorem.Soundness.ActualCanonicalPullback.canonical_private_input_locality line 196

    Source documentation

    Lemma 6.2 for the actual pullbacks in the shared F₂ coordinate model.

    theorem canonical_private_input_locality [DecidableEq R]
    {Id Name : Type} [DecidableEq Id] [DecidableEq Name]
    (names : Id → Fin 3 → Name) (rhs : Id → F2)
    (occ occ' : Fin k → Id) (slot slot' : Fin k → Slot)
    (gamma : RawCoefficients J R)
    (hfull : ∀ j, j ∉ J → occ j = occ' j)
    (hsingle : ∀ j, j ∈ J → names (occ j) (ConcreteExtraction.slotIndex (slot j)) =
      names (occ' j) (ConcreteExtraction.slotIndex (slot' j))) :
    ActualCanonical.canonical occ names rhs
      (freePullback (fun j => toBit (rhs (occ j))) J R gamma slot) =
    ActualCanonical.canonical occ' names rhs
      (freePullback (fun j => toBit (rhs (occ' j))) J R gamma slot') := by
…

    Mentions: OAI.UniqueGamesTheorem.Soundness.ConcreteExtraction.slotIndex, OAI.UniqueGamesTheorem.Soundness.ActualCanonicalPullback.freePullback

  18. def OAI.UniqueGamesTheorem.Soundness.BinaryRowTransport.rowBits line 230
  19. theorem OAI.UniqueGamesTheorem.Soundness.BinaryRowTransport.rowBits_zero line 232
  20. theorem OAI.UniqueGamesTheorem.Soundness.BinaryRowTransport.rowBits_add line 237
  21. theorem OAI.UniqueGamesTheorem.Soundness.BinaryRowTransport.rowBits_smul line 241
  22. theorem OAI.UniqueGamesTheorem.Soundness.BinaryRowTransport.rowBits_list_sum line 245
  23. theorem OAI.UniqueGamesTheorem.Soundness.BinaryRowTransport.rowBits_sum line 252
  24. def OAI.UniqueGamesTheorem.Soundness.BinaryRowTransport.rowBitsEquiv line 257
  25. theorem OAI.UniqueGamesTheorem.Soundness.BinaryRowTransport.rowBits_eq_zero line 263
  26. def OAI.UniqueGamesTheorem.Soundness.BinaryRowTransport.rowCoefficients line 272
  27. theorem OAI.UniqueGamesTheorem.Soundness.BinaryRowTransport.zeroSet_rowCoefficients line 275
  28. theorem OAI.UniqueGamesTheorem.Soundness.BinaryRowTransport.actual_pullbackRow line 286
  29. theorem OAI.UniqueGamesTheorem.Soundness.BinaryRowTransport.actual_partnerRow line 318
  30. def OAI.UniqueGamesTheorem.Soundness.BinaryRowTransport.rawBitsEquiv line 347
  31. def OAI.UniqueGamesTheorem.Soundness.BinaryRowTransport.bitsMapEquiv line 351
  32. theorem OAI.UniqueGamesTheorem.Soundness.BinaryRowTransport.uniform_bit_coefficients_maps line 358

    Source documentation

    Uniform raw bit coefficients are exactly uniform genuine partner row maps.

    theorem uniform_bit_coefficients_maps {P : Type} [Fintype P] [DecidableEq P]
    [Fintype Q] [DecidableEq Q] (rhs : P → Bool) (J : Finset P)
    (H : (PartnerProjection.PartnerPoint rhs (activeOf J) →ₗ[F2] (Q → F2)) → ℝ) :
    (𝔼 gamma : RawCoefficients J (ZeroInformation.Bits Q), H (bitsMapEquiv rhs J gamma)) =
      𝔼 Y, H Y :=
…

    Mentions: OAI.UniqueGamesTheorem.Soundness.PartnerProjection.PartnerPoint, OAI.UniqueGamesTheorem.Soundness.ZeroInformation.Bits, OAI.UniqueGamesTheorem.Soundness.BinaryRowTransport.bitsMapEquiv

  33. abbrev OAI.UniqueGamesTheorem.Soundness.RawPartnerTarget.RawPoint line 384
  34. def OAI.UniqueGamesTheorem.Soundness.RawPartnerTarget.rawProjection line 388
  35. def OAI.UniqueGamesTheorem.Soundness.RawPartnerTarget.gammaOfRawMap line 394
  36. theorem OAI.UniqueGamesTheorem.Soundness.RawPartnerTarget.rawPoint_decomposition line 397
  37. theorem OAI.UniqueGamesTheorem.Soundness.RawPartnerTarget.rawMap_expansion line 402
  38. theorem OAI.UniqueGamesTheorem.Soundness.RawPartnerTarget.rawMap_on_partner line 409
  39. theorem OAI.UniqueGamesTheorem.Soundness.RawPartnerTarget.rawMap_pullback line 415
  40. def OAI.UniqueGamesTheorem.Soundness.ActualInputRows.restrictedFirst line 448
  41. def OAI.UniqueGamesTheorem.Soundness.ActualInputRows.firstMap line 454
  42. theorem OAI.UniqueGamesTheorem.Soundness.ActualInputRows.firstMap_eq line 459
  43. def OAI.UniqueGamesTheorem.Soundness.ActualInputRows.restrictedSecond line 468
  44. def OAI.UniqueGamesTheorem.Soundness.ActualInputRows.secondMap line 474
  45. theorem OAI.UniqueGamesTheorem.Soundness.ActualInputRows.secondMap_eq line 479
  46. theorem OAI.UniqueGamesTheorem.Soundness.ActualInputRows.firstMap_actual line 490

    Source documentation

    The first player's extraction on the actual sampled input equals Y π. There is no assumption that an arbitrary input row is linear.

    theorem firstMap_actual [Fintype Q] [DecidableEq Q]
    (J : Finset (Fin k)) (rhs : Id → Bool) (occ : Fin k → Id)
    (slot : Fin k → PartnerProjection.Slot) (Y : RawPoint J →ₗ[F2] (Q → F2)) :
    firstMap rhs (actualFirst J (rowCoefficients J (gammaOfRawMap J Y))
      (fun j => (occ j, ConcreteExtraction.slotIndex (slot j)))) =
      Y.comp (rawProjection (fun j => rhs (occ j)) J slot) := by
…

    Mentions: OAI.UniqueGamesTheorem.Soundness.PartnerProjection.Slot, OAI.UniqueGamesTheorem.Soundness.ActualInputRows.firstMap, OAI.UniqueGamesTheorem.Soundness.ConcreteExtraction.slotIndex

  47. theorem OAI.UniqueGamesTheorem.Soundness.ActualInputRows.secondMap_actual line 510

    Source documentation

    The second player's extraction equals the genuine supplied raw target map.

    theorem secondMap_actual [Fintype Q] [DecidableEq Q]
    (J : Finset (Fin k)) (names : Id → Fin 3 → Name) (draw : Draw (Fin k) Id)
    (Y : RawPoint J →ₗ[F2] (Q → F2)) :
    secondMap J (actualSecond J names (rowCoefficients J (gammaOfRawMap J Y)) draw) = Y := by
…

    Mentions: OAI.UniqueGamesTheorem.Soundness.ActualInputRows.secondMap

  48. def OAI.UniqueGamesTheorem.Soundness.RawMapLaw.rawMap line 546
  49. theorem OAI.UniqueGamesTheorem.Soundness.RawMapLaw.coefficients_rawMap line 550
  50. theorem OAI.UniqueGamesTheorem.Soundness.RawMapLaw.rawMap_coefficients line 561
  51. def OAI.UniqueGamesTheorem.Soundness.RawMapLaw.rawMapEquiv line 570
  52. instance OAI.UniqueGamesTheorem.Soundness.RawMapLaw.rawMapsFintype line 576
  53. def OAI.UniqueGamesTheorem.Soundness.RawMapLaw.bitsRawMapEquiv line 580
  54. theorem OAI.UniqueGamesTheorem.Soundness.RawMapLaw.bits_coefficients line 584
  55. theorem OAI.UniqueGamesTheorem.Soundness.RawMapLaw.uniform_bits_rawMaps line 590

    Source documentation

    This equality counts every raw coefficient and every genuine row map once.

    theorem uniform_bits_rawMaps {Q : Type} [Fintype Q] [DecidableEq Q]
    (H : (RawPoint J →ₗ[F2] (Q → F2)) → ℝ) :
    (𝔼 gamma : RawCoefficients J (ZeroInformation.Bits Q), H (bitsRawMapEquiv J gamma)) =
      𝔼 Y, H Y :=
…

    Mentions: OAI.UniqueGamesTheorem.Soundness.ZeroInformation.Bits, OAI.UniqueGamesTheorem.Soundness.RawMapLaw.bitsRawMapEquiv