LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-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.

Observed-data likelihood under a response model

Statement

Assume AC. Let $W = (W_{1}, \dots, W_{k})$ have a full-data model dominated by a common sigma-finite positive measure $μ$ on the finite product measurable space $W = \prod_{j = 1}^{k} W_{j}$ , with selected finite-valued density representatives $p_{θ}$ as in Dominated statistical experiments and Likelihood densities. Let $R$ be a nonempty finite pattern set, let $I_{r}$ and $J_{r}$ be the observed and missing coordinate sets for pattern $r$ , and write $π_{r} (w) = W_{o b s} (r)$ for its measurable coordinate projection. Let $g_{ψ} (r ∣ w)$ be a supplied response probability kernel as in MCAR, MAR, and MNAR relative to an observation pattern, and define the joint model by $P_{θ, ψ} (d w, {r}) = g_{ψ} (r ∣ w) P_{θ} (d w) .$

Fix a finite positive measure $ρ$ equivalent to $μ$ ; such a measure exists for every sigma-finite $μ$ . For each pattern put $κ_{r} (B) = ρ (π_{r}^{- 1} (B))$ for measurable $B \subseteq W_{o b s} (r)$ , and define the finite measure on the observed disjoint union by $λ_{O} (A) = \sum_{r \in R} κ_{r} ({x : (r, x) \in A}) .$ The full-data marginal law of $W_{o b s} (r)$ and the pattern- $r$ observed sublaw $B \mapsto P_{θ, ψ} (R = r, π_{r} (W) \in B)$ are absolutely continuous with respect to $κ_{r}$ . Choose finite-valued nonnegative Radon--Nikodym density representatives $q_{θ, r}$ and $ℓ_{θ, ψ, r}$ for these measures. Then the observed record $O = (R, W_{o b s} (R))$ is dominated by $λ_{O}$ and has density $ℓ_{θ, ψ} (r, x) = ℓ_{θ, ψ, r} (x)$ at $(r, x)$ .

In the product-reference special case where $μ = ν = ⨂_{j = 1}^{k} ν_{j}$ , each $ν_{j}$ is sigma-finite, and the coordinate reordering $w = (x, z) = (W_{o b s} (r), W_{m i s} (r))$ identifies $ν$ with $ν_{r}^{o b s} \times ν_{r}^{m i s}$ , where $ν_{r}^{o b s} = ⨂_{j \in I_{r}} ν_{j}$ and $ν_{r}^{m i s} = ⨂_{j \in J_{r}} ν_{j}$ , one may instead use the pattern reference $ν_{r}^{o b s}$ , with disjoint-union reference $λ_{O}^{p r o d} (A) = \sum_{r} ν_{r}^{o b s} ({x : (r, x) \in A})$ . The observed record is dominated by this sigma-finite measure, and Tonelli's theorem gives the density versions ${\overset{ˉ}{q}}_{θ, r} (x) = \int p_{θ} (x, z) ν_{r}^{m i s} (d z), ℓ_{θ, ψ, r} (x) = \int p_{θ} (x, z) g_{ψ} (r ∣ x, z) ν_{r}^{m i s} (d z) .$ An empty coordinate block is a one-point space with unit mass.

Facts & Assumptions

Given: AC, the finite-coordinate model dominated by a common sigma-finite measure, its supplied response kernel, and, for the coordinate integral specialization, the product reference and pattern-specific product decompositions in the Statement.

[F1]

Full and observed data under a missingness pattern: the full data are $W = (W_{1}, \dots, W_{k})$ , pattern $R$ selects the recorded coordinates, and the observed record is $O = (R, W_{o b s} (R))$ .

[F2]

MCAR, MAR, and MNAR relative to an observation pattern: a response mechanism is a supplied conditional law $g (r ∣ w)$ represented by a probability kernel.

[F3]

Dominated statistical experiments: the common supplied dominator is sigma-finite and dominates every full-data law.

[F4]

Finite, sigma-finite, and semifinite measures: sigma-finiteness supplies a countable cover by sets of finite $μ$ -measure.

[F5]

Parametric statistical models: a parametric model is the parameter map from labels $θ$ to their sampling laws $P_{θ}$ .

[F6]

Likelihood densities: under AC, select finite-valued measurable nonnegative representatives of density classes.

[F7]

Measure kernel and probability kernel: every response-kernel section has total mass one.

[F8]

