LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge 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.

The Gaussian-mixture threshold is the stated square-root boundary

Statement

Let $α \in (0, 1)$ , $ρ > 0$ , $v \geq 0$ , and $s \in R$ . Define $M (v, s) : = \sqrt{\frac{ρ}{v + ρ}} \exp ⁣ (\frac{s^{2}}{2 (v + ρ)}) .$ For $u_{α}$ from Gaussian-mixture confidence-sequence boundary, $M (v, s) \geq \frac{1}{α} ⟺ ∣ s ∣ \geq u_{α} (v) .$

Facts & Assumptions

Given: $α \in (0, 1)$ , $ρ > 0$ , $v \geq 0$ , and $s \in R$ .

[F1]

Gaussian-mixture confidence-sequence boundary: $u_{α} (v) = \sqrt{(v + ρ) \log ((v + ρ) / (α^{2} ρ))}$ .

[F2]

Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm: the natural logarithm is strictly increasing on $(0, \infty)$ and satisfies $\log (x y) = \log x + \log y$ for positive $x, y$ .

[F3]

Square roots exist: a unique $\sqrt{a} \geq 0$ with $(\sqrt{a})^{2} = a$ ; the positives are ${x^{2} : x \neq 0}$ : every nonnegative real has a unique nonnegative square root.

Proof

1.1givenF2algebra

Since $M (v, s) > 0$ , applying the strictly increasing logarithm [F2] shows $M (v, s) \geq 1 / α$ iff $s^{2} / [2 (v + ρ)] - \frac{1}{2} \log ((v + ρ) / ρ) \geq \log (1 / α)$ . Multiplying by $2 (v + ρ) > 0$ and combining logarithms gives $s^{2} \geq (v + ρ) \log ((v + ρ) / (α^{2} ρ))$ .

2.1F1F3step 1.1∎

The ratio $(v + ρ) / (α^{2} ρ)$ exceeds $1$ , so its logarithm is positive and [F3] supplies the nonnegative root in [F1]. Thus the last inequality in step 1.1 is exactly $∣ s ∣ \geq u_{α} (v)$ .

Depends on

Used by

A Gaussian mixture confidence sequence for conditional sub-Gaussian means Theorem

Dependency tree · two levels

15 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

Steven R. Howard, Aaditya Ramdas, Jon McAuliffe, and Jasjeet Sekhon, Time-uniform, nonparametric, nonasymptotic confidence sequences, Proposition 5 (standard reference, not scraped)
Aaditya Ramdas, Martingales 1: Concentration Inequalities — Conjugate Mixtures, 36-771 lecture notes, Carnegie Mellon University, Fall 2018, Proposition 1 (standard reference, not scraped)