Lax Lean Archive

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

Uniform finite probability and even-moment tail bounds

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

    An event in a finite sample space has probability equal to its cardinality divided by the cardinality of the space. Event inclusion preserves this probability, and the probability of a finite union is at most the sum of the member probabilities. Restriction to a subset of mass at least 1/K1/K increases event probabilities by at most a factor KK.

    For a real random variable XX on a nonempty finite space, t>0t>0, and even mm, Markov's inequality applied to XmX^m gives Pr⁡[X≥t]≤E[Xm]/tm\Pr[X\geq t]\leq\mathbb E[X^m]/t^m. This is the finite tail estimate used in Corollaries 4.6 and 4.11. For 0≤X≤10\leq X\leq1 and q≥0q\geq0, we also prove EXℓ≤qℓ+Pr⁡[X>q]\mathbb E X^\ell\leq q^\ell+\Pr[X>q] by splitting at qq.

    Concept map
    1 concept; 36 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_power_mean proven

    2 even_moment_bound proven

    3 finite_union_bound proven

    4 monotone proven

    5 restriction_bound proven

    6 union_bound proven

    Lean source view on GitHub

    1import Mathlib.Data.Real.Basic
    2import Mathlib.Data.Fintype.Card
    3import Mathlib.Algebra.BigOperators.Expect
    4import Mathlib.Algebra.Ring.Parity
    5
    6/-!
    7---
    8title: Uniform finite probability and even-moment tail bounds
    9type: theorem
    10---
    11An event in a finite sample space has probability equal to its cardinality
    12divided by the cardinality of the space. Event inclusion preserves this
    13probability, and the probability of a finite union is at most the sum of
    14the member probabilities. Restriction to a subset of mass at least 1/K1/K
    15increases event probabilities by at most a factor KK.
    16
    17For a real random variable XX on a nonempty finite space, t>0t>0, and even
    18mm, Markov's inequality applied to XmX^m gives
    19Pr⁡[X≥t]≤E[Xm]/tm\Pr[X\geq t]\leq\mathbb E[X^m]/t^m. This is the finite tail estimate
    20used in Corollaries 4.6 and 4.11. For 0≤X≤10\leq X\leq1 and q≥0q\geq0, we
    21also prove EXℓ≤qℓ+Pr⁡[X>q]\mathbb E X^\ell\leq q^\ell+\Pr[X>q] by splitting at qq.
    22-/
    23
    24namespace Lax253009.FiniteProbability
    25
    26open scoped BigOperators
    27
    28noncomputable def probability {α : Type} [Fintype α] (P : α → Prop) : ℝ := by
    29 classical
    30 exact ((Finset.univ.filter P).card : ℝ) / (Fintype.card α : ℝ)
    31
    32axiom monotone {α : Type} [Fintype α] (P Q : α → Prop) (h : ∀ x, P x → Q x) :
    33 probability P ≤ probability Q
    34
    35axiom union_bound {α : Type} [Fintype α] (P Q : α → Prop) :
    36 probability (fun x ↦ P x ∨ Q x) ≤ probability P + probability Q
    37
    38axiom even_moment_bound {α : Type} [Fintype α] [Nonempty α]
    39 (X : α → ℝ) (t : ℝ) (ht : 0 < t) (m : ℕ) (hm : Even m) :
    40 probability (fun x ↦ t ≤ X x) ≤ (𝔼 x, X x ^ m) / t ^ m
    41
    42axiom restriction_bound {α : Type} [Fintype α] (s : Finset α) (hs : s.Nonempty)
    43 (K : ℝ) (hcard : (Fintype.card α : ℝ) ≤ K * s.card) (P : α → Prop) :
    44 probability (fun x : s ↦ P x.val) ≤ K * probability P
    45
    46axiom finite_union_bound {α ι : Type} [Fintype α] [Fintype ι] (P : ι → α → Prop) :
    47 probability (fun x ↦ ∃ i, P i x) ≤ ∑ i, probability (P i)
    48
    49axiom bounded_power_mean {α : Type} [Fintype α] [Nonempty α]
    50 (X : α → ℝ) (hX : ∀ x, 0 ≤ X x ∧ X x ≤ 1) (q : ℝ) (hq : 0 ≤ q) (l : ℕ) :
    51 (𝔼 x, X x ^ l) ≤ q ^ l + probability (fun x ↦ q < X x)
    52
    53end Lax253009.FiniteProbability
    54
    Show ProofShow ProofShow ProofShow ProofShow ProofShow Proof
    Builds on

    none

    Used by
    From Mathlib

    Discussion

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

    Loading discussion…