Agreement among many decoded tables
Lax253009.ManyTableConsistency · concepts/Lax253009/ManyTableConsistency.lean · lax-253009
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Theorem
The finite counting argument behind Lemmas 5.7 and 5.8. Each independently sampled table supplies at most projected assignments, and each fixed assignment occurs with probability at most . A selection with at most distinct assignments forces all remaining tables to meet the union of at most representative tables. Random Boolean functions are unlikely to be constant on a selection with many distinct assignments.
These bounds concern finite probability spaces. They do not assert a PCP construction or its computational complexity.
Concept map
Evidence
Lean source view on GitHub
| 1 | import Lax253009.FiniteProbability |
| 2 | import Mathlib.Data.Fintype.Pi |
| 3 | import Mathlib.Data.Finset.Powerset |
| 4 | |
| 5 | /-! |
| 6 | --- |
| 7 | title: Agreement among many decoded tables |
| 8 | type: theorem |
| 9 | --- |
| 10 | The finite counting argument behind Lemmas 5.7 and 5.8. Each independently |
| 11 | sampled table supplies at most projected assignments, and each fixed |
| 12 | assignment occurs with probability at most . A selection with at most |
| 13 | distinct assignments forces all remaining tables to meet the union |
| 14 | of at most representative tables. Random Boolean functions are unlikely |
| 15 | to be constant on a selection with many distinct assignments. |
| 16 | |
| 17 | These bounds concern finite probability spaces. They do not assert a PCP |
| 18 | construction or its computational complexity. |
| 19 | -/ |
| 20 | |
| 21 | namespace Lax253009.ManyTableConsistency |
| 22 | |
| 23 | open FiniteProbability |
| 24 | |
| 25 | def LowDiversity {ι Ω X : Type} [Fintype ι] [DecidableEq X] |
| 26 | (S : Ω → Finset X) (k : ℕ) (w : ι → Ω) : Prop := |
| 27 | ∃ y : ι → X, (∀ i, y i ∈ S (w i)) ∧ (Finset.univ.image y).card ≤ k |
| 28 | |
| 29 | def Agreement {ι Ω X : Type} (S : Ω → Finset X) (q : ℕ) |
| 30 | (w : ι → Ω) (g : Fin q → X → Bool) : Prop := |
| 31 | ∃ y : ι → X, (∀ i, y i ∈ S (w i)) ∧ ∀ j, ∃ b, ∀ i, g j (y i) = b |
| 32 | |
| 33 | axiom low_diversity_bound {ι Ω X : Type} [Fintype ι] [DecidableEq ι] |
| 34 | [Fintype Ω] [Nonempty Ω] [Fintype X] [DecidableEq X] |
| 35 | (S : Ω → Finset X) (B k : ℕ) (p : ℝ) (hp : 0 ≤ p) |
| 36 | (hB : ∀ w, (S w).card ≤ B) |
| 37 | (hpoint : ∀ x, probability (fun w ↦ x ∈ S w) ≤ p) |
| 38 | (hsmall : (Fintype.card ι : ℝ) * B * p ≤ 1) : |
| 39 | probability (LowDiversity (ι := ι) S k) ≤ |
| 40 | (2 : ℝ) ^ Fintype.card ι * ((Fintype.card ι : ℝ) * B * p) ^ (Fintype.card ι - k) |
| 41 | |
| 42 | axiom agreement_bound {ι Ω X : Type} [Fintype ι] [DecidableEq ι] |
| 43 | [Fintype Ω] [Nonempty Ω] [Fintype X] [DecidableEq X] |
| 44 | (S : Ω → Finset X) (B k q : ℕ) (p : ℝ) (hp : 0 ≤ p) |
| 45 | (hB : ∀ w, (S w).card ≤ B) |
| 46 | (hpoint : ∀ x, probability (fun w ↦ x ∈ S w) ≤ p) |
| 47 | (hsmall : (Fintype.card ι : ℝ) * B * p ≤ 1) : |
| 48 | probability (fun z : (ι → Ω) × (Fin q → X → Bool) ↦ Agreement S q z.1 z.2) ≤ |
| 49 | (2 : ℝ) ^ Fintype.card ι * ((Fintype.card ι : ℝ) * B * p) ^ (Fintype.card ι - k) + |
| 50 | (B : ℝ) ^ Fintype.card ι * (2 * (1 / 2 : ℝ) ^ (k + 1)) ^ q |
| 51 | |
| 52 | end Lax253009.ManyTableConsistency |
| 53 |
Builds on
Used by
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments