Alphabeta Math
ExampleConstruction: AI-adaptedVerification: AI-generatedPipeline-generatedprecheck pending
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 X1∼N(0,4) and X2∼N(0,1) be independent, and use total squared-error budget D=5/2. The water level is θ=3/2, the optimal coordinate distortions are (3/2,1), and the information rate is 12log⁡2(8/3) bits per vector. An attaining reconstruction is Y1=5/2U, Y2=0, where X1=5/2U+3/2V for standard normals U,V that are mutually independent and jointly independent of X2.

Facts & Assumptions

Given: Independent centered Gaussian coordinates of variances 4 and 1, squared-error budget 5/2, and AC.

[F1]

Finite Gaussian water-level allocation: the optimum allocates min⁡(λi,θ) with unique θ satisfying the total-distortion equation.

[F2]

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.

[F3]

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.

[F4]

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.

[F5]

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.

[F6]

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

1.1F1F2givenalgebra

Since 1<θ<4, the water-level equation is min⁡(4,θ)+min⁡(1,θ)=θ+1=5/2, so θ=3/2. The allocated distortions are (min⁡(4,3/2),min⁡(1,3/2))=(3/2,1). By [F1]–[F2], R(5/2)=12(log⁡243/2+log⁡2+13/2)=12log⁡283.

1.2F4F5givenconstructalgebra

Put a=5/2 and b=3/2. Choose independent standard normals U,V,X2 by [F5], and set X1=aU+bV, Y1=aU, Y2=0. The matrix with rows (a,b)/2 and (b,−a)/2 is orthogonal, so [F4] gives X1∼N(0,4), independently of X2. The errors are bV and X2, with total mean square b2+1=5/2.

2.1F3F4F5F6step 1.1step 1.2algebra∎

Write fs(t)=(2πs)−1/2exp⁡(−t2/(2s)) for the N(0,s) density. By [F4]–[F6], (X1,Y1) has density fa2(y)fb2(x−y). Relative to Lebesgue measure in (x1,x2,y1) times the point mass at y2=0, the joint law and product of the marginals therefore have respective positive densities fa2(y1)fb2(x1−y1)f1(x2) and f4(x1)f1(x2)fa2(y1). Their log ratio is 12ln⁡4b2−(x1−y1)22b2+x128. It is integrable since both quadratic terms have finite expectations. By [F3] and step 1.2 its joint expectation is 12ln⁡(8/3)−12+12=12ln⁡(8/3) nats. Dividing by ln⁡2 yields the rate in step 1.1, proving attainment without assuming a Lebesgue density for the constant reconstruction coordinate.

Depends on

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