Agreement among many decoded tables
Lax323828.ManyTableConsistency · concepts/Lax323828/ManyTableConsistency.lean · lax-323828
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 Lax323828.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 Lax323828.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 Lax323828.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