OAI/Computability/MaxCut/Estimates/Clip.lean

GitHub source file

60 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.OptimalMaxCut.MISProof.degree_cons line 12
  2. theorem OAI.OptimalMaxCut.MISProof.corrAverage_sum line 18
  3. theorem OAI.OptimalMaxCut.MISProof.corrAverage_walsh line 26
  4. theorem OAI.OptimalMaxCut.MISProof.corrAverage_polynomial line 46
  5. theorem OAI.OptimalMaxCut.MISProof.corrAverage_stability line 65
  6. def OAI.OptimalMaxCut.MISProof.clip line 74
  7. theorem OAI.OptimalMaxCut.MISProof.clip_mem line 76
  8. theorem OAI.OptimalMaxCut.MISProof.clip_eq line 81
  9. theorem OAI.OptimalMaxCut.MISProof.clip_lipschitz line 84
  10. def OAI.OptimalMaxCut.MISProof.interiorClip line 91
  11. theorem OAI.OptimalMaxCut.MISProof.interiorClip_mem line 93
  12. theorem OAI.OptimalMaxCut.MISProof.interiorClip_lipschitz line 102
  13. theorem OAI.OptimalMaxCut.MISProof.interiorClip_approx line 112
  14. theorem OAI.OptimalMaxCut.MISProof.mean_abs_diff_le line 127
  15. theorem OAI.OptimalMaxCut.MISProof.correlation_diff_le line 136
  16. theorem OAI.OptimalMaxCut.MISProof.centered_half_correlation line 150
  17. def OAI.OptimalMaxCut.MISProof.smoothedTruncCoeff line 160
  18. theorem OAI.OptimalMaxCut.MISProof.smoothedTrunc_high line 163
  19. theorem OAI.OptimalMaxCut.MISProof.smoothedTrunc_sq_le line 167
  20. theorem OAI.OptimalMaxCut.MISProof.smoothedTrunc_second_le line 176
  21. theorem OAI.OptimalMaxCut.MISProof.smoothedTrunc_diff_second line 182
  22. theorem OAI.OptimalMaxCut.MISProof.coefficient_sub line 197
  23. theorem OAI.OptimalMaxCut.MISProof.smoothedTrunc_tail_second line 201
  24. theorem OAI.OptimalMaxCut.MISProof.mean_abs_le_of_second line 221
  25. theorem OAI.OptimalMaxCut.MISProof.smoothedTrunc_tail_first line 227
  26. theorem OAI.OptimalMaxCut.MISProof.clipped_polynomial_bellman line 233
  27. theorem OAI.OptimalMaxCut.MISProof.mean_mem_Icc line 268
  28. theorem OAI.OptimalMaxCut.MISProof.smoothed_stability_bellman line 273
  29. theorem OAI.OptimalMaxCut.MISProof.majority_is_stablest line 326
  30. theorem OAI.OptimalMaxCut.MISProof.cutoffInfluence_le_influence line 358
  31. theorem OAI.OptimalMaxCut.MISProof.untruncated_majority_is_stablest line 367
  32. structure OAI.OptimalMaxCut.LongCode.Law line 384

    Source documentation

    Explicit rational finite probability law. The weighted test below is a finite rational graph construction, not an oracle distribution.

    structure Law (I : Type*) [Fintype I] where
…
  33. def OAI.OptimalMaxCut.LongCode.Law.avg line 392
  34. theorem OAI.OptimalMaxCut.LongCode.Law.weight_nonneg line 394
  35. theorem OAI.OptimalMaxCut.LongCode.Law.total_real line 397
  36. theorem OAI.OptimalMaxCut.LongCode.Law.avg_const line 400
  37. theorem OAI.OptimalMaxCut.LongCode.Law.avg_mono line 403
  38. theorem OAI.OptimalMaxCut.LongCode.Law.avg_nonneg line 406
  39. theorem OAI.OptimalMaxCut.LongCode.Law.avg_add line 409
  40. theorem OAI.OptimalMaxCut.LongCode.Law.avg_sub line 412
  41. theorem OAI.OptimalMaxCut.LongCode.Law.avg_mul line 415
  42. theorem OAI.OptimalMaxCut.LongCode.Law.avg_smul line 418
  43. theorem OAI.OptimalMaxCut.LongCode.Law.avg_div line 421
  44. theorem OAI.OptimalMaxCut.LongCode.Law.avg_sum line 424
  45. theorem OAI.OptimalMaxCut.LongCode.Law.avg_avg line 429
  46. theorem OAI.OptimalMaxCut.LongCode.Law.avg_sq_le line 435
  47. theorem OAI.OptimalMaxCut.LongCode.Law.avg_mem line 444
  48. theorem OAI.OptimalMaxCut.LongCode.Law.avg_expect line 450
  49. theorem OAI.OptimalMaxCut.LongCode.Law.coefficient_avg line 454
  50. theorem OAI.OptimalMaxCut.LongCode.Law.cutoffInfluence_avg line 459
  51. structure OAI.OptimalMaxCut.LongCode.Game line 475

    Source documentation

    The generative presentation of a finite rational weighted Unique Game: choose a right question, then an incident edge. All actual games have this presentation after deleting zero-marginal right questions.

    structure Game (X Y E : Type*) [Fintype X] [Fintype Y] [Fintype E] (q : ℕ) where
…
  52. def OAI.OptimalMaxCut.LongCode.Game.satisfied line 484
  53. def OAI.OptimalMaxCut.LongCode.Game.Sound line 490

    Source documentation

    A semantic bound on this input game, not a hypothesis asserting NP-hardness or an assumed Max-Cut reduction.

    def Sound (G : Game X Y E q) (δ : ℝ) : Prop := ∀ lx ly, G.satisfied lx ly ≤ δ
…

    Mentions: OAI.OptimalMaxCut.LongCode.Game

  54. def OAI.OptimalMaxCut.LongCode.antipode line 494
  55. theorem OAI.OptimalMaxCut.LongCode.antipode_involutive line 496
  56. def OAI.OptimalMaxCut.LongCode.oddPart line 501
  57. def OAI.OptimalMaxCut.LongCode.evenPart line 503
  58. theorem OAI.OptimalMaxCut.LongCode.oddPart_bounded line 506
  59. theorem OAI.OptimalMaxCut.LongCode.oddPart_mean line 513
  60. theorem OAI.OptimalMaxCut.LongCode.sum_cutoffInfluences line 520