OAI/Computability/MaxCut/Games/SplitMaps.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Actual splitting of linear-map questions and their uniform laws.

  1. def OAI.MaxCutGames.Fourier.SplitMaps.codomainSplit line 21

    Source documentation

    A question into the symbol/perpendicular product is exactly a pair of independent coordinate questions.

    def codomainSplit : (E →ₗ[K] C × D) ≃ₗ[K] (E →ₗ[K] C) × (E →ₗ[K] D) :=
…
  2. def OAI.MaxCutGames.Fourier.SplitMaps.domainSplit line 25

    Source documentation

    A dual Fourier index on a product is exactly its two restrictions.

    def domainSplit : (C × D →ₗ[K] E) ≃ₗ[K] (C →ₗ[K] E) × (D →ₗ[K] E) :=
…
  3. theorem OAI.MaxCutGames.Fourier.SplitMaps.codomainSplit_symm_apply line 28
  4. theorem OAI.MaxCutGames.Fourier.SplitMaps.domainSplit_symm_apply line 31
  5. theorem OAI.MaxCutGames.Fourier.SplitMaps.expect_codomain_product line 34
  6. theorem OAI.MaxCutGames.Fourier.SplitMaps.expect_domain_product line 44
  7. theorem OAI.MaxCutGames.Fourier.SplitMaps.sum_domain_product line 56