OAI/Computability/MaxCut/Games/LabelBound.lean

GitHub source file

78 declarations, 0 contain sorry, 0 declared as axioms

Per-label diagonal lower bounds for the actual finite shared sampler. These bounds retain the output label, which is necessary for comparing the sampler's output distribution with a prescribed diagonal distribution.

  1. def OAI.MaxCutGames.Foundations.CorrelatedSampling.localSample line 18
  2. def OAI.MaxCutGames.Foundations.CorrelatedSampling.localDiagonal line 22
  3. def OAI.MaxCutGames.Foundations.CorrelatedSampling.goodLabel line 27
  4. theorem OAI.MaxCutGames.Foundations.CorrelatedSampling.common_first_label_lower line 31
  5. theorem OAI.MaxCutGames.Foundations.CorrelatedSampling.finite_label_diagonal_bound line 63

    Source documentation

    The finite shared-list sampler's mass on the particular diagonal output (a,a) is at least the common-first-label mass. Exhaustion uses a fixed local fallback; its contribution is nonnegative and is not counted in this bound.

    theorem finite_label_diagonal_bound (w : σ → ℝ) (left right : σ → Bool)
    (decode : σ → α) (fallback a : α) (hw : ∀ s, 0 ≤ w s)
    (hw_sum : ∑ s, w s = 1) (hu : 0 < eventMass w (fun s => left s || right s)) (n : Nat) :
    eventMass w (goodLabel left right decode a) / eventMass w (fun s => left s || right s) *
        (1 - eventMass w (fun s => !(left s || right s)) ^ n) ≤
      traceAverage w n (localDiagonal left right decode fallback a) := by
…

    Mentions: OAI.MaxCutGames.Foundations.CorrelatedSampling.eventMass, OAI.MaxCutGames.Foundations.CorrelatedSampling.goodLabel, OAI.MaxCutGames.Foundations.CorrelatedSampling.traceAverage, OAI.MaxCutGames.Foundations.CorrelatedSampling.localDiagonal

  6. theorem OAI.MaxCutGames.Foundations.CorrelatedSampling.rectangle_label_diagonal_bound line 79

    Source documentation

    Concrete normalized-density instance of the per-label bound. All random proposals come from the finite rectangle constructed from thresholds.

    theorem rectangle_label_diagonal_bound (thresholds : List ℝ) (p q : α → ℝ)
    (fallback a : α)
    (hpm : ∀ x, p x ∈ thresholds) (hqm : ∀ x, q x ∈ thresholds)
    (hp0 : ∀ x, 0 ≤ p x) (hq0 : ∀ x, 0 ≤ q x)
    (hp1 : ∀ x, p x ≤ 1) (hq1 : ∀ x, q x ≤ 1)
    (hpsum : ∑ x, p x = 1) (hqsum : ∑ x, q x = 1) (n : Nat) :
    min (p a) (q a) / (1 + totalVariation p q) *
        (1 - eventMass (rectangleWeight thresholds)
          (fun s => !(rectangleAccept thresholds p s || rectangleAccept thresholds q s)) ^ n) ≤
      traceAverage (rectangleWeight thresholds) n
        (localDiagonal (rectangleAccept thresholds p) (rectangleAccept thresholds q)
          Prod.fst fallback a) := by
