Lax Lean Archive

A tuple sampler with alphabet-independent mixing

Lax323828.TupleSampler · concepts/Lax323828/TupleSampler.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

    For an event S on t-tuples, plant a specified letter in a uniformly chosen coordinate and sample the remaining coordinates independently. Let p_S(a) be the probability of S under this experiment. Its mean is Pr[S], and the square of its mean absolute deviation from Pr[S] is at most 1/t.

    The alphabet size does not enter the bound. Using all tuples as questions therefore gives a polynomial-size sampler for each fixed accuracy.

    Concept map
    3 concepts
    100%
    Proven claimThis conceptRelated conceptA → B: B builds on A
    Evidence

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

    1 bounds proven

    2 mean proven

    3 mixing proven

    Lean source view on GitHub

    1import Lax323828.TupleAveraging
    2
    3/-!
    4---
    5title: A tuple sampler with alphabet-independent mixing
    6type: theorem
    7---
    8For an event S on t-tuples, plant a specified letter in a uniformly chosen
    9coordinate and sample the remaining coordinates independently. Let p_S(a)
    10be the probability of S under this experiment. Its mean is Pr[S], and
    11the square of its mean absolute deviation from Pr[S] is at most 1/t.
    12
    13The alphabet size does not enter the bound. Using all tuples as questions
    14therefore gives a polynomial-size sampler for each fixed accuracy.
    15-/
    16
    17namespace Lax323828.TupleSampler
    18
    19open scoped Classical
    20
    21open FiniteProbability
    22open scoped BigOperators
    23
    24/-- The value one on the event `S`, and zero outside it. -/
    25noncomputable def indicator {A : Type} (S : A → Prop) (a : A) : ℝ :=
    26 if S a then 1 else 0
    27
    28/-- The average indicator after planting `a` at a uniformly chosen coordinate of a uniformly chosen tuple. -/
    29noncomputable def mass {A : Type} [Fintype A] (t : ℕ)
    30 (S : (Fin t → A) → Prop) (a : A) : ℝ :=
    31 𝔼 i : Fin t, 𝔼 z : Fin t → A, indicator S (Function.update z i a)
    32
    33axiom bounds {A : Type} [Fintype A] [Nonempty A] (t : ℕ) (ht : 0 < t)
    34 (S : (Fin t → A) → Prop) (a : A) : 0 ≤ mass t S a ∧ mass t S a ≤ 1
    35
    36axiom mean {A : Type} [Fintype A] [Nonempty A] (t : ℕ) (ht : 0 < t)
    37 (S : (Fin t → A) → Prop) : (𝔼 a, mass t S a) = probability S
    38
    39axiom mixing {A : Type} [Fintype A] [Nonempty A] (t : ℕ) (ht : 0 < t)
    40 (S : (Fin t → A) → Prop) :
    41 (𝔼 a, |mass t S a - probability S|) ^ 2 ≤ 1 / (t : ℝ)
    42
    43end Lax323828.TupleSampler
    44
    Show ProofShow ProofShow Proof
    Builds on
    Used by

    none

    From Mathlib

    none

    Discussion

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

    Loading discussion…