OAI/Computability/UniqueGames/PCP/ExpandersLemmas.lean

GitHub source file

60 declarations, 0 contain sorry, 0 declared as axioms

Finite existence of the Cayley expander base

The sample space is the actual finite type of indexed Boolean-cube generators. For each nonzero character, the checked sign sampling equivalence supplies its uniform word law. A finite union bound then selects a generator family whose nonconstant character biases are small. There is no random-graph hypothesis.

The fixed numbers below are manipulated symbolically; no enumeration of the generator sample space is executed. The subsequent square-and-zigzag family is a separate construction.

  1. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.Expanders.Generators line 36
  2. def OAI.UniqueGamesTheorem.Foundations.PCP.Expanders.badFrequency line 39

    Source documentation

    The zero character is excluded from the bad-event count.

    def badFrequency {n m : Nat} (g : Generators n m) (s : Cube (Fin n)) : ℝ :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.Expanders.Generators

  3. def OAI.UniqueGamesTheorem.Foundations.PCP.Expanders.badMass line 43
  4. theorem OAI.UniqueGamesTheorem.Foundations.PCP.Expanders.badFrequency_nonnegative line 46
  5. theorem OAI.UniqueGamesTheorem.Foundations.PCP.Expanders.mean_badFrequency_le line 51
  6. theorem OAI.UniqueGamesTheorem.Foundations.PCP.Expanders.mean_badMass_le line 63
  7. theorem OAI.UniqueGamesTheorem.Foundations.PCP.Expanders.exists_generators line 78

    Source documentation

    Actual finite generators with a simultaneous bound for every nonconstant Walsh character. The proof selects a point with bad-event count less than one.

    theorem exists_generators (n m : Nat) (hm : 3 * (n + 2) ≤ m) :
    ∃ g : Generators n m, ∀ s : Cube (Fin n),
      s ≠ zeroFrequency → |eigenvalue g s| ≤ (1 / 2 : ℝ) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.Expanders.Generators

  8. def OAI.UniqueGamesTheorem.Foundations.PCP.Expanders.baseDimension line 99
  9. def OAI.UniqueGamesTheorem.Foundations.PCP.Expanders.initialDegree line 100
  10. def OAI.UniqueGamesTheorem.Foundations.PCP.Expanders.initialQuarterDegree line 101
  11. def OAI.UniqueGamesTheorem.Foundations.PCP.Expanders.basePower line 102
  12. theorem OAI.UniqueGamesTheorem.Foundations.PCP.Expanders.base_arithmetic line 104
  13. theorem OAI.UniqueGamesTheorem.Foundations.PCP.Expanders.exists_initial_generators line 116
  14. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.Expanders.BaseVertex line 122
  15. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.Expanders.BasePort line 123
  16. def OAI.UniqueGamesTheorem.Foundations.PCP.Expanders.baseDegree line 124
  17. theorem OAI.UniqueGamesTheorem.Foundations.PCP.Expanders.card_basePort line 126
  18. theorem OAI.UniqueGamesTheorem.Foundations.PCP.Expanders.card_baseVertex line 131
  19. theorem OAI.UniqueGamesTheorem.Foundations.PCP.Expanders.exists_baseGraph line 138

    Source documentation

    A genuine finite regular graph with the exact degree/size relation needed for zigzag. Its spectral certificate follows from the actual generator witness.

    theorem exists_baseGraph :
    ∃ H : PoweringWalks.PortGraph BaseVertex BasePort,
      SpectralReturn.SpectralCertificate H (1 / 100 : ℝ) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PoweringWalks.PortGraph, OAI.UniqueGamesTheorem.Foundations.PCP.Expanders.BaseVertex, OAI.UniqueGamesTheorem.Foundations.PCP.Expanders.BasePort, OAI.UniqueGamesTheorem.Foundations.PCP.SpectralReturn.SpectralCertificate

  20. def OAI.UniqueGamesTheorem.Foundations.PCP.GraphTransport.reindex line 161
  21. theorem OAI.UniqueGamesTheorem.Foundations.PCP.GraphTransport.reindex_rot line 173
  22. theorem OAI.UniqueGamesTheorem.Foundations.PCP.GraphTransport.operator_reindex line 182
  23. theorem OAI.UniqueGamesTheorem.Foundations.PCP.GraphTransport.energy_reindex line 191
  24. theorem OAI.UniqueGamesTheorem.Foundations.PCP.GraphTransport.reindex_spectralCertificate line 197

    Source documentation

    A coordinate change preserves the actual spectral certificate, including the uniform measure on the port alphabet.

    theorem reindex_spectralCertificate (G : PortGraph V D) (vertices : V ≃ W)
    (ports : D ≃ E) (lambda : ℝ) (certificate : SpectralCertificate G lambda) :
    SpectralCertificate (reindex G vertices ports) lambda where
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.GraphTransport.reindex

  25. def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringWalks.lazyRotate line 228
  26. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringWalks.lazyRotate_involutive line 232
  27. def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringWalks.lazyGraph line 240
  28. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringWalks.lazyGraph_rot_false line 248
  29. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringWalks.lazyGraph_rot_true line 251
  30. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringLazy.operator_binomialMean line 262
  31. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringLazy.averagingOperator_lazy line 270
  32. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringLazy.iterate_lazy_eq_binomialMean line 283

    Source documentation

    The exact Boolean-tape mixture for the actual lazy transition operator.

    theorem iterate_lazy_eq_binomialMean [Fintype D] [Nonempty D]
    (G : PortGraph V D) (n : Nat) (f : V → ℝ) :
    iterateOperator (lazyGraph G) n f =
      fun v => LazySmoothing.binomialMean n (fun k => iterateOperator G k f v) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.LazySmoothing.binomialMean

  33. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringLazy.iterate_mem_Icc line 297
  34. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringLazy.lazy_endpoint_modal_transfer line 313

    Source documentation

    The modal lower bound survives every allowed nearby actual lazy length.

    theorem lazy_endpoint_modal_transfer [Fintype D] [Nonempty D]
    (G : PortGraph V D) (q M m : Nat) (hq : 1 ≤ q) (hM : 1 ≤ M)
    (hlo : (4 * q * M) ^ 2 - M ≤ m) (hhi : m ≤ (4 * q * M) ^ 2 + M)
    (f : V → ℝ) (hf : ∀ w, f w ∈ Set.Icc (0 : ℝ) 1) (v : V)
    (hmodal : 1 / (q : ℝ) ≤ iterateOperator (lazyGraph G) ((4 * q * M) ^ 2) f v) :
    1 / (2 * (q : ℝ)) ≤ iterateOperator (lazyGraph G) m f v := by
