TheoremStatement: AI-adaptedProof: 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.

Conditional-error budget for two-stage adaptation

Statement

Assume AC. Let $P_{0}$ be one fixed null probability law on $(Ω, F)$ , and let $F_{1} \subseteq F$ be the interim sigma-algebra. Let $R_{0} \in F$ be the original design's rejection event, and let $R_{1} \in F$ be the adapted design's event of any eventual rejection, including early and final decisions. Choose versions $A = E_{0} [1_{R_{0}} ∣ F_{1}], Q = E_{0} [1_{R_{1}} ∣ F_{1}] .$ For $α \in [0, 1]$ , if $P_{0} (R_{0}) \leq α$ and $Q \leq A$ almost surely, then $P_{0} (R_{1}) \leq α$ . The original conditional error $A$ is an almost-sure class; changing its version does not change any rejection probability.

Facts & Assumptions

Given: AC; one probability space and one fixed null law $P_{0}$ ; a sub-sigma-algebra $F_{1}$ ; events $R_{0}, R_{1} \in F$ ; $α \in [0, 1]$ ; $P_{0} (R_{0}) \leq α$ ; and versions $A, Q$ of the stated conditional expectations with $Q \leq A$ almost surely.

[A1]

AC is assumed for the library's conditional-expectation existence interface. The Axiom of Choice

[F1]

Under AC, the conditional expectation is the unique almost-sure class of integrable, $F_{1}$ -measurable versions satisfying all $F_{1}$ event-integral identities. Conditional expectation as an ae class

[F2]

Conditional expectation preserves order and ordinary expectation, and a constant is its own conditional expectation. Basic algebra and order properties of conditional expectation

[F3]

For nested sigma-algebras, conditioning twice gives the conditional expectation at the smaller sigma-algebra. Tower property of conditional expectation

[F4]

The expectation of an event indicator is the probability of that event. The expectation of an indicator is the probability of the event

Proof

technique · identify the mean conditional errors by the tower property, then compare their expectations

1.1A1F1F2

By [A1] and [F1], both conditional-expectation classes exist. Since $0 \leq 1_{R_{j}} \leq 1$ for $j = 0, 1$ , order preservation and the constant rule in [F2] give $0 \leq A, Q \leq 1$ almost surely. All representatives of either class agree almost surely by [F1], so the rejection probabilities do not depend on the chosen versions.

2.1F2F3F4given∎

Let $F_{0} = {\emptyset, Ω}$ . By [F3], $E_{0} [A ∣ F_{0}] = E_{0} [1_{R_{0}} ∣ F_{0}]$ . Each side is constant almost surely because it is $F_{0}$ -measurable; testing its defining event identity at $Ω$ shows its constant is its ordinary expectation. Thus [F4] gives $E_{0} A = E_{0} 1_{R_{0}} = P_{0} (R_{0}) \leq α$ . The same argument gives $E_{0} Q = P_{0} (R_{1})$ . Order preservation [F2], applied to $Q \leq A$ with conditioning sigma-algebra $F_{0}$ , gives $E_{0} [Q ∣ F_{0}] \leq E_{0} [A ∣ F_{0}]$ ; these constants are $E_{0} Q$ and $E_{0} A$ , so $P_{0} (R_{1}) = E_{0} Q \leq E_{0} A \leq α$ .

Source notes

Both treatments express the global null rejection probability as the mean of the interim conditional rejection probability. The proof here states the event and sigma-algebra hypotheses directly and uses the published conditional-expectation tower and order properties; the source exposition alone is not used as a proof.

Depends on

Used by

A conditionally superuniform stage-2 p-value preserves conditional error Corollary

Dependency tree · two levels

18 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

Kenkichi Sugiura and Hiroyuki Uesaka, Theoretical Basis of Adaptive Designs for Clinical Trials in Phase II and III, Japanese Journal of Biometrics 29, Special Issue 1 (2008), S33–S52 (standard reference, not scraped)
Giorgos Minas, Multivariate Global Testing and Adaptive Designs, PhD thesis, University of Warwick (2013) (standard reference, not scraped)