OAI/Computability/MaxCut/Games/Basic2.lean

GitHub source file

81 declarations, 0 contain sorry, 0 declared as axioms

Finite prerequisites for Holenstein's consistent sampling argument (Lemma 5.2).

firstAccepted is an actual bounded rejection sampler on a shared finite list of proposals. first_union_common proves its synchronization property. The remaining theorems establish the exact overlap/union mass formulas and the agreement lower bound used to analyze a first accepted shared proposal.

No infinite random process or locally computable embedding is asserted here.

  1. def OAI.MaxCutGames.Foundations.CorrelatedSampling.firstAccepted line 24

    Source documentation

    Return the first proposal accepted by the given test, or report exhaustion.

    def firstAccepted {σ : Type*} (accept : σ → Bool) : List σ → Option σ
  | [] => none
  | proposal :: rest =>
      if accept proposal then some proposal else firstAccepted accept rest

/-- If the first proposal accepted by either sampler is accepted by both,
the two samplers return exactly that same proposal. -/
  2. theorem OAI.MaxCutGames.Foundations.CorrelatedSampling.first_union_common line 31

    Source documentation

    If the first proposal accepted by either sampler is accepted by both, the two samplers return exactly that same proposal.

    theorem first_union_common {σ : Type*} (left right : σ → Bool)
    (proposals : List σ) (proposal : σ)
    (hfirst : firstAccepted (fun s => left s || right s) proposals = some proposal)
    (hleft : left proposal = true) (hright : right proposal = true) :
    firstAccepted left proposals = some proposal ∧
      firstAccepted right proposals = some proposal := by
…

    Mentions: OAI.MaxCutGames.Foundations.CorrelatedSampling.firstAccepted

  3. def OAI.MaxCutGames.Foundations.CorrelatedSampling.thresholdSample line 56

    Source documentation

    Finite integer-threshold rejection sampling. A mass table can be sampled using shared proposals (label, height) drawn from a finite rectangle.

    def thresholdSample {α : Type*} (mass : α → Nat) (proposals : List (α × Nat)) :
    Option α :=
…
  4. theorem OAI.MaxCutGames.Foundations.CorrelatedSampling.thresholdSample_agreement line 60
  5. def OAI.MaxCutGames.Foundations.CorrelatedSampling.totalVariation line 79

    Source documentation

    Total variation for real-valued finite mass functions. Distribution normalization is supplied explicitly in theorems that need it.

    def totalVariation (p q : α → ℝ) : ℝ := (∑ a, |p a - q a|) / 2
  6. def OAI.MaxCutGames.Foundations.CorrelatedSampling.overlapMass line 81
  7. def OAI.MaxCutGames.Foundations.CorrelatedSampling.unionMass line 83
  8. theorem OAI.MaxCutGames.Foundations.CorrelatedSampling.totalVariation_nonneg line 85
  9. theorem OAI.MaxCutGames.Foundations.CorrelatedSampling.overlapMass_nonneg line 89
  10. theorem OAI.MaxCutGames.Foundations.CorrelatedSampling.min_abs_identity_inline_Basic line 93
  11. theorem OAI.MaxCutGames.Foundations.CorrelatedSampling.max_abs_identity_inline_Basic line 100
  12. theorem OAI.MaxCutGames.Foundations.CorrelatedSampling.overlapMass_eq line 108

    Source documentation

    The overlap of two probability masses is exactly one minus their TV.

    theorem overlapMass_eq (p q : α → ℝ) (hp : ∑ a, p a = 1) (hq : ∑ a, q a = 1) :
    overlapMass p q = 1 - totalVariation p q := by
…

    Mentions: OAI.MaxCutGames.Foundations.CorrelatedSampling.overlapMass, OAI.MaxCutGames.Foundations.CorrelatedSampling.totalVariation

  13. theorem OAI.MaxCutGames.Foundations.CorrelatedSampling.unionMass_eq line 117

    Source documentation

    The union of two probability masses is exactly one plus their TV.

    theorem unionMass_eq (p q : α → ℝ) (hp : ∑ a, p a = 1) (hq : ∑ a, q a = 1) :
    unionMass p q = 1 + totalVariation p q := by
…

    Mentions: OAI.MaxCutGames.Foundations.CorrelatedSampling.unionMass, OAI.MaxCutGames.Foundations.CorrelatedSampling.totalVariation

  14. theorem OAI.MaxCutGames.Foundations.CorrelatedSampling.totalVariation_le_one line 125
  15. theorem OAI.MaxCutGames.Foundations.CorrelatedSampling.overlap_union_ratio line 133

    Source documentation

    The first-union-point agreement ratio appearing in Holenstein Lemma 5.2.

    theorem overlap_union_ratio (p q : α → ℝ)
    (hp : ∑ a, p a = 1) (hq : ∑ a, q a = 1) :
    overlapMass p q / unionMass p q =
      (1 - totalVariation p q) / (1 + totalVariation p q) := by