…

    Mentions: OAI.MaxCutGames.Foundations.CorrelatedSampling.totalVariation, OAI.MaxCutGames.Foundations.CorrelatedSampling.eventMass, OAI.MaxCutGames.Foundations.CorrelatedSampling.rectangleWeight, OAI.MaxCutGames.Foundations.CorrelatedSampling.rectangleAccept, OAI.MaxCutGames.Foundations.CorrelatedSampling.traceAverage, OAI.MaxCutGames.Foundations.CorrelatedSampling.localDiagonal

  7. def OAI.MaxCutGames.Foundations.CorrelatedSampling.profileThresholds line 121
  8. theorem OAI.MaxCutGames.Foundations.CorrelatedSampling.mem_profileThresholds line 126
  9. theorem OAI.MaxCutGames.Foundations.CorrelatedSampling.distribution_weight_le_one line 131
  10. def OAI.MaxCutGames.Foundations.CorrelatedSampling.sharedProfileThresholds line 140
  11. theorem OAI.MaxCutGames.Foundations.CorrelatedSampling.left_mem_sharedProfileThresholds line 144
  12. theorem OAI.MaxCutGames.Foundations.CorrelatedSampling.right_mem_sharedProfileThresholds line 149
  13. abbrev OAI.MaxCutGames.Foundations.CorrelatedSampling.SharedProfileSeed line 154
  14. def OAI.MaxCutGames.Foundations.CorrelatedSampling.sharedProfileLeft line 158
  15. def OAI.MaxCutGames.Foundations.CorrelatedSampling.sharedProfileRight line 162
  16. def OAI.MaxCutGames.Foundations.CorrelatedSampling.sharedProfileReject line 166
  17. def OAI.MaxCutGames.Foundations.CorrelatedSampling.uniformRejectionRate line 171
  18. theorem OAI.MaxCutGames.Foundations.CorrelatedSampling.uniformRejectionRate_nonnegative line 174
  19. theorem OAI.MaxCutGames.Foundations.CorrelatedSampling.uniformRejectionRate_lt_one line 183
  20. theorem OAI.MaxCutGames.Foundations.CorrelatedSampling.sharedProfileReject_nonnegative line 191
  21. theorem OAI.MaxCutGames.Foundations.CorrelatedSampling.sharedProfile_reject_le_rate line 197
  22. theorem OAI.MaxCutGames.Foundations.CorrelatedSampling.nonnegative_powers_mono_inline_SharedProfiles line 229
  23. theorem OAI.MaxCutGames.Foundations.CorrelatedSampling.sharedProfile_label_diagonal_bound line 238
  24. theorem OAI.MaxCutGames.Foundations.CorrelatedSampling.exists_uniformRejectionRate_pow_lt line 272
  25. def OAI.MaxCutGames.Foundations.Information.IsProbability line 296
  26. def OAI.MaxCutGames.Foundations.Information.SupportedBy line 299
  27. def OAI.MaxCutGames.Foundations.Information.relativeEntropy line 301
  28. def OAI.MaxCutGames.Foundations.Information.totalVariation line 304
  29. def OAI.MaxCutGames.Foundations.Information.posterior line 307
  30. theorem OAI.MaxCutGames.Foundations.Information.posterior_isProbability line 310
  31. theorem OAI.MaxCutGames.Foundations.Information.posterior_supportedBy line 320
  32. theorem OAI.MaxCutGames.Foundations.Information.mul_log_div_ge_sub line 325
  33. theorem OAI.MaxCutGames.Foundations.Information.relativeEntropy_nonneg line 333
  34. theorem OAI.MaxCutGames.Foundations.Information.posterior_relativeEntropy_le line 345
  35. theorem OAI.MaxCutGames.Foundations.Information.totalVariation_nonneg line 369
  36. theorem OAI.MaxCutGames.Foundations.Information.totalVariation_symm line 372
  37. theorem OAI.MaxCutGames.Foundations.Information.totalVariation_le_one line 375
  38. theorem OAI.MaxCutGames.Foundations.Information.le_binaryLog_of_le_log line 386
  39. theorem OAI.MaxCutGames.Foundations.Information.weighted_sum_sq_le line 398

    Source documentation

    Finite weighted Cauchy–Schwarz for probability weights. The summands need not be nonnegative.

    theorem weighted_sum_sq_le (w x : α → ℝ) (hw : IsProbability w) :
    (∑ a, w a * x a)^2 ≤ ∑ a, w a * (x a)^2 := by
