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

Optimal discriminator and Jensen–Shannon divergence in the unrestricted GAN game

Statement

Let $(X, A, μ)$ be a measure space and let $P, Q$ be probability measures with finite-valued nonnegative measurable densities $p, q$ relative to $μ$ , normalized by $\int p d μ = \int q d μ = 1$ . For every measurable discriminator $D : X \to [0, 1]$ , define

V (D; P, Q) = \int p \ln D d μ + \int q \ln (1 - D) d μ,

extending $\ln 0 = - \infty$ and making each zero-density term $0 \cdot (- \infty)$ equal to $0$ . Let $C (P, Q)$ be the supremum of $V (D; P, Q)$ over all such $D$ . Put $m = (p + q) / 2$ , $r = p / m$ and $s = q / m$ where $m > 0$ , set $r = s = 0$ where $m = 0$ , define $ϕ (0) = 0$ and $ϕ (t) = t \ln t$ for $t > 0$ , and set ${JS}_{μ} (P, Q) = \frac{1}{2} \int m ϕ (r) d μ + \frac{1}{2} \int m ϕ (s) d μ$ . Then the measurable discriminator

D^{*} (x) = {\begin{cases} \frac{p (x)}{p (x) + q (x)}, & p (x) + q (x) > 0, \\ \frac{1}{2}, & p (x) + q (x) = 0 \end{cases}

maximizes $V$ , and $C (P, Q) = - \ln 4 + 2 {JS}_{μ} (P, Q)$ . Consequently $C (P, Q) \geq - \ln 4$ , with equality if and only if $P = Q$ . Over the unrestricted class of probability densities, equality of the generator law with the data law is the unique global distribution optimum. This identity does not assert convergence of finite neural alternating optimization.

Statement references

GAN minimax objective and density domain

Density-defined Jensen–Shannon divergence

Jensen–Shannon nonnegativity and equality

Goodfellow et al., §4.1, Proposition 1, Theorem 1, equations (2)–(6), complete 9-page paper

Li, §1.2, equations (9)–(11), complete 6-page lecture note

Facts & Assumptions

Given: A measure space $(X, A, μ)$ , probability measures $P, Q$ with finite-valued nonnegative measurable densities $p, q$ , and a measurable discriminator $D : X \to [0, 1]$ .

[F1]

GAN minimax objective and its distributional domain: $V (D; P, Q) = - \int p (- \ln D) d μ - \int q (- \ln (1 - D)) d μ$ , where $0 \cdot (+ \infty) = 0$ , and $C (P, Q)$ is the supremum over every measurable $D : X \to [0, 1]$ .

[F2]

Density-defined Jensen–Shannon divergence: with $m = (p + q) / 2$ , $r = p / m$ , $s = q / m$ on $m > 0$ and $r = s = 0$ otherwise, ${JS}_{μ} (P, Q) = \frac{1}{2} \int m ϕ (r) d μ + \frac{1}{2} \int m ϕ (s) d μ$ .

[F3]

Nonnegativity and equality for density Jensen–Shannon divergence: the two integrands $m ϕ (r)$ and $m ϕ (s)$ are integrable, and ${JS}_{μ} (P, Q)$ is finite and nonnegative, with equality exactly when $P = Q$ .

[F4]

The natural logarithm has derivative 1/x and equals the integral from 1 to x of 1/t: $\ln$ is differentiable on $(0, \infty)$ with derivative $1 / t$ .

[F5]

Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm: $\ln$ is strictly increasing, $\ln 1 = 0$ , and $\ln (x y) = \ln x + \ln y$ for $x, y > 0$ .

[F6]

Monotonicity and nonnegative homogeneity of the nonnegative integral: the nonnegative integral is monotone.

[F7]

The Lebesgue integral is linear on $L^{1} (μ)$ : the Lebesgue integral is linear on integrable functions.

[F8]

A map into $R^{n}$ is measurable exactly when its coordinates are measurable: a map into $R^{2}$ is measurable if its two coordinates are measurable.

[F9]

Composition with a Borel measurable outer map preserves measurability: composing a measurable map with a Borel map preserves measurability.

[F10]

The chain rule, in one line from Carathéodory: if $g$ is differentiable at $c$ and $f$ is differentiable at $g (c)$ , then $f \circ g$ is differentiable at $c$ with $(f \circ g)^{'} (c) = f^{'} (g (c)) g^{'} (c)$ : if $g$ is differentiable at $c$ and $f$ is differentiable at $g (c)$ , then $(f \circ g)^{'} (c) = f^{'} (g (c)) g^{'} (c)$ .

[F11]

Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ : sums and scalar multiples of differentiable functions are differentiable, with the sum and scalar-multiple derivative formulas.

[F12]

A function differentiable at $c$ is continuous at $c$ : a function differentiable at every point of an open interval is continuous at every point of that interval.

[F13]

The mean value theorem, as the case $g (x) = x$ of Cauchy's: for $f$ continuous on $[a, b]$ with $a < b$ and differentiable on $(a, b)$ there is $c \in (a, b)$ with $f (b) - f (a) = f^{'} (c) (b - a)$ : a function continuous on a closed interval and differentiable on its interior has a point where its derivative equals the average rate of change across the interval.