…

    Mentions: OAI.MaxCutGames.Foundations.CorrelatedSampling.overlapMass, OAI.MaxCutGames.Foundations.CorrelatedSampling.unionMass, OAI.MaxCutGames.Foundations.CorrelatedSampling.totalVariation

  16. theorem OAI.MaxCutGames.Foundations.CorrelatedSampling.overlap_union_ratio_lower_bound line 141

    Source documentation

    Exact algebra behind the linear agreement estimate. This is a proved bound on the overlap/union ratio, not an assumed sampler law.

    theorem overlap_union_ratio_lower_bound (p q : α → ℝ)
    (hp : ∑ a, p a = 1) (hq : ∑ a, q a = 1) :
    1 - 2 * totalVariation p q ≤ overlapMass p q / unionMass p q := by
…

    Mentions: OAI.MaxCutGames.Foundations.CorrelatedSampling.totalVariation, OAI.MaxCutGames.Foundations.CorrelatedSampling.overlapMass, OAI.MaxCutGames.Foundations.CorrelatedSampling.unionMass

  17. theorem OAI.MaxCutGames.Foundations.CorrelatedSampling.first_union_disagreement_upper_bound line 152

    Source documentation

    Equivalent upper bound on the probability of the first union point belonging to just one density.

    theorem first_union_disagreement_upper_bound (p q : α → ℝ)
    (hp : ∑ a, p a = 1) (hq : ∑ a, q a = 1) :
    1 - overlapMass p q / unionMass p q ≤ 2 * totalVariation p q := by
…

    Mentions: OAI.MaxCutGames.Foundations.CorrelatedSampling.overlapMass, OAI.MaxCutGames.Foundations.CorrelatedSampling.unionMass, OAI.MaxCutGames.Foundations.CorrelatedSampling.totalVariation

  18. def OAI.MaxCutGames.Foundations.CorrelatedSampling.eventMass line 173
  19. theorem OAI.MaxCutGames.Foundations.CorrelatedSampling.eventMass_nonneg line 176
  20. theorem OAI.MaxCutGames.Foundations.CorrelatedSampling.eventMass_complement line 182
  21. def OAI.MaxCutGames.Foundations.CorrelatedSampling.geometricMass line 194
  22. theorem OAI.MaxCutGames.Foundations.CorrelatedSampling.geometricMass_nonneg line 198
  23. theorem OAI.MaxCutGames.Foundations.CorrelatedSampling.geometricMass_identity line 204
  24. def OAI.MaxCutGames.Foundations.CorrelatedSampling.firstHitWeight line 218

    Source documentation

    Probability transition for a finite first-acceptance process. A successful first trial contributes its own mass; a rejected first trial continues with one fewer trial.

    def firstHitWeight (w : σ → ℝ) (accept : σ → Bool) : Nat → Option σ → ℝ
  | 0, none => 1
  | 0, some _ => 0
  | n + 1, none => eventMass w (fun s => !(accept s)) * firstHitWeight w accept n none
  | n + 1, some s =>
      (if accept s then w s else 0) +
        eventMass w (fun s => !(accept s)) * firstHitWeight w accept n (some s)

    Mentions: OAI.MaxCutGames.Foundations.CorrelatedSampling.eventMass

  25. theorem OAI.MaxCutGames.Foundations.CorrelatedSampling.firstHitWeight_nonneg line 226
  26. theorem OAI.MaxCutGames.Foundations.CorrelatedSampling.firstHitWeight_none line 240
  27. theorem OAI.MaxCutGames.Foundations.CorrelatedSampling.firstHitWeight_some line 246
  28. theorem OAI.MaxCutGames.Foundations.CorrelatedSampling.firstHitWeight_normalized line 256
  29. def OAI.MaxCutGames.Foundations.CorrelatedSampling.goodFirstMass line 272

    Source documentation

    Probability that the first accepted proposal satisfies an additional test. For two threshold samplers, take accept = left || right and good = left && right. first_union_common gives deterministic agreement on this event.

    def goodFirstMass (w : σ → ℝ) (accept good : σ → Bool) (n : Nat) : ℝ :=
