OAI/Computability/MaxCut/Encoding/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.MaxCutGames.Decoder.PaddedLaw.pushforwardWeight line 33
  2. theorem OAI.MaxCutGames.Decoder.PaddedLaw.pushforwardWeight_pi line 36
  3. theorem OAI.MaxCutGames.Decoder.PaddedLaw.pushforwardWeight_joint_uniform_intercept line 48
  4. abbrev OAI.MaxCutGames.Decoder.PaddedLaw.BlockDraw line 75
  5. def OAI.MaxCutGames.Decoder.PaddedLaw.decodeSlot line 77
  6. theorem OAI.MaxCutGames.Decoder.PaddedLaw.slotIndex_decodeSlot line 80
  7. def OAI.MaxCutGames.Decoder.PaddedLaw.blockAmbient line 83
  8. def OAI.MaxCutGames.Decoder.PaddedLaw.blockSlopes line 87
  9. def OAI.MaxCutGames.Decoder.PaddedLaw.blockThird line 90
  10. theorem OAI.MaxCutGames.Decoder.PaddedLaw.blockSlopes_full line 93
  11. theorem OAI.MaxCutGames.Decoder.PaddedLaw.blockSlopes_first line 97
  12. theorem OAI.MaxCutGames.Decoder.PaddedLaw.blockSlopes_second line 102
  13. theorem OAI.MaxCutGames.Decoder.PaddedLaw.blockSlopes_third line 107
  14. def OAI.MaxCutGames.Decoder.PaddedLaw.singletonPositions line 111
  15. def OAI.MaxCutGames.Decoder.PaddedLaw.drawSlots line 114
  16. def OAI.MaxCutGames.Decoder.PaddedLaw.drawCoefficients line 119
  17. def OAI.MaxCutGames.Decoder.PaddedLaw.paddedMap line 131
  18. theorem OAI.MaxCutGames.Decoder.PaddedLaw.ambientCoefficients_draw line 137
  19. def OAI.MaxCutGames.Decoder.PaddedLaw.interceptShift line 149
  20. theorem OAI.MaxCutGames.Decoder.PaddedLaw.paddedMap_toCoefficients line 152
  21. theorem OAI.MaxCutGames.Decoder.PaddedLaw.uniform_rawMaps line 171

    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.MaxCutGames.Decoder.PaddedLaw.RawTuple line 178

    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.MaxCutGames.Decoder.PaddedLaw.rawTupleEquiv line 181
  24. def OAI.MaxCutGames.Decoder.PaddedLaw.tupleDraw line 202
  25. theorem OAI.MaxCutGames.Decoder.PaddedLaw.tupleDraw_ambient line 208
  26. theorem OAI.MaxCutGames.Decoder.PaddedLaw.paddedMap_tupleDraw line 218
  27. theorem OAI.MaxCutGames.Decoder.PaddedLaw.uniform_fixed_projection_tuple line 236

    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.MaxCutGames.Decoder.PaddedLaw.RawTuple, OAI.MaxCutGames.Decoder.PaddedLaw.paddedMap, OAI.MaxCutGames.Decoder.PaddedLaw.tupleDraw

  28. def OAI.MaxCutGames.Decoder.PaddedLaw.blockWeights line 248

    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.MaxCutGames.Decoder.PaddedLaw.BlockDraw

  29. theorem OAI.MaxCutGames.Decoder.PaddedLaw.blockWeights_isProbability line 253
  30. theorem OAI.MaxCutGames.Decoder.PaddedLaw.blockWeights_slopes line 267
  31. def OAI.MaxCutGames.Decoder.PaddedLaw.drawWeights line 295
  32. def OAI.MaxCutGames.Decoder.PaddedLaw.paddedWeights line 298
  33. theorem OAI.MaxCutGames.Decoder.PaddedLaw.paddedWeights_eq line 302
  34. theorem OAI.MaxCutGames.Decoder.PaddedLaw.uniformWeights_prod line 325
  35. theorem OAI.MaxCutGames.Decoder.PaddedLaw.totalVariation_uniform_front line 329
  36. theorem OAI.MaxCutGames.Decoder.PaddedLaw.paddedWeights_totalVariation_eq_slope line 340
  37. theorem OAI.MaxCutGames.Decoder.PaddedLaw.paddedWeights_totalVariation line 358

    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) :
    MaxCutGames.Foundations.Information.totalVariation (paddedWeights (V := V) rhs β)
