Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

Multiplicative soundness bounds for sampled tests

Lax253009.BernoulliSampling · concepts/Lax253009/BernoulliSampling.lean · lax-253009

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 Lax253009.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 Lax253009.BernoulliSampling
    21
    22open FiniteProbability
    23
    24noncomputable def count {Ω : Type} [Fintype Ω] (N : ℕ) (P : Ω → Prop)
    25 (z : Fin N → Ω) : ℕ := by
    26 classical
    27 exact (Finset.univ.filter (fun i ↦ P (z i))).card
    28
    29axiom upper_tail {Ω : Type} [Fintype Ω] [Nonempty Ω]
    30 (N : ℕ) (P : Ω → Prop) (p : ℝ) (hp : 0 ≤ p) (hP : probability P ≤ p) :
    31 probability (fun z : Fin N → Ω ↦ 4 * N * p ≤ (count N P z : ℝ)) ≤
    32 Real.exp (-(N : ℝ) * p)
    33
    34axiom uniform_upper_tail {Ω I : Type} [Fintype Ω] [Nonempty Ω] [Fintype I]
    35 (N m : ℕ) (P : I → Ω → Prop) (p : ℝ) (hp : 0 ≤ p)
    36 (hI : Fintype.card I ≤ 2 ^ m) (hP : ∀ i, probability (P i) ≤ p)
    37 (hN : (m : ℝ) + 2 ≤ N * p) :
    38 probability (fun z : Fin N → Ω ↦ ∃ i, 4 * N * p ≤ (count N (P i) z : ℝ)) ≤ 1 / 4
    39
    40end Lax253009.BernoulliSampling
    41
    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…