TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generated

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.

Evidence lower bound is log evidence minus reverse KL

Statement

Let $μ, γ, Z, π, q$ satisfy Variational family and evidence lower bound, and put $Q = q μ$ and $Π = π μ$ . The choice-free density-ratio identity $\log Z = ELBO (q) + \int q \log (q / π) d μ$ holds, with the ratio integrand set to zero where $q = 0$ . Under AC, the final integral is the library reverse divergence $D (Q ∥ Π)$ and is nonnegative. Consequently $ELBO (q) \leq \log Z .$

Facts & Assumptions

Given: A measure space $(Ω, A, μ)$ , measurable $γ \geq 0$ with $0 < Z = \int γ d μ < \infty$ , $π = γ / Z$ , an admissible density $q$ , and AC for the library KL clause.

[F1]

Variational family and evidence lower bound: for densities, $q ≪_{μ} π$ means $q = 0$ $μ$ -almost everywhere on ${π = 0}$ .

[F2]

Variational family and evidence lower bound: admissibility requires $\int q (∣ \log γ ∣ + ∣ \log q ∣) d μ < \infty$ .

[F3]

Variational family and evidence lower bound: $ELBO (q) = \int q (\log γ - \log q) d μ$ .

[F4]

A nonnegative measurable function has integral $0$ exactly when it vanishes almost everywhere: a nonnegative measurable function has integral zero exactly when it vanishes almost everywhere.

[F5]

Kullback–Leibler divergence: for probability measures $P ≪ R$ , under AC the directional divergence is $D (P ∥ R) = \int \log (d P / d R) d P$ ; its first argument is the measure absolutely continuous with respect to the second.

[F6]

Kullback–Leibler divergence is nonnegative: under the published directional convention and AC, $D (P ∥ R) \geq 0$ for probability measures $P, R$ .

[F7]

The indefinite integral of a nonnegative measurable function is a measure: integrating a nonnegative measurable density over measurable sets defines a measure.

[A1]

The Axiom of Choice: AC states that every family of nonempty sets has a choice function. It is invoked here only through [F5] and [F6].

Proof

Given: The hypotheses in the Statement.

1.1F1F4F7constructalgebra

Define $Q (A) = \int_{A} q d μ$ and $Π (A) = \int_{A} π d μ$ . These are probability measures by [F1] and [F7]. If $Π (A) = 0$ , [F4] applied to $π 1_{A}$ gives $π = 0$ $μ$ -almost everywhere on $A$ . Then [F1] gives $q = 0$ almost everywhere on $A$ , so $Q (A) = 0$ and $Q ≪ Π$ . Define $r = q / π$ on ${π > 0}$ and $r = 0$ on ${π = 0}$ . For every measurable $A$ , $\int_{A} r d Π = \int_{A \cap {π > 0}} q d μ = Q (A)$ , so $r = d Q / d Π$ .

2.1F1F2F3step 1.1algebra

On ${q > 0}$ , $π = γ / Z > 0$ and $\log r = \log q - \log γ + \log Z$ . The assumed absolute integrability and $\int q d μ = 1$ make all terms integrable. Hence $\int \log r d Q = \int q \log (q / π) d μ = \log Z - ELBO (q)$ . This algebraic identity uses the explicit density ratio and no choice axiom.

3.1A1F5step 2.1algebra

By [A1] and [F5], the integral $\int \log r d Q$ is $D (Q ∥ Π)$ under the library convention. Rearranging step 2.1 gives $\log Z = ELBO (q) + D (Q ∥ Π)$ .

4.1F6step 3.1algebra∎

The measures $Q$ and $Π$ are probabilities, so [F6] gives $D (Q ∥ Π) \geq 0$ . Step 3.1 then yields $ELBO (q) \leq \log Z$ .

Depends on

Used by

A high ELBO alone does not certify posterior calibration Remark

Dependency tree · two levels

59 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

David M. Blei, Alp Kucukelbir, and Jon D. McAuliffe, Variational Inference: A Review for Statisticians (2017) (standard reference, not scraped)
Ronghuo Zheng, Zhiting Hu, and Yuntian Deng, 10-708 Probabilistic Graphical Models, Lecture 13: Variational Inference II (2015) (standard reference, not scraped)