ExampleConstruction: AI-generatedVerification: AI-generatedPipeline-generated

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.

Selective inference after choosing the larger of two means

Example

Assume AC, as in the standard-normal, multivariate-normal, and selective-pivot conventions. Let $W = (W_{1}, W_{2})^{T}$ have independent standard normal coordinates, fix $μ = (μ_{1}, μ_{2})^{T} \in R^{2}$ and known $σ > 0$ , and set $Y = μ + σ W$ . Then $Y$ is the concrete realization of $N_{2} (μ, σ^{2} I_{2})$ in the multivariate normal definition, with coordinates $Y_{i} = μ_{i} + σ W_{i}$ . Select index 1 on $S = {Y_{1} \geq Y_{2}}$ and then infer about the fixed contrast $μ_{1}$ . Take $n = 2$ , $η = (1, 0)^{T}$ , $A = (- 1, 1)$ and $b = 0$ . The selected contrast is $T = Y_{1}$ , the orthogonal residual is $Z = (0, Y_{2})$ , and the truncation interval is $[Y_{2}, + \infty)$ .

At the observed data $(Y_{1}, Y_{2}) = (1, 0)$ , with $σ = 1$ , the pivot for the null value $ϑ = 0$ and the two-sided selective p-value are $q_{0} = \frac{Φ (1) - Φ (0)}{1 - Φ (0)}, p_{0} = 2 \min {q_{0}, 1 - q_{0}} .$ The expression conditions out the fact that the first observation was selected because it was larger. For a fixed $α \in [0, 1]$ , the corresponding central confidence set is $C_{η} (Y) = {ϑ \in Θ_{η} : α / 2 \leq q_{ϑ} (Y) \leq 1 - α / 2}$ , where $Θ_{η} = {η^{T} μ : P_{μ} (S) > 0}$ as in Exact selective tests and confidence sets from the pivot.

Facts & Assumptions

Given: AC, independent standard-normal variables $W_{1}, W_{2}$ , means $μ_{1}, μ_{2} \in R$ , known $σ > 0$ , the fixed selection event $Y_{1} \geq Y_{2}$ , and the observed pair $(1, 0)$ for the numerical illustration.

[A1]

AC is assumed by the standard-normal and multivariate-normal laws, the polyhedral pivot definition, and the conditional-uniform theorem. The Axiom of Choice

[F1]

For $η = (1, 0)^{T}$ and $A = (- 1, 1)$ , the polyhedral interval is computed by the row-coefficient formulas in the definition. Polyhedral selection event and contrast interval

[F2]

The candidate-contrast pivot is the standard-normal CDF difference divided by the truncation normalizer, with $s = σ ∥ η ∥$ and $Φ (+ \infty) = 1$ . Polyhedral selective normal pivot

[F3]

The pivot is Uniform $(0, 1)$ conditionally on the fixed selection event and residual, whenever the selection probability is positive. The truncated normal selective pivot is conditionally uniform

[F4]

The two-sided pivot p-value is valid under the point null, and $C_{η} (Y) = {ϑ \in Θ_{η} : α / 2 \leq q_{ϑ} (Y) \leq 1 - α / 2}$ has exact conditional coverage, where $Θ_{η} = {η^{T} μ : P_{μ} (S) > 0}$ . Exact selective tests and confidence sets from the pivot

[F5]

A scalar normal law with positive variance is the affine image of the standard normal law. Standard normal and normal laws

[F6]

The standard normal CDF is strictly increasing. The standard normal CDF is continuous and strictly increasing

[F7]

Independent random elements have their product joint law. Independent random elements have product joint law

[F8]

The isotropic multivariate normal law has the realization $Y = μ + σ W$ with independent standard-normal coordinates. Multivariate normal law, including singular covariance

Verification

1.1A1F1F5F6F7F8algebra

The model is the isotropic Gaussian construction in [F8]; [F5] gives each scalar marginal as an affine image of a standard normal. For $σ > 0$ , [F6] gives $P_{μ} (1 < Y_{1} \leq 2) = Φ ((2 - μ_{1}) / σ) - Φ ((1 - μ_{1}) / σ) > 0$ and $P_{μ} (0 < Y_{2} \leq 1) = Φ ((1 - μ_{2}) / σ) - Φ ((0 - μ_{2}) / σ) > 0$ . By [F7], the rectangle $(1, 2] \times (0, 1]$ has probability equal to the product of these positive probabilities; it lies in $S$ , so $P_{μ} (S) > 0$ . Here $c_{η} = (1, 0)^{T}$ . The single row has $r_{1} = (- 1, 1) c_{η} = - 1$ and, at $z = (0, Y_{2})$ , $d_{1} (z) = - Y_{2}$ . Thus $L (z) = d_{1} (z) / r_{1} = Y_{2}$ , there are no upper constraints so $U (z) = + \infty$ , and $G (z)$ is true. The event is exactly $Y_{1} \geq Y_{2}$ , giving interval $[Y_{2}, + \infty)$ .

2.1A1F2step 1.1algebra

Since $T = Y_{1}$ , $θ = μ_{1}$ , and $s = σ$ , the definition [F2] gives $q_{ϑ} (Y_{1}, Y_{2}) = [Φ ((Y_{1} - ϑ) / σ) - Φ ((Y_{2} - ϑ) / σ)] / [1 - Φ ((Y_{2} - ϑ) / σ)]$ . At $(Y_{1}, Y_{2}) = (1, 0)$ , $σ = 1$ , and $ϑ = 0$ , this becomes the displayed $q_{0}$ .

3.1A1F3F4step 2.1∎

Under the point null $μ_{1} = 0$ , [F3] makes $q_{0}$ Uniform $(0, 1)$ conditionally on selection, so [F4] gives the stated two-sided p-value and exact selective test. For general $ϑ$ , the set retaining $α / 2 \leq q_{ϑ} \leq 1 - α / 2$ has conditional coverage $1 - α$ by [F4]. No claim about a selected-family simultaneous guarantee is used.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

45 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

Jason D. Lee, Dennis L. Sun, Yuekai Sun, and Jonathan E. Taylor, Exact Post-Selection Inference, with Application to the Lasso (standard reference, not scraped)
William Fithian, Dennis L. Sun, and Jonathan E. Taylor, Optimal Inference After Model Selection (standard reference, not scraped)