InformationTheory.Shannon.ShannonHartley.Preequalizer

Imports 3

Pre-equalizer: bounded-below endomorphisms are invertible with norm control #

The geometric core of the Shannon–Hartley achievability route ("route (ii)", the operator lower bound). A linear endomorphism A of a finite-dimensional inner-product space that is bounded below, c ‖v‖² ≤ ‖A v‖² with c > 0, is surjective, and every target t has a preimage a whose energy is controlled: ‖a‖² ≤ (1/c) ‖t‖². This replaces the matrix-inverse G⁻¹ step of the informal sketch with a self-contained finite-dimensional fact.

theorem

InformationTheory.Shannon.ShannonHartleyPreequalizer.exists_preequalizer

source

{n : ℕ} {c : ℝ} (hc : 0 < c) (A : EuclideanSpace ℝ (Fin n) →ₗ[ℝ ] EuclideanSpace ℝ (Fin n)) (hbdd : ∀ (v : EuclideanSpace ℝ (Fin n)), c * ‖v‖ ^ 2 ≤ ‖A v‖ ^ 2) (t : EuclideanSpace ℝ (Fin n)) :

∃ (a : EuclideanSpace ℝ (Fin n)), A a = t ∧ ‖a‖ ^ 2 ≤ 1 / c * ‖t‖ ^ 2

A bounded-below (c ‖v‖² ≤ ‖A v‖², c > 0) linear endomorphism of a finite-dimensional inner-product space is surjective with a norm-controlled preimage: every target t has an a with A a = t and ‖a‖² ≤ (1/c) ‖t‖².

Injectivity: A v = 0 forces c ‖v‖² ≤ 0, so v = 0. On a finite-dimensional space an injective endomorphism is surjective, giving the preimage a; feeding it back through the lower bound and dividing by c > 0 yields the energy control.

Used by