…
  35. theorem OAI.UniqueGamesTheorem.Foundations.PCP.LazySpectral.half_sum_sq_le line 337
  36. theorem OAI.UniqueGamesTheorem.Foundations.PCP.LazySpectral.lazy_energy_le_average line 342

    Source documentation

    Lazification averages the input and one actual graph step, so its energy is at most the corresponding average of the two energies.

    theorem lazy_energy_le_average [Fintype V] [Fintype D] [Nonempty D]
    (G : PortGraph V D) (f : V → ℝ) :
    energy (averagingOperator (lazyGraph G) f) ≤
      (energy f + energy (averagingOperator G f)) / 2 := by
…
  37. theorem OAI.UniqueGamesTheorem.Foundations.PCP.LazySpectral.lazy_energy_bound line 366

    Source documentation

    The concrete lazy graph inherits a squared-energy bound from an actual certificate for its underlying graph.

    theorem lazy_energy_bound [Fintype V] [Fintype D] [Nonempty D]
    (G : PortGraph V D) (lambda : ℝ) (hG : SpectralCertificate G lambda)
    (f : V → ℝ) (hf : mean f = 0) :
    energy (averagingOperator (lazyGraph G) f) ≤
      ((1 + lambda ^ 2) / 2) * energy f := by
…
  38. theorem OAI.UniqueGamesTheorem.Foundations.PCP.LazySpectral.lazy_certificate_31_32 line 381

    Source documentation

    An actual 7/8 certificate gives the stated 31/32 certificate after lazification: its intermediate squared-energy factor is 113/128.

    theorem lazy_certificate_31_32 [Fintype V] [Fintype D] [Nonempty D]
    (G : PortGraph V D) (hG : SpectralCertificate G (7 / 8)) :
    SpectralCertificate (lazyGraph G) (31 / 32) where