A sigma-finite signed measure that is absolutely continuous with respect to a sigma-finite positive measure has a unique almost-everywhere density and A sigma-finite positive measure has a nonnegative Radon–Nikodym density version: finite positive measures absolutely continuous with respect to a finite positive reference have finite-valued nonnegative density representatives under AC.

[F9]

Tonelli's theorem for nonnegative measurable functions on a sigma-finite product: nonnegative product-measurable functions have measurable section integrals, and integrating a section integral equals integrating over the product.

[A1]

The Axiom of Choice: AC permits selection from a family of nonempty sets.

Proof

Proof technique: Construct an equivalent finite reference, take patternwise pushforwards, and use Tonelli in the product-reference specialization.

1.1F3F4F9construct

By [F3] and [F4], choose a countable cover $E_{n}$ of $W$ with $μ (E_{n}) < \infty$ , replace it by the increasing cover $F_{n} = ⋃_{j \leq n} E_{j}$ , and put $A_{1} = F_{1}$ and $A_{n} = F_{n} ∖ F_{n - 1}$ for $n \geq 2$ . The $A_{n}$ partition $W$ and each has finite $μ$ -measure. Set $c_{n} = 2^{- n} / (1 + μ (A_{n}))$ and define $ρ (E) = \sum_{n \geq 1} c_{n} μ (E \cap A_{n})$ . Rearrangement of nonnegative double series shows that $ρ$ is countably additive; moreover $ρ (W) \leq \sum_{n} 2^{- n} < \infty$ , and $ρ (E) = 0$ exactly when $μ (E) = 0$ , since every $c_{n} > 0$ and the $A_{n}$ partition $W$ . Thus $ρ$ is finite and equivalent to $μ$ .

1.2A1F1F3F6F8given

For every pattern $r$ , the coordinate projection $π_{r}$ is measurable by [F1], so $κ_{r} = ρ \circ π_{r}^{- 1}$ is a finite measure. If $κ_{r} (B) = 0$ , equivalence gives $μ (π_{r}^{- 1} B) = 0$ , and [F3] gives $P_{θ} (π_{r}^{- 1} B) = 0$ . Thus the full-data marginal $B \mapsto P_{θ} (π_{r}^{- 1} B)$ is absolutely continuous with respect to $κ_{r}$ . The pattern sublaw $B \mapsto \int_{π_{r}^{- 1} B} g_{ψ} (r ∣ w) P_{θ} (d w)$ is bounded above by that marginal because the kernel section lies in $[0, 1]$ , so it too is absolutely continuous. By [A1, F6, F8], choose finite-valued nonnegative densities $q_{θ, r}$ and $ℓ_{θ, ψ, r}$ for these finite measures.

2.1F1F7step 1.2given

For a measurable set $A$ in the observed disjoint union, its pattern sections $A_{r} = {x : (r, x) \in A}$ satisfy $P_{θ, ψ} (O \in A) = \sum_{r} \int_{A_{r}} ℓ_{θ, ψ, r} d κ_{r} = \int_{A} ℓ_{θ, ψ} (r, x) d λ_{O}$ . These densities therefore represent the observed-record law relative to the stated $λ_{O}$ ; their total mass is one because $\sum_{r} P_{θ, ψ} (R = r) = \int \sum_{r} g_{ψ} (r ∣ w) P_{θ} (d w) = 1$ . The full-data marginal densities $q_{θ, r}$ likewise integrate to one.

3.1A1F1F2F5F7F9given∎

In the product-reference case, for each pattern $r$ and observed-coordinate measurable set $B$ , the product decomposition in the Statement gives the pattern sublaw as $\int_{B \times W_{m i s} (r)} p_{θ} (x, z) g_{ψ} (r ∣ x, z) d (ν_{r}^{o b s} \times ν_{r}^{m i s})$ . Its integrand is nonnegative and product-measurable, so [F9] gives the displayed missing-coordinate integral as a density relative to $ν_{r}^{o b s}$ . Applying the same argument with $g$ omitted gives the displayed marginal density ${\overset{ˉ}{q}}_{θ, r}$ . Empty blocks use the one-point unit measure as stated.

Depends on

Used by

MAR factorization and likelihood ignorability for the full-data parameter Theorem

Dependency tree · two levels

39 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

Lu Mao, Missing Data: Foundations and Methods, Chapter 1, §1.2 (standard reference, not scraped)
National Research Council, The Prevention and Treatment of Missing Data in Clinical Trials, Chapter 4, pp. 60–61 (standard reference, not scraped)