Lax Lean Archive

Dimension-independent bounds for tuple averaging

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

    The average of t independent samples of a function in [-1,1] has variance at most 1/t. Restricting to any event cannot increase its unnormalized correlation with the centered sample average beyond 1/sqrt(t). These bounds do not depend on the size of the sample alphabet. They provide the averaging estimate for fortifying projection games by tuple questions.

    Concept map
    2 concepts; 1 descendant 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 restriction_correlation proven

    2 variance_bound proven

    Lean source view on GitHub

    1import Lax323828.FiniteProbability
    2import Mathlib.Data.Fintype.Pi
    3
    4/-!
    5---
    6title: Dimension-independent bounds for tuple averaging
    7type: theorem
    8---
    9The average of t independent samples of a function in [-1,1] has variance
    10at most 1/t. Restricting to any event cannot increase its unnormalized
    11correlation with the centered sample average beyond 1/sqrt(t).
    12These bounds do not depend on the size of the sample alphabet. They provide
    13the averaging estimate for fortifying projection games by tuple questions.
    14-/
    15
    16namespace Lax323828.TupleAveraging
    17
    18open scoped BigOperators
    19
    20axiom variance_bound {A : Type} [Fintype A] [Nonempty A]
    21 (t : ℕ) (ht : 0 < t) (f : A → ℝ) (hf : ∀ a, |f a| ≤ 1) :
    22 (𝔼 z : Fin t → A, ((𝔼 i, f (z i)) - (𝔼 a, f a)) ^ 2) ≤ 1 / (t : ℝ)
    23
    24axiom restriction_correlation {A : Type} [Fintype A] [Nonempty A]
    25 (t : ℕ) (ht : 0 < t) (f : A → ℝ) (hf : ∀ a, |f a| ≤ 1)
    26 (S : (Fin t → A) → Prop) [DecidablePred S] :
    27 |𝔼 z : Fin t → A, if S z then (𝔼 i, f (z i)) - (𝔼 a, f a) else 0| ^ 2 ≤
    28 1 / (t : ℝ)
    29
    30end Lax323828.TupleAveraging
    31
    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…