…

    Mentions: OAI.MaxCutGames.Foundations.Information.IsProbability

  40. def OAI.MaxCutGames.Foundations.Information.firstMarginal line 418
  41. def OAI.MaxCutGames.Foundations.Information.secondMarginal line 420
  42. def OAI.MaxCutGames.Foundations.Information.product line 422
  43. theorem OAI.MaxCutGames.Foundations.Information.firstMarginal_isProbability line 424
  44. theorem OAI.MaxCutGames.Foundations.Information.secondMarginal_isProbability line 431
  45. theorem OAI.MaxCutGames.Foundations.Information.product_isProbability line 440
  46. theorem OAI.MaxCutGames.Foundations.Information.point_le_firstMarginal line 447
  47. theorem OAI.MaxCutGames.Foundations.Information.point_le_secondMarginal line 452
  48. theorem OAI.MaxCutGames.Foundations.Information.joint_supportedBy_product_marginals line 457
  49. theorem OAI.MaxCutGames.Foundations.Information.relativeEntropy_product_reference line 465
  50. theorem OAI.MaxCutGames.Foundations.Information.marginal_relativeEntropy_sum_le line 499
  51. def OAI.MaxCutGames.Foundations.Information.conditionalKernel line 516
  52. theorem OAI.MaxCutGames.Foundations.Information.conditionalKernel_isProbability line 522
  53. theorem OAI.MaxCutGames.Foundations.Information.marginal_mul_conditionalKernel line 538
  54. theorem OAI.MaxCutGames.Foundations.Information.law_of_total_probability line 555
  55. theorem OAI.MaxCutGames.Foundations.Information.kernelProduct_isProbability line 562
  56. theorem OAI.MaxCutGames.Foundations.Information.alternativeInput_conditionalProduct_isProbability line 572
  57. def OAI.MaxCutGames.Foundations.Games.FiniteDistribution.totalVariation line 591
  58. theorem OAI.MaxCutGames.Foundations.Games.FiniteDistribution.totalVariation_nonnegative line 594
  59. theorem OAI.MaxCutGames.Foundations.Games.FiniteDistribution.totalVariation_comm line 598
  60. theorem OAI.MaxCutGames.Foundations.Games.FiniteDistribution.probability_sub_le_totalVariation line 609

    Source documentation

    A one-sided event difference is bounded by half the total absolute mass difference. Normalization is used; the full absolute-mass sum would lose a factor of two needed in the repetition argument.

    theorem probability_sub_le_totalVariation (μ ν : FiniteDistribution Ω)
    (event : Ω → Bool) :
    μ.probability event - ν.probability event ≤ μ.totalVariation ν := by
…

    Mentions: OAI.MaxCutGames.Foundations.Games.FiniteDistribution

  61. theorem OAI.MaxCutGames.Foundations.Games.FiniteDistribution.probability_abs_sub_le_totalVariation line 625
  62. theorem OAI.MaxCutGames.Foundations.Games.FiniteDistribution.probability_le_add_totalVariation line 635
  63. def OAI.MaxCutGames.Foundations.Games.FiniteDistribution.condition line 657
  64. theorem OAI.MaxCutGames.Foundations.Games.FiniteDistribution.probability_condition line 673
  65. theorem OAI.MaxCutGames.Foundations.Games.FiniteDistribution.probability_inter_eq_mul_conditional line 682
  66. theorem OAI.MaxCutGames.Foundations.Games.FiniteDistribution.probability_and_le_left line 690
  67. theorem OAI.MaxCutGames.Foundations.Games.FiniteDistribution.probability_and_le_right line 697
  68. theorem OAI.MaxCutGames.Foundations.Games.FiniteDistribution.probability_and_eq_zero_of_probability_eq_zero line 704
  69. theorem OAI.MaxCutGames.Foundations.Games.FiniteDistribution.probability_condition_given line 711
  70. theorem OAI.MaxCutGames.Foundations.Games.Game.selectedWins_insert line 725
  71. def OAI.MaxCutGames.Foundations.Games.Game.selectedSuccess line 736
  72. theorem OAI.MaxCutGames.Foundations.Games.Game.selectedSuccess_nonnegative line 741
  73. theorem OAI.MaxCutGames.Foundations.Games.Game.selectedSuccess_le_one line 746
  74. theorem OAI.MaxCutGames.Foundations.Games.Game.selectedSuccess_empty line 751
  75. theorem OAI.MaxCutGames.Foundations.Games.Game.selectedSuccess_univ line 758
  76. theorem OAI.MaxCutGames.Foundations.Games.Game.selectedSuccess_antitone line 764
  77. theorem OAI.MaxCutGames.Foundations.Games.Game.selectedSuccess_insert line 770
  78. theorem OAI.MaxCutGames.Foundations.Games.Game.selectedSuccess_insert_eq_zero line 782