Lax Lean Archive

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

A tuple sampler with alphabet-independent mixing

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

    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 Lax253009.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 Lax253009.TupleSampler
    18
    19open FiniteProbability
    20open scoped BigOperators
    21
    22noncomputable def indicator {A : Type} (S : A → Prop) (a : A) : ℝ := by
    23 classical
    24 exact if S a then 1 else 0
    25
    26noncomputable def mass {A : Type} [Fintype A] (t : ℕ)
    27 (S : (Fin t → A) → Prop) (a : A) : ℝ := by
    28 classical
    29 exact 𝔼 i : Fin t, 𝔼 z : Fin t → A, indicator S (Function.update z i a)
    30
    31axiom bounds {A : Type} [Fintype A] [Nonempty A] (t : ℕ) (ht : 0 < t)
    32 (S : (Fin t → A) → Prop) (a : A) : 0 ≤ mass t S a ∧ mass t S a ≤ 1
    33
    34axiom mean {A : Type} [Fintype A] [Nonempty A] (t : ℕ) (ht : 0 < t)
    35 (S : (Fin t → A) → Prop) : (𝔼 a, mass t S a) = probability S
    36
    37axiom mixing {A : Type} [Fintype A] [Nonempty A] (t : ℕ) (ht : 0 < t)
    38 (S : (Fin t → A) → Prop) :
    39 (𝔼 a, |mass t S a - probability S|) ^ 2 ≤ 1 / (t : ℝ)
    40
    41end Lax253009.TupleSampler
    42
    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…