OAI/Computability/MaxCut/Games/A4IndexCount.lean

GitHub source file

59 declarations, 0 contain sorry, 0 declared as axioms

The actual Appendix A.4 index encoding. Its kernel and range recover the two subspaces, and its quotient relation recovers the linear map. The final count follows from this injection into a genuine binary linear-map space.

  1. def OAI.MaxCutGames.Appendix.A4IndexCount.factorViaRange line 18
  2. theorem OAI.MaxCutGames.Appendix.A4IndexCount.factorViaRange_apply line 25
  3. theorem OAI.MaxCutGames.Appendix.A4IndexCount.factorViaRange_injective line 36
  4. theorem OAI.MaxCutGames.Appendix.A4IndexCount.factorViaRange_range line 54
  5. def OAI.MaxCutGames.Appendix.A4IndexCount.quotientRestriction line 71
  6. theorem OAI.MaxCutGames.Appendix.A4IndexCount.ker_quotientRestriction line 74
  7. def OAI.MaxCutGames.Appendix.A4IndexCount.aToRange line 80
  8. theorem OAI.MaxCutGames.Appendix.A4IndexCount.aToRange_surjective line 87
  9. def OAI.MaxCutGames.Appendix.A4IndexCount.encodeFixed line 95
  10. theorem OAI.MaxCutGames.Appendix.A4IndexCount.encodeFixed_relation line 102
  11. theorem OAI.MaxCutGames.Appendix.A4IndexCount.ker_encodeFixed line 115
  12. theorem OAI.MaxCutGames.Appendix.A4IndexCount.range_encodeFixed line 123
  13. theorem OAI.MaxCutGames.Appendix.A4IndexCount.recover_A0 line 131
  14. theorem OAI.MaxCutGames.Appendix.A4IndexCount.recover_B0 line 144
  15. theorem OAI.MaxCutGames.Appendix.A4IndexCount.encodeFixed_injective line 162
  16. def OAI.MaxCutGames.Appendix.A4IndexCount.Valid line 179
  17. abbrev OAI.MaxCutGames.Appendix.A4IndexCount.Index line 184
  18. abbrev OAI.MaxCutGames.Appendix.A4IndexCount.GeometricIndex line 187
  19. def OAI.MaxCutGames.Appendix.A4IndexCount.encode line 189
  20. theorem OAI.MaxCutGames.Appendix.A4IndexCount.encode_injective line 194
  21. theorem OAI.MaxCutGames.Appendix.A4IndexCount.card_index_le line 226
  22. theorem OAI.MaxCutGames.Appendix.A4IndexCount.card_geometricIndex_le line 236
  23. theorem OAI.MaxCutGames.Appendix.OperatorPartitions.indicator_eq_sum_of_unique_inline_OperatorPartitions line 258
  24. theorem OAI.MaxCutGames.Appendix.OperatorPartitions.spectralProjector_partition line 285
  25. theorem OAI.MaxCutGames.Appendix.OperatorPartitions.spectralProjector_restriction_projector line 299
  26. abbrev OAI.MaxCutGames.Appendix.OperatorPartitions.A4Geometry line 319
  27. abbrev OAI.MaxCutGames.Appendix.OperatorPartitions.A4GeometricIndex line 322
  28. def OAI.MaxCutGames.Appendix.OperatorPartitions.a4Mask line 325
  29. theorem OAI.MaxCutGames.Appendix.OperatorPartitions.a4Mask_unique line 331
  30. theorem OAI.MaxCutGames.Appendix.OperatorPartitions.a4Mask_implies_weak line 346
  31. theorem OAI.MaxCutGames.Appendix.OperatorPartitions.a4_projector_partition line 354
  32. def OAI.MaxCutGames.Appendix.OperatorPartitions.A5Geometry line 361
  33. abbrev OAI.MaxCutGames.Appendix.OperatorPartitions.A5GeometricIndex line 366
  34. def OAI.MaxCutGames.Appendix.OperatorPartitions.a5Mask line 370
  35. def OAI.MaxCutGames.Appendix.OperatorPartitions.a5OuterMask line 375
  36. theorem OAI.MaxCutGames.Appendix.OperatorPartitions.a5Mask_unique line 382
  37. theorem OAI.MaxCutGames.Appendix.OperatorPartitions.a5Mask_implies_outer line 399
  38. theorem OAI.MaxCutGames.Appendix.OperatorPartitions.a5_projector_partition line 410
  39. def OAI.MaxCutGames.Appendix.RestrictionTransport.nestedEmbedding line 446

    Source documentation

    Compose the two actual quotient-domain and target-subspace embeddings.

    def nestedEmbedding (A : Submodule F2 E) (B : Submodule F2 F)
    (C : Submodule F2 (E ⧸ A)) (D : Submodule F2 B) :
    Parameter C D →ₗ[F2] (E →ₗ[F2] F) :=
