Skip to content

InformationTheory.Shannon.ShannonHartley.Rotation

Imports 6

Shannon–Hartley converse — isotropic-Gaussian rotation invariance #

The measure-theoretic crux of the Shannon–Hartley converse rotation. An isotropic Gaussian on Fin k → ℝ with per-coordinate mean v i and common variance N is invariant under an orthogonal transformation, up to rotating the mean:

(Measure.pi (fun i => gaussianReal (v i) N)).map (O.mulVec) = Measure.pi (fun i => gaussianReal ((O v) i) N)

for O ∈ Matrix.orthogonalGroup (Fin k) ℝ. This will be consumed by the downstream errorProbAt rotation, which rotates a code's testFn family by the real orthogonal eigenvector matrix of the band-Gram operator.

Approach #

The proof goes through characteristic functions on EuclideanSpace ℝ (Fin k). By charFun_eq_pi_iff, the product-measure equality reduces to the pointwise identity of characteristic functions. Pushing the map through charFun (change of variables) plus the orthogonal-matrix adjoint identities (x ⬝ᵥ (O *ᵥ y) = (Oᵀ *ᵥ x) ⬝ᵥ y and O * Oᵀ = 1) turns the left-hand product into the right-hand one after expanding charFun_gaussianReal and combining the exponentials.

theorem

InformationTheory.Shannon.ShannonHartley.measurePi_gaussianReal_map_orthogonal

{k : ℕ} (N : NNReal) (v : Fin k → ℝ) (O : Matrix (Fin k) (Fin k) ℝ) (hO : O ∈ Matrix.orthogonalGroup (Fin k) ℝ) :

MeasureTheory.Measure.map (fun (y : Fin k → ℝ) => O.mulVec y) (MeasureTheory.Measure.pi fun (i : Fin k) => ProbabilityTheory.gaussianReal (v i) N) = MeasureTheory.Measure.pi fun (i : Fin k) => ProbabilityTheory.gaussianReal (O.mulVec v i) N

Isotropic Gaussian rotation invariance: the law of v + Z with Z ~ N(0, N·I) on Fin k → ℝ, pushed forward by an orthogonal matrix O, equals the law of (O v) + Z. Concretely, the pushforward of Measure.pi (fun i => gaussianReal (v i) N) under O.mulVec is Measure.pi (fun i => gaussianReal ((O.mulVec v) i) N).

Used by

noncomputable def

InformationTheory.Shannon.ShannonHartley.ContAwgnCode.rotate

{T W P : ℝ} {M : ℕ} (c : ContAwgnCode T W P M) (O : Matrix (Fin c.k) (Fin c.k) ℝ) (hO : O ∈ Matrix.orthogonalGroup (Fin c.k) ℝ) :

ContAwgnCode T W P M

The rotated code: rotate a ContAwgnCode's orthonormal test-function family by an orthogonal matrix O and post-compose the decoder with Oᵀ = O⁻¹. The encoder (hence the transmitted signals and the power budget) is untouched; only the receiver's coordinate frame turns. Because O is orthogonal, the rotated test functions stay orthonormal and supported in the window, so this is again a valid ContAwgnCode, and (by ContAwgnCode.rotate_averageError) it has exactly the same error probability. This is the coordinate change that diagonalizes the band-Gram operator in the Shannon–Hartley converse.

Equations

One or more equations did not get rendered due to their size.

Instances For

Used by

theorem

InformationTheory.Shannon.ShannonHartley.ContAwgnCode.rotate_observation

{T W P : ℝ} {M : ℕ} (c : ContAwgnCode T W P M) (O : Matrix (Fin c.k) (Fin c.k) ℝ) (hO : O ∈ Matrix.orthogonalGroup (Fin c.k) ℝ) (m : Fin M) :

(c.rotate O hO).observation m = O.mulVec (c.observation m)

Rotating the test functions rotates the observation vector by the same matrix: (c.rotate O hO).observation m = O.mulVec (c.observation m).

Used by

theorem

InformationTheory.Shannon.ShannonHartley.ContAwgnCode.rotate_averageError

