OAI/Computability/UniqueGames/Decoding/PaddedLaw.lean

GitHub source file

80 declarations, 0 contain sorry, 0 declared as axioms

Actual linear-map realization of the sparse padded-table experiment. The finite sample has one independent full pair or singleton coefficient at each occurrence position and one independent homogeneous intercept. Its map is formed by composing a genuine map on the raw projected target with the actual parity projection. The third position contributes its parity-dependent intercept; it is not treated as a homogeneous two-coordinate projection.

  1. def OAI.UniqueGamesTheorem.Decoder.PaddedLaw.pushforwardWeight line 35
  2. theorem OAI.UniqueGamesTheorem.Decoder.PaddedLaw.pushforwardWeight_pi line 38
  3. theorem OAI.UniqueGamesTheorem.Decoder.PaddedLaw.pushforwardWeight_joint_uniform_intercept line 50
  4. abbrev OAI.UniqueGamesTheorem.Decoder.PaddedLaw.BlockDraw line 77
  5. def OAI.UniqueGamesTheorem.Decoder.PaddedLaw.decodeSlot line 79
  6. theorem OAI.UniqueGamesTheorem.Decoder.PaddedLaw.slotIndex_decodeSlot line 82
  7. def OAI.UniqueGamesTheorem.Decoder.PaddedLaw.blockAmbient line 85
  8. def OAI.UniqueGamesTheorem.Decoder.PaddedLaw.blockSlopes line 89
  9. def OAI.UniqueGamesTheorem.Decoder.PaddedLaw.blockThird line 92
  10. theorem OAI.UniqueGamesTheorem.Decoder.PaddedLaw.blockSlopes_full line 95
  11. theorem OAI.UniqueGamesTheorem.Decoder.PaddedLaw.blockSlopes_first line 99
  12. theorem OAI.UniqueGamesTheorem.Decoder.PaddedLaw.blockSlopes_second line 104
  13. theorem OAI.UniqueGamesTheorem.Decoder.PaddedLaw.blockSlopes_third line 109
  14. def OAI.UniqueGamesTheorem.Decoder.PaddedLaw.singletonPositions line 113
  15. def OAI.UniqueGamesTheorem.Decoder.PaddedLaw.drawSlots line 116
  16. def OAI.UniqueGamesTheorem.Decoder.PaddedLaw.drawCoefficients line 121
  17. def OAI.UniqueGamesTheorem.Decoder.PaddedLaw.paddedMap line 133
  18. theorem OAI.UniqueGamesTheorem.Decoder.PaddedLaw.ambientCoefficients_draw line 139
  19. def OAI.UniqueGamesTheorem.Decoder.PaddedLaw.interceptShift line 151
  20. theorem OAI.UniqueGamesTheorem.Decoder.PaddedLaw.paddedMap_toCoefficients line 154
  21. theorem OAI.UniqueGamesTheorem.Decoder.PaddedLaw.uniform_rawMaps line 173

    Source documentation

    Uniform raw coefficients are exactly uniform genuine maps on the actual projected target, for each fixed mask and projection choice.

    theorem uniform_rawMaps [Fintype V] (J : Finset (Fin k))
    (H : (RawPoint J →ₗ[F2] V) → ℝ) :
    (𝔼 gamma : RawCoefficients J V, H (rawMap J V gamma)) = 𝔼 Y, H Y := by
…
  22. abbrev OAI.UniqueGamesTheorem.Decoder.PaddedLaw.RawTuple line 180

    Source documentation

    The conditional coefficient sample, with full pairs and singleton values kept at their occurrence-local positions.

    abbrev RawTuple (J : Finset (Fin k)) (V : Type) :=
