OAI/Computability/UniqueGames/Soundness/LinearMapDensityLemmas.lean

GitHub source file

85 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.UniqueGamesTheorem.Soundness.LinearMapDensity.uniformMean line 32
2. theorem OAI.UniqueGamesTheorem.Soundness.LinearMapDensity.uniformMean_eq_sum_div_card line 35
3. theorem OAI.UniqueGamesTheorem.Soundness.LinearMapDensity.uniformMean_comm line 39
4. theorem OAI.UniqueGamesTheorem.Soundness.LinearMapDensity.uniformMean_const_mul line 45
5. theorem OAI.UniqueGamesTheorem.Soundness.LinearMapDensity.uniformMean_const line 49
6. theorem OAI.UniqueGamesTheorem.Soundness.LinearMapDensity.restriction_surjective line 54
7. theorem OAI.UniqueGamesTheorem.Soundness.LinearMapDensity.restriction_zero_iff line 61
8. def OAI.UniqueGamesTheorem.Soundness.LinearMapDensity.pullbackMap line 72

   Source documentation

   Pulling back a map along a projection produces a map annihilating its kernel.

   def pullbackMap {V : Type*} [AddCommGroup V] [Module (ZMod 2) V]
       (π : E →ₗ[ZMod 2] V) (B : V →ₗ[ZMod 2] R) :
       {M : E →ₗ[ZMod 2] R // π.ker ≤ M.ker} :=
   …

9. theorem OAI.UniqueGamesTheorem.Soundness.LinearMapDensity.pullbackMap_bijective line 84

   Source documentation

   The pullback map is a bijection onto the genuine kernel-annihilator event. This connects the density calculation to uniform maps on the partner space.

   theorem pullbackMap_bijective {V : Type*} [AddCommGroup V] [Module (ZMod 2) V]
       (π : E →ₗ[ZMod 2] V) (hπ : Function.Surjective π) :
       Function.Bijective (pullbackMap (R := R) π) := by
   …

   Mentions: OAI.UniqueGamesTheorem.Soundness.LinearMapDensity.pullbackMap

10. theorem OAI.UniqueGamesTheorem.Soundness.LinearMapDensity.annihilator_count line 107
11. def OAI.UniqueGamesTheorem.Soundness.LinearMapDensity.kernelDensity line 122
12. theorem OAI.UniqueGamesTheorem.Soundness.LinearMapDensity.kernelDensity_mean line 128
13. theorem OAI.UniqueGamesTheorem.Soundness.LinearMapDensity.kernelDensity_product line 146

    Source documentation

    Pointwise overlap formula, using the actual dimension formula for subspaces.

    theorem kernelDensity_product (K L : Submodule (ZMod 2) E)
        (M : E →ₗ[ZMod 2] R) :
        kernelDensity K M * kernelDensity L M =
          (2 : ℝ) ^ (Module.finrank (ZMod 2) R * Module.finrank (ZMod 2) ↥(K ⊓ L : Submodule (ZMod 2) E)) *
            kernelDensity (K ⊔ L) M := by
    …

    Mentions: OAI.UniqueGamesTheorem.Soundness.LinearMapDensity.kernelDensity

14. theorem OAI.UniqueGamesTheorem.Soundness.LinearMapDensity.kernelDensity_pair_mean line 171

    Source documentation

    The two-kernel second-moment identity for the uniform law on all genuine linear maps E→R. No annihilator probability is a hypothesis.

    theorem kernelDensity_pair_mean [Fintype (E →ₗ[ZMod 2] R)]
        (K L : Submodule (ZMod 2) E) :
        uniformMean (fun M : E →ₗ[ZMod 2] R => kernelDensity K M * kernelDensity L M) =
          (2 : ℝ) ^ (Module.finrank (ZMod 2) R * Module.finrank (ZMod 2) ↥(K ⊓ L : Submodule (ZMod 2) E)) := by
    …

    Mentions: OAI.UniqueGamesTheorem.Soundness.LinearMapDensity.uniformMean, OAI.UniqueGamesTheorem.Soundness.LinearMapDensity.kernelDensity

15. def OAI.UniqueGamesTheorem.Soundness.LinearMapDensity.mixtureDensity line 178
16. theorem OAI.UniqueGamesTheorem.Soundness.LinearMapDensity.mixtureDensity_mean line 182
17. theorem OAI.UniqueGamesTheorem.Soundness.LinearMapDensity.mixtureDensity_second_moment line 193

    Source documentation

    Lemma 6.3's exact second-moment identity for an arbitrary finite uniform list of genuine kernel subspaces. The two partner indices are independent because the right side is an iterated uniform expectation.

    theorem mixtureDensity_second_moment {Partner : Type w} [Fintype Partner]
        [Fintype (E →ₗ[ZMod 2] R)] (kernels : Partner → Submodule (ZMod 2) E) :
        uniformMean (fun M : E →ₗ[ZMod 2] R => (mixtureDensity kernels M) ^ 2) =
          uniformMean (fun p => uniformMean (fun q => (2 : ℝ) ^
            (Module.finrank (ZMod 2) R * Module.finrank (ZMod 2) ↥(kernels p ⊓ kernels q : Submodule (ZMod 2) E)))) := by
    …

    Mentions: OAI.UniqueGamesTheorem.Soundness.LinearMapDensity.uniformMean, OAI.UniqueGamesTheorem.Soundness.LinearMapDensity.mixtureDensity

18. theorem OAI.UniqueGamesTheorem.Soundness.LinearMapDensity.kernelDensity_weighted_mean line 212
19. theorem OAI.UniqueGamesTheorem.Soundness.LinearMapDensity.pullback_uniformMean line 243
20. theorem OAI.UniqueGamesTheorem.Soundness.LinearMapDensity.mixture_pullback_uniformMean line 254
21. inductive OAI.UniqueGamesTheorem.Soundness.PartnerProjection.Slot line 279
22. structure OAI.UniqueGamesTheorem.Soundness.PartnerProjection.Triple line 283
23. def OAI.UniqueGamesTheorem.Soundness.PartnerProjection.zeroTriple line 289
24. def OAI.UniqueGamesTheorem.Soundness.PartnerProjection.parity line 291
25. def OAI.UniqueGamesTheorem.Soundness.PartnerProjection.addTriple line 293
26. theorem OAI.UniqueGamesTheorem.Soundness.PartnerProjection.parity_add line 296
27. theorem OAI.UniqueGamesTheorem.Soundness.PartnerProjection.and_xor line 302
28. def OAI.UniqueGamesTheorem.Soundness.PartnerProjection.retained line 306
29. def OAI.UniqueGamesTheorem.Soundness.PartnerProjection.freeBit line 312
30. theorem OAI.UniqueGamesTheorem.Soundness.PartnerProjection.retained_add line 318
31. theorem OAI.UniqueGamesTheorem.Soundness.PartnerProjection.freeBit_add line 322
32. def OAI.UniqueGamesTheorem.Soundness.PartnerProjection.complete line 327

    Source documentation

    Reconstruct a parity-constrained triple from its retained bit and one free bit.

    def complete (s : Slot) (p r f : Bool) : Triple :=
    …

    Mentions: OAI.UniqueGamesTheorem.Soundness.PartnerProjection.Slot, OAI.UniqueGamesTheorem.Soundness.PartnerProjection.Triple

33. theorem OAI.UniqueGamesTheorem.Soundness.PartnerProjection.parity_complete line 333
34. theorem OAI.UniqueGamesTheorem.Soundness.PartnerProjection.retained_complete line 337
35. theorem OAI.UniqueGamesTheorem.Soundness.PartnerProjection.freeBit_complete line 341
36. theorem OAI.UniqueGamesTheorem.Soundness.PartnerProjection.complete_coordinates line 345
37. theorem OAI.UniqueGamesTheorem.Soundness.PartnerProjection.retained_zero line 350
38. theorem OAI.UniqueGamesTheorem.Soundness.PartnerProjection.freeBit_zero line 353
39. theorem OAI.UniqueGamesTheorem.Soundness.PartnerProjection.complete_zero line 356
40. theorem OAI.UniqueGamesTheorem.Soundness.PartnerProjection.complete_kernel_add line 359
41. structure OAI.UniqueGamesTheorem.Soundness.PartnerProjection.SourcePoint line 366
42. structure OAI.UniqueGamesTheorem.Soundness.PartnerProjection.PartnerPoint line 371
43. theorem OAI.UniqueGamesTheorem.Soundness.PartnerProjection.source_ext line 379
44. theorem OAI.UniqueGamesTheorem.Soundness.PartnerProjection.partner_ext line 387
45. def OAI.UniqueGamesTheorem.Soundness.PartnerProjection.project line 397
46. def OAI.UniqueGamesTheorem.Soundness.PartnerProjection.lift line 406

    Source documentation

    The constructive preimage used in Lemma 6.1: choose the free bit to be zero.

    def lift (y : PartnerPoint rhs active) : SourcePoint rhs where
    …

    Mentions: OAI.UniqueGamesTheorem.Soundness.PartnerProjection.PartnerPoint, OAI.UniqueGamesTheorem.Soundness.PartnerProjection.SourcePoint

47. theorem OAI.UniqueGamesTheorem.Soundness.PartnerProjection.project_lift line 417
48. theorem OAI.UniqueGamesTheorem.Soundness.PartnerProjection.project_surjective line 430
49. theorem OAI.UniqueGamesTheorem.Soundness.PartnerProjection.homogeneous_preserved line 435
50. def OAI.UniqueGamesTheorem.Soundness.PartnerProjection.zeroSource line 438
51. def OAI.UniqueGamesTheorem.Soundness.PartnerProjection.zeroPartner line 443
52. def OAI.UniqueGamesTheorem.Soundness.PartnerProjection.addSource line 451
53. def OAI.UniqueGamesTheorem.Soundness.PartnerProjection.addPartner line 458
54. theorem OAI.UniqueGamesTheorem.Soundness.PartnerProjection.project_add line 475

    Source documentation

    The projection preserves F₂ addition, as well as zero.

    theorem project_add (x y : SourcePoint rhs) :
        project rhs active slot (addSource rhs x y) =
          addPartner rhs active (project rhs active slot x) (project rhs active slot y) := by
    …

    Mentions: OAI.UniqueGamesTheorem.Soundness.PartnerProjection.SourcePoint, OAI.UniqueGamesTheorem.Soundness.PartnerProjection.project, OAI.UniqueGamesTheorem.Soundness.PartnerProjection.addSource, OAI.UniqueGamesTheorem.Soundness.PartnerProjection.addPartner

55. theorem OAI.UniqueGamesTheorem.Soundness.PartnerProjection.project_zero line 485
56. def OAI.UniqueGamesTheorem.Soundness.PartnerProjection.InKernel line 494
57. theorem OAI.UniqueGamesTheorem.Soundness.PartnerProjection.kernel_characterization line 497
58. structure OAI.UniqueGamesTheorem.Soundness.PartnerProjection.ActiveBits line 524

    Source documentation

    One coefficient bit at every active position; all other coefficients vanish.

    structure ActiveBits where
    …

59. theorem OAI.UniqueGamesTheorem.Soundness.PartnerProjection.activeBits_ext line 528
60. def OAI.UniqueGamesTheorem.Soundness.PartnerProjection.addActiveBits line 535
61. def OAI.UniqueGamesTheorem.Soundness.PartnerProjection.kernelPoint line 542
62. theorem OAI.UniqueGamesTheorem.Soundness.PartnerProjection.kernelPoint_add line 547
63. theorem OAI.UniqueGamesTheorem.Soundness.PartnerProjection.kernelPoint_mem line 555
64. def OAI.UniqueGamesTheorem.Soundness.PartnerProjection.kernelCoefficients line 564
65. theorem OAI.UniqueGamesTheorem.Soundness.PartnerProjection.kernelPoint_coefficients line 572
66. theorem OAI.UniqueGamesTheorem.Soundness.PartnerProjection.coefficients_kernelPoint line 588
67. theorem OAI.UniqueGamesTheorem.Soundness.PartnerProjection.kernelPoint_injective line 595
68. theorem OAI.UniqueGamesTheorem.Soundness.PartnerProjection.kernel_unique_coefficients line 607

    Source documentation

    Every kernel vector is uniquely determined by one bit per active position.

    theorem kernel_unique_coefficients (x : SourcePoint rhs) (hx : InKernel rhs active slot x) :
        ∃ a : ActiveBits active, kernelPoint rhs active slot a = x ∧
          ∀ b : ActiveBits active, kernelPoint rhs active slot b = x → b = a := by
    …

    Mentions: OAI.UniqueGamesTheorem.Soundness.PartnerProjection.SourcePoint, OAI.UniqueGamesTheorem.Soundness.PartnerProjection.InKernel, OAI.UniqueGamesTheorem.Soundness.PartnerProjection.ActiveBits, OAI.UniqueGamesTheorem.Soundness.PartnerProjection.kernelPoint

69. def OAI.UniqueGamesTheorem.Soundness.PartnerProjection.extendActive line 617

    Source documentation

    Extend an arbitrary function on the active positions by zero.

    def extendActive (f : {j : Position // active j = true} → Bool) : ActiveBits active where
    …

    Mentions: OAI.UniqueGamesTheorem.Soundness.PartnerProjection.ActiveBits

70. theorem OAI.UniqueGamesTheorem.Soundness.PartnerProjection.kernel_realizes_active line 621
71. theorem OAI.UniqueGamesTheorem.Soundness.PartnerProjection.kernel_determined_by_active line 630
72. theorem OAI.UniqueGamesTheorem.Soundness.PartnerProjection.disjoint_kernels_intersection_zero line 648

    Source documentation

    The final assertion of Lemma 6.1, including arbitrary retained indices.

    theorem disjoint_kernels_intersection_zero
        (active' : Position → Bool) (slot' : Position → Slot)
        (hdisjoint : ∀ j, active j = true → active' j = false)
        (x : SourcePoint rhs)
        (hx : InKernel rhs active slot x)
        (hx' : InKernel rhs active' slot' x) : x = zeroSource rhs := by
    …

    Mentions: OAI.UniqueGamesTheorem.Soundness.PartnerProjection.Slot, OAI.UniqueGamesTheorem.Soundness.PartnerProjection.SourcePoint, OAI.UniqueGamesTheorem.Soundness.PartnerProjection.InKernel, OAI.UniqueGamesTheorem.Soundness.PartnerProjection.zeroSource

73. def OAI.UniqueGamesTheorem.Soundness.ConcreteExtraction.slotIndex line 678
74. def OAI.UniqueGamesTheorem.Soundness.ConcreteExtraction.tripleCoordinates line 683
75. theorem OAI.UniqueGamesTheorem.Soundness.ConcreteExtraction.parity_coordinates line 686
76. theorem OAI.UniqueGamesTheorem.Soundness.ConcreteExtraction.retained_coordinates line 689
77. def OAI.UniqueGamesTheorem.Soundness.ConcreteExtraction.fullPoint line 693
78. def OAI.UniqueGamesTheorem.Soundness.ConcreteExtraction.partnerPoint line 697
79. theorem OAI.UniqueGamesTheorem.Soundness.ConcreteExtraction.actual_projection_accepts line 703

    Source documentation

    Concrete projection acceptance implies the coordinate-level acceptance relation used to extract a repeated incidence strategy.

    theorem actual_projection_accepts
        {P O N : Type} (g : IncidenceExtraction.Incidence O N) (u : P → O)
        (active : P → Bool) (slot : P → PartnerProjection.Slot)
        (x : PartnerProjection.SourcePoint (fun j => g.rhs (u j)))
        (y : PartnerProjection.PartnerPoint (fun j => g.rhs (u j)) active)
        (hone : x.homogeneous = true)
        (hproject : PartnerProjection.project (fun j => g.rhs (u j)) active slot x = y) :
        IncidenceExtraction.AugmentedAccepts g u (fun j => active j = true)
          (fun j => slotIndex (slot j)) (fullPoint x) (partnerPoint y) := by
    …

    Mentions: OAI.UniqueGamesTheorem.Soundness.IncidenceExtraction.Incidence, OAI.UniqueGamesTheorem.Soundness.PartnerProjection.Slot, OAI.UniqueGamesTheorem.Soundness.PartnerProjection.SourcePoint, OAI.UniqueGamesTheorem.Soundness.PartnerProjection.PartnerPoint, OAI.UniqueGamesTheorem.Soundness.PartnerProjection.project, OAI.UniqueGamesTheorem.Soundness.IncidenceExtraction.AugmentedAccepts, OAI.UniqueGamesTheorem.Soundness.ConcreteExtraction.slotIndex, OAI.UniqueGamesTheorem.Soundness.ConcreteExtraction.fullPoint, OAI.UniqueGamesTheorem.Soundness.ConcreteExtraction.partnerPoint

80. theorem OAI.UniqueGamesTheorem.Soundness.ConcreteExtraction.actual_projection_implies_named_repetition line 726
81. abbrev OAI.UniqueGamesTheorem.Soundness.KernelCardinality.Kernel line 760
82. def OAI.UniqueGamesTheorem.Soundness.KernelCardinality.kernelEquiv line 763

    Source documentation

    Exactly one freely chosen bit per active position parametrizes the kernel.

    def kernelEquiv : Kernel rhs active slot ≃ ({j : P // active j = true} → Bool) where
    …

    Mentions: OAI.UniqueGamesTheorem.Soundness.KernelCardinality.Kernel

83. instance OAI.UniqueGamesTheorem.Soundness.KernelCardinality.kernelFintype line 778
84. theorem OAI.UniqueGamesTheorem.Soundness.KernelCardinality.kernel_card line 783

    Source documentation

    The actual kernel has 2^t points when there are t active positions.

    theorem kernel_card [Fintype P] :
        Fintype.card (Kernel rhs active slot) = 2 ^ Fintype.card {j : P // active j = true} := by
    …

    Mentions: OAI.UniqueGamesTheorem.Soundness.KernelCardinality.Kernel

85. theorem OAI.UniqueGamesTheorem.Soundness.KernelCardinality.kernel_card_of_active_card line 792