LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-6-luna)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

One-sided concentration bound for independent median trials

Statement

Let $R \geq 1$ be an integer, let $Z_{1}, \dots, Z_{R}$ be independent Bernoulli random variables on a finite probability space with $E [Z_{i}] \leq p < 1 / 2$ , and put $S = \sum_{i = 1}^{R} Z_{i}$ . For every $t \geq 0$ , $\Pr (S - E S \geq t) \leq e^{- 2 t^{2} / R} .$ Consequently, let $R$ be odd and let $T_{1}, \dots, T_{R}$ be independent finite-valued real estimates on a finite probability space. If $I \subseteq R$ is an interval and $\Pr (T_{i} \in I) \geq 1 - p$ for every $i$ , then their median (the middle order statistic) lies in $I$ except with probability at most $\exp (- 2 R (1 / 2 - p)^{2}) .$

Facts & Assumptions

Given: A finite probability space, an integer $R \geq 1$ , and an independent Bernoulli family $Z_{1}, \dots, Z_{R}$ with means $p_{i} = E Z_{i} \leq p < 1 / 2$ . For the median consequence, also the independent finite-valued estimates $T_{1}, \dots, T_{R}$ , the interval $I$ , and $\Pr (T_{i} \in I) \geq 1 - p$ for each $i$ .

[F1]

Bernoulli random variables and binomial random variables as sums of independent Bernoulli trials: a Bernoulli variable takes values $0, 1$ with probabilities $1 - p_{i}, p_{i}$ .

[F2]

Independent random elements: mutual independence means the generated event sigma-algebras factor on finite intersections.

[F3]

Expectation factors over a finite product of mutually independent random variables: expectations of finite products of independent finite-valued real variables factor.

[F4]

Markov's inequality on a finite probability space: for nonnegative $W$ and $c > 0$ , $\Pr (W \geq c) \leq E [W] / c$ .

[F5]

The real exponential function and the number $e$ by a power series fixes $\exp$ and $e = \exp (1)$ ; The exponential is positive and satisfies $\exp (- x) = 1 / \exp (x)$ gives $\exp (x) > 0$ ; The exponential addition formula $\exp (x + y) = \exp (x) \exp (y)$ gives $\exp (x + y) = \exp (x) \exp (y)$ ; The exponential function is strictly increasing makes $\exp$ order preserving; and The natural logarithm as the inverse of the exponential function defines $\ln$ as its inverse.

[F6]

The exponential function is smooth and $(\exp)^{'} = \exp$ , The natural logarithm has derivative 1/x and equals the integral from 1 to x of 1/t, The chain rule, in one line from Carathéodory: if $g$ is differentiable at $c$ and $f$ is differentiable at $g (c)$ , then $f \circ g$ is differentiable at $c$ with $(f \circ g)^{'} (c) = f^{'} (g (c)) g^{'} (c)$ , and Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ give the derivative rules for the positive exponential, logarithm, sums, products, and quotients used below.

[F7]

The mean value theorem, as the case $g (x) = x$ of Cauchy's: for $f$ continuous on $[a, b]$ with $a < b$ and differentiable on $(a, b)$ there is $c \in (a, b)$ with $f (b) - f (a) = f^{'} (c) (b - a)$ : if a function is continuous on $[a, b]$ and differentiable on $(a, b)$ , then its endpoint increment is its derivative at some interior point times $b - a$ .

[F8]

Expectation of a real random variable on a finite probability space: the expectation of a finite-valued variable is the finite weighted sum of its values, including the Bernoulli formula.

[F9]

Linearity, monotonicity, and the modulus bound for expectation: expectation is linear for the finite-valued real random variables below.

[F10]

A function differentiable at $c$ is continuous at $c$ : a function differentiable at a point is continuous there.

[F11]

Expectation agrees with the published finite weighted sum identifies general expectations of finite random variables on this probability space with the finite weighted sums in [F8].

Proof

1.1givenF1F5F6F8algebra