…
  23. def OAI.UniqueGamesTheorem.Decoder.PaddedLaw.rawTupleEquiv line 183
  24. def OAI.UniqueGamesTheorem.Decoder.PaddedLaw.tupleDraw line 204
  25. theorem OAI.UniqueGamesTheorem.Decoder.PaddedLaw.tupleDraw_ambient line 210
  26. theorem OAI.UniqueGamesTheorem.Decoder.PaddedLaw.paddedMap_tupleDraw line 220
  27. theorem OAI.UniqueGamesTheorem.Decoder.PaddedLaw.uniform_fixed_projection_tuple line 238

    Source documentation

    Conditional on every fixed mask and position choice, independently uniform full pairs/singletons and intercept give the uniform law on genuine projected-target maps followed by the actual projection.

    theorem uniform_fixed_projection_tuple [Fintype V] (rhs : Fin k → Bool)
    (J : Finset (Fin k)) (slot : Fin k → Slot)
    (H : (ActualHomogeneous.E k →ₗ[F2] V) → ℝ) :
    (𝔼 a : RawTuple J V, H (paddedMap rhs (tupleDraw J slot a) a.1)) =
      𝔼 Y : RawPoint J →ₗ[F2] V, H (Y.comp (rawProjection rhs J slot)) := by
…

    Mentions: OAI.UniqueGamesTheorem.Decoder.PaddedLaw.RawTuple, OAI.UniqueGamesTheorem.Decoder.PaddedLaw.paddedMap, OAI.UniqueGamesTheorem.Decoder.PaddedLaw.tupleDraw

  28. def OAI.UniqueGamesTheorem.Decoder.PaddedLaw.blockWeights line 252

    Source documentation

    Retain a full pair with probability 1-beta, or choose one of three singleton positions with probability beta/3 and its uniform slope.

    def blockWeights (β : ℝ) : BlockDraw V → ℝ
  | .inl ab => (1 - β) * uniformWeights (V × V) ab
  | .inr ia => (β / 3) * uniformWeights V ia.2

