A5ReverseIndex.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.UniqueGamesTheorem.Appendix.A5ReverseIndex.EarlierA line 21
Source documentation
Earlier codomain constraints inside the final codomain constraint.
```
abbrev EarlierA (A' : Submodule F2 V) (i : ℕ) :=
…
```
abbrev OAI.UniqueGamesTheorem.Appendix.A5ReverseIndex.EarlierB line 25
Source documentation
Earlier retained domains containing the final retained domain.
```
abbrev EarlierB (B' : Submodule F2 W) (j : ℕ) :=
…
```

def OAI.UniqueGamesTheorem.Appendix.A5ReverseIndex.frequencyEquiv line 30

Source documentation

Natural frequency coordinates for an earlier pair inside a fixed final pair. This is a change of domain and codomain separately.

def frequencyEquiv (A A' : Submodule F2 V) (B' B : Submodule F2 W)
    (hA : A ≤ A') (hB : B' ≤ B) :
    (B' →ₗ[F2] (V ⧸ A')) ≃ₗ[F2]
      ((B'.comap B.subtype) →ₗ[F2] ((V ⧸ A) ⧸ A'.map A.mkQ)) :=
…

def OAI.UniqueGamesTheorem.Appendix.A5ReverseIndex.relativeFrequency line 38
theorem OAI.UniqueGamesTheorem.Appendix.A5ReverseIndex.relativeFrequency_rank line 42
abbrev OAI.UniqueGamesTheorem.Appendix.A5ReverseIndex.Ancestor line 52
Source documentation
The exact reverse fiber after the earlier dimensions are fixed.
```
abbrev Ancestor (A' : Submodule F2 V) (B' : Submodule F2 W)
    (Y : B' →ₗ[F2] (V ⧸ A')) (i j : ℕ) :=
…
```
theorem OAI.UniqueGamesTheorem.Appendix.A5ReverseIndex.relative_codomain_dimension line 60
theorem OAI.UniqueGamesTheorem.Appendix.A5ReverseIndex.relative_domain_codimension_le line 69

theorem OAI.UniqueGamesTheorem.Appendix.A5ReverseIndex.card_local_antecedent_le line 80

Source documentation

Each fixed earlier pair contributes at most two graph-parameter budgets.

theorem card_local_antecedent_le (A A' : Submodule F2 V)
    (B' B : Submodule F2 W) (hA : A ≤ A') (hB : B' ≤ B)
    (Y : B' →ₗ[F2] (V ⧸ A')) (d k : ℕ)
    (hY : Module.finrank F2 Y.range ≤ k)
    (hAd : Module.finrank F2 A' ≤ d)
    (hBd : Module.finrank F2 (W ⧸ B') ≤ d) :
    Nat.card (AntecedentCount.Antecedent
      (B'.comap B.subtype) (A'.map A.mkQ)
      (relativeFrequency A A' B' B hA hB Y)) ≤ 2 ^ (2 * d * k) := by
…

Mentions: OAI.UniqueGamesTheorem.Appendix.AntecedentCount.Antecedent, OAI.UniqueGamesTheorem.Appendix.A5ReverseIndex.relativeFrequency

theorem OAI.UniqueGamesTheorem.Appendix.A5ReverseIndex.card_sigma_le line 104

theorem OAI.UniqueGamesTheorem.Appendix.A5ReverseIndex.card_ancestor_le line 117

Source documentation

Sharp graph-based upper bound for the entire actual reverse fiber.

theorem card_ancestor_le (A' : Submodule F2 V) (B' : Submodule F2 W)
    (Y : B' →ₗ[F2] (V ⧸ A')) (d i j k : ℕ)
    (hY : Module.finrank F2 Y.range ≤ k)
    (hA : Module.finrank F2 A' ≤ d)
    (hB : Module.finrank F2 (W ⧸ B') ≤ d) :
    Nat.card (Ancestor A' B' Y i j) ≤ 2 ^ (d * (i + j) + 2 * d * k) := by
…

Mentions: OAI.UniqueGamesTheorem.Appendix.A5ReverseIndex.Ancestor

theorem OAI.UniqueGamesTheorem.Appendix.A5ReverseIndex.card_ancestor_le_source line 146