For one Bernoulli variable $Z_{i}$ , [F1] and [F8] give $E Z_{i} = p_{i}$ . Define $M_{i} (λ) = E [\exp (λ (Z_{i} - p_{i}))] = \exp (- λ p_{i}) (1 - p_{i} + p_{i} \exp (λ)) > 0$ by its two possible values and [F5], and put $G_{i} (λ) = \ln M_{i} (λ)$ . Set $q_{i} (λ) = p_{i} \exp (λ) / (1 - p_{i} + p_{i} \exp (λ)) \in [0, 1]$ . Differentiating by [F6] gives $G_{i} (0) = G_{i}^{'} (0) = 0$ and $G_{i}^{''} (λ) = q_{i} (λ) (1 - q_{i} (λ)) \leq 1 / 4$ , including $p_{i} = 0$ and $p_{i} = 1$ .

2.1step 1.1F5F6F7F10algebra

At $λ = 0$ the desired bound is equality. For $λ > 0$ , put $H_{i} (t) = G_{i} (t) - t^{2} / 8$ on $[0, λ]$ . By step 1.1, $H_{i}^{''} (t) \leq 0$ . The functions $H_{i}$ and $H_{i}^{'}$ are continuous by [F10], so the hypotheses of [F7] apply. For any $0 < v \leq λ$ , [F7] applied to $H_{i}^{'}$ on $[0, v]$ gives $H_{i}^{'} (v) - H_{i}^{'} (0) = H_{i}^{''} (c) v \leq 0$ for some $c \in (0, v)$ ; since $H_{i}^{'} (0) = 0$ , this shows $H_{i}^{'} (v) \leq 0$ . Applying [F7] to $H_{i}$ on $[0, λ]$ then gives $H_{i} (λ) - H_{i} (0) = H_{i}^{'} (d) λ \leq 0$ for some $d \in (0, λ)$ . As $H_{i} (0) = 0$ , $G_{i} (λ) \leq λ^{2} / 8$ . Therefore $E [\exp (λ (Z_{i} - p_{i}))] \leq \exp (λ^{2} / 8)$ for every $λ \geq 0$ .

3.1givenF2F3F5F8F9F11step 2.1algebra

By [F11], the general expectations in [F3] and [F9] agree with the finite weighted sums in [F8]. Thus [F8]–[F9] give $E S = \sum_{i} p_{i}$ and $S - E S = \sum_{i} (Z_{i} - p_{i})$ . For $λ \geq 0$ , put $W_{i} = \exp (λ (Z_{i} - p_{i}))$ . Since each $Z_{i}$ is finite-valued, every event defined by $W_{i}$ is a union of level sets of $Z_{i}$ , so $σ (W_{i}) \subseteq σ (Z_{i})$ ; the independence in [F2] therefore makes the $W_{i}$ independent. The exponential addition law [F5] and finite product factorization [F3] now give $E [\exp (λ (S - E S))] = \prod_{i} E [W_{i}] \leq \exp (R λ^{2} / 8)$ by step 2.1.

4.1givenF4step 3.1algebra

For $t > 0$ , choose $λ = 4 t / R > 0$ and apply [F4] to the nonnegative variable $e^{λ (S - E S)}$ at threshold $e^{λ t}$ . Step 3.1 gives $\Pr (S - E S \geq t) \leq e^{- λ t + R λ^{2} / 8} = e^{- 2 t^{2} / R}$ . For $t = 0$ , the probability is at most one, equal to the stated bound.

5.1givenF1F2F8F9F11step 4.1algebra∎

Let $Y_{i}$ indicate the event $T_{i} \notin I$ . Each $Y_{i}$ is Bernoulli with mean at most $p$ by [F1], [F8], and the interval-success hypothesis. Each $Y_{i}$ is a function of the finite-valued $T_{i}$ , so every event defined by $Y_{i}$ is a union of level sets of $T_{i}$ ; hence $σ (Y_{i}) \subseteq σ (T_{i})$ and [F2] makes the $Y_{i}$ independent. By [F11], [F9] applies to the same finite weighted-sum expectations as [F8], so $E S = \sum_{i} E Y_{i} \leq p R$ . If the odd median is outside $I$ , at least $(R + 1) / 2$ estimates lie on one side of $I$ and fail, so $S = \sum_{i} Y_{i} \geq R / 2$ and $S - E S \geq R (1 / 2 - p)$ . Apply step 4.1 with this $t$ to get the stated median bound.

Depends on

Used by

Dependency tree · two levels

74 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Ashley Montanaro, Quantum speedup of Monte Carlo methods, Lemma 1 and Theorems 3 and 5 (standard reference, not scraped)
Andrew M. Childs, Lecture Notes on Quantum Algorithms, Section 19.3 (standard reference, not scraped)