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

Product likelihood tilts have the product density

Statement

Under the setup of Likelihood-tilted measures at a KL projection and Likelihood tilts are sigma-finite measures, for each $θ$ and integer $n \geq 1$ , the sigma-finite product measure $Q_{θ}^{n}$ exists and has density $\prod_{i = 1}^{n} r_{θ} (x_{i}), r_{θ} (x) : = \frac{p_{θ} (x)}{p_{θ^{*}} (x)},$ relative to $P_{0}^{n}$ . Ratios are zero where $p_{θ^{*}} = 0$ , as in the likelihood-tilt definition.

Facts & Assumptions

Given: A probability measure $P_{0}$ , its product measure $P_{0}^{n}$ , the likelihood tilt $Q_{θ} = r_{θ} P_{0}$ , and the finite product sigma-algebra.

[F1]

Likelihood-tilted measures at a KL projection: $Q_{θ} (A) = \int_{A} r_{θ} d P_{0}$ with $r_{θ}$ nonnegative and finite.

[F2]

Likelihood tilts are sigma-finite measures: $Q_{θ}$ is a sigma-finite measure.

[F3]

Probability measures and probability spaces: $P_{0}$ is finite, hence sigma-finite.

[F4]

For sigma-finite factors, the product measure exists, has the rectangle formula, is sigma-finite, and is unique: repeated application gives finite products of sigma-finite measures; these have the rectangle formula and are unique among measures with that formula.

[F5]

Tonelli's theorem for nonnegative measurable functions on a sigma-finite product: nonnegative product-measurable functions may be integrated by repeated nonnegative integration, and the iterated integrals equal the product integral.

[F6]

The measure with density $f$ relative to $μ$ : a nonnegative measurable density relative to a measure defines a measure by integration.

[F7]

Coordinate maps and permutations are measurable on finite products: coordinate maps on a finite product are measurable.

[F8]

Arithmetic and lattice operations preserve measurability whenever they are defined: finite products of nonnegative measurable functions are measurable.

Proof

Given: The hypotheses and conventions in the Statement.

1.1F1F2F3F7F8given

Fix $θ$ and $n \geq 1$ . By [F2] and [F3], the product measures $Q_{θ}^{n}$ and $P_{0}^{n}$ exist and are sigma-finite. For $x_{1 : n} = (x_{1}, \dots, x_{n})$ , every coordinate map is measurable by [F7], so $f_{n} (x_{1 : n}) : = \prod_{i = 1}^{n} r_{θ} (x_{i})$ is nonnegative and measurable.

2.1F1F4F5F6step 1.1

Define $R_{n} (A) : = \int_{A} f_{n} d P_{0}^{n}$ on the product sigma-algebra. By [F6], $R_{n}$ is a measure. For every measurable rectangle $A_{1} \times \dots \times A_{n}$ , repeated Tonelli integration [F5] gives $R_{n} (A_{1} \times \dots \times A_{n}) = \prod_{i = 1}^{n} \int_{A_{i}} r_{θ} d P_{0} = \prod_{i = 1}^{n} Q_{θ} (A_{i}) = Q_{θ}^{n} (A_{1} \times \dots \times A_{n}),$ where the final equality is [F4]'s rectangle formula.

3.1F4step 2.1∎

The measures $R_{n}$ and $Q_{θ}^{n}$ agree on the generating pi-system of measurable rectangles by step 2.1. The product-measure theorem [F4] gives uniqueness for this rectangle formula, so $R_{n} = Q_{θ}^{n}$ on the whole product sigma-algebra. By the definition of $R_{n}$ , its density is $f_{n} = \prod_{i = 1}^{n} r_{θ} (x_{i})$ , as claimed.

Depends on

Used by

Dependency tree · two levels

35 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

B. J. K. Kleijn and A. W. van der Vaart, The Bernstein-Von-Mises Theorem under Misspecification, §3.2, pp. 368–370 (standard reference, not scraped)