…
  30. theorem OAI.MaxCutGames.Foundations.CorrelatedSampling.goodFirstMass_eq line 275
  31. theorem OAI.MaxCutGames.Foundations.CorrelatedSampling.goodFirstMass_exact line 289

    Source documentation

    Exact finite geometric law: the first accepted proposal lies in the good part with probability (good accepted mass / total accepted mass) times the probability of seeing any accepted proposal within the trial bound.

    theorem goodFirstMass_exact (w : σ → ℝ) (accept good : σ → Bool)
    (hw : ∑ s, w s = 1) (ha : eventMass w accept ≠ 0) (n : Nat) :
    goodFirstMass w accept good n =
      eventMass w (fun s => accept s && good s) / eventMass w accept *
        (1 - eventMass w (fun s => !(accept s)) ^ n) := by
…

    Mentions: OAI.MaxCutGames.Foundations.CorrelatedSampling.eventMass, OAI.MaxCutGames.Foundations.CorrelatedSampling.goodFirstMass

  32. theorem OAI.MaxCutGames.Foundations.CorrelatedSampling.commonMass_le_acceptMass line 305
  33. theorem OAI.MaxCutGames.Foundations.CorrelatedSampling.goodFirstMass_lower_bound line 315

    Source documentation

    A finite truncation loses at most its exhaustion probability in addition to the conditional bad-first-proposal probability. All quantities are exact finite sums; the rightmost term is the explicit geometric tail.

    theorem goodFirstMass_lower_bound (w : σ → ℝ) (accept good : σ → Bool)
    (hw : ∀ s, 0 ≤ w s) (hw_sum : ∑ s, w s = 1)
    (ha : 0 < eventMass w accept) (n : Nat) :
    eventMass w (fun s => accept s && good s) / eventMass w accept -
        eventMass w (fun s => !(accept s)) ^ n ≤ goodFirstMass w accept good n := by
…

    Mentions: OAI.MaxCutGames.Foundations.CorrelatedSampling.eventMass, OAI.MaxCutGames.Foundations.CorrelatedSampling.goodFirstMass

  34. def OAI.MaxCutGames.Foundations.CorrelatedSampling.traceAverage line 337

    Source documentation

    Expectation over a length-n list of independent proposals with mass w. This is defined directly as a finite nested weighted sum.

    def traceAverage (w : σ → ℝ) : Nat → (List σ → ℝ) → ℝ
  | 0, observable => observable []
  | n + 1, observable => ∑ s, w s * traceAverage w n (fun tail => observable (s :: tail))
  35. theorem OAI.MaxCutGames.Foundations.CorrelatedSampling.traceAverage_const line 341
  36. theorem OAI.MaxCutGames.Foundations.CorrelatedSampling.traceAverage_mono line 347
  37. theorem OAI.MaxCutGames.Foundations.CorrelatedSampling.traceAverage_sum line 359
  38. theorem OAI.MaxCutGames.Foundations.CorrelatedSampling.firstAccepted_law line 373

    Source documentation

    The recursively constructed first-hit distribution is the actual law of the finite shared-list rejection sampler.

    theorem firstAccepted_law (w : σ → ℝ) (accept : σ → Bool)
    (hw : ∑ s, w s = 1) (n : Nat) (output : Option σ) :
    traceAverage w n (fun proposals =>
      if firstAccepted accept proposals = output then 1 else 0) =
      firstHitWeight w accept n output := by
…

    Mentions: OAI.MaxCutGames.Foundations.CorrelatedSampling.traceAverage, OAI.MaxCutGames.Foundations.CorrelatedSampling.firstAccepted, OAI.MaxCutGames.Foundations.CorrelatedSampling.firstHitWeight

  39. def OAI.MaxCutGames.Foundations.CorrelatedSampling.goodFirstIndicator line 420

    Source documentation

    Indicator of the first accepted proposal passing a second test.

    def goodFirstIndicator (accept good : σ → Bool) (proposals : List σ) : ℝ :=
…
  40. theorem OAI.MaxCutGames.Foundations.CorrelatedSampling.goodFirstIndicator_expansion line 425
  41. theorem OAI.MaxCutGames.Foundations.CorrelatedSampling.goodFirstIndicator_law line 442

    Source documentation

    Exact good-event probability of the actual bounded sampler.

    theorem goodFirstIndicator_law (w : σ → ℝ) (accept good : σ → Bool)
    (hw : ∑ s, w s = 1) (n : Nat) :
    traceAverage w n (goodFirstIndicator accept good) = goodFirstMass w accept good n := by
