OAI/Computability/UniqueGames/PCP/ExpanderTables.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTables.rowIndex line 12
  2. theorem OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTables.rowIndex_val line 14
  3. structure OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTables.Table line 18

    Source documentation

    Stored reverse-dart indices, with a proof of the finite involution law.

    structure Table (v d : Nat) where
…
  4. def OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTables.reverseIndex line 22
  5. def OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTables.lookup line 25
  6. theorem OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTables.lookup_involutive line 28
  7. def OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTables.graph line 35
  8. theorem OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTables.graph_rot line 39
  9. def OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTables.ofGraph line 42
  10. theorem OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTables.lookup_ofGraph line 50
  11. theorem OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTables.graph_ext line 55
  12. theorem OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTables.graph_ofGraph line 63
  13. theorem OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTables.row_count line 66
  14. def OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTables.vertexIndex line 70

    Source documentation

    Explicit mixed-radix vertex coordinates for one square/zigzag step.

    def vertexIndex (v q : Nat) : Fin v × (Fin q × Fin q) ≃ Fin (v * (q * q)) :=
…
  15. def OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTables.stepGraph line 74

    Source documentation

    The actual square/zigzag graph, expressed in the table's integer coordinates.

    def stepGraph {v d : Nat} (G : Table v (d * d))
    (H : Table ((d * d) * (d * d)) d) :
    PortGraph (Fin (v * ((d * d) * (d * d)))) (Fin (d * d)) :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTables.Table

  16. def OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTables.step line 83

    Source documentation

    Materialize every row of the next table in the declared order.

    def step {v d : Nat} (G : Table v (d * d))
    (H : Table ((d * d) * (d * d)) d) :
    Table (v * ((d * d) * (d * d))) (d * d) := ofGraph (stepGraph G H)

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTables.ofGraph, OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTables.stepGraph

  17. def OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTables.stepLookup line 88

    Source documentation

    A row uses exactly the displayed four lookups in already stored tables.

    def stepLookup {v d : Nat} (G : Table v (d * d))
    (H : Table ((d * d) * (d * d)) d)
    (x : Fin (v * ((d * d) * (d * d))) × Fin (d * d)) :
    Fin (v * ((d * d) * (d * d))) × Fin (d * d) :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTables.Table

  18. theorem OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTables.lookup_step line 102
  19. theorem OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTables.step_certificate line 114
  20. def OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTables.initial line 125
  21. theorem OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTables.initial_certificate line 128
  22. def OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTables.vertexCount line 138
  23. theorem OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTables.vertexCount_eq line 142
  24. theorem OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTables.vertexCount_positive line 147
  25. def OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTables.family line 154

    Source documentation

    A bottom-up vector of rotation rows. The recursive result is passed once to step, whose row formula reads only that already materialized table.

    def family {d : Nat} (H : Table ((d * d) * (d * d)) d) :
    (n : Nat) → Table (vertexCount (d * d) n) (d * d)
  | 0 => initial d
  | n + 1 => step (family H n) H

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTables.vertexCount, OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTables.initial, OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTables.step

  26. theorem OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTables.family_certificate line 159
  27. theorem OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTables.family_row_count line 170
  28. theorem OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTables.exists_base_table line 175

    Source documentation

    The only selected data is one fixed finite table, independent of the input.

    theorem exists_base_table : ∃ H : Table
    ((Expanders.baseDegree * Expanders.baseDegree) *
      (Expanders.baseDegree * Expanders.baseDegree)) Expanders.baseDegree,
    SpectralCertificate (graph H) (1 / 100 : ℝ) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.Expanders.baseDegree, OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTables.graph