Alphabeta Math
TheoremStatement: Literature-sourcedProof: 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.

Loss-discrepancy domain-adaptation bound

Statement

Let P,Q be the source and target input marginals on a common measurable space X. Let Y be a measurable output space, H a nonempty class of measurable functions h:X→Y, and fP,fQ:X→Y measurable labeling functions. Let L:Y×Y→[0,+∞] be product-measurable, symmetric, and satisfy the triangle inequality. Define LD(g1,g2):=∫XL(g1(x),g2(x)) D(dx)(D∈{P,Q}),disc⁡L(P,Q):=sup⁡g1,g2∈H∣LP(g1,g2)−LQ(g1,g2)∣. Assume that every pairwise integral in this discrepancy definition is finite and that source and target minimizers hP∗∈arg⁡min⁡g∈HLP(g,fP) and hQ∗∈arg⁡min⁡g∈HLQ(g,fQ) exist. Then every h∈H satisfies LP(h,fP)≤LP(hP∗,fP)+LQ(h,hQ∗)+disc⁡L(P,Q)+min⁡{LQ(hQ∗,hP∗),LP(hQ∗,hP∗)}. The supremum defining disc⁡L may be infinite, in which case the inequality is interpreted in the extended nonnegative reals.

Statement references

Mansour, Mohri, and Rostamizadeh, Definition 4 and Theorem 8, arXiv version 3, §§3–4.1, pp. 3–6: the discrepancy definition and the bound with the minimum of both cross-domain terms (Theorem 8, Eq. (11)); its proof gives both triangle-inequality routes.

Facts & Assumptions

Given: Probability input marginals P,Q; a nonempty measurable hypothesis class H; measurable labeling functions fP,fQ; a measurable symmetric loss satisfying the triangle inequality; finite pairwise risks for the discrepancy; and attained source and target minima. Labeling risks may be extended nonnegative values.

[F1]

Source and target joint laws, risks, and covariate shift: the input marginals P,Q are probability measures on the common measurable input space.

[F2]

Loss discrepancy between domains: every pair g1,g2∈H has finite LP(g1,g2),LQ(g1,g2), and ∣LP(g1,g2)−LQ(g1,g2)∣≤disc⁡L(P,Q).

[F3]

A measurable function between measurable spaces: a map is measurable when preimages of measurable sets are measurable.

[F4]

The product sigma-algebra and its finite iterates: the product sigma-algebra on Y×Y is generated by measurable rectangles.

[F5]

Additivity of the nonnegative Lebesgue integral: the nonnegative integral is additive for sums of nonnegative measurable functions.

Proof

1.1F2F3F4given

For measurable g1,g2:X→Y, let G(x)=(g1(x),g2(x)). For each measurable rectangle A×B, G−1(A×B)=g1−1(A)∩g2−1(B)∈ΣX, so G is measurable into ΣY⊗ΣY by [F3] and [F4]. For each Borel C⊆[0,+∞], (L∘G)−1(C)=G−1(L−1(C))∈ΣX; hence all displayed loss integrands are measurable. Pairwise integrals with both arguments in H are finite by [F2], while integrals involving fP or fQ are defined extended nonnegative values.

1.2F1F2F5F6givenalgebra

Fix h∈H. Applying the triangle inequality twice pointwise and then using monotonicity and additivity of the nonnegative integral [F5, F6] under P gives LP(h,fP)≤LP(h,hQ∗)+LP(hQ∗,hP∗)+LP(hP∗,fP).

1.3F1F2F5F6givenalgebra

A second triangle inequality, integrated under P using monotonicity and additivity of the nonnegative integral [F5, F6], gives LP(h,fP)≤LP(h,hP∗)+LP(hP∗,fP). Apply [F2] to the first term, then integrate the triangle inequality under Q using [F5, F6] to obtain LQ(h,hP∗)≤LQ(h,hQ∗)+LQ(hQ∗,hP∗). Hence LP(h,fP)≤LP(hP∗,fP)+LQ(h,hQ∗)+disc⁡L(P,Q)+LQ(hQ∗,hP∗).

2.1F2F5F6step 1.2algebra

By [F2], LP(h,hQ∗)≤LQ(h,hQ∗)+disc⁡L(P,Q). Substitution in step 1.2 yields LP(h,fP)≤LP(hP∗,fP)+LQ(h,hQ∗)+disc⁡L(P,Q)+LP(hQ∗,hP∗).

3.1step 2.1step 1.3algebra∎

The bounds in steps 2.1 and 1.3 have the same terms except for the final cross-domain term. Taking the smaller of those terms proves the stated minimum bound.

Remarks

The discrepancy in this theorem is a population quantity. Estimating it from finite samples, or replacing the input laws by empirical laws, requires additional bounded-loss and complexity assumptions and is a separate result.

Remarks references

Mansour, Mohri, and Rostamizadeh, §§3–4.1, arXiv version 3, pp. 3–7: finite-sample discrepancy estimation and the empirical target-risk bound are stated separately with Rademacher and bounded-loss hypotheses.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

21 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