RoundingSampling.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Correlated rounding of finite partial assignments of equal density. A common finite list of seeds is scanned locally at every vertex. An edge succeeds when the first seed accepted by either endpoint is a jointly accepted good seed. The finite truncation error is at most (1 - density)^n. Maximizing over the finite set of deterministic labelings removes that error. No infinite random seed or assumed rounding principle is used.

def OAI.UniqueGamesTheorem.Repetition.partialPairMass line 28
def OAI.UniqueGamesTheorem.Repetition.partialEdgeMass line 32
def OAI.UniqueGamesTheorem.Repetition.partialLabelScore line 37
def OAI.UniqueGamesTheorem.Repetition.partialSample line 41
theorem OAI.UniqueGamesTheorem.Repetition.expectation_mono' line 45
theorem OAI.UniqueGamesTheorem.Repetition.expectation_const' line 52
theorem OAI.UniqueGamesTheorem.Repetition.first_good_relation_le line 57
theorem OAI.UniqueGamesTheorem.Repetition.partial_mass_bounds line 80
theorem OAI.UniqueGamesTheorem.Repetition.partial_ratio_bound line 110

theorem OAI.UniqueGamesTheorem.Repetition.partialSample_pair_lower line 133

Source documentation

Pointwise success bound for the actual shared finite first-accept sampler. The relation may depend on the ordered pair and need not be symmetric.

theorem partialSample_pair_lower (μ : FiniteDistribution S)
    (accept : V → S → Bool) (label : V → S → A)
    (R : V → V → A → A → Bool) (fallback : A) (density : ℝ)
    (hdensity₀ : 0 < density) (hdensity : ∀ v, μ.probability (accept v) = density)
    (x y : V) (n : Nat) :
    2 * (partialPairMass μ accept label R x y / density) - 1 - (1 - density) ^ n ≤
      traceAverage μ.weight n (fun proposals =>
        if R x y (partialSample accept label fallback proposals x)
          (partialSample accept label fallback proposals y) then 1 else 0) := by
…

Mentions: OAI.UniqueGamesTheorem.Repetition.partialPairMass, OAI.UniqueGamesTheorem.Repetition.partialSample

theorem OAI.UniqueGamesTheorem.Repetition.expectation_partial_lower line 172

theorem OAI.UniqueGamesTheorem.Repetition.exists_labeling_ge_partial line 189

Source documentation

Finite partial-assignment correlated rounding. Every vertex has acceptance probability density. The normalized accepted good-pair mass T gives an actual deterministic labeling with success at least 2*T - 1.

theorem exists_labeling_ge_partial {E : Type*} [Fintype E] [Nonempty V] [Nonempty A]
    (μ : FiniteDistribution S) (ν : FiniteDistribution E)
    (accept : V → S → Bool) (label : V → S → A)
    (left right : E → V) (R : E → A → A → Bool) (density : ℝ) (hdensity₀ : 0 < density)
    (hdensity : ∀ v, μ.probability (accept v) = density) :
    ∃ f : V → A,
      2 * (ν.expectation (partialEdgeMass μ accept label left right R) / density) - 1 ≤
        partialLabelScore ν left right R f := by
…

Mentions: OAI.UniqueGamesTheorem.Repetition.partialEdgeMass, OAI.UniqueGamesTheorem.Repetition.partialLabelScore