OAI/Computability/MaxCut/Encoding/BinaryRowTransport.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Exact transport from genuine binary linear maps to the complete private rows used by the conditional game.

  1. def OAI.MaxCutGames.Soundness.BinaryRowTransport.rowBits line 18
  2. theorem OAI.MaxCutGames.Soundness.BinaryRowTransport.rowBits_zero line 20
  3. theorem OAI.MaxCutGames.Soundness.BinaryRowTransport.rowBits_add line 25
  4. theorem OAI.MaxCutGames.Soundness.BinaryRowTransport.rowBits_smul line 29
  5. theorem OAI.MaxCutGames.Soundness.BinaryRowTransport.rowBits_list_sum line 33
  6. theorem OAI.MaxCutGames.Soundness.BinaryRowTransport.rowBits_sum line 40
  7. def OAI.MaxCutGames.Soundness.BinaryRowTransport.rowBitsEquiv line 45
  8. theorem OAI.MaxCutGames.Soundness.BinaryRowTransport.rowBits_eq_zero line 51
  9. def OAI.MaxCutGames.Soundness.BinaryRowTransport.rowCoefficients line 60
  10. theorem OAI.MaxCutGames.Soundness.BinaryRowTransport.zeroSet_rowCoefficients line 63
  11. theorem OAI.MaxCutGames.Soundness.BinaryRowTransport.actual_pullbackRow line 74
  12. theorem OAI.MaxCutGames.Soundness.BinaryRowTransport.actual_partnerRow line 106
  13. def OAI.MaxCutGames.Soundness.BinaryRowTransport.rawBitsEquiv line 135
  14. def OAI.MaxCutGames.Soundness.BinaryRowTransport.bitsMapEquiv line 139
  15. theorem OAI.MaxCutGames.Soundness.BinaryRowTransport.uniform_bit_coefficients_maps line 146

    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.MaxCutGames.Soundness.PartnerProjection.PartnerPoint, OAI.MaxCutGames.Soundness.ZeroInformation.Bits, OAI.MaxCutGames.Soundness.BinaryRowTransport.bitsMapEquiv