LabelBound.lean`

6 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.

def OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.localSample line 18
def OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.localDiagonal line 22
def OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.goodLabel line 27
theorem OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.common_first_label_lower line 31
theorem OAI.UniqueGamesTheorem.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.UniqueGamesTheorem.Foundations.CorrelatedSampling.eventMass, OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.goodLabel, OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.traceAverage, OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.localDiagonal

theorem OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.rectangle_label_diagonal_bound line 81

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.UniqueGamesTheorem.Foundations.CorrelatedSampling.totalVariation, OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.eventMass, OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.rectangleWeight, OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.rectangleAccept, OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.traceAverage, OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.localDiagonal