Lax Lean Archive

Multiplicative soundness bounds for sampled tests

Lax323828.BernoulliSampling · concepts/Lax323828/BernoulliSampling.lean · lax-323828

proven

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Theorem

    If a test accepts with probability at most pp, the probability that at least 4Np4Np of NN independent samples accept is at most e−Npe^{-Np}. The exponent is linear in pp, which is essential for the randomized PCP-to-clique reduction: an additive bound with exponent Np2Np^2 gives a weaker approximation exponent.

    For a family of at most 2m2^m tests, a union bound gives failure probability at most 2me−Np2^m e^{-Np}. If Np≥m+2Np\geq m+2, this is at most 1/41/4.

    Concept map
    2 concepts; 6 descendants hidden
    100%
    Proven claimThis conceptRelated conceptA → B: B builds on A
    Evidence

    This concept declares 2 statements. Each proof establishes one of them relative to its assumptions.

    1 uniform_upper_tail proven

    2 upper_tail proven

    Lean source view on GitHub

    1import Lax323828.FiniteProbability
    2import Mathlib.Analysis.SpecialFunctions.Exp
    3import Mathlib.Data.Fintype.Pi
    4
    5/-!
    6---
    7title: Multiplicative soundness bounds for sampled tests
    8type: theorem
    9---
    10If a test accepts with probability at most pp, the probability that at
    11least 4Np4Np of NN independent samples accept is at most e−Npe^{-Np}.
    12The exponent is linear in pp, which is essential for the randomized
    13PCP-to-clique reduction: an additive bound with exponent Np2Np^2 gives
    14a weaker approximation exponent.
    15
    16For a family of at most 2m2^m tests, a union bound gives failure probability
    17at most 2me−Np2^m e^{-Np}. If Np≥m+2Np\geq m+2, this is at most 1/41/4.
    18-/
    19
    20namespace Lax323828.BernoulliSampling
    21
    22open scoped Classical
    23
    24open FiniteProbability
    25
    26/-- Count how many of the sampled points satisfy the event `P`. -/
    27noncomputable def count {Ω : Type} [Fintype Ω] (N : ℕ) (P : Ω → Prop)
    28 (z : Fin N → Ω) : ℕ :=
    29 (Finset.univ.filter (fun i ↦ P (z i))).card
    30
    31axiom upper_tail {Ω : Type} [Fintype Ω] [Nonempty Ω]
    32 (N : ℕ) (P : Ω → Prop) (p : ℝ) (hp : 0 ≤ p) (hP : probability P ≤ p) :
    33 probability (fun z : Fin N → Ω ↦ 4 * N * p ≤ (count N P z : ℝ)) ≤
    34 Real.exp (-(N : ℝ) * p)
    35
    36axiom uniform_upper_tail {Ω I : Type} [Fintype Ω] [Nonempty Ω] [Fintype I]
    37 (N m : ℕ) (P : I → Ω → Prop) (p : ℝ) (hp : 0 ≤ p)
    38 (hI : Fintype.card I ≤ 2 ^ m) (hP : ∀ i, probability (P i) ≤ p)
    39 (hN : (m : ℝ) + 2 ≤ N * p) :
    40 probability (fun z : Fin N → Ω ↦ ∃ i, 4 * N * p ≤ (count N (P i) z : ℝ)) ≤ 1 / 4
    41
    42end Lax323828.BernoulliSampling
    43
    Show ProofShow Proof
    Builds on
    Used by
    From Mathlib

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…