Lax Lean Archive

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

Refined sample

Lax457868.RefinedSample · concepts/Lax457868/RefinedSample.lean · lax-457868

definition

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

    Definition

    A refined sample of a set system on a finite ground set is a subset of the ground set of a prescribed maximum size such that any two members of the system with the same trace on the sample differ on at most a prescribed number of ground-set elements.

    Concept map
    2 concepts
    100%
    DefinitionThis conceptRelated conceptA → B: B builds on A

    Lean source view on GitHub

    1import Lax195003.WelzlOrders
    2import Mathlib.Data.Set.Card
    3
    4/-!
    5---
    6title: Refined sample
    7type: definition
    8---
    9A refined sample of a set system on a finite ground set is a subset of the
    10ground set of a prescribed maximum size such that any two members of the
    11system with the same trace on the sample differ on at most a prescribed
    12number of ground-set elements.
    13
    14# Formalization notes
    15
    16The size and disagreement thresholds are parameters. This separates the
    17mathematical output contract from the randomized procedure that produces a
    18sample; the procedure and its probability analysis remain in the proof
    19package.
    20-/
    21
    22namespace Lax457868.RefinedSample
    23
    24open Lax195003.WelzlOrders
    25
    26/-- `W` is a refined sample of `𝓕` inside `A`, with size threshold `m` and
    27disagreement threshold `k`. -/
    28def IsRefinedSample {α : Type*} (𝓕 : SetSystem α) (A W : Set α)
    29 (m k : ℕ) : Prop :=
    30 A.Finite ∧
    31 (∀ X ∈ 𝓕, X ⊆ A) ∧
    32 W ⊆ A ∧
    33 W.ncard ≤ m ∧
    34 ∀ X ∈ 𝓕, ∀ Y ∈ 𝓕, X ∩ W = Y ∩ W →
    35 ((X \ Y) ∪ (Y \ X)).ncard ≤ k
    36
    37end Lax457868.RefinedSample
    38
    Formalization notes

    The size and disagreement thresholds are parameters. This separates the mathematical output contract from the randomized procedure that produces a sample; the procedure and its probability analysis remain in the proof package.

    Builds on
    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…