omit [Module F2 V] in

    Mentions: OAI.UniqueGamesTheorem.Decoder.PaddedLaw.BlockDraw

  29. theorem OAI.UniqueGamesTheorem.Decoder.PaddedLaw.blockWeights_isProbability line 257
  30. theorem OAI.UniqueGamesTheorem.Decoder.PaddedLaw.blockWeights_slopes line 271
  31. def OAI.UniqueGamesTheorem.Decoder.PaddedLaw.drawWeights line 299
  32. def OAI.UniqueGamesTheorem.Decoder.PaddedLaw.paddedWeights line 302
  33. theorem OAI.UniqueGamesTheorem.Decoder.PaddedLaw.paddedWeights_eq line 306
  34. theorem OAI.UniqueGamesTheorem.Decoder.PaddedLaw.uniformWeights_prod line 329
  35. theorem OAI.UniqueGamesTheorem.Decoder.PaddedLaw.totalVariation_uniform_front line 333
  36. theorem OAI.UniqueGamesTheorem.Decoder.PaddedLaw.paddedWeights_totalVariation_eq_slope line 344
  37. theorem OAI.UniqueGamesTheorem.Decoder.PaddedLaw.paddedWeights_totalVariation line 362

    Source documentation

    Full-table bound on the coordinates of the genuine composed maps. It includes the affine intercept and averages all projection choices.

    theorem paddedWeights_totalVariation (rhs : Fin k → Bool) (β : ℝ)
    (hβ : 0 ≤ β) (hβ' : β ≤ 1) :
    UniqueGamesTheorem.Foundations.Information.totalVariation (paddedWeights (V := V) rhs β)
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Information.totalVariation, OAI.UniqueGamesTheorem.Decoder.PaddedLaw.paddedWeights

  38. abbrev OAI.UniqueGamesTheorem.Decoder.PaddedLaw.ProjectionChoice line 370
  39. def OAI.UniqueGamesTheorem.Decoder.PaddedLaw.choiceWeight line 372
  40. theorem OAI.UniqueGamesTheorem.Decoder.PaddedLaw.choiceWeight_isProbability line 376
  41. def OAI.UniqueGamesTheorem.Decoder.PaddedLaw.blockKernel line 387
  42. def OAI.UniqueGamesTheorem.Decoder.PaddedLaw.choiceTupleWeight line 392
  43. theorem OAI.UniqueGamesTheorem.Decoder.PaddedLaw.choiceTupleWeight_isProbability line 395
  44. def OAI.UniqueGamesTheorem.Decoder.PaddedLaw.kernelTupleWeight line 400
  45. theorem OAI.UniqueGamesTheorem.Decoder.PaddedLaw.blockWeights_choice_mixture line 404
  46. theorem OAI.UniqueGamesTheorem.Decoder.PaddedLaw.independent_blockWeights_mixture line 410
  47. theorem OAI.UniqueGamesTheorem.Decoder.PaddedLaw.drawWeights_choice_mixture line 421
  48. theorem OAI.UniqueGamesTheorem.Decoder.PaddedLaw.draw_expectation_choice_mixture line 432

    Source documentation

    This is the unconditioned law identity before replacing the coefficient kernel by uniform projected-target maps. No division by a mask probability.

    theorem draw_expectation_choice_mixture (β : ℝ)
    (H : ((Fin k → BlockDraw V) × V) → ℝ) :
    (∑ dz, drawWeights β k dz * H dz) =
      ∑ c : Fin k → ProjectionChoice, choiceTupleWeight β c *
        ∑ dz, (kernelTupleWeight c dz.1 * uniformWeights V dz.2) * H dz := by
…

    Mentions: OAI.UniqueGamesTheorem.Decoder.PaddedLaw.BlockDraw, OAI.UniqueGamesTheorem.Decoder.PaddedLaw.drawWeights, OAI.UniqueGamesTheorem.Decoder.PaddedLaw.ProjectionChoice, OAI.UniqueGamesTheorem.Decoder.PaddedLaw.choiceTupleWeight, OAI.UniqueGamesTheorem.Decoder.PaddedLaw.kernelTupleWeight

  49. def OAI.UniqueGamesTheorem.Decoder.PaddedLaw.ChoiceValue line 447

    Source documentation

    The actual coefficient type after a choice has been fixed.

    def ChoiceValue (V : Type) : ProjectionChoice → Type
  | none => V × V
  | some _ => V

    Mentions: OAI.UniqueGamesTheorem.Decoder.PaddedLaw.ProjectionChoice

  50. instance OAI.UniqueGamesTheorem.Decoder.PaddedLaw.choiceValueFintype line 451
  51. def OAI.UniqueGamesTheorem.Decoder.PaddedLaw.choiceEmbed line 454
  52. theorem OAI.UniqueGamesTheorem.Decoder.PaddedLaw.blockKernel_uniform_pushforward line 459
  53. theorem OAI.UniqueGamesTheorem.Decoder.PaddedLaw.pushforwardWeight_pi_dep line 476
  54. theorem OAI.UniqueGamesTheorem.Decoder.PaddedLaw.uniformWeights_pi line 489
  55. theorem OAI.UniqueGamesTheorem.Decoder.PaddedLaw.kernelTuple_uniform_pushforward line 496
  56. theorem OAI.UniqueGamesTheorem.Decoder.PaddedLaw.sum_pushforwardWeight_mul line 514
  57. theorem OAI.UniqueGamesTheorem.Decoder.PaddedLaw.sum_uniformWeights_mul line 524
  58. def OAI.UniqueGamesTheorem.Decoder.PaddedLaw.choiceMask line 530
  59. def OAI.UniqueGamesTheorem.Decoder.PaddedLaw.choiceSlot line 533
  60. def OAI.UniqueGamesTheorem.Decoder.PaddedLaw.choiceSlots line 537
  61. theorem OAI.UniqueGamesTheorem.Decoder.PaddedLaw.not_mem_choiceMask line 540
  62. def OAI.UniqueGamesTheorem.Decoder.PaddedLaw.fullChoiceValue line 544
  63. def OAI.UniqueGamesTheorem.Decoder.PaddedLaw.singleChoiceValue line 548
  64. def OAI.UniqueGamesTheorem.Decoder.PaddedLaw.readChoiceValue line 552
  65. theorem OAI.UniqueGamesTheorem.Decoder.PaddedLaw.readChoiceValue_roundtrip line 559
  66. theorem OAI.UniqueGamesTheorem.Decoder.PaddedLaw.readChoiceValue_full line 565
  67. theorem OAI.UniqueGamesTheorem.Decoder.PaddedLaw.readChoiceValue_single line 572
  68. def OAI.UniqueGamesTheorem.Decoder.PaddedLaw.choiceValuesToRawTuple line 579
  69. def OAI.UniqueGamesTheorem.Decoder.PaddedLaw.rawTupleToChoiceValues line 585
  70. def OAI.UniqueGamesTheorem.Decoder.PaddedLaw.choiceValuesRawTupleEquiv line 593

    Source documentation

    Choice fibers and the RawTuple model contain exactly the same coefficients, with no unused coordinate and no multiplicity.

    def choiceValuesRawTupleEquiv (c : Fin k → ProjectionChoice) :
    ((∀ j, ChoiceValue V (c j)) × V) ≃ RawTuple (choiceMask c) V where
…

    Mentions: OAI.UniqueGamesTheorem.Decoder.PaddedLaw.ProjectionChoice, OAI.UniqueGamesTheorem.Decoder.PaddedLaw.ChoiceValue, OAI.UniqueGamesTheorem.Decoder.PaddedLaw.RawTuple, OAI.UniqueGamesTheorem.Decoder.PaddedLaw.choiceMask

  71. theorem OAI.UniqueGamesTheorem.Decoder.PaddedLaw.restoreChoiceDraw line 615
  72. theorem OAI.UniqueGamesTheorem.Decoder.PaddedLaw.tupleDraw_choiceValues line 624
  73. theorem OAI.UniqueGamesTheorem.Decoder.PaddedLaw.fixed_choice_kernel_map_expectation line 639

    Source documentation

    The whole fixed-choice kernel is precisely the uniform actual-map law. This lemma closes the gap between an arbitrary fixed-mask sampling experiment and the conditioning kernel that actually occurs in drawWeights.

    theorem fixed_choice_kernel_map_expectation
    (rhs : Fin k → Bool) (c : Fin k → ProjectionChoice)
    (H : (ActualHomogeneous.E k →ₗ[F2] V) → ℝ) :
    (∑ dz : (Fin k → BlockDraw V) × V,
      (kernelTupleWeight c dz.1 * uniformWeights V dz.2) *
        H (paddedMap rhs dz.1 dz.2)) =
      𝔼 Y : RawPoint (choiceMask c) →ₗ[F2] V,
        H (Y.comp (rawProjection rhs (choiceMask c) (choiceSlots c))) := by
…

    Mentions: OAI.UniqueGamesTheorem.Decoder.PaddedLaw.ProjectionChoice, OAI.UniqueGamesTheorem.Decoder.PaddedLaw.BlockDraw, OAI.UniqueGamesTheorem.Decoder.PaddedLaw.kernelTupleWeight, OAI.UniqueGamesTheorem.Decoder.PaddedLaw.paddedMap, OAI.UniqueGamesTheorem.Decoder.PaddedLaw.choiceMask, OAI.UniqueGamesTheorem.Decoder.PaddedLaw.choiceSlots

  74. theorem OAI.UniqueGamesTheorem.Decoder.PaddedLaw.actual_projection_mixture_expectation line 680
  75. theorem OAI.UniqueGamesTheorem.Decoder.PaddedLaw.uniform_rawMap_pair line 695

    Source documentation

    Combining independently uniform M and T into a map with product codomain is exactly uniform; the preceding law may take V = K × W.

    theorem uniform_rawMap_pair {K W : Type}
    [AddCommGroup K] [Module F2 K] [Fintype K]
    [AddCommGroup W] [Module F2 W] [Fintype W]
    (J : Finset (Fin k)) (H : (RawPoint J →ₗ[F2] K × W) → ℝ) :
    (𝔼 MT : (RawPoint J →ₗ[F2] K) × (RawPoint J →ₗ[F2] W),
      H (MT.1.prod MT.2)) = 𝔼 Y : RawPoint J →ₗ[F2] K × W, H Y := by
…
  76. def OAI.UniqueGamesTheorem.Decoder.PaddedLaw.paddedMapWeights line 707
  77. theorem OAI.UniqueGamesTheorem.Decoder.PaddedLaw.paddedMapWeights_eq line 712
  78. theorem OAI.UniqueGamesTheorem.Decoder.PaddedLaw.uniform_sourceMap_coordinates line 726
  79. theorem OAI.UniqueGamesTheorem.Decoder.PaddedLaw.paddedMapWeights_totalVariation_eq_slope line 733
  80. theorem OAI.UniqueGamesTheorem.Decoder.PaddedLaw.paddedMapWeights_totalVariation line 760