{T W P : ℝ} {M : ℕ} (c : ContAwgnCode T W P M) (O : Matrix (Fin c.k) (Fin c.k) ℝ) (hO : O ∈ Matrix.orthogonalGroup (Fin c.k) ℝ) (N₀ : ℝ) :

(c.rotate O hO).averageError N₀ = c.averageError N₀

Rotating the code by an orthogonal matrix leaves the average error probability unchanged: the isotropic AWGN law is rotation-invariant (S1), and the decoder is pre-composed with the inverse rotation, so the error set transports back exactly.

Used by

S2 — real orthogonal eigenbasis of the band-Gram + count bridge #

For a real, orthonormal, [0,T]-supported test family φ : Fin k → ℝ → ℝ, the band-limited Gram Gᵢⱼ = ⟪P_W (φᵢ)ℂ, P_W (φⱼ)ℂ⟫_ℂ has real entries (the lifted functions are self-conjugate, so each entry equals its own complex conjugate). Hence the complex-Hermitian band-Gram is the ℝ → ℂ-image of a genuine real symmetric matrix bandGramRealMatrix, which the real spectral theorem diagonalizes by an orthogonal matrix. This exposes, for the S3 rotation:

bandGramRealMatrix / bandGramRealEigenvalues (μ) / bandGramRealUnitary (O);
bandGramRealUnitary_mem_orthogonalGroup (↑O ∈ orthogonalGroup, feeds ContAwgnCode.rotate);
bandGramRealMatrix_diagonalize (Oᵀ Gᵣ O = diagonal μ);
bandGramReal_high_count_le (#{c < μⱼ} ≤ prolateCount T W c, the count bound of the converse).

noncomputable def

InformationTheory.Shannon.ShannonHartley.bandGramRealMatrix

(W : ℝ) {k : ℕ} (φ : Fin k → ℝ → ℝ) (hmem : ∀ (i : Fin k), MeasureTheory.MemLp (φ i) 2 MeasureTheory.volume) :

Matrix (Fin k) (Fin k) ℝ

The real symmetric band-Gram matrix Gᵣ ᵢⱼ = Re ⟪P_W (φᵢ)ℂ, P_W (φⱼ)ℂ⟫_ℂ of a real test family φ. Its complex lift is the band-limited Gram of testFnLift φ hmem, and its real eigen-decomposition diagonalizes the band-Gram for the Shannon–Hartley converse rotation.

Equations

One or more equations did not get rendered due to their size.

Instances For

Used by

theorem

InformationTheory.Shannon.ShannonHartley.bandGram_eq_map_real

(W : ℝ) {k : ℕ} (φ : Fin k → ℝ → ℝ) (hmem : ∀ (i : Fin k), MeasureTheory.MemLp (φ i) 2 MeasureTheory.volume) :

(Matrix.gram ℂ fun (i : Fin k) => (TimeBandLimiting.bandLimitSubspace W).starProjection (testFnLift φ hmem i)) = (bandGramRealMatrix W φ hmem).map ⇑(algebraMap ℝ ℂ)

The band-limited Gram of the complex lift of a real test family has real entries: it is the ℝ → ℂ-image of bandGramRealMatrix.

Used by

theorem

InformationTheory.Shannon.ShannonHartley.bandGramRealMatrix_isHermitian

(W : ℝ) {k : ℕ} (φ : Fin k → ℝ → ℝ) (hmem : ∀ (i : Fin k), MeasureTheory.MemLp (φ i) 2 MeasureTheory.volume) :

(bandGramRealMatrix W φ hmem).IsHermitian

bandGramRealMatrix is real-symmetric (Hermitian).

Used by

noncomputable def

InformationTheory.Shannon.ShannonHartley.bandGramRealEigenvalues

(W : ℝ) {k : ℕ} (φ : Fin k → ℝ → ℝ) (hmem : ∀ (i : Fin k), MeasureTheory.MemLp (φ i) 2 MeasureTheory.volume) :

Fin k → ℝ

The eigenvalues μ of the real band-Gram (= per-coordinate channel gains for the converse).

Equations

InformationTheory.Shannon.ShannonHartley.bandGramRealEigenvalues W φ hmem = ⋯.eigenvalues

Instances For

Used by

noncomputable def

InformationTheory.Shannon.ShannonHartley.bandGramRealUnitary

(W : ℝ) {k : ℕ} (φ : Fin k → ℝ → ℝ) (hmem : ∀ (i : Fin k), MeasureTheory.MemLp (φ i) 2 MeasureTheory.volume) :

↥(Matrix.unitaryGroup (Fin k) ℝ)

The orthogonal eigenvector matrix O diagonalizing the real band-Gram.

Equations

InformationTheory.Shannon.ShannonHartley.bandGramRealUnitary W φ hmem = ⋯.eigenvectorUnitary

Instances For

Used by

theorem

InformationTheory.Shannon.ShannonHartley.bandGramRealUnitary_mem_orthogonalGroup

(W : ℝ) {k : ℕ} (φ : Fin k → ℝ → ℝ) (hmem : ∀ (i : Fin k), MeasureTheory.MemLp (φ i) 2 MeasureTheory.volume) :

↑(bandGramRealUnitary W φ hmem) ∈ Matrix.orthogonalGroup (Fin k) ℝ

↑O ∈ orthogonalGroup, the hypothesis consumed by ContAwgnCode.rotate.

Used by

theorem

InformationTheory.Shannon.ShannonHartley.bandGramRealUnitary_transpose_mem_orthogonalGroup

(W : ℝ) {k : ℕ} (φ : Fin k → ℝ → ℝ) (hmem : ∀ (i : Fin k), MeasureTheory.MemLp (φ i) 2 MeasureTheory.volume) :

(↑(bandGramRealUnitary W φ hmem)).transpose ∈ Matrix.orthogonalGroup (Fin k) ℝ

↑Oᵀ ∈ orthogonalGroup (the orthogonal group is closed under transpose).

Used by

theorem

InformationTheory.Shannon.ShannonHartley.bandGramRealMatrix_diagonalize

(W : ℝ) {k : ℕ} (φ : Fin k → ℝ → ℝ) (hmem : ∀ (i : Fin k), MeasureTheory.MemLp (φ i) 2 MeasureTheory.volume) :

(↑(bandGramRealUnitary W φ hmem)).transpose * bandGramRealMatrix W φ hmem * ↑(bandGramRealUnitary W φ hmem) = Matrix.diagonal (bandGramRealEigenvalues W φ hmem)

Real spectral diagonalization of the band-Gram: Oᵀ Gᵣ O = diagonal μ, the frame the converse rotates the code into.

Used by

theorem

InformationTheory.Shannon.ShannonHartley.bandGramReal_high_count_le

(T W : ℝ) {c : ℝ} (hc : 0 < c) {k : ℕ} (φ : Fin k → ℝ → ℝ) (hmem : ∀ (i : Fin k), MeasureTheory.MemLp (φ i) 2 MeasureTheory.volume) (h_on : ∀ (i j : Fin k), ∫ (t : ℝ), φ i t * φ j t = if i = j then 1 else 0) (h_supp : ∀ (i : Fin k), Function.support (φ i) ⊆ Set.Icc 0 T) :

{j : Fin k | c < bandGramRealEigenvalues W φ hmem j}.card ≤ TimeBandLimiting.prolateCount T W c

The number of real band-Gram eigenvalues exceeding c is at most prolateCount T W c, the head-count the converse consumes. The real-eigenvalue façade of gram_high_eigen_finrank_le_prolateCount_real, obtained by matching the real spectrum against the complex band-Gram spectrum at the characteristic-polynomial level.

Used by

S3 — second-moment identity for the rotated converse code #

For an arbitrary code c, rotating by Oᵀ (O = the band-Gram eigenvector matrix) makes the rotated observation's per-coordinate second moment factor as νᵢ · Qᵢ, where νᵢ = bandGramRealEigenvalues and Qᵢ is a per-mode input power with ∑Qᵢ ≤ T·P. The three public deliverables consumed by the downstream ellipsoid/water-filling leg are:

bandGramRealEigenvalues_nonneg — the band-Gram is PSD, so νᵢ ≥ 0;
bandGramRealEigenvalues_le_one — νᵢ ≤ 1 (projection contracts the orthonormal raw frame);
contAwgn_rotated_secondMoment — ∫ (x i)² ∂(rotated signal law) = νᵢ · Qᵢ, ∑Qᵢ ≤ T·P, Qᵢ ≥ 0.

theorem

InformationTheory.Shannon.ShannonHartley.bandGramRealEigenvalues_nonneg

(W : ℝ) {k : ℕ} (φ : Fin k → ℝ → ℝ) (hmem : ∀ (i : Fin k), MeasureTheory.MemLp (φ i) 2 MeasureTheory.volume) (i : Fin k) :

0 ≤ bandGramRealEigenvalues W φ hmem i

The band-Gram is positive semidefinite, so its eigenvalues are nonnegative.

Used by

theorem

InformationTheory.Shannon.ShannonHartley.bandGramRealEigenvalues_le_one

(W : ℝ) {k : ℕ} (φ : Fin k → ℝ → ℝ) (hmem : ∀ (i : Fin k), MeasureTheory.MemLp (φ i) 2 MeasureTheory.volume) (h_on : ∀ (i j : Fin k), ∫ (t : ℝ), φ i t * φ j t = if i = j then 1 else 0) (i : Fin k) :

bandGramRealEigenvalues W φ hmem i ≤ 1

The band-Gram eigenvalues are at most 1 (the projection P_W contracts the orthonormal raw frame).

Used by

theorem

InformationTheory.Shannon.ShannonHartley.contAwgn_rotated_secondMoment

{T W P N₀ : ℝ} {M : ℕ} [NeZero M] (c : ContAwgnCode T W P M) :

∃ (Q : Fin c.k → ℝ), (∀ (i : Fin c.k), 0 ≤ Q i) ∧ ∑ i : Fin c.k, Q i ≤ T * P ∧ ∀ (i : Fin (c.rotate (↑(bandGramRealUnitary W c.testFn ⋯)).transpose ⋯).k), ∫ (x : Fin (c.rotate (↑(bandGramRealUnitary W c.testFn ⋯)).transpose ⋯).k → ℝ), x i ^ 2 ∂contAwgnSignalLaw (c.rotate (↑(bandGramRealUnitary W c.testFn ⋯)).transpose ⋯) N₀ = bandGramRealEigenvalues W c.testFn ⋯ i * Q i

For an arbitrary code c, rotating by Oᵀ (the transpose of the band-Gram eigenvector matrix) factors the rotated observation's per-coordinate second moment as νᵢ · Qᵢ, where νᵢ = bandGramRealEigenvalues and the per-mode powers Qᵢ ≥ 0 satisfy ∑Qᵢ ≤ T·P. This is the ellipsoid data the water-filling converse consumes.

Used by

theorem

InformationTheory.Shannon.ShannonHartley.contAwgn_converse_ellipsoid

{T W P N₀ : ℝ} {M : ℕ} (hN₀ : 0 < N₀) (hP : 0 ≤ P) (hM : 2 ≤ M) (c : ContAwgnCode T W P M) (Pe : ℝ) (hPe : Pe = (c.averageError N₀).toReal) :

∃ (Q : Fin c.k → ℝ), (∀ (i : Fin c.k), 0 ≤ Q i) ∧ ∑ i : Fin c.k, Q i ≤ T * P ∧ Real.log ↑M ≤ ∑ i : Fin c.k, 1 / 2 * Real.log (1 + bandGramRealEigenvalues W c.testFn ⋯ i * Q i / (N₀ / 2)) + Real.binEntropy Pe + Pe * Real.log (↑M - 1)

Per-code ellipsoid converse: rotating a ContAwgnCode by the real orthogonal eigenvector matrix of the band-Gram operator turns the operational parallel-Gaussian converse into the diagonal (eigenbasis) form: the log message count is bounded by the per-eigenvalue parallel-Gaussian sum with gains νᵢ = bandGramRealEigenvalues … folded into an ellipsoid power budget ∑ᵢ Qᵢ ≤ T·P. Mechanically assembles the per-coordinate converse contAwgn_operational_converse_percoord applied to the rotated code with the rotation second-moment factorization contAwgn_rotated_secondMoment.

Used by