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

Equivalent dominating measures give equivalent likelihood ratios

Statement

Assume AC. Let μ and ν be mutually absolutely continuous sigma-finite positive measures on one measurable space, and let E=((X,A),Θ,(Pθ)θ∈Θ) be dominated by both. Choose nonnegative density representatives pθμ=dPθ/dμ, pθν=dPθ/dν, and h=dν/dμ. Then h>0 μ-almost everywhere and, for each fixed θ, pθμ=h pθνμ-almost everywhere. Thus, for each fixed pair θ,η, the ratios pθμ/pημ and pθν/pην agree μ-almost everywhere wherever the denominator is positive. The factor h depends only on the two dominating measures. For an arbitrary uncountable Θ, no single exceptional null set valid for every pair is asserted; the density versions are not pointwise canonical, and no ratio value is specified at a zero denominator.

Facts & Assumptions

Given: AC; mutually absolutely continuous sigma-finite positive measures μ,ν; and an experiment whose probability laws satisfy Pθ≪μ and Pθ≪ν for every θ.

[F1]

Finite, sigma-finite, and semifinite measures: sigma-finiteness gives countable covers by measurable sets finite under the corresponding measure.

[A1]

The Axiom of Choice: AC says every family of nonempty sets has a choice function, permitting simultaneous selection of density representatives.

[F3]

A sigma-finite signed measure that is absolutely continuous with respect to a sigma-finite positive measure has a unique almost-everywhere density and The Radon-Nikodym derivative as an almost-everywhere equivalence class: under AC and a common finite exhaustion, each derivative is a finite-valued measurable representative class satisfying the setwise integral formula.

[F4]

A sigma-finite positive measure has a nonnegative Radon–Nikodym density version: for sigma-finite positive measures with absolute continuity, the RN class has a finite-valued nonnegative representative.

[F5]

Radon-Nikodym derivatives satisfy the chain rule along nu << mu << lambda: if λ,ρ are sigma-finite positive measures and σ has a common finite exhaustion with them, with σ≪ρ≪λ, then dσ/dλ=(dσ/dρ)(dρ/dλ) λ-almost everywhere.

[F6]

Absolute continuity of a signed or complex measure with respect to a positive measure: μ≪ν means every ν-null measurable set is μ-null.

[F7]

Likelihood densities: for observed x, the likelihood under a chosen dominating measure is Lx(θ)=pθ(x), with each density specified only up to its own null set.

[F8]

The total variation |nu|(E) from countable measurable partitions and Probability measures and probability spaces: on a measurable set, total variation of a positive measure equals its measure; in particular ∣Pθ∣(Xn)=Pθ(Xn)≤1.

Proof

technique · direct
1.1A1F1F5F8givenconstruct

Choose increasing finite-measure covers (Ai) for μ and (Bj) for ν by [F1], and set Xn=⋃i,j≤n(Ai∩Bj). Then Xn↑X, μ(Xn)<∞, and ν(Xn)<∞. Since Pθ is a probability measure, [F8] gives ∣Pθ∣(Xn)≤1. This is a common finite exhaustion for μ,ν,Pθ, so the hypotheses in [F5] hold for every θ, with (λ,ρ,σ)=(μ,ν,Pθ).

1.2A1F3F4F6givenchoose

By [A1], [F3], and [F4], choose nonnegative representatives h=dν/dμ and pθμ,pθν for the stated classes. The measurable set H={x:h(x)=0} satisfies ν(H)=∫Hh dμ=0 by [F3]; then μ(H)=0 by [F6]. Hence h>0 μ-almost everywhere.

2.1A1F3F5F7step 1.1step 1.2givenalgebra∎

Fix θ. Applying [F5] on the common exhaustion from step 1.1 gives pθμ=h pθν μ-almost everywhere. For a fixed pair θ,η, remove the union of their two exceptional null sets and the null set H from step 1.2. On the remaining set, both density identities hold and h>0, so division by the positive common factor gives pθμ/pημ=pθν/pην wherever the denominators are positive. The exceptional set may depend on the pair, which proves the stated scope.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

31 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