…
  39. def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringReturn.portConsEquiv line 403
  40. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringReturn.mean_word_cons_head line 416
  41. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringReturn.mean_word_cons_tail line 424
  42. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringReturn.iterateOperator_succ_right line 432
  43. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringReturn.mean_wordEnd line 439
  44. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringReturn.mean_pivot_endpoints line 461

    Source documentation

    Conditional endpoint factorization at an arbitrary fixed pivot dart.

    theorem mean_pivot_endpoints [Fintype D] [Nonempty D] (G : PortGraph V D) :
    ∀ (n : Nat) (k : Fin (n + 1)) (e : Edge V D) (φ ψ : V → ℝ),
      mean (fun r : Fin n → D =>
        φ (leftFromPivot G n k e.1 r) * ψ (rightFromPivot G n k e r)) =
        iterateOperator G k.val φ e.1 *
          iterateOperator G (n - k.val) ψ (next G e.1 e.2) := by
…
  45. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringReturn.mean_edge_endpoints line 504

    Source documentation

    The pivot and both endpoint opinions are averaged over actual walks.

    theorem mean_edge_endpoints [Fintype V] [Fintype D] [Nonempty D]
    (G : PortGraph V D) (n : Nat) (k : Fin (n + 1)) (φ ψ : Edge V D → V → ℝ) :
    mean (fun w : Walk V D (n + 1) =>
      φ (edgeAt G n w k) w.1 * ψ (edgeAt G n w k) (endpoint G w)) =
      mean (fun e : Edge V D =>
        iterateOperator G k.val (φ e) e.1 *
          iterateOperator G (n - k.val) (ψ e) (next G e.1 e.2)) := by
…
  46. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringReturn.bit_bool line 528
  47. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringReturn.mean_edge_bit line 531
  48. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringReturn.mean_marked_bit line 535
  49. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringReturn.edgeAt_zero line 545
  50. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringReturn.word_first_hit_mean line 549
  51. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringReturn.word_hit_mean line 560
  52. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringReturn.word_pair_hit_mean line 587
  53. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringReturn.hit_mean line 645
  54. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringReturn.pair_hit_mean line 661
  55. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringReturn.pair_event_mean line 682
  56. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringMomentBound.symmetric_gap_matrix_sum line 701
  57. def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringMomentBound.windowIndex line 756
  58. def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringMomentBound.windowEvent line 761
  59. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringMomentBound.window_second_moment_eq line 765
  60. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringMomentBound.window_second_moment_le line 791

    Source documentation

    All moment terms come from actual walk events; the only analytic input is the stated spectral contraction certificate of the given graph.

    theorem window_second_moment_le (G : PortGraph V D) (lambda : ℝ)
    (certificate : SpectralCertificate G lambda) (bad : V × D → Bool)
    (reversal : ∀ e, bad (G.rot e) = bad e)
    (n start m : Nat) (h : start + m ≤ n + 1) :
    mean (fun w => hits (windowEvent G bad n start m h) w ^ 2) ≤
      (m : ℝ) * edgeDensity bad *
        (1 + 2 / (1 - lambda) + ((m : ℝ) - 1) * edgeDensity bad) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PoweringMomentBound.windowEvent