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.
Finite Gaussian-vector distortion waterline
Statement
Assume AC. Let and be independent, and use total squared-error budget . The water level is , the optimal coordinate distortions are , and the information rate is bits per vector. An attaining reconstruction is , , where for standard normals that are mutually independent and jointly independent of .
Facts & Assumptions
Given: Independent centered Gaussian coordinates of variances 4 and 1, squared-error budget , and AC.
Finite Gaussian water-level allocation: the optimum allocates with unique satisfying the total-distortion equation.
Finite-dimensional Gaussian vector squared-error rate-distortion function: for independent Gaussian coordinates, the standard-Borel information rate in bits is the half-sum of positive log variance-to-water-level ratios.
Mutual information for standard-Borel random elements and Kullback–Leibler divergence: mutual information in nats is joint-law KL from the product of the marginals, computed as the joint expectation of the log Radon–Nikodym density.
Standard normal and normal laws and Orthogonal transformations preserve the standard normal product law: normal laws are scaled standard-normal laws, and orthogonal transforms preserve independent standard normals under AC.
For sigma-finite factors, the product measure exists, has the rectangle formula, is sigma-finite, and is unique and Tonelli's theorem for nonnegative measurable functions on a sigma-finite product: finite independent product laws exist; independent variables with densities have the product density, as verified by integration on rectangles and uniqueness.
A C^1 diffeomorphism satisfies the change-of-variables formula for nonnegative Lebesgue measurable functions: an invertible linear change of variables transforms densities by the absolute inverse determinant. Its Countable Choice hypothesis follows from AC by restricting a choice function to a countable family.
Proof
Since , the water-level equation is , so . The allocated distortions are . By [F1]–[F2],
Put and . Choose independent standard normals by [F5], and set , , . The matrix with rows and is orthogonal, so [F4] gives , independently of . The errors are and , with total mean square .
Write for the density. By [F4]–[F6], has density . Relative to Lebesgue measure in times the point mass at , the joint law and product of the marginals therefore have respective positive densities and . Their log ratio is It is integrable since both quadratic terms have finite expectations. By [F3] and step 1.2 its joint expectation is nats. Dividing by yields the rate in step 1.1, proving attainment without assuming a Lebesgue density for the constant reconstruction coordinate.
Depends on
- The Axiom of Choice
- Finite Gaussian water-level allocation
- Finite-dimensional Gaussian vector squared-error rate-distortion function
- Mutual information for standard-Borel random elements
- Kullback–Leibler divergence
- Standard normal and normal laws
- Orthogonal transformations preserve the standard normal product law
- For sigma-finite factors, the product measure exists, has the rectangle formula, is sigma-finite, and is unique
- Tonelli's theorem for nonnegative measurable functions on a sigma-finite product
- A C^1 diffeomorphism satisfies the change-of-variables formula for nonnegative Lebesgue measurable functions
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
70 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
- Thomas M. Cover and Joy A. Thomas, Elements of Information Theory, 2nd ed. (standard reference, not scraped)