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

Circular complex Gaussian maximizes differential entropy at fixed second moment

Statement

Assume AC. Let $Z \in C$ have a Lebesgue density, finite mean $μ$ , finite differential entropy, and positive-definite real covariance matrix $K$ for $(Re Z, Im Z)$ . Put $σ^{2} = E ∣ Z - μ ∣^{2} = tr K$ . Then $h (Z) \leq \ln (π e σ^{2}) .$ Equality holds exactly for the circular complex Gaussian law $C N (μ, σ^{2})$ with density $(π σ^{2})^{- 1} \exp (- ∣ z - μ ∣^{2} / σ^{2})$ .

Facts & Assumptions

Given: AC and the density, mean, entropy, and positive-definite real covariance hypotheses in the Statement.

[A1]

The Axiom of Choice: AC is required by the Gaussian-law and entropy supplier.

[F1]

Gaussian maximizes differential entropy at fixed positive-definite covariance: a real vector with positive-definite covariance $K$ and finite differential entropy satisfies $h \leq \frac{1}{2} \ln ((2 π e)^{d} \det K)$ , with equality exactly for the matching real Gaussian law.

Proof

1.1A1F1givenalgebra

Identify $Z$ with the real vector $(Re Z, Im Z)$ . This identification preserves Lebesgue measure and the differential-entropy integral, so [F1] with $d = 2$ gives $h (Z) \leq \frac{1}{2} \ln ((2 π e)^{2} \det K) .$

2.1F1step 1.1algebra∎

Let $λ_{1}, λ_{2} > 0$ be the eigenvalues of $K$ . Then $\det K = λ_{1} λ_{2} \leq ((λ_{1} + λ_{2}) / 2)^{2} = (σ^{2} / 2)^{2}$ , because $(λ_{1} - λ_{2})^{2} \geq 0$ . Substitution into step 1.1 gives $h (Z) \leq \ln (π e σ^{2})$ . Equality requires equality in [F1] and $λ_{1} = λ_{2}$ , so $Z$ is Gaussian with real covariance $(σ^{2} / 2) I_{2}$ , exactly $C N (μ, σ^{2})$ . Conversely, substituting that circular Gaussian density gives entropy $\ln (π e σ^{2})$ .

Depends on

Used by

Dependency tree · two levels

5 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

Yury Polyanskiy and Yihong Wu, Information Theory: From Coding to Learning, author prepublication (standard reference, not scraped)
John Duchi, Lecture Notes on Statistics and Information Theory (standard reference, not scraped)