Basic.lean`

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

def OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.firstAccepted line 27

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

theorem OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.first_union_common line 34

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.UniqueGamesTheorem.Foundations.CorrelatedSampling.firstAccepted

def OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.thresholdSample line 59
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 α :=
…
```
theorem OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.thresholdSample_agreement line 63
def OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.totalVariation line 84
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
```
def OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.overlapMass line 86
def OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.unionMass line 88
theorem OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.totalVariation_nonneg line 90
theorem OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.overlapMass_nonneg line 94
theorem OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.min_abs_identity line 98
theorem OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.max_abs_identity line 105
theorem OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.overlapMass_eq line 113
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.UniqueGamesTheorem.Foundations.CorrelatedSampling.overlapMass, OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.totalVariation
theorem OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.unionMass_eq line 122
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.UniqueGamesTheorem.Foundations.CorrelatedSampling.unionMass, OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.totalVariation
theorem OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.totalVariation_le_one line 130
theorem OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.overlap_union_ratio line 138
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.UniqueGamesTheorem.Foundations.CorrelatedSampling.overlapMass, OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.unionMass, OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.totalVariation
theorem OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.overlap_union_ratio_lower_bound line 146
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.UniqueGamesTheorem.Foundations.CorrelatedSampling.totalVariation, OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.overlapMass, OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.unionMass
theorem OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.first_union_disagreement_upper_bound line 157
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.UniqueGamesTheorem.Foundations.CorrelatedSampling.overlapMass, OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.unionMass, OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.totalVariation