Lax Lean Archive

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

A uniform sample is unlikely to miss a large set

Lax235315.UniformSampleAvoidance · concepts/Lax235315/UniformSampleAvoidance.lean · lax-235315

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

    Lemma

    Let A be nonempty, let X be a subset of A of size at least 6c²L, and suppose c≥1 and |A|≤N≤2^L. A uniformly chosen subset of A of size ceil(|A|/(2c²)) avoids X with probability at most 1/N³. This is the finite counting form of Lemma 3.7 of Dreier–Kuske.

    Concept map
    1 concept
    100%
    Proven claimThis concept
    Evidence

    Each proof establishes this claim relative to its assumptions.

    Lean source view on GitHub

    1import Mathlib.Data.Finset.Powerset
    2import Mathlib.Data.Real.Basic
    3
    4/-!
    5---
    6title: A uniform sample is unlikely to miss a large set
    7type: lemma
    8---
    9Let A be nonempty, let X be a subset of A of size at least 6c²L, and suppose
    10c≥1 and |A|≤N≤2^L. A uniformly chosen subset of A of size ceil(|A|/(2c²))
    11avoids X with probability at most 1/N³. This is the finite counting form of
    12Lemma 3.7 of Dreier--Kuske.
    13
    14# Formalization notes
    15
    16The numerator counts samples disjoint from X and the denominator counts
    17all subsets of the prescribed size. The assumptions guarantee that the
    18denominator is positive. Natural ceiling division is written explicitly.
    19This is a theorem about ideal fixed-size uniform samples; its connection
    20to the program's finite random keys is a separate proof obligation.
    21-/
    22
    23namespace Lax235315.UniformSampleAvoidance
    24
    25/-- The fraction of fixed-size samples avoiding X is at most N to the power -3. -/
    26axiom miss_fraction_le {n : ℕ} {A X : Finset (Fin n)} {c N L : ℕ}
    27 (hc : 1 ≤ c) (hA : A.Nonempty) (hX : X ⊆ A)
    28 (hXcard : 6 * c ^ 2 * L ≤ X.card)
    29 (hAN : A.card ≤ N) (hNpow : N ≤ 2 ^ L) :
    30 let s := (A.card + 2 * c ^ 2 - 1) / (2 * c ^ 2)
    31 (((A.powersetCard s).filter (fun W => Disjoint W X)).card : ℝ) /
    32 (A.powersetCard s).card ≤ 1 / (N : ℝ) ^ 3
    33
    34end Lax235315.UniformSampleAvoidance
    35
    Show Proof
    Formalization notes

    The numerator counts samples disjoint from X and the denominator counts all subsets of the prescribed size. The assumptions guarantee that the denominator is positive. Natural ceiling division is written explicitly. This is a theorem about ideal fixed-size uniform samples; its connection to the program's finite random keys is a separate proof obligation.

    Builds on

    none

    Used by

    none

    From Mathlib

    Discussion

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

    Loading discussion…