…

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

  38. abbrev OAI.MaxCutGames.Decoder.PaddedLaw.ProjectionChoice line 366
  39. def OAI.MaxCutGames.Decoder.PaddedLaw.choiceWeight line 368
  40. theorem OAI.MaxCutGames.Decoder.PaddedLaw.choiceWeight_isProbability line 372
  41. def OAI.MaxCutGames.Decoder.PaddedLaw.blockKernel line 383
  42. def OAI.MaxCutGames.Decoder.PaddedLaw.choiceTupleWeight line 388
  43. theorem OAI.MaxCutGames.Decoder.PaddedLaw.choiceTupleWeight_isProbability line 391
  44. def OAI.MaxCutGames.Decoder.PaddedLaw.kernelTupleWeight line 396
  45. theorem OAI.MaxCutGames.Decoder.PaddedLaw.blockWeights_choice_mixture line 400
  46. theorem OAI.MaxCutGames.Decoder.PaddedLaw.independent_blockWeights_mixture line 406
  47. theorem OAI.MaxCutGames.Decoder.PaddedLaw.drawWeights_choice_mixture line 417
  48. theorem OAI.MaxCutGames.Decoder.PaddedLaw.draw_expectation_choice_mixture line 428

    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.MaxCutGames.Decoder.PaddedLaw.BlockDraw, OAI.MaxCutGames.Decoder.PaddedLaw.drawWeights, OAI.MaxCutGames.Decoder.PaddedLaw.ProjectionChoice, OAI.MaxCutGames.Decoder.PaddedLaw.choiceTupleWeight, OAI.MaxCutGames.Decoder.PaddedLaw.kernelTupleWeight

  49. def OAI.MaxCutGames.Decoder.PaddedLaw.ChoiceValue line 443

    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.MaxCutGames.Decoder.PaddedLaw.ProjectionChoice

  50. instance OAI.MaxCutGames.Decoder.PaddedLaw.choiceValueFintype line 447
  51. def OAI.MaxCutGames.Decoder.PaddedLaw.choiceEmbed line 450
  52. theorem OAI.MaxCutGames.Decoder.PaddedLaw.blockKernel_uniform_pushforward line 455
  53. theorem OAI.MaxCutGames.Decoder.PaddedLaw.pushforwardWeight_pi_dep line 472
  54. theorem OAI.MaxCutGames.Decoder.PaddedLaw.uniformWeights_pi line 485
  55. theorem OAI.MaxCutGames.Decoder.PaddedLaw.kernelTuple_uniform_pushforward line 492
  56. theorem OAI.MaxCutGames.Decoder.PaddedLaw.sum_pushforwardWeight_mul line 509
  57. theorem OAI.MaxCutGames.Decoder.PaddedLaw.sum_uniformWeights_mul line 519
  58. def OAI.MaxCutGames.Decoder.PaddedLaw.choiceMask line 525
  59. def OAI.MaxCutGames.Decoder.PaddedLaw.choiceSlot line 528
  60. def OAI.MaxCutGames.Decoder.PaddedLaw.choiceSlots line 532
  61. theorem OAI.MaxCutGames.Decoder.PaddedLaw.not_mem_choiceMask line 535
  62. def OAI.MaxCutGames.Decoder.PaddedLaw.fullChoiceValue line 539
  63. def OAI.MaxCutGames.Decoder.PaddedLaw.singleChoiceValue line 543
  64. def OAI.MaxCutGames.Decoder.PaddedLaw.readChoiceValue line 547
  65. theorem OAI.MaxCutGames.Decoder.PaddedLaw.readChoiceValue_roundtrip line 554
  66. theorem OAI.MaxCutGames.Decoder.PaddedLaw.readChoiceValue_full line 560
  67. theorem OAI.MaxCutGames.Decoder.PaddedLaw.readChoiceValue_single line 567
  68. def OAI.MaxCutGames.Decoder.PaddedLaw.choiceValuesToRawTuple line 574
  69. def OAI.MaxCutGames.Decoder.PaddedLaw.rawTupleToChoiceValues line 580
  70. def OAI.MaxCutGames.Decoder.PaddedLaw.choiceValuesRawTupleEquiv line 588

    Source documentation

    Choice fibers and the already-verified 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.MaxCutGames.Decoder.PaddedLaw.ProjectionChoice, OAI.MaxCutGames.Decoder.PaddedLaw.ChoiceValue, OAI.MaxCutGames.Decoder.PaddedLaw.RawTuple, OAI.MaxCutGames.Decoder.PaddedLaw.choiceMask

  71. theorem OAI.MaxCutGames.Decoder.PaddedLaw.restoreChoiceDraw line 610
  72. theorem OAI.MaxCutGames.Decoder.PaddedLaw.tupleDraw_choiceValues line 619
  73. theorem OAI.MaxCutGames.Decoder.PaddedLaw.fixed_choice_kernel_map_expectation line 634

    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.MaxCutGames.Decoder.PaddedLaw.ProjectionChoice, OAI.MaxCutGames.Decoder.PaddedLaw.BlockDraw, OAI.MaxCutGames.Decoder.PaddedLaw.kernelTupleWeight, OAI.MaxCutGames.Decoder.PaddedLaw.paddedMap, OAI.MaxCutGames.Decoder.PaddedLaw.choiceMask, OAI.MaxCutGames.Decoder.PaddedLaw.choiceSlots

  74. theorem OAI.MaxCutGames.Decoder.PaddedLaw.actual_projection_mixture_expectation line 675
  75. theorem OAI.MaxCutGames.Decoder.PaddedLaw.uniform_rawMap_pair line 690

    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.MaxCutGames.Decoder.PaddedLaw.paddedMapWeights line 700
  77. theorem OAI.MaxCutGames.Decoder.PaddedLaw.paddedMapWeights_eq line 705
  78. theorem OAI.MaxCutGames.Decoder.PaddedLaw.uniform_sourceMap_coordinates line 719
  79. theorem OAI.MaxCutGames.Decoder.PaddedLaw.paddedMapWeights_totalVariation_eq_slope line 726
  80. theorem OAI.MaxCutGames.Decoder.PaddedLaw.paddedMapWeights_totalVariation line 753