LemmaStatement: AI-adaptedProof: AI-generatedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-07

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.

Tail comparisons under independent-copy symmetrization

Statement

Let $X^{'}$ be an independent copy of a real random variable $X$ . For every $t > 0$ , $P (∣ X - X^{'} ∣ > t) \leq 2 P (∣ X ∣ > t / 2) .$ There exists a finite $M \geq 0$ with $P (∣ X ∣ \leq M) \geq 1 / 2$ ; for every such $M$ , $P (∣ X - X^{'} ∣ > t) \geq \frac{1}{2} P (∣ X ∣ > t + M) .$

Facts & Assumptions

[F1]

Independent-copy symmetrization of random series: Given an independent sequence $(X_{n})_{n \geq 1}$ on $(Ω, F, P)$ , form the product probability space $(Ω^{2}, F \otimes F, P \otimes P)$ . Write $U_{n} (ω, ω^{'}) = X_{n} (ω)$ , $V_{n} (ω, ω^{'}) = X_{n} (ω^{'})$ , and $Z_{n} = U_{n} - V_{n}$ . Then $(U_{n})$ and $(V_{n})$ are independent copies of the whole sequence, and the $Z_{n}$ are independent symmetric real random variables. Almost-sure convergence of $\sum_{n} X_{n}$ implies almost-sure convergence of $\sum_{n} Z_{n}$ . If $∣ X_{n} ∣ \leq A$ almost surely for every $n$ , with $0 \leq A < \infty$ , then $∣ Z_{n} ∣ \leq 2 A$ almost surely, $E Z_{n} = 0$ , and $Var (Z_{n}) = 2 Var (X_{n})$ .

[F2]

Continuity from below for measures: Let $(E_{n})_{n \in N}$ be an increasing sequence of measurable sets for a measure $μ$ , so $E_{n} \subseteq E_{n + 1}$ . Then $μ (⋃_{n \in N} E_{n}) = \sup_{n \in N} μ (E_{n}) .$ No finiteness hypothesis is required.

Proof

Given: The objects and hypotheses of the statement.

1.1

The triangle inequality gives ${∣ X - X' ∣ > t} \subseteq {∣ X ∣ > t / 2} \cup {∣ X' ∣ > t / 2}$ . The union bound and equality of the two marginal laws give the upper estimate. Independent copies can be realized on the two-factor product described by symmetrization.

F1givenalgebra

2.1

The intervals $[- m, m]$ increase to $R$ as positive integers $m$ increase. Continuity from below gives $P (∣ X ∣ \leq m) \to 1$ , so there is a suitable finite $M$ . For any such $M$ , the event ${∣ X ∣ > t + M, ∣ X' ∣ \leq M}$ implies $∣ X - X' ∣ > t$ . Independence makes its probability $P (∣ X ∣ > t + M) P (∣ X ∣ \leq M)$ , giving the lower bound. This includes $M = 0$ when allowed by the law.

F2step 1.1algebra∎

Depends on

Used by

Exact tail criterion for a truncated-centered IID weak law Theorem

Dependency tree · two levels

14 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

Appendix A, Lemma 4.18 and proof, pp. 9–10; symmetric-interval variant (standard reference, not scraped)