OAI/Computability/UniqueGames/Analysis/HybridCounting.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Frequency-conditioned counts of actual Hybrid pairs and derivative indices.

  1. theorem OAI.UniqueGamesTheorem.Appendix.HybridCounting.comap_subtype_injective line 16
  2. theorem OAI.UniqueGamesTheorem.Appendix.HybridCounting.map_quotient_injective line 29
  3. theorem OAI.UniqueGamesTheorem.Appendix.HybridCounting.finite_submodules line 47
  4. theorem OAI.UniqueGamesTheorem.Appendix.HybridCounting.card_hybrid_pairs_le line 57

    Source documentation

    All actual Hybrid pairs for this frequency, with no ambient-dimension factor.

    theorem card_hybrid_pairs_le (Y : F →ₗ[F2] E) (d : ℕ)
    (hY : finrank F2 Y.range ≤ d) :
    Nat.card {p : Submodule F2 E × Submodule F2 F //
      LinearIdentities.Hybrid Y p.1 p.2} ≤ 2 ^ (2 * d * d) := by
…

    Mentions: OAI.UniqueGamesTheorem.Appendix.LinearIdentities.Hybrid

  5. theorem OAI.UniqueGamesTheorem.Appendix.HybridCounting.card_hybridIndex_le_two line 101

    Source documentation

    The actual order-bounded index subtype injects into the conditioned pairs.

    theorem card_hybridIndex_le_two (Y : F →ₗ[F2] E) (d : ℕ)
    (hY : finrank F2 Y.range ≤ d) :
    Nat.card {s : Derivatives.HybridIndex (E := E) (F := F) d //
…

    Mentions: OAI.UniqueGamesTheorem.Appendix.Derivatives.HybridIndex

  6. theorem OAI.UniqueGamesTheorem.Appendix.HybridCounting.card_hybridIndex_le line 120