OAI/Computability/MaxCut/PCP/Overlay.lean

GitHub source file

72 declarations, 0 contain sorry, 0 declared as axioms

Overlay a regular constraint graph with an actual regular port graph whose new constraints always accept. The port sets are disjoint, so all original rejected darts are retained exactly. The averaging operator is the actual degree-weighted mixture of the two graph averages.

  1. def OAI.MaxCutGames.Foundations.PCP.Overlay.originalPortGraph line 23
  2. def OAI.MaxCutGames.Foundations.PCP.Overlay.rotate line 27
  3. theorem OAI.MaxCutGames.Foundations.PCP.Overlay.rotate_involutive line 32
  4. def OAI.MaxCutGames.Foundations.PCP.Overlay.portGraph line 41
  5. theorem OAI.MaxCutGames.Foundations.PCP.Overlay.portGraph_rot_inl line 49
  6. theorem OAI.MaxCutGames.Foundations.PCP.Overlay.portGraph_rot_inr line 54
  7. def OAI.MaxCutGames.Foundations.PCP.Overlay.constraintGraph line 60

    Source documentation

    Keep the original tests and add always-accepting tests on the overlay ports.

    def constraintGraph (G : ConstraintGraph V (V × D) A) (H : PortGraph V E) :
    ConstraintGraph V (V × (D ⊕ E)) A where
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.ConstraintGraph

  8. theorem OAI.MaxCutGames.Foundations.PCP.Overlay.constraintGraph_tail line 74
  9. theorem OAI.MaxCutGames.Foundations.PCP.Overlay.constraintGraph_portGraph line 77
  10. theorem OAI.MaxCutGames.Foundations.PCP.Overlay.edgeSatisfied_inl line 81
  11. theorem OAI.MaxCutGames.Foundations.PCP.Overlay.edgeSatisfied_inr line 91
  12. theorem OAI.MaxCutGames.Foundations.PCP.Overlay.complete line 95
  13. theorem OAI.MaxCutGames.Foundations.PCP.Overlay.satisfiable_iff line 105
  14. theorem OAI.MaxCutGames.Foundations.PCP.Overlay.rejectionCount_eq line 118

    Source documentation

    Every labeling rejects exactly the same number of darts before and after overlay.

    theorem rejectionCount_eq [Fintype V] [Fintype D] [Fintype E]
    (G : ConstraintGraph V (V × D) A) (H : PortGraph V E)
    (htail : G.tail = Prod.fst) (labeling : V → A) :
    (constraintGraph G H).rejectionCount labeling = G.rejectionCount labeling := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.ConstraintGraph, OAI.MaxCutGames.Foundations.PCP.Overlay.constraintGraph

  15. theorem OAI.MaxCutGames.Foundations.PCP.Overlay.card_ports line 127
  16. theorem OAI.MaxCutGames.Foundations.PCP.Overlay.card_darts line 130
  17. theorem OAI.MaxCutGames.Foundations.PCP.Overlay.operator_mix line 139

    Source documentation

    The normalized graph average weights the components by their actual port counts.

    theorem operator_mix [Nonempty D] [Nonempty E]
    (G : PortGraph V D) (H : PortGraph V E) (f : V → ℝ) (v : V) :
    averagingOperator (portGraph G H) f v =
      (Fintype.card D : ℝ) / ((Fintype.card D : ℝ) + Fintype.card E) *
        averagingOperator G f v +
      (Fintype.card E : ℝ) / ((Fintype.card D : ℝ) + Fintype.card E) *
        averagingOperator H f v := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.Overlay.portGraph

  18. theorem OAI.MaxCutGames.Foundations.PCP.Overlay.energy_convex_mix line 159

    Source documentation

    Convexity of the squared energy, proved pointwise before taking the finite mean.

    theorem energy_convex_mix (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1)
    (f g : V → ℝ) :
    energy (fun v => a * f v + b * g v) ≤ a * energy f + b * energy g := by
