OAI/Computability/MaxCut/PCP/CayleySampling.lean

GitHub source file

84 declarations, 0 contain sorry, 0 declared as axioms

Actual finite binary-word tail counts for the proposed Cayley base graph.

No expander, independence, spectral, or random-generator existence result is assumed here.

  1. abbrev OAI.MaxCutGames.Foundations.PCP.CayleySampling.FalseFiber line 17

    Source documentation

    The common fiber left after separating a Boolean character's sign.

    abbrev FalseFiber (χ : V → Bool) := {x : V // χ x = false}
  2. def OAI.MaxCutGames.Foundations.PCP.CayleySampling.falseRepresentative line 19
  3. def OAI.MaxCutGames.Foundations.PCP.CayleySampling.booleanSplitEquiv line 24
  4. theorem OAI.MaxCutGames.Foundations.PCP.CayleySampling.booleanSplitEquiv_fst line 40
  5. def OAI.MaxCutGames.Foundations.PCP.CayleySampling.sampleSplitEquiv line 44
  6. theorem OAI.MaxCutGames.Foundations.PCP.CayleySampling.sampleSplitEquiv_fst line 50
  7. theorem OAI.MaxCutGames.Foundations.PCP.CayleySampling.card_boolean_split line 54
  8. theorem OAI.MaxCutGames.Foundations.PCP.CayleySampling.expect_boolean_samples line 59
  9. theorem OAI.MaxCutGames.Foundations.PCP.CayleySampling.exists_true_of_ne_zero line 79
  10. theorem OAI.MaxCutGames.Foundations.PCP.CayleySampling.expect_parity_samples line 90

    Source documentation

    Actual parity words from independently indexed uniform cube vectors have exactly the uniform Boolean-word distribution.

    theorem expect_parity_samples (s : Cube I) (hs : s ≠ fun _ => false)
    (F : (D → Bool) → ℝ) :
    (𝔼 g : D → Cube I, F (fun d => AssignmentTester.parity s (g d))) =
      𝔼 b : D → Bool, F b := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.AssignmentTester.parity

  11. theorem OAI.MaxCutGames.Foundations.PCP.CayleySampling.expect_walsh_samples line 100

    Source documentation

    The same joint law expressed with the actual real Walsh character values.

    theorem expect_walsh_samples (s : Cube I) (hs : s ≠ fun _ => false)
    (F : (D → ℝ) → ℝ) :
    (𝔼 g : D → Cube I, F (fun d => walsh s (g d))) =
      𝔼 b : D → Bool, F (fun d => bitSign (b d)) := by
…
  12. theorem OAI.MaxCutGames.Foundations.PCP.CayleySampling.expect_walsh_mean line 109

    Source documentation

    In particular, any test of the empirical Walsh bias has the corresponding uniform Boolean-word average. This is the eigenvalue sampling law.

    theorem expect_walsh_mean (s : Cube I) (hs : s ≠ fun _ => false) (F : ℝ → ℝ) :
    (𝔼 g : D → Cube I, F (𝔼 d, walsh s (g d))) =
      𝔼 b : D → Bool, F (𝔼 d, bitSign (b d)) :=
…
  13. def OAI.MaxCutGames.Foundations.PCP.CayleyTailCount.upperMasks line 131
  14. def OAI.MaxCutGames.Foundations.PCP.CayleyTailCount.lowerMasks line 134
  15. def OAI.MaxCutGames.Foundations.PCP.CayleyTailCount.badMasks line 137
  16. theorem OAI.MaxCutGames.Foundations.PCP.CayleyTailCount.upperMasks_weight line 142

    Source documentation

    Weight every actual upper-tail mask by at least 3 ^ (3 * m).

    theorem upperMasks_weight (s : Finset α) (m : ℕ) (hcard : s.card = 4 * m) :
    (upperMasks s m).card * 3 ^ (3 * m) ≤ 4 ^ (4 * m) := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.CayleyTailCount.upperMasks

  17. theorem OAI.MaxCutGames.Foundations.PCP.CayleyTailCount.lowerMasks_complement_image line 160

    Source documentation

    Complementation preserves multiplicity and exchanges the two closed tails.

    theorem lowerMasks_complement_image (s : Finset α) (m : ℕ)
    (hcard : s.card = 4 * m) :
    (lowerMasks s m).image (fun t => s \ t) = upperMasks s m := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.CayleyTailCount.lowerMasks, OAI.MaxCutGames.Foundations.PCP.CayleyTailCount.upperMasks

  18. theorem OAI.MaxCutGames.Foundations.PCP.CayleyTailCount.lowerMasks_card_eq_upperMasks line 183
  19. theorem OAI.MaxCutGames.Foundations.PCP.CayleyTailCount.ratio_le_of_weight_inline_CayleyTailCount line 197
  20. theorem OAI.MaxCutGames.Foundations.PCP.CayleyTailCount.upperMasks_ratio_le line 211
  21. theorem OAI.MaxCutGames.Foundations.PCP.CayleyTailCount.lowerMasks_ratio_le line 216
  22. theorem OAI.MaxCutGames.Foundations.PCP.CayleyTailCount.badMasks_ratio_le_sharp line 221
  23. theorem OAI.MaxCutGames.Foundations.PCP.CayleyTailCount.badMasks_ratio_le line 236
  24. def OAI.MaxCutGames.Foundations.PCP.CayleyTailCount.trueMask line 246
  25. def OAI.MaxCutGames.Foundations.PCP.CayleyTailCount.countTrue line 249
  26. def OAI.MaxCutGames.Foundations.PCP.CayleyTailCount.badWord line 251
  27. instance OAI.MaxCutGames.Foundations.PCP.CayleyTailCount.(instance at line 254) line 254
  28. theorem OAI.MaxCutGames.Foundations.PCP.CayleyTailCount.bitSign_mean_eq line 258

    Source documentation

    The sign convention is the existing Walsh convention: false is +1, true is -1.

    theorem bitSign_mean_eq [Nonempty D] (word : D → Bool) :
    (𝔼 i, bitSign (word i)) =
      1 - 2 * ((countTrue word : ℝ) / Fintype.card D) := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.CayleyTailCount.countTrue

  29. theorem OAI.MaxCutGames.Foundations.PCP.CayleyTailCount.not_badWord_bias line 275

    Source documentation

    Excluding both closed integer tails bounds the actual mean Walsh sign.

    theorem not_badWord_bias (m : ℕ) (hcard : Fintype.card D = 4 * m) (hm : 0 < m)
    (word : D → Bool) (hword : ¬ badWord m word) :
    |𝔼 i, bitSign (word i)| ≤ (1 / 2 : ℝ) := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.CayleyTailCount.badWord

  30. def OAI.MaxCutGames.Foundations.PCP.CayleyTailCount.wordMaskEquiv line 296

    Source documentation

    All words occur once, so subset counting keeps the actual uniform law.

    def wordMaskEquiv [DecidableEq D] : (D → Bool) ≃ Finset D where
…
  31. theorem OAI.MaxCutGames.Foundations.PCP.CayleyTailCount.twoTail_probability line 307

    Source documentation

    Actual real uniform expectation on binary words, including both closed tails.

    theorem twoTail_probability [DecidableEq D] (m : ℕ) (hcard : Fintype.card D = 4 * m) :
    (𝔼 word : D → Bool, if badWord m word then (1 : ℝ) else 0) ≤
      2 * (2 / 3 : ℝ) ^ m := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.CayleyTailCount.badWord

  32. theorem OAI.MaxCutGames.Foundations.PCP.CayleyTailCount.union_bound_le_half line 329

    Source documentation

    Numerical budget for a union bound over at most 2 ^ n frequencies.

    theorem union_bound_le_half (n m : ℕ) (hm : 3 * (n + 2) ≤ m) :
    (2 : ℝ) ^ n * (2 * (2 / 3 : ℝ) ^ m) ≤ 1 / 2 := by
…
  33. theorem OAI.MaxCutGames.Foundations.PCP.CayleyTailCount.fixed_parameters line 347

    Source documentation

    The proposed fixed parameters meet the elementary counting margin.

    theorem fixed_parameters : 3 * (448 + 2) ≤ 16384 ∧ 4 * 16384 = 2 ^ 16 := by
…
  34. theorem OAI.MaxCutGames.Foundations.PCP.CayleyTailCount.fixed_union_bound line 350
  35. theorem OAI.MaxCutGames.Foundations.PCP.CayleyTailCount.seventh_power_size line 355

    Source documentation

    Pure parameter identity; this does not assert existence of a graph.

    theorem seventh_power_size : (2 : ℕ) ^ 448 = (((2 : ℕ) ^ 16) ^ 7) ^ 4 := by
…
  36. theorem OAI.MaxCutGames.Foundations.PCP.CayleyTailCount.seventh_power_abs_le line 359

    Source documentation

    Pure scalar estimate, ready for a separately proved spectral powering theorem.

    theorem seventh_power_abs_le {a : ℝ} (ha : |a| ≤ 1 / 2) : |a ^ 7| ≤ 1 / 128 := by
…
  37. def OAI.MaxCutGames.Foundations.PCP.SpectralReturn.mean line 374
  38. def OAI.MaxCutGames.Foundations.PCP.SpectralReturn.energy line 376
  39. def OAI.MaxCutGames.Foundations.PCP.SpectralReturn.correlation line 378
  40. def OAI.MaxCutGames.Foundations.PCP.SpectralReturn.averagingOperator line 381
  41. def OAI.MaxCutGames.Foundations.PCP.SpectralReturn.iterateOperator line 384
  42. def OAI.MaxCutGames.Foundations.PCP.SpectralReturn.edgeProfile line 389
  43. def OAI.MaxCutGames.Foundations.PCP.SpectralReturn.edgeDensity line 392
  44. def OAI.MaxCutGames.Foundations.PCP.SpectralReturn.markedStep line 395
  45. def OAI.MaxCutGames.Foundations.PCP.SpectralReturn.returnMass line 399
  46. structure OAI.MaxCutGames.Foundations.PCP.SpectralReturn.SpectralCertificate line 403
  47. theorem OAI.MaxCutGames.Foundations.PCP.SpectralReturn.mean_eq_sum_div_card line 416
  48. theorem OAI.MaxCutGames.Foundations.PCP.SpectralReturn.mean_equiv line 420
  49. theorem OAI.MaxCutGames.Foundations.PCP.SpectralReturn.mean_prod line 424
  50. theorem OAI.MaxCutGames.Foundations.PCP.SpectralReturn.mean_const line 429
  51. theorem OAI.MaxCutGames.Foundations.PCP.SpectralReturn.mean_add line 432
  52. theorem OAI.MaxCutGames.Foundations.PCP.SpectralReturn.mean_sub line 436
  53. theorem OAI.MaxCutGames.Foundations.PCP.SpectralReturn.mean_mul_left line 440
  54. theorem OAI.MaxCutGames.Foundations.PCP.SpectralReturn.mean_mul_right line 444
  55. theorem OAI.MaxCutGames.Foundations.PCP.SpectralReturn.mean_nonnegative line 448
  56. theorem OAI.MaxCutGames.Foundations.PCP.SpectralReturn.mean_mono line 451
  57. theorem OAI.MaxCutGames.Foundations.PCP.SpectralReturn.energy_nonnegative line 454
  58. theorem OAI.MaxCutGames.Foundations.PCP.SpectralReturn.correlation_sq_le line 458

    Source documentation

    The finite Cauchy--Schwarz inequality, in the chosen normalized convention.

    theorem correlation_sq_le (f g : A → ℝ) :
    correlation f g ^ 2 ≤ energy f * energy g :=
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.SpectralReturn.correlation, OAI.MaxCutGames.Foundations.PCP.SpectralReturn.energy

  59. theorem OAI.MaxCutGames.Foundations.PCP.SpectralReturn.energy_sub_const line 462
  60. theorem OAI.MaxCutGames.Foundations.PCP.SpectralReturn.correlation_sub_const line 471
  61. theorem OAI.MaxCutGames.Foundations.PCP.SpectralReturn.mean_operator line 491
  62. theorem OAI.MaxCutGames.Foundations.PCP.SpectralReturn.operator_sub_const line 501
  63. theorem OAI.MaxCutGames.Foundations.PCP.SpectralReturn.mean_iterate line 509
  64. theorem OAI.MaxCutGames.Foundations.PCP.SpectralReturn.iterate_sub_const line 515
  65. theorem OAI.MaxCutGames.Foundations.PCP.SpectralReturn.mean_markedStep line 524

    Source documentation

    Reversal moves the first marked edge to its endpoint. The profile therefore appears at the endpoint, before the gap remaining vertex transitions.

    theorem mean_markedStep (bad : V × D → Bool)
    (reversal : ∀ e, bad (G.rot e) = bad e) (f : V → ℝ) :
    mean (markedStep G bad f) = correlation (edgeProfile bad) f := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.SpectralReturn.mean, OAI.MaxCutGames.Foundations.PCP.SpectralReturn.markedStep, OAI.MaxCutGames.Foundations.PCP.SpectralReturn.correlation, OAI.MaxCutGames.Foundations.PCP.SpectralReturn.edgeProfile

  66. theorem OAI.MaxCutGames.Foundations.PCP.SpectralReturn.returnMass_eq_correlation line 552
  67. theorem OAI.MaxCutGames.Foundations.PCP.SpectralReturn.iterate_energy_bound line 561
  68. theorem OAI.MaxCutGames.Foundations.PCP.SpectralReturn.zero_mean_correlation_bound line 576
  69. theorem OAI.MaxCutGames.Foundations.PCP.SpectralReturn.correlation_centered line 591
  70. theorem OAI.MaxCutGames.Foundations.PCP.SpectralReturn.edgeDensity_eq_edge_mean line 608

    Source documentation

    Density is exactly the uniform probability of a marked directed port-edge.

    theorem edgeDensity_eq_edge_mean (bad : V × D → Bool) :
    edgeDensity bad = mean (fun e => if bad e then (1 : ℝ) else 0) :=
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.SpectralReturn.edgeDensity, OAI.MaxCutGames.Foundations.PCP.SpectralReturn.mean

  71. theorem OAI.MaxCutGames.Foundations.PCP.SpectralReturn.edgeDensity_eq_card line 615

    Source documentation

    The edge convention counts each directed port once, including parallel edges and loops. Thus the density is literally the marked-edge cardinal ratio.

    theorem edgeDensity_eq_card (bad : V × D → Bool) :
    edgeDensity bad =
      ((Finset.univ.filter (fun e => bad e = true)).card : ℝ) /
        (Fintype.card (V × D) : ℝ) := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.SpectralReturn.edgeDensity

  72. theorem OAI.MaxCutGames.Foundations.PCP.SpectralReturn.edgeProfile_nonnegative line 623
  73. theorem OAI.MaxCutGames.Foundations.PCP.SpectralReturn.edgeProfile_le_one line 627
  74. theorem OAI.MaxCutGames.Foundations.PCP.SpectralReturn.edgeDensity_nonnegative line 635
  75. theorem OAI.MaxCutGames.Foundations.PCP.SpectralReturn.edgeDensity_le_one line 638
  76. theorem OAI.MaxCutGames.Foundations.PCP.SpectralReturn.edgeProfile_energy_le_density line 644
  77. theorem OAI.MaxCutGames.Foundations.PCP.SpectralReturn.edgeProfile_centered_energy line 651
  78. theorem OAI.MaxCutGames.Foundations.PCP.SpectralReturn.returnMass_le_sharp line 662

    Source documentation

    Sharp return bound. No division by the bad-edge density occurs, so the empty bad set is covered. gap = 0 gives the adjacent-edge upper bound epsilon.

    theorem returnMass_le_sharp (G : PortGraph V D) (lambda : ℝ)
    (certificate : SpectralCertificate G lambda) (bad : V × D → Bool)
    (reversal : ∀ e, bad (G.rot e) = bad e) (gap : Nat) :
    returnMass G bad gap ≤ edgeDensity bad ^ 2 +
      lambda ^ gap * (edgeDensity bad * (1 - edgeDensity bad)) := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.SpectralReturn.SpectralCertificate, OAI.MaxCutGames.Foundations.PCP.SpectralReturn.returnMass, OAI.MaxCutGames.Foundations.PCP.SpectralReturn.edgeDensity

  79. theorem OAI.MaxCutGames.Foundations.PCP.SpectralReturn.returnMass_le line 679

    Source documentation

    The simple bound used in the second-moment estimate.

    theorem returnMass_le (G : PortGraph V D) (lambda : ℝ)
    (certificate : SpectralCertificate G lambda) (bad : V × D → Bool)
    (reversal : ∀ e, bad (G.rot e) = bad e) (gap : Nat) :
    returnMass G bad gap ≤ edgeDensity bad ^ 2 + edgeDensity bad * lambda ^ gap := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.SpectralReturn.SpectralCertificate, OAI.MaxCutGames.Foundations.PCP.SpectralReturn.returnMass, OAI.MaxCutGames.Foundations.PCP.SpectralReturn.edgeDensity

  80. theorem OAI.MaxCutGames.Foundations.PCP.SpectralReturn.adjacent_returnMass_le line 689
  81. theorem OAI.MaxCutGames.Foundations.PCP.SpectralReturn.geometric_sum_le line 701

    Source documentation

    The finite geometric-series bound that absorbs forward and reverse returns. It applies to every finite window, with no limiting probability argument.

    theorem geometric_sum_le (lambda : ℝ) (h0 : 0 ≤ lambda) (h1 : lambda < 1) (n : Nat) :
    (∑ k ∈ Finset.range n, lambda ^ k) ≤ 1 / (1 - lambda) := by
…
  82. theorem OAI.MaxCutGames.Foundations.PCP.SpectralReturn.sum_returnMass_le line 715

    Source documentation

    The return contribution from one marked edge, over a finite forward window.

    theorem sum_returnMass_le (G : PortGraph V D) (lambda : ℝ)
    (certificate : SpectralCertificate G lambda) (bad : V × D → Bool)
    (reversal : ∀ e, bad (G.rot e) = bad e) (n : Nat) :
    (∑ gap ∈ Finset.range n, returnMass G bad gap) ≤
      (n : ℝ) * edgeDensity bad ^ 2 + edgeDensity bad / (1 - lambda) := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.SpectralReturn.SpectralCertificate, OAI.MaxCutGames.Foundations.PCP.SpectralReturn.returnMass, OAI.MaxCutGames.Foundations.PCP.SpectralReturn.edgeDensity

  83. theorem OAI.MaxCutGames.Foundations.PCP.SpectralReturn.triangular_returnMass_sum_le line 737

    Source documentation

    Sum over all distinct ordered-time pairs, counting each pair once. The row for the later edge j has gaps 0,...,j-1.

    theorem triangular_returnMass_sum_le (G : PortGraph V D) (lambda : ℝ)
    (certificate : SpectralCertificate G lambda) (bad : V × D → Bool)
    (reversal : ∀ e, bad (G.rot e) = bad e) (n : Nat) :
    (∑ j ∈ Finset.range n, ∑ gap ∈ Finset.range j, returnMass G bad gap) ≤
      ((n : ℝ) * ((n : ℝ) - 1) / 2) * edgeDensity bad ^ 2 +
        (n : ℝ) * (edgeDensity bad / (1 - lambda)) := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.SpectralReturn.SpectralCertificate, OAI.MaxCutGames.Foundations.PCP.SpectralReturn.returnMass, OAI.MaxCutGames.Foundations.PCP.SpectralReturn.edgeDensity

  84. theorem OAI.MaxCutGames.Foundations.PCP.SpectralReturn.secondMoment_return_envelope line 759

    Source documentation

    The exact finite envelope needed after expanding the square of the hit count. The diagonal contributes n * epsilon; both off-diagonal triangles contribute twice the return sum. The actual walk-event identity is supplied by PoweringMoment and PoweringReturn.

    theorem secondMoment_return_envelope (G : PortGraph V D) (lambda : ℝ)
    (certificate : SpectralCertificate G lambda) (bad : V × D → Bool)
    (reversal : ∀ e, bad (G.rot e) = bad e) (n : Nat) :
    (n : ℝ) * edgeDensity bad +
        2 * (∑ j ∈ Finset.range n, ∑ gap ∈ Finset.range j, returnMass G bad gap) ≤
      (n : ℝ) * edgeDensity bad *
        (1 + 2 / (1 - lambda) + ((n : ℝ) - 1) * edgeDensity bad) := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.SpectralReturn.SpectralCertificate, OAI.MaxCutGames.Foundations.PCP.SpectralReturn.edgeDensity, OAI.MaxCutGames.Foundations.PCP.SpectralReturn.returnMass