…
  40. theorem OAI.MaxCutGames.Appendix.RestrictionTransport.nestedEmbedding_injective line 451
  41. theorem OAI.MaxCutGames.Appendix.RestrictionTransport.exists_nested_embed_iff line 460

    Source documentation

    Exact effective annihilator and target of a nested restriction.

    theorem exists_nested_embed_iff (A : Submodule F2 E) (B : Submodule F2 F)
    (C : Submodule F2 (E ⧸ A)) (D : Submodule F2 B) (M : E →ₗ[F2] F) :
    (∃ N : Parameter C D, nestedEmbedding A B C D N = M) ↔
      C.comap A.mkQ ≤ M.ker ∧ M.range ≤ D.map B.subtype := by
…

    Mentions: OAI.MaxCutGames.Appendix.RestrictionTransport.nestedEmbedding

  42. theorem OAI.MaxCutGames.Appendix.RestrictionTransport.nested_range_eq line 512

    Source documentation

    Nested and effective direct restrictions describe exactly the same perturbations.

    theorem nested_range_eq (A : Submodule F2 E) (B : Submodule F2 F)
    (C : Submodule F2 (E ⧸ A)) (D : Submodule F2 B) :
    (nestedEmbedding A B C D).range =
      (embedding (C.comap A.mkQ) (D.map B.subtype)).range := by
…

    Mentions: OAI.MaxCutGames.Appendix.RestrictionTransport.nestedEmbedding

  43. theorem OAI.MaxCutGames.Appendix.RestrictionTransport.exists_range_preimage_inline_RestrictionTransport line 529
  44. def OAI.MaxCutGames.Appendix.RestrictionTransport.sameRangeEquiv line 533

    Source documentation

    The actual linear change of parameters between two injective presentations.

    def sameRangeEquiv (f : P →ₗ[K] G) (g : Q →ₗ[K] G)
    (hf : Function.Injective f) (hg : Function.Injective g)
    (h : f.range = g.range) : P ≃ₗ[K] Q := by
…
  45. theorem OAI.MaxCutGames.Appendix.RestrictionTransport.sameRangeEquiv_commutes line 563
  46. theorem OAI.MaxCutGames.Appendix.RestrictionTransport.expect_eq_of_same_range line 572

    Source documentation

    Injective parameter changes preserve normalized uniform expectations.

    theorem expect_eq_of_same_range (f : P →ₗ[K] G) (g : Q →ₗ[K] G)
    (hf : Function.Injective f) (hg : Function.Injective g)
    (h : f.range = g.range) (observable : G → ℝ) :
    (𝔼 x, observable (f x)) = 𝔼 y, observable (g y) := by
…
  47. theorem OAI.MaxCutGames.Appendix.RestrictionTransport.restriction_secondMoment_eq_of_same_range line 580

    Source documentation

    Preserve second moments at the same full ambient translate.

    theorem restriction_secondMoment_eq_of_same_range
    (f : P →ₗ[K] G) (g : Q →ₗ[K] G)
    (hf : Function.Injective f) (hg : Function.Injective g)
    (h : f.range = g.range) (observable : G → ℝ) (T : G) :
    (𝔼 x, observable (T + f x) ^ 2) = 𝔼 y, observable (T + g y) ^ 2 :=
…
  48. theorem OAI.MaxCutGames.Appendix.RestrictionTransport.restriction_energySquare_average_eq_of_same_range line 588

    Source documentation

    Preserve the outer mean of squared restriction energies, with the square outside.

    theorem restriction_energySquare_average_eq_of_same_range [Fintype G]
    (f : P →ₗ[K] G) (g : Q →ₗ[K] G)
    (hf : Function.Injective f) (hg : Function.Injective g)
    (h : f.range = g.range) (observable : G → ℝ) :
    (𝔼 T, (𝔼 x, observable (T + f x) ^ 2) ^ 2) =
      𝔼 T, (𝔼 y, observable (T + g y) ^ 2) ^ 2 := by
