InformationTheory

InformationTheory.Shannon.ShannonHartley.ConverseCount

source

Imports 4

Count domination for the Shannon–Hartley converse #

For an arbitrary code's orthonormal, time-limited test family φ : Fin k → E (with E = L²(ℝ;ℂ)), the number of band-limited Gram eigenvalues exceeding c is at most prolateCount T W c. This is the bridge that dominates an arbitrary code's Gram spectrum by the operator spectrum of A = timeBandLimitingOp T W; it feeds the water-filling head-count.

The band-limited Gram matrix is Gᵢⱼ = ⟪P_W φᵢ, P_W φⱼ⟫, whose eigenvalues are counted by bandGramEigenvalues. The proof realizes the high-eigenvalue eigenspace inside E (via the eigenvector images gramEig), where the operator-side Bessel domination frame_form_le_op_form supplies the Rayleigh bound feeding finrank_le_prolateCount_of_form_gt (the abstract min-max half of Cauchy interlacing).

It is non-circular: it does not assume codewords = prolate basis.

noncomputable def

InformationTheory.Shannon.bandGramEigenvalues

source
(W : ℝ) {k : ℕ} (φ : Fin k → TimeBandLimiting.E) :
Fin k → ℝ

The eigenvalues of the band-limited Gram matrix Gᵢⱼ = ⟪P_W φᵢ, P_W φⱼ⟫ of a test family φ : Fin k → E. These are the per-coordinate channel gains consumed by the water-filling converse.

Non-degenerate: this is the spectrum of the band-limited Gram (Matrix.gram ℂ on v i = P_W φᵢ, so Gᵢⱼ = ⟪P_W φᵢ, P_W φⱼ⟫), not the raw ⟪φᵢ,φⱼ⟫ = δᵢⱼ (which would force every gain = 1), nor a constant/zero. It pins the fine per-coordinate band-limited gain structure the water-filling converse consumes. @audit:ok

Equations
Instances For
    Used by
      theorem

      InformationTheory.Shannon.gram_high_eigen_finrank_le_prolateCount

      source
      (T W : ℝ) {c : ℝ} (hc : 0 < c) {k : ℕ} (φ : Fin k → TimeBandLimiting.E) (h_on : Orthonormal ℂ φ) (h_tl : ∀ (i : Fin k), φ i ∈ TimeBandLimiting.timeLimitSubspace T) :
      {j : Fin k | c < bandGramEigenvalues W φ j}.card ≤ TimeBandLimiting.prolateCount T W c

      Count domination in the converse min-max direction: the number of band-limited Gram eigenvalues of an orthonormal, time-limited test family φ that exceed c is at most prolateCount T W c. Dominates the arbitrary code's Gram spectrum by the operator spectrum of A = timeBandLimitingOp T W.

      sorryAx-free (#print axioms = [propext, Classical.choice, Quot.sound]). Count-domination, not false-as-framed: (1) bandGramEigenvalues W φ is the non-degenerate band-limited-Gram spectrum (see its docstring), so the count pins the fine structure water-filling needs. (2) h_on/h_tl are pure structural preconditions (orthonormal signals confined to [0,T]); neither bundles a count/eigenvalue/prolate claim — no :True slot, no circular := h, no *Hypothesis. (3) The eigenimages realize the high-ν Gram eigenspace as S ⊆ bandLimitSubspace W with finrank S = #{νⱼ > c} and A-Rayleigh > c on S (Bessel frame_form_le_op_form giving ∑ᵢ‖⟪g,φᵢ⟫‖² ≤ Re⟪Ag,g⟫, then the νⱼ > c strict comparison c∑‖aⱼ‖²νⱼ < ∑‖aⱼ‖²νⱼ²), so the min-max bound applies. Non-circular: no "codewords = prolate basis" assumption. @audit:ok

      Used by
        noncomputable def

        InformationTheory.Shannon.testFnLift

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

        The complex L² lift of a real, square-integrable test family: ψᵢ = (φᵢ : ℝ → ℂ) as an Lp element. This bridges a real code's testFn : Fin k → ℝ → ℝ to the operator-theoretic E-space, feeding the count domination gram_high_eigen_finrank_le_prolateCount.

        Non-degenerate: MemLp.coeFn_toLp (via hcoe in the wrapper) confirms its coercion is =ᵐ fun t => (φ i t : ℂ), i.e. the complex embedding of the real φ i, not the zero/constant class. @audit:ok

        Equations
        Instances For
          Used by
            theorem

            InformationTheory.Shannon.gram_high_eigen_finrank_le_prolateCount_real

            source
            (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 < bandGramEigenvalues W (testFnLift φ hmem) j}.card ≤ TimeBandLimiting.prolateCount T W c

            Count domination for a real test family: for an orthonormal, [0,T]-supported real test family φ, the number of band-limited Gram eigenvalues of its complex lift exceeding c is at most prolateCount T W c. Real-ℝ → ℝ façade of gram_high_eigen_finrank_le_prolateCount, consumed by the continuous-time AWGN code's testFn.

            sorryAx-free (#print axioms = [propext, Classical.choice, Quot.sound]). Thin façade — the count core is done by the already-audited E-level gram_high_eigen_finrank_le_prolateCount; the body only transfers hypotheses (h_on → complex Orthonormal, h_supp → timeLimitSubspace). hmem : ∀ i, MemLp (φ i) 2 is pure regularity, NOT load-bearing and NOT derivable from h_on/h_supp: a family φ₀ = 𝟙_A - 𝟙_{[0,1]\A} for a non-measurable A ⊆ [0,1] satisfies ∫ φ₀² = ∫ 𝟙_[0,1] = 1 (h_on) and support ⊆ [0,T] (h_supp) yet is not AEStronglyMeasurable, so hmem fails — confirming it is a non-vacuous measurability/L² precondition threaded from the code side. No laundering. @audit:ok

            Used by