Channel and question
- Input
- A real transmit vector \(X\in\mathbb R^{n_t}\) with covariance \(Q\succeq0\) and \(\operatorname{tr}Q\le P\).
- Output
- \(Y=HX+Z\in\mathbb R^{n_r}\), where \(Z\sim\mathcal N(0,\sigma^2I)\).
- Law
- A fixed real channel matrix \(H\) is known at encoder and decoder.
- Quantity
- Gaussian MIMO capacity \(C(H,P)\), measured in bits per channel use.
Criterion. Arbitrary blocklength vector codes under the total average power constraint. Resource averaging is fixed by the explicit model assumption below.
- Average decoding error vanishes.
- Real-channel normalization contributes a factor one half.
- For every message m, sum_t sum_k x_{t,k}(m)^2 <= n P. This is a shared transmit-antenna budget for each codeword, not a separate per-antenna or message-averaged budget.
Current status
\[C(H,P)=\max_{Q\succeq0,\,\operatorname{tr}Q\le P}\frac12\log_2\det\!\left(I+\sigma^{-2}HQH^{\mathsf T}\right)\]
The maximizing covariance is obtained by water-filling over the eigenmodes of \(H^{\mathsf T}H\).
| Result | Relation | Method | Year |
|---|---|---|---|
| Exact | \(C(H,P)=\max_{Q\succeq0,\operatorname{tr}Q\le P}\frac12\log_2\det(I+\sigma^{-2}HQH^{\mathsf T})\) | Gaussian extremality and eigenmode water-filling. | 1999 |
Formal verification
Lean coverageFormally stated
New statements await mathematical review and proofs. Power convention: CodewordVectorPowerAdmissible. No equivalence to another power convention is assumed.
Claims
- Real Gaussian MIMO operational capacity under the registered total power constraint.
operational-capacity· exact capacity · solved · Formally stated · v2 - The covariance supremum is attained by an admissible real positive-semidefinite covariance.
optimizer-attainment· structural · solved · Formally stated · v1 - A spectral basis and water level produce an optimal covariance, including zero-gain modes.
water-filling-optimizer· structural · solved · Formally stated · v1
Lean declarations (4)
CapacityAtlas.Channel.RealGaussianMIMOModeldefinition
lean/CapacityAtlas/Channels/GaussianMIMO.lean — Real channel matrix, white-noise variance, and total-power model.CapacityAtlas.Claims.gaussianMIMOclaim · operational-capacity
lean/CapacityAtlas/Claims/GaussianMIMO.lean — Real Gaussian MIMO operational capacity under the registered total power constraint.CapacityAtlas.Claims.gaussianMIMOAttainmentclaim · optimizer-attainment
lean/CapacityAtlas/Claims/GaussianMIMO.lean — The covariance supremum is attained by an admissible real positive-semidefinite covariance.CapacityAtlas.Claims.gaussianMIMOWaterFillingclaim · water-filling-optimizer
lean/CapacityAtlas/Claims/GaussianMIMO.lean — A spectral basis and water level produce an optimal covariance, including zero-gain modes.
References
- Emre Telatar (1999). Capacity of Multi-antenna Gaussian Channels. European Transactions on Telecommunications. DOI 10.1002/ett.4460100604.