InformationTheory.Shannon.AWGN.JointlyTypicalSet

source

Imports 3

AWGN jointly typical set #

The continuous jointly typical set for the AWGN channel coding theorem (Cover–Thomas).

Main definitions #

AWGNJointlyTypicalSet n P N ε — the jointly typical set on ℝⁿ × ℝⁿ cut out by three empirical power bounds.

Main statements #

AWGNJointlyTypicalSet_zero, AWGNJointlyTypicalSet_subset_of_le_ε, AWGNJointlyTypicalSet_measurable — degenerate case, monotonicity in the slack, and measurability of the jointly typical set.

AWGN jointly typical set #

def

InformationTheory.Shannon.AWGN.AWGNJointlyTypicalSet

source

(n : ℕ) (P N ε : ℝ) :

Set ((Fin n → ℝ) × (Fin n → ℝ))

The AWGN continuous jointly typical set (Cover–Thomas).

On ℝⁿ × ℝⁿ, the joint typical set for an AWGN channel with input power P, noise power N, and slack ε > 0, consists of pairs (x, y) such that

(1/n) ∑ xᵢ² ≤ P + ε — input power within slack of P,
(1/n) ∑ (xᵢ - yᵢ)² ≤ N + ε — empirical noise power within slack of N,
(1/n) ∑ yᵢ² ≤ (P + N) + ε — output power within slack of P + N.

For n = 0 the constraints are vacuous and the set is Set.univ.

Equations

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

Instances For

Used by

theorem

InformationTheory.Shannon.AWGN.mem_AWGNJointlyTypicalSet

source

@[simp]

{n : ℕ} {P N ε : ℝ} {p : (Fin n → ℝ) × (Fin n → ℝ)} :

p ∈ AWGNJointlyTypicalSet n P N ε ↔ ∑ i : Fin n, p.1 i ^ 2 ≤ ↑n * (P + ε) ∧ ∑ i : Fin n, (p.1 i - p.2 i) ^ 2 ≤ ↑n * (N + ε) ∧ ∑ i : Fin n, p.2 i ^ 2 ≤ ↑n * (P + N + ε)

Membership in AWGNJointlyTypicalSet unfolded.

Used by

theorem