Lax Lean Archive

Uniform finite probability and even-moment tail bounds

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

    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; 39 descendants hidden
    100%
    Proven claimDefinitionThis 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 Lax323828.FiniteProbability
    25
    26open scoped Classical
    27
    28open scoped BigOperators
    29
    30/-- The proportion of points in the finite sample space satisfying the event `P`. -/
    31noncomputable def probability {α : Type} [Fintype α] (P : α → Prop) : ℝ :=
    32 ((Finset.univ.filter P).card : ℝ) / (Fintype.card α : ℝ)
    33
    34axiom monotone {α : Type} [Fintype α] (P Q : α → Prop) (h : ∀ x, P x → Q x) :
    35 probability P ≤ probability Q
    36
    37axiom union_bound {α : Type} [Fintype α] (P Q : α → Prop) :
    38 probability (fun x ↦ P x ∨ Q x) ≤ probability P + probability Q
    39
    40axiom even_moment_bound {α : Type} [Fintype α] [Nonempty α]
    41 (X : α → ℝ) (t : ℝ) (ht : 0 < t) (m : ℕ) (hm : Even m) :
    42 probability (fun x ↦ t ≤ X x) ≤ (𝔼 x, X x ^ m) / t ^ m
    43
    44axiom restriction_bound {α : Type} [Fintype α] (s : Finset α) (hs : s.Nonempty)
    45 (K : ℝ) (hcard : (Fintype.card α : ℝ) ≤ K * s.card) (P : α → Prop) :
    46 probability (fun x : s ↦ P x.val) ≤ K * probability P
    47
    48axiom finite_union_bound {α ι : Type} [Fintype α] [Fintype ι] (P : ι → α → Prop) :
    49 probability (fun x ↦ ∃ i, P i x) ≤ ∑ i, probability (P i)
    50
    51axiom bounded_power_mean {α : Type} [Fintype α] [Nonempty α]
    52 (X : α → ℝ) (hX : ∀ x, 0 ≤ X x ∧ X x ≤ 1) (q : ℝ) (hq : 0 ≤ q) (l : ℕ) :
    53 (𝔼 x, X x ^ l) ≤ q ^ l + probability (fun x ↦ q < X x)
    54
    55end Lax323828.FiniteProbability
    56
    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…