Lax Lean Archive

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

Exponential concentration on finite product spaces

Lax253009.ExponentialBounds · concepts/Lax253009/ExponentialBounds.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 a finite random variable, exponential Markov bounds its upper tail by e−utEeuXe^{-ut}\mathbb E e^{uX} for u≥0u\geq0. A centered variable in [−1,1][-1,1] has exponential moment at most eu2/2e^{u^2/2}. Independence multiplies these bounds on a uniform finite product space.

    For independent uniform signs and real coefficients aia_i with ∑iai2≤v\sum_i a_i^2\leq v, v>0v>0, the upper tail at t≥0t\geq0 is at most e−t2/(2v)e^{-t^2/(2v)}, and the absolute tail is at most twice this quantity. These finite concentration estimates supply the Chernoff step in the soundness analysis.

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

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

    1 bounded_mgf proven

    2 exponential_markov proven

    3 independent_bounded_upper_tail proven

    4 rademacher_abs_tail proven

    5 rademacher_mgf proven

    6 rademacher_upper_tail proven

    Lean source view on GitHub

    1import Lax253009.BooleanFourier
    2import Lax253009.FiniteProbability
    3import Mathlib.Analysis.SpecialFunctions.Exp
    4
    5/-!
    6---
    7title: Exponential concentration on finite product spaces
    8type: theorem
    9---
    10For a finite random variable, exponential Markov bounds its upper tail by
    11e−utEeuXe^{-ut}\mathbb E e^{uX} for u≥0u\geq0.
    12A centered variable in [−1,1][-1,1] has exponential moment at most eu2/2e^{u^2/2}.
    13Independence multiplies these bounds on a uniform finite product space.
    14
    15For independent uniform signs and real coefficients aia_i with
    16∑iai2≤v\sum_i a_i^2\leq v, v>0v>0, the upper tail at t≥0t\geq0 is at most
    17e−t2/(2v)e^{-t^2/(2v)}, and the absolute tail is at most twice this quantity.
    18These finite concentration estimates supply the Chernoff step in the
    19soundness analysis.
    20-/
    21
    22namespace Lax253009.ExponentialBounds
    23
    24open BooleanFourier FiniteProbability
    25open scoped BigOperators
    26
    27axiom exponential_markov {α : Type} [Fintype α] [Nonempty α]
    28 (X : α → ℝ) (t u : ℝ) (hu : 0 ≤ u) :
    29 probability (fun x ↦ t ≤ X x) ≤ Real.exp (-u * t) * (𝔼 x, Real.exp (u * X x))
    30
    31axiom bounded_mgf {α : Type} [Fintype α] [Nonempty α]
    32 (X : α → ℝ) (hX : ∀ x, |X x| ≤ 1) (hmean : (𝔼 x, X x) = 0) (u : ℝ) :
    33 (𝔼 x, Real.exp (u * X x)) ≤ Real.exp (u ^ 2 / 2)
    34
    35axiom independent_bounded_upper_tail {ι κ : Type} [Fintype ι] [DecidableEq ι]
    36 [Fintype κ] [Nonempty κ] (F : ι → κ → ℝ)
    37 (hF : ∀ i z, |F i z| ≤ 1) (hmean : ∀ i, (𝔼 z, F i z) = 0)
    38 (hN : 0 < Fintype.card ι) (t : ℝ) (ht : 0 ≤ t) :
    39 probability (fun x : ι → κ ↦ t ≤ ∑ i, F i (x i)) ≤
    40 Real.exp (-t ^ 2 / (2 * Fintype.card ι))
    41
    42axiom rademacher_mgf {ι : Type} [Fintype ι] [DecidableEq ι] (a : ι → ℝ) (u : ℝ) :
    43 (𝔼 x : Cube ι, Real.exp (u * ∑ i, a i * sign (x i))) ≤
    44 Real.exp (u ^ 2 / 2 * ∑ i, a i ^ 2)
    45
    46axiom rademacher_upper_tail {ι : Type} [Fintype ι] [DecidableEq ι]
    47 (a : ι → ℝ) (v : ℝ) (hv : 0 < v) (hvar : ∑ i, a i ^ 2 ≤ v)
    48 (t : ℝ) (ht : 0 ≤ t) :
    49 probability (fun x : Cube ι ↦ t ≤ ∑ i, a i * sign (x i)) ≤
    50 Real.exp (-t ^ 2 / (2 * v))
    51
    52axiom rademacher_abs_tail {ι : Type} [Fintype ι] [DecidableEq ι]
    53 (a : ι → ℝ) (v : ℝ) (hv : 0 < v) (hvar : ∑ i, a i ^ 2 ≤ v)
    54 (t : ℝ) (ht : 0 ≤ t) :
    55 probability (fun x : Cube ι ↦ t ≤ |∑ i, a i * sign (x i)|) ≤
    56 2 * Real.exp (-t ^ 2 / (2 * v))
    57
    58end Lax253009.ExponentialBounds
    59
    Show ProofShow ProofShow ProofShow ProofShow 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…