…
  49. theorem OAI.MaxCutGames.Appendix.RestrictionTransport.nested_restriction_secondMoment_eq line 607

    Source documentation

    The genuine nested affine restriction has the effective direct second moment.

    theorem nested_restriction_secondMoment_eq
    (A : Submodule F2 E) (B : Submodule F2 F)
    (C : Submodule F2 (E ⧸ A)) (D : Submodule F2 B)
    (h : (E →ₗ[F2] F) → ℝ) (T : E →ₗ[F2] F) :
    (𝔼 N, h (T + nestedEmbedding A B C D N) ^ 2) =
      𝔼 M, h (T + embed (C.comap A.mkQ) (D.map B.subtype) M) ^ 2 := by
…

    Mentions: OAI.MaxCutGames.Appendix.RestrictionTransport.nestedEmbedding

  50. theorem OAI.MaxCutGames.Appendix.RestrictionTransport.nested_restriction_energySquare_average_eq line 630

    Source documentation

    Squared normalized energies also agree before averaging over the full translate.

    theorem nested_restriction_energySquare_average_eq [Fintype (E →ₗ[F2] F)]
    (A : Submodule F2 E) (B : Submodule F2 F)
    (C : Submodule F2 (E ⧸ A)) (D : Submodule F2 B)
    (h : (E →ₗ[F2] F) → ℝ) :
    (𝔼 T, (𝔼 N, h (T + nestedEmbedding A B C D N) ^ 2) ^ 2) =
      𝔼 T, (𝔼 M, h (T + embed (C.comap A.mkQ) (D.map B.subtype) M) ^ 2) ^ 2 := by
…

    Mentions: OAI.MaxCutGames.Appendix.RestrictionTransport.nestedEmbedding

  51. theorem OAI.MaxCutGames.Appendix.LinearIdentities.a5_preimage_eq_ker line 648

    Source documentation

    A subspace disjoint from the image has exactly the original kernel as preimage.

    theorem a5_preimage_eq_ker (X : W →ₗ[K] V) (A₀ : Submodule K V)
    (hd : Disjoint A₀ (LinearMap.range X)) : A₀.comap X = LinearMap.ker X := by
…
  52. theorem OAI.MaxCutGames.Appendix.LinearIdentities.a5_range_domRestrict_eq_of_cover line 660

    Source documentation

    Restricting to a subspace that covers the domain modulo the kernel preserves the image.

    theorem a5_range_domRestrict_eq_of_cover (X : W →ₗ[K] V) (B₀ : Submodule K W)
    (hc : B₀ ⊔ LinearMap.ker X = ⊤) :
    LinearMap.range (X.domRestrict B₀) = LinearMap.range X := by
…
  53. theorem OAI.MaxCutGames.Appendix.LinearIdentities.a5_effective_annihilator line 672

    Source documentation

    The A.5 compressed image pulls back to its exact effective annihilator.

    theorem a5_effective_annihilator (X : W →ₗ[K] V)
    (A₀ A : Submodule K V) (B₀ : Submodule K W)
    (hA : A₀ ⊔ LinearMap.range X = A)
    (hc : B₀ ⊔ LinearMap.ker X = ⊤) :
    (LinearMap.range (compress X A₀ B₀)).comap A₀.mkQ = A := by
…

    Mentions: OAI.MaxCutGames.Appendix.LinearIdentities.compress

  54. theorem OAI.MaxCutGames.Appendix.LinearIdentities.a5_effective_codomain line 681

    Source documentation

    The A.5 compressed kernel maps to its exact effective codomain.

    theorem a5_effective_codomain (X : W →ₗ[K] V)
    (A₀ : Submodule K V) (B B₀ : Submodule K W)
    (hd : Disjoint A₀ (LinearMap.range X))
    (hB : B₀ ⊓ LinearMap.ker X = B) :
    (LinearMap.ker (compress X A₀ B₀)).map B₀.subtype = B := by
…

    Mentions: OAI.MaxCutGames.Appendix.LinearIdentities.compress

  55. theorem OAI.MaxCutGames.Appendix.HybridComposition.effective_hybrid_iff line 722
  56. theorem OAI.MaxCutGames.Appendix.HybridComposition.nested_hybridDerivative_energy line 764
  57. theorem OAI.MaxCutGames.Appendix.HybridComposition.nested_hybridDerivative_energySquare_average line 793
  58. theorem OAI.MaxCutGames.Appendix.HybridComposition.finrank_comap_mkQ line 806
  59. theorem OAI.MaxCutGames.Appendix.HybridComposition.order_effective line 852