[F14]

Additivity of the nonnegative Lebesgue integral: for nonnegative measurable functions $u, v$ , $\int (u + v) d μ = \int u d μ + \int v d μ$ .

Proof

1.1F8F9construct

Define $F : [0, \infty)^{2} \to [0, 1]$ by $F (a, b) = a / (a + b)$ when $a + b > 0$ and $F (0, 0) = 1 / 2$ . It is continuous on the Borel set ${a + b > 0}$ and constant on its singleton complement, hence Borel. By [F8], $x \mapsto (p (x), q (x))$ is measurable, and [F9] makes $D^{*} = F (p, q)$ measurable.

1.2givenF4F5F10F11F12F13algebra

Fix $x$ and write $a = p (x)$ and $b = q (x)$ . If $a, b > 0$ , the function $f (y) = a \ln y + b \ln (1 - y)$ on $0 < y < 1$ is differentiable with $f^{'} (y) = a / y - b / (1 - y) = (a - (a + b) y) / (y (1 - y))$ : the derivative of $1 - y$ is $- 1$ by its difference quotient, [F4] differentiates $\ln$ , [F10] applies the chain rule, and [F11] gives the sum and scalar rules. The denominator is positive; the numerator is positive for $y < y^{*} : = a / (a + b)$ and negative for $y > y^{*}$ . By [F12], $f$ is continuous on every closed subinterval of $(0, 1)$ . For any $y \in (0, y^{*})$ , [F13] on $[y, y^{*}]$ gives $c \in (y, y^{*})$ with $f (y^{*}) - f (y) = f^{'} (c) (y^{*} - y) > 0$ . For any $y \in (y^{*}, 1)$ , [F13] on $[y^{*}, y]$ gives $c \in (y^{*}, y)$ with $f (y) - f (y^{*}) = f^{'} (c) (y - y^{*}) < 0$ . At $y = 0, 1$ the payoff is $- \infty$ . If $a = 0 < b$ , then $f (y) = b \ln (1 - y) \leq 0 = f (0)$ , with equality at $y = 0$ . If $b = 0 < a$ , then $f (y) = a \ln y \leq 0 = f (1)$ , with equality at $y = 1$ . If $a = b = 0$ , every $y$ gives value $0$ . In all four cases, $D^{*} (x)$ maximizes the pointwise payoff.

2.1F1F6F14step 1.1step 1.2

For any measurable $D$ , step 1.2 gives the pointwise loss inequality $p (- \ln D) + q (- \ln (1 - D)) \geq p (- \ln D^{*}) + q (- \ln (1 - D^{*}))$ , with zero-density endpoint terms interpreted as in [F1]. These are nonnegative measurable losses by the definition and its measurability dependencies [F1]. Additivity [F14] and monotonicity [F6] therefore give $\int p (- \ln D) d μ + \int q (- \ln (1 - D)) d μ \geq \int p (- \ln D^{*}) d μ + \int q (- \ln (1 - D^{*})) d μ$ . Taking negatives and using [F1] yields $V (D; P, Q) \leq V (D^{*}; P, Q)$ . Since $D^{*}$ is measurable by step 1.1, the supremum is attained and $C (P, Q) = V (D^{*}; P, Q)$ .

3.1F1F2F3F5F7step 2.1algebra

On $m > 0$ , one has $p = m r$ , $q = m s$ , $D^{*} = r / 2$ and $1 - D^{*} = s / 2$ . Using $0 \ln 0 = 0$ when $r = 0$ or $s = 0$ , the pointwise optimized payoff is $m ϕ (r) + m ϕ (s) - m (r + s) \ln 2 = m ϕ (r) + m ϕ (s) - 2 m \ln 2$ . On $m = 0$ , both densities and all displayed products are zero, so the same identity holds. The first two terms are integrable by [F3]; [F1] and [F7] give $\int m d μ = 1$ . Hence [F7], [F2] and $\ln 4 = 2 \ln 2$ [F5] give $C (P, Q) = 2 {JS}_{μ} (P, Q) - \ln 4$ .

4.1F3step 3.1algebra∎

By [F3], ${JS}_{μ} (P, Q) \geq 0$ , and it vanishes exactly when $P = Q$ . Step 3.1 therefore gives $C (P, Q) \geq - \ln 4$ with equality exactly at $P = Q$ . The unrestricted density class contains the data law itself, so this value is attained there and no other generator law attains it. The argument establishes only the distribution-space optimum stated here.

Depends on

Used by

A finite adversarial gradient game can cycle Example
Separated supports saturate the ideal discriminator Example

Dependency tree · two levels

56 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

Ian J. Goodfellow et al., Generative Adversarial Nets, arXiv:1406.2661v1 (standard reference, not scraped)
Yingzhen Li, Lecture notes on generative adversarial networks (GANs), Deep Learning (Winter 2022, Imperial College London) (standard reference, not scraped)