…
  19. theorem OAI.MaxCutGames.Foundations.PCP.Overlay.energy_bound line 176

    Source documentation

    Actual overlay contraction from the supplied graph's spectral bound and the proved energy contraction of an arbitrary reversible regular graph.

    theorem energy_bound [Nonempty V] [Nonempty D] [Nonempty E]
    (G : PortGraph V D) (H : PortGraph V E) (lambda : ℝ)
    (certificate : SpectralCertificate H lambda) (f : V → ℝ) (hf : mean f = 0) :
    energy (averagingOperator (portGraph G H) f) ≤
      ((Fintype.card D : ℝ) + (Fintype.card E : ℝ) * lambda ^ 2) /
        ((Fintype.card D : ℝ) + Fintype.card E) * energy f := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.Overlay.portGraph

  20. theorem OAI.MaxCutGames.Foundations.PCP.Overlay.energy_bound_three_quarters line 213

    Source documentation

    With one more original port than overlay ports, a half-spectral overlay has squared contraction at most three quarters.

    theorem energy_bound_three_quarters [Nonempty V]
    (G : PortGraph V D) (H : PortGraph V E)
    (hdegree : Fintype.card D = Fintype.card E + 1) (hpositive : 1 ≤ Fintype.card E)
    (certificate : SpectralCertificate H (1 / 2 : ℝ))
    (f : V → ℝ) (hf : mean f = 0) :
    energy (averagingOperator (portGraph G H) f) ≤ (3 / 4 : ℝ) * energy f := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.Overlay.portGraph

  21. theorem OAI.MaxCutGames.Foundations.PCP.Overlay.spectralCertificate_seven_eighths line 232
  22. theorem OAI.MaxCutGames.Foundations.PCP.Overlay.constraintGraph_spectralCertificate line 246

    Source documentation

    The certificate belongs to the exact underlying graph of the overlaid constraints.

    theorem constraintGraph_spectralCertificate [Nonempty V]
    (G : ConstraintGraph V (V × D) A) (H : PortGraph V E)
    (hdegree : Fintype.card D = Fintype.card E + 1) (hpositive : 1 ≤ Fintype.card E)
    (certificate : SpectralCertificate H (1 / 2 : ℝ)) :
    SpectralCertificate (originalPortGraph (constraintGraph G H)) (7 / 8 : ℝ) := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.ConstraintGraph, OAI.MaxCutGames.Foundations.PCP.Overlay.originalPortGraph, OAI.MaxCutGames.Foundations.PCP.Overlay.constraintGraph

  23. def OAI.MaxCutGames.Foundations.PCP.LazySmoothing.bitCount line 266
  24. def OAI.MaxCutGames.Foundations.PCP.LazySmoothing.binomialMean line 269
  25. def OAI.MaxCutGames.Foundations.PCP.LazySmoothing.splitTape line 272
  26. theorem OAI.MaxCutGames.Foundations.PCP.LazySmoothing.bitCount_succ line 280
  27. theorem OAI.MaxCutGames.Foundations.PCP.LazySmoothing.mean_congr line 284
  28. theorem OAI.MaxCutGames.Foundations.PCP.LazySmoothing.mean_const line 289
  29. theorem OAI.MaxCutGames.Foundations.PCP.LazySmoothing.mean_add line 292
  30. theorem OAI.MaxCutGames.Foundations.PCP.LazySmoothing.mean_sub line 296
  31. theorem OAI.MaxCutGames.Foundations.PCP.LazySmoothing.mean_mul line 300
  32. theorem OAI.MaxCutGames.Foundations.PCP.LazySmoothing.mean_zero line 304
  33. theorem OAI.MaxCutGames.Foundations.PCP.LazySmoothing.expect_bool line 307
  34. theorem OAI.MaxCutGames.Foundations.PCP.LazySmoothing.mean_succ line 311
  35. def OAI.MaxCutGames.Foundations.PCP.LazySmoothing.score line 322
  36. def OAI.MaxCutGames.Foundations.PCP.LazySmoothing.scoreMean line 324
  37. theorem OAI.MaxCutGames.Foundations.PCP.LazySmoothing.scoreMean_zero line 327
  38. theorem OAI.MaxCutGames.Foundations.PCP.LazySmoothing.scoreMean_succ line 330
  39. theorem OAI.MaxCutGames.Foundations.PCP.LazySmoothing.score_identity line 350

    Source documentation

    Exact finite integration by parts for the fair Boolean-tape law.

    theorem score_identity (n : ℕ) (g : ℕ → ℝ) :
    scoreMean (n + 1) g = ((n : ℝ) + 1) / 2 *
      (binomialMean n g - binomialMean n (fun k => g (k + 1))) := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.LazySmoothing.scoreMean, OAI.MaxCutGames.Foundations.PCP.LazySmoothing.binomialMean

  40. theorem OAI.MaxCutGames.Foundations.PCP.LazySmoothing.score_mean_zero line 360
  41. theorem OAI.MaxCutGames.Foundations.PCP.LazySmoothing.score_second_moment line 368

    Source documentation

    The score variance is proved from the actual tape distribution.

    theorem score_second_moment (n : ℕ) :
    binomialMean n (fun k => score n k ^ 2) = (n : ℝ) := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.LazySmoothing.binomialMean, OAI.MaxCutGames.Foundations.PCP.LazySmoothing.score

  42. theorem OAI.MaxCutGames.Foundations.PCP.LazySmoothing.score_difference line 387
  43. theorem OAI.MaxCutGames.Foundations.PCP.LazySmoothing.adjacent_difference_sq line 395

    Source documentation

    Cauchy--Schwarz yields an adjacent-length bound without any support or small-parameter caveat. The square form avoids introducing square roots.

    theorem adjacent_difference_sq (n : ℕ) (g : ℕ → ℝ)
    (hg : ∀ k, 0 ≤ g k ∧ g k ≤ 1) :
    4 * ((n : ℝ) + 1) *
      (binomialMean n g - binomialMean (n + 1) g) ^ 2 ≤ 1 := by
