OAI/Computability/UniqueGames/Analysis/DegreeCover.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.UniqueGamesTheorem.Appendix.DegreeCover.F2 line 14
2. theorem OAI.UniqueGamesTheorem.Appendix.DegreeCover.binary_add_self line 18
3. theorem OAI.UniqueGamesTheorem.Appendix.DegreeCover.binary_neg line 22
4. theorem OAI.UniqueGamesTheorem.Appendix.DegreeCover.exists_glue_zero line 27

   Source documentation

   Glue a linear map on P to zero on Q when the restrictions agree.

   theorem exists_glue_zero (P Q : Submodule F2 W) (f : W →ₗ[F2] V)
       (cover : P ⊔ Q = ⊤) (compatible : ∀ w ∈ P, w ∈ Q → f w = 0) :
       ∃ g : W →ₗ[F2] V,
         (∀ w ∈ P, g w = f w) ∧ (∀ w ∈ Q, g w = 0) := by
   …

   Mentions: OAI.UniqueGamesTheorem.Appendix.DegreeCover.F2

5. theorem OAI.UniqueGamesTheorem.Appendix.DegreeCover.binary_cross line 49
6. theorem OAI.UniqueGamesTheorem.Appendix.DegreeCover.exists_cover_component line 57
7. theorem OAI.UniqueGamesTheorem.Appendix.DegreeCover.exists_disjoint_decomposition line 97

   Source documentation

   A general, dimension-free decomposition with pairwise disjoint images. These are exactly the linear-algebra data used to establish the cover in A.1.

   theorem exists_disjoint_decomposition (Y Z : W →ₗ[F2] V)
       (triple : (LinearMap.range (Y + Z) ⊓ LinearMap.range Y) ⊓ LinearMap.range Z = ⊥)
       (cover : LinearMap.ker (Y + Z) ⊔ LinearMap.ker Y ⊔ LinearMap.ker Z = ⊤) :
       ∃ R S C : W →ₗ[F2] V,
         Y + Z = R + S ∧ Y = R + C ∧ Z = S + C ∧
         Disjoint (LinearMap.range R) (LinearMap.range S) ∧
         Disjoint (LinearMap.range R) (LinearMap.range C) ∧
         Disjoint (LinearMap.range S) (LinearMap.range C) ∧
         LinearMap.range R ≤ LinearMap.range (Y + Z) ⊓ LinearMap.range Y ∧
         LinearMap.range S ≤ LinearMap.range (Y + Z) ⊓ LinearMap.range Z ∧
         LinearMap.range C ≤ LinearMap.range Y ⊓ LinearMap.range Z := by
   …

   Mentions: OAI.UniqueGamesTheorem.Appendix.DegreeCover.F2

8. theorem OAI.UniqueGamesTheorem.Appendix.DegreeCover.rank_add_of_disjoint line 160

   Source documentation

   Rank additivity needs image containment as well as disjointness.

   theorem rank_add_of_disjoint [FiniteDimensional F2 V] (R S : W →ₗ[F2] V)
       (hd : Disjoint (LinearMap.range R) (LinearMap.range S))
       (hR : LinearMap.range R ≤ LinearMap.range (R + S))
       (hS : LinearMap.range S ≤ LinearMap.range (R + S)) :
       Module.finrank F2 (LinearMap.range (R + S)) =
         Module.finrank F2 (LinearMap.range R) + Module.finrank F2 (LinearMap.range S) := by
   …

   Mentions: OAI.UniqueGamesTheorem.Appendix.DegreeCover.F2

9. theorem OAI.UniqueGamesTheorem.Appendix.DegreeCover.outside_bad_rank_cover line 175

   Source documentation

   The cover F(X) \ F₂(X) ⊆ F₁(X), with all three rank-additive decompositions. There is no bound on dimension, and both bad-event exclusions are discharged.

   theorem outside_bad_rank_cover [FiniteDimensional F2 V] (Y Z : W →ₗ[F2] V)
       (triple : (LinearMap.range (Y + Z) ⊓ LinearMap.range Y) ⊓ LinearMap.range Z = ⊥)
       (cover : LinearMap.ker (Y + Z) ⊔ LinearMap.ker Y ⊔ LinearMap.ker Z = ⊤) :
       ∃ R S C : W →ₗ[F2] V,
         Y + Z = R + S ∧ Y = R + C ∧ Z = S + C ∧
         Module.finrank F2 (LinearMap.range (Y + Z)) =
           Module.finrank F2 (LinearMap.range R) + Module.finrank F2 (LinearMap.range S) ∧
         Module.finrank F2 (LinearMap.range Y) =
           Module.finrank F2 (LinearMap.range R) + Module.finrank F2 (LinearMap.range C) ∧
         Module.finrank F2 (LinearMap.range Z) =
           Module.finrank F2 (LinearMap.range S) + Module.finrank F2 (LinearMap.range C) := by
   …

   Mentions: OAI.UniqueGamesTheorem.Appendix.DegreeCover.F2