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

Unbiased randomized-tree residual correlation bounds forest risk

Statement

Fix a finite training dataset and a jointly measurable real-valued tree predictor $h (x, θ)$ . Let $Z = (X, Y)$ have test law $P$ . Let $Θ, Θ^{'}$ be independent randomizations with common law $Q$ , assume the pair $(Θ, Θ^{'})$ is independent of $Z$ , and assume $E_{P} Y^{2} < \infty$ and $h (X, Θ) \in L^{2} (P \times Q)$ . For every allowed tree randomization $θ$ , assume $h (X, θ) \in L^{2} (P)$ and $E_{P} Y = E_{P} h (X, θ)$ . Put $e_{θ} (Z) = Y - h (X, θ)$ and $s d (θ) = \sqrt{{Var}_{P} (e_{θ} (Z))}$ . Define

$P E^{*} (f o r e s t) = E_{P} {(Y - E_{Q} h (X, Θ))}^{2}$

$P E^{*} (t r e e) = E_{Q} E_{P} e_{Θ} (Z)^{2}$

$d = E_{Q} [s d (Θ)]$

If $d = 0$ , then both risks are zero. If $d > 0$ , define

ρ = \frac{E_{Q \times Q} [{Cov}_{P} (e_{Θ} (Z), e_{Θ^{'}} (Z))]}{d^{2}} .

Then $ρ \geq 0$ and

P E^{*} (f o r e s t) \leq ρ P E^{*} (t r e e) .

The covariance formula for $ρ$ is Breiman's weighted mean residual correlation written without undefined zero-standard-deviation correlation terms.

Statement references

Breiman, “Random Forests,” Theorem 11.2, printed pp. 25–26

Hastie, Tibshirani, and Friedman, The Elements of Statistical Learning, §§15.1 and 15.4.1–15.4.3, printed pp. 587, 597–602; used for the regression forest and variance/correlation context, not as a proof of this bound

Facts & Assumptions

Given: The fixed data, jointly measurable square-integrable predictor, unbiasedness condition for every allowed tree randomization, and independent randomizations and test pair in the Statement.

[F1]

Bagged random-forest construction on a fixed finite sample: For regression, each tree predicts its leaf sample mean and the forest prediction is the average of its tree predictions.

[F2]

Expectation of a nonnegative or integrable random variable: Expectation on a probability space is integration against its probability measure.

[F3]

Moments, variance, and covariance on a probability space: For square-integrable real random variables, variance is the mean squared centered value and covariance is the mean product of centered values.

[F4]

Independent random elements have product joint law: The joint law of a finite independent family of random elements is the product of their marginal laws.

[F5]

Fubini's theorem for L^1 functions on a sigma-finite product: For an integrable function on a product of sigma-finite measure spaces, either order of iterated integration gives the product integral.

[F6]

Cauchy-Schwarz for random variables: If $U, V \in L^{2} (Q)$ , then $E_{Q} ∣ U V ∣ \leq (E_{Q} U^{2})^{1 / 2} (E_{Q} V^{2})^{1 / 2}$ .

Proof

1.1givenF2F3F6algebra

For every allowed $θ$ , the mean condition gives $E_{P} e_{θ} (Z) = 0$ . Hence [F3] gives ${Cov}_{P} (e_{θ}, e_{θ^{'}}) = E_{P} [e_{θ} e_{θ^{'}}]$ . If both residual standard deviations are positive, define their correlation as this covariance divided by their product; if either is zero, the covariance is zero. Thus the covariance expression for $ρ$ agrees with Breiman's weighted mean residual correlation, including zero-standard-deviation pairs. The products are integrable by [F6] and square-integrability. Also $E_{P \times Q} e_{Θ}^{2} < \infty$ , since $(a - b)^{2} \leq 2 a^{2} + 2 b^{2}$ and both $Y$ and $h (X, Θ)$ are square-integrable.

2.1F1F2F4F5F6step 1.1algebra

By [F4] the pair $(Θ, Θ^{'}, Z)$ has product law. For $P$ -almost every $z$ , [F6] gives $(E_{Q} ∣ e_{Θ} (z) ∣)^{2} \leq E_{Q} e_{Θ} (z)^{2}$ ; integrating and using step 1.1 shows $e_{θ} (z) e_{θ^{'}} (z)$ is integrable on $P \times Q \times Q$ . Thus [F5] permits the following integrations. The $Q$ -average is the infinite-forest prediction obtained from the same regression tree predictions that the algorithm averages at finite $B$ [F1]. Also $E_{Q} e_{Θ} (Z) = Y - E_{Q} h (X, Θ)$ for $P$ -almost every $Z$ . Consequently $P E^{*} (f o r e s t) = E_{P} [(E_{Q} e_{Θ} (Z))^{2}] = E_{Q \times Q} [E_{P} (e_{Θ} (Z) e_{Θ^{'}} (Z))] = E_{Q \times Q} [{Cov}_{P} (e_{Θ} (Z), e_{Θ^{'}} (Z))]$ . Thus when $d > 0$ , $P E^{*} (f o r e s t) = ρ d^{2}$ and $ρ \geq 0$ .

3.1F2F3F6step 2.1algebra

The zero-mean condition and [F3] give $P E^{*} (t r e e) = E_{Q} [s d (Θ)^{2}]$ . By [F6] with one factor equal to $1$ , $d^{2} = (E_{Q} s d (Θ))^{2} \leq E_{Q} [s d (Θ)^{2}]$ . For $d > 0$ , combining with step 2.1 and $ρ \geq 0$ yields $P E^{*} (f o r e s t) \leq ρ P E^{*} (t r e e)$ .

4.1F2F3F5step 1.1∎

If $d = 0$ , then the nonnegative function $s d$ vanishes $Q$ -almost everywhere: each set ${s d \geq 1 / n}$ has measure zero since otherwise $E_{Q} s d > 0$ . For $Q$ -almost every $θ$ , the mean-zero residual has variance zero, so the same argument applied to $(e_{θ} - E_{P} e_{θ})^{2}$ gives $e_{θ} = 0$ $P$ -almost surely. Fubini then gives $e_{Θ} (Z) = 0$ for $P \times Q$ -almost every $(Z, Θ)$ ; both displayed risks are zero.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

23 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

Leo Breiman, "Random Forests," Machine Learning 45 (2001), 5–32; full text hosted by the University of Chicago Macro Finance Research Program (standard reference, not scraped)
Trevor Hastie, Robert Tibshirani, and Jerome Friedman, The Elements of Statistical Learning, 2nd ed., corrected 12th printing, Chapter 15 (standard reference, not scraped)