…

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

  44. theorem OAI.MaxCutGames.Foundations.PCP.LazySmoothing.adjacent_difference_le line 429
  45. theorem OAI.MaxCutGames.Foundations.PCP.LazySmoothing.mean_shift_le line 442
  46. theorem OAI.MaxCutGames.Foundations.PCP.LazySmoothing.mean_ordered_difference_le line 461
  47. theorem OAI.MaxCutGames.Foundations.PCP.LazySmoothing.mean_window_le line 467
  48. theorem OAI.MaxCutGames.Foundations.PCP.LazySmoothing.square_window_le line 490

    Source documentation

    A convenient square center for a fixed alphabet.

    theorem square_window_le (q M m : ℕ) (hq : 1 ≤ q) (hM : 1 ≤ M)
    (hlo : (4 * q * M) ^ 2 - M ≤ m) (hhi : m ≤ (4 * q * M) ^ 2 + M)
    (g : ℕ → ℝ) (hg : ∀ k, 0 ≤ g k ∧ g k ≤ 1) :
    |binomialMean m g - binomialMean ((4 * q * M) ^ 2) g| ≤ 1 / (4 * (q : ℝ)) := by
…

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

  49. theorem OAI.MaxCutGames.Foundations.PCP.LazySmoothing.modal_transfer line 518

    Source documentation

    A modal event of probability at least 1/q retains probability 1/(2q) throughout the middle window used in lazy-walk powering.

    theorem modal_transfer (q M m : ℕ) (hq : 1 ≤ q) (hM : 1 ≤ M)
    (hlo : (4 * q * M) ^ 2 - M ≤ m) (hhi : m ≤ (4 * q * M) ^ 2 + M)
    (g : ℕ → ℝ) (hg : ∀ k, 0 ≤ g k ∧ g k ≤ 1)
    (hmodal : 1 / (q : ℝ) ≤ binomialMean ((4 * q * M) ^ 2) g) :
    1 / (2 * (q : ℝ)) ≤ binomialMean m g := by
…

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

  50. def OAI.MaxCutGames.Foundations.PCP.PoweringWalks.lazyRotate line 545
  51. theorem OAI.MaxCutGames.Foundations.PCP.PoweringWalks.lazyRotate_involutive line 549
  52. def OAI.MaxCutGames.Foundations.PCP.PoweringWalks.lazyGraph line 557
  53. theorem OAI.MaxCutGames.Foundations.PCP.PoweringWalks.lazyGraph_rot_false line 565
  54. theorem OAI.MaxCutGames.Foundations.PCP.PoweringWalks.lazyGraph_rot_true line 568
  55. theorem OAI.MaxCutGames.Foundations.PCP.PoweringLazy.operator_binomialMean line 579
  56. theorem OAI.MaxCutGames.Foundations.PCP.PoweringLazy.averagingOperator_lazy line 587
  57. theorem OAI.MaxCutGames.Foundations.PCP.PoweringLazy.iterate_lazy_eq_binomialMean line 600

    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.MaxCutGames.Foundations.PCP.LazySmoothing.binomialMean

  58. theorem OAI.MaxCutGames.Foundations.PCP.PoweringLazy.iterate_mem_Icc line 614
  59. theorem OAI.MaxCutGames.Foundations.PCP.PoweringLazy.lazy_endpoint_modal_transfer line 630

    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
…
  60. def OAI.MaxCutGames.Foundations.PCP.LazyConstraint.constraintGraph line 653
  61. theorem OAI.MaxCutGames.Foundations.PCP.LazyConstraint.constraintGraph_tail line 665
  62. theorem OAI.MaxCutGames.Foundations.PCP.LazyConstraint.constraintGraph_reverse line 668
  63. theorem OAI.MaxCutGames.Foundations.PCP.LazyConstraint.constraintGraph_portGraph line 671
  64. theorem OAI.MaxCutGames.Foundations.PCP.LazyConstraint.edgeSatisfied_false line 675
  65. theorem OAI.MaxCutGames.Foundations.PCP.LazyConstraint.edgeSatisfied_true line 679
  66. theorem OAI.MaxCutGames.Foundations.PCP.LazyConstraint.complete line 688
  67. theorem OAI.MaxCutGames.Foundations.PCP.LazyConstraint.complete_iff line 698
  68. theorem OAI.MaxCutGames.Foundations.PCP.LazyConstraint.satisfiable_iff line 709
  69. theorem OAI.MaxCutGames.Foundations.PCP.LazyConstraint.rejectionCount_eq line 718

    Source documentation

    The equality holds for every labeling, including nonsatisfying ones.

    theorem rejectionCount_eq [Fintype V] [Fintype D]
    (G : ConstraintGraph V (V × D) A) (htail : G.tail = Prod.fst)
    (labeling : V → A) :
    (constraintGraph G).rejectionCount labeling = G.rejectionCount labeling := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.ConstraintGraph, OAI.MaxCutGames.Foundations.PCP.LazyConstraint.constraintGraph

  70. theorem OAI.MaxCutGames.Foundations.PCP.LazyConstraint.card_ports line 727
  71. theorem OAI.MaxCutGames.Foundations.PCP.LazyConstraint.card_darts line 731
  72. theorem OAI.MaxCutGames.Foundations.PCP.LazyConstraint.rejection_density_eq_half line 737

    Source documentation

    The actual normalized rejection probability is halved. The identity also holds for empty dart types, using the field's totalized division.

    theorem rejection_density_eq_half [Fintype V] [Fintype D]
    (G : ConstraintGraph V (V × D) A) (htail : G.tail = Prod.fst)
    (labeling : V → A) :
    ((constraintGraph G).rejectionCount labeling : ℝ) /
        (Fintype.card (V × (Bool × D)) : ℝ) =
      ((G.rejectionCount labeling : ℝ) / (Fintype.card (V × D) : ℝ)) / 2 := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.ConstraintGraph, OAI.MaxCutGames.Foundations.PCP.LazyConstraint.constraintGraph