…

    Mentions: OAI.MaxCutGames.Foundations.CorrelatedSampling.traceAverage, OAI.MaxCutGames.Foundations.CorrelatedSampling.goodFirstIndicator, OAI.MaxCutGames.Foundations.CorrelatedSampling.goodFirstMass

  42. structure OAI.MaxCutGames.Foundations.CorrelatedSampling.ThresholdInterval line 462
  43. def OAI.MaxCutGames.Foundations.CorrelatedSampling.splitPoint line 467
  44. def OAI.MaxCutGames.Foundations.CorrelatedSampling.splitLeft line 469
  45. def OAI.MaxCutGames.Foundations.CorrelatedSampling.splitRight line 472
  46. def OAI.MaxCutGames.Foundations.CorrelatedSampling.cutAt line 475
  47. def OAI.MaxCutGames.Foundations.CorrelatedSampling.intervalCDF line 477
  48. theorem OAI.MaxCutGames.Foundations.CorrelatedSampling.split_cdf line 479
  49. theorem OAI.MaxCutGames.Foundations.CorrelatedSampling.accepted_interval_mass line 484
  50. theorem OAI.MaxCutGames.Foundations.CorrelatedSampling.splitLeft_cut line 492
  51. theorem OAI.MaxCutGames.Foundations.CorrelatedSampling.splitRight_cut line 497
  52. theorem OAI.MaxCutGames.Foundations.CorrelatedSampling.splitLeft_preserves_cut line 505
  53. theorem OAI.MaxCutGames.Foundations.CorrelatedSampling.splitRight_preserves_cut line 511
  54. def OAI.MaxCutGames.Foundations.CorrelatedSampling.splitAll line 517
  55. def OAI.MaxCutGames.Foundations.CorrelatedSampling.unitThresholdInterval line 521
  56. def OAI.MaxCutGames.Foundations.CorrelatedSampling.thresholdPartition line 523
  57. def OAI.MaxCutGames.Foundations.CorrelatedSampling.sumOnIntervals line 527
  58. theorem OAI.MaxCutGames.Foundations.CorrelatedSampling.sumOn_splitAll line 531
  59. theorem OAI.MaxCutGames.Foundations.CorrelatedSampling.partition_sum line 541
  60. theorem OAI.MaxCutGames.Foundations.CorrelatedSampling.partition_total_mass line 550
  61. theorem OAI.MaxCutGames.Foundations.CorrelatedSampling.partition_cdf line 556
  62. theorem OAI.MaxCutGames.Foundations.CorrelatedSampling.splitAll_new_cuts line 561
  63. theorem OAI.MaxCutGames.Foundations.CorrelatedSampling.splitAll_preserves_cuts line 573
  64. theorem OAI.MaxCutGames.Foundations.CorrelatedSampling.partition_cuts line 587
  65. theorem OAI.MaxCutGames.Foundations.CorrelatedSampling.sumOnIntervals_congr line 597
  66. theorem OAI.MaxCutGames.Foundations.CorrelatedSampling.partition_acceptance_mass line 607
  67. theorem OAI.MaxCutGames.Foundations.CorrelatedSampling.sum_interval_get line 617
  68. theorem OAI.MaxCutGames.Foundations.CorrelatedSampling.sum_div_const_inline_Rectangle line 630
  69. abbrev OAI.MaxCutGames.Foundations.CorrelatedSampling.RectangleSeed line 634
  70. def OAI.MaxCutGames.Foundations.CorrelatedSampling.rectangleWeight line 637
  71. def OAI.MaxCutGames.Foundations.CorrelatedSampling.rectangleAccept line 641
  72. theorem OAI.MaxCutGames.Foundations.CorrelatedSampling.rectangleWeight_nonnegative line 645
  73. theorem OAI.MaxCutGames.Foundations.CorrelatedSampling.rectangleWeight_normalized line 649
  74. def OAI.MaxCutGames.Foundations.CorrelatedSampling.rectangleDistribution line 660
  75. theorem OAI.MaxCutGames.Foundations.CorrelatedSampling.rectangle_row_mass line 666
  76. theorem OAI.MaxCutGames.Foundations.CorrelatedSampling.rectangle_acceptance_mass line 683
  77. theorem OAI.MaxCutGames.Foundations.CorrelatedSampling.rectangle_label_mass line 693
  78. theorem OAI.MaxCutGames.Foundations.CorrelatedSampling.min_mem_thresholds line 722
  79. theorem OAI.MaxCutGames.Foundations.CorrelatedSampling.max_mem_thresholds line 726
  80. theorem OAI.MaxCutGames.Foundations.CorrelatedSampling.rectangle_union_mass line 730
  81. theorem OAI.MaxCutGames.Foundations.CorrelatedSampling.rectangle_common_label_mass line 742