InformationTheory

InformationTheory.Shannon.ShannonHartley.Converse

source

Imports 10

Shannon-Hartley converse — the operational parallel-Gaussian converse (equal-noise form) #

The converse chain for a ContAwgnCode T W P M, reducing the operational rate log M to the per-coordinate parallel-Gaussian sum plus Fano's error terms:

log M ≤ ∑ᵢ ½·log(1 + P'ᵢ/(N₀/2)) + binEntropy(Pe) + Pe·log(M − 1)

with ∑ᵢ P'ᵢ ≤ T·P. This is the equal-noise form (constant per-coordinate noise N₀/2); the Gram/prolate gains νᵢ enter downstream (rotation + water-filling) on the signal-power side.

The chain (mirroring the discrete AWGN converse's wiring):

  1. Fano + DPI single-shot: log M ≤ I(W; Y).toReal + Fano (shannon_converse_single_shot).
  2. Markov DPI W → S → Y, S = observation ∘ W: I(W; Y) ≤ I(S; Y) (mutualInfo_le_of_markov).
  3. RV ↔ channel bridge: I(S; Y) = mutualInfoOfChannel p_S W_chan.
  4. Parallel MI bound: (mutualInfoOfChannel p_S W_chan).toReal ≤ ∑ᵢ ½log(1 + P'ᵢ/(N₀/2)), ∑ P'ᵢ ≤ T·P (parallel_per_input_mi_le_sum + Bessel constraint membership).

References #

  • T. M. Cover and J. A. Thomas, Elements of Information Theory (2nd ed.), Wiley, 2006.

§L0 — The canonical joint law and its probability-measure instance #

noncomputable def

InformationTheory.Shannon.ShannonHartley.contAwgnConverseJoint

source
{T W P : ℝ} {M : ℕ} (c : ContAwgnCode T W P M) (N₀ : ℝ) :
MeasureTheory.Measure (Fin M × (Fin c.k → ℝ))

Canonical joint law of (W, Y) for a ContAwgnCode under a uniform message and the inlined per-observation AWGN law — the ContAwgn analog of AWGN.awgnConverseJoint.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    Used by
      instance

      InformationTheory.Shannon.ShannonHartley.contAwgnConverseJoint.instIsProbabilityMeasure

      source
      {T W P : ℝ} {M : ℕ} [NeZero M] (c : ContAwgnCode T W P M) (N₀ : ℝ) :
      MeasureTheory.IsProbabilityMeasure (contAwgnConverseJoint c N₀)

      contAwgnConverseJoint is a probability measure for M ≥ 1.

      Used by

        Constant-noise parallel channel and its measurability discharge #

        theorem

        InformationTheory.Shannon.ShannonHartley.contAwgn_isParallelAwgnChannelMeasurable

        source
        {k : ℕ} (Nv : NNReal) :
        ParallelGaussian.IsParallelAwgnChannelMeasurable fun (x : Fin k) => Nv

        The per-coordinate AWGN measurability hypothesis for the constant noise family.

        Used by
          theorem

          InformationTheory.Shannon.ShannonHartley.contAwgn_isParallelGaussianKernelMeasurable

          source
          {k : ℕ} (Nv : NNReal) :
          ParallelGaussian.IsParallelGaussianKernelMeasurable fun (x : Fin k) => Nv

          The parallel-kernel measurability hypothesis for the constant noise family: the product Gaussian map x ↦ Measure.pi (fun i ↦ gaussianReal (x i) Nv) is measurable.

          Used by
            noncomputable def

            InformationTheory.Shannon.ShannonHartley.contAwgnConstChannel

            source
            (k : ℕ) (Nv : NNReal) :
            ChannelCoding.Channel (Fin k → ℝ) (Fin k → ℝ)

            The constant-noise parallel Gaussian channel Fin k → ℝ → Fin k → ℝ.

            Equations
            Instances For
              Used by
                theorem

                InformationTheory.Shannon.ShannonHartley.contAwgnConstChannel_apply

                source
                @[simp]
                (k : ℕ) (Nv : NNReal) (x : Fin k → ℝ) :
                (contAwgnConstChannel k Nv) x = MeasureTheory.Measure.pi fun (i : Fin k) => ProbabilityTheory.gaussianReal (x i) Nv
                Used by
                  instance

                  InformationTheory.Shannon.ShannonHartley.contAwgnConstChannel.instIsMarkovKernel

                  source
                  (k : ℕ) (Nv : NNReal) :
                  ProbabilityTheory.IsMarkovKernel (contAwgnConstChannel k Nv)
                  Used by
                    noncomputable def

                    InformationTheory.Shannon.ShannonHartley.contAwgnSignalLaw

                    source
                    {T W P : ℝ} {M : ℕ} (c : ContAwgnCode T W P M) (N₀ : ℝ) :
                    MeasureTheory.Measure (Fin c.k → ℝ)

                    The signal (codeword) law p_S: the law of S = observation ∘ W under the uniform message.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      Used by
                        instance

                        InformationTheory.Shannon.ShannonHartley.contAwgnSignalLaw.instIsProbabilityMeasure

                        source
                        {T W P : ℝ} {M : ℕ} [NeZero M] (c : ContAwgnCode T W P M) (N₀ : ℝ) :
                        MeasureTheory.IsProbabilityMeasure (contAwgnSignalLaw c N₀)
                        Used by

                          §L1 — Single-shot converse wiring #

                          theorem

                          InformationTheory.Shannon.ShannonHartley.contAwgnConverseJoint_map_fst

                          source
                          {T W P : ℝ} {M : ℕ} [NeZero M] (c : ContAwgnCode T W P M) (N₀ : ℝ) :
                          MeasureTheory.Measure.map Prod.fst (contAwgnConverseJoint c N₀) = (↑(Fintype.card (Fin M)))⁻¹ • MeasureTheory.Measure.count

                          The message marginal (contAwgnConverseJoint c N₀).map Prod.fst is uniform.

                          Used by
                            theorem

                            InformationTheory.Shannon.ShannonHartley.contAwgn_errorProb_eq_averageError

                            source
                            {T W P : ℝ} {M : ℕ} [NeZero M] (c : ContAwgnCode T W P M) (N₀ : ℝ) :
                            MeasureFano.errorProb (contAwgnConverseJoint c N₀) Prod.fst Prod.snd c.decoder = (c.averageError N₀).toReal

                            The Fano error probability equals the ContAwgn average error (c.averageError N₀).toReal.

                            Used by

                              §L3 — RV ↔ channel bridge #

                              theorem

                              InformationTheory.Shannon.ShannonHartley.contAwgnSignalLaw_eq_mixture

                              source
                              {T W P : ℝ} {M : ℕ} [NeZero M] (c : ContAwgnCode T W P M) (N₀ : ℝ) :
                              contAwgnSignalLaw c N₀ = (↑M)⁻¹ • ∑ m : Fin M, MeasureTheory.Measure.dirac (c.observation m)

                              The signal law as a mixture of Diracs (1/M) ∑ₘ δ(observation m).

                              Used by
                                theorem

                                InformationTheory.Shannon.ShannonHartley.contAwgnConverseJoint_map_pair_eq_compProd

                                source
                                {T W P : ℝ} {M : ℕ} [NeZero M] (c : ContAwgnCode T W P M) (N₀ : ℝ) :
                                MeasureTheory.Measure.map (fun (ω : Fin M × (Fin c.k → ℝ)) => (c.observation ω.1, ω.2)) (contAwgnConverseJoint c N₀) = (contAwgnSignalLaw c N₀).compProd (contAwgnConstChannel c.k (N₀ / 2).toNNReal)

                                The signal-vs-output pair law factors as p_S ⊗ₘ W_chan.

                                Used by
                                  theorem

                                  InformationTheory.Shannon.ShannonHartley.contAwgn_outputDistribution_eq

                                  source
                                  {T W P : ℝ} {M : ℕ} [NeZero M] (c : ContAwgnCode T W P M) (N₀ : ℝ) :
                                  ChannelCoding.outputDistribution (contAwgnSignalLaw c N₀) (contAwgnConstChannel c.k (N₀ / 2).toNNReal) = MeasureTheory.Measure.map Prod.snd (contAwgnConverseJoint c N₀)

                                  The output distribution equals the Prod.snd marginal of the joint.

                                  Used by
                                    theorem

                                    InformationTheory.Shannon.ShannonHartley.contAwgn_mi_S_eq_mutualInfoOfChannel

                                    source
                                    {T W P : ℝ} {M : ℕ} [NeZero M] (c : ContAwgnCode T W P M) (N₀ : ℝ) :
                                    mutualInfo (contAwgnConverseJoint c N₀) (fun (ω : Fin M × (Fin c.k → ℝ)) => c.observation ω.1) Prod.snd = ChannelCoding.mutualInfoOfChannel (contAwgnSignalLaw c N₀) (contAwgnConstChannel c.k (N₀ / 2).toNNReal)

                                    I(S; Y) = mutualInfoOfChannel p_S W_chan for S = observation ∘ W and the constant-noise parallel channel W_chan. @audit:ok

                                    Used by

                                      §L2 — Markov DPI W → S → Y #

                                      theorem

                                      InformationTheory.Shannon.ShannonHartley.contAwgnConverseMarkov_holds

                                      source
                                      {T W P : ℝ} {M : ℕ} [NeZero M] (c : ContAwgnCode T W P M) (N₀ : ℝ) :
                                      IsMarkovChain (contAwgnConverseJoint c N₀) Prod.fst (fun (ω : Fin M × (Fin c.k → ℝ)) => c.observation ω.1) Prod.snd

                                      The Markov chain W → observation ∘ W → Y factorization for the ContAwgn joint. The signal-level analog of AWGN.awgnConverseMarkov_holds: observation is the deterministic encoder, so Y depends on W only through S = observation ∘ W. @audit:ok

                                      Used by

                                        §L4 — Power-constraint set membership (Bessel) #

                                        theorem

                                        InformationTheory.Shannon.ShannonHartley.contAwgn_sum_observation_sq_le

                                        source
                                        {T W P : ℝ} {M : ℕ} (c : ContAwgnCode T W P M) (m : Fin M) :
                                        ∑ i : Fin c.k, c.observation m i ^ 2 ≤ T * P

                                        Bessel's inequality against the orthonormal test family: the total observed energy of any codeword is capped by its whole-line L² energy, hence by the power budget T·P. @audit:ok

                                        Used by
                                          theorem

                                          InformationTheory.Shannon.ShannonHartley.contAwgn_signalLaw_mem_constraint

                                          source
                                          {T W P : ℝ} {M : ℕ} [NeZero M] (c : ContAwgnCode T W P M) (N₀ : ℝ) (hTP : 0 ≤ T * P) :
                                          contAwgnSignalLaw c N₀ ∈ ParallelGaussian.parallelGaussianPowerConstraintSet (T * P)

                                          The signal law lies in the parallel power constraint set with budget T·P.

                                          Used by

                                            §L5 — MI-finiteness #

                                            theorem

                                            InformationTheory.Shannon.ShannonHartley.contAwgn_mi_W_ne_top

                                            source
                                            {T W P : ℝ} {M : ℕ} [NeZero M] (c : ContAwgnCode T W P M) {N₀ : ℝ} (hN₀ : 0 < N₀) :
                                            mutualInfo (contAwgnConverseJoint c N₀) Prod.fst Prod.snd ≠ ⊤

                                            I(W; Y) ≠ ∞ on the ContAwgn converse joint. Reduces to the discrete AWGN converse finiteness AWGN.awgnConverseJoint_mutualInfo_ne_top by identifying contAwgnConverseJoint with AWGN.awgnConverseJoint at encoder = observation, N = (N₀/2).toNNReal. The identification is definitional (awgnChannel x N = gaussianReal x N, Fintype.card (Fin M) = M); the discrete finiteness needs only N ≠ 0, so the power value T·P is irrelevant to the reduction.

                                            @audit:ok

                                            Used by

                                              §C — the operational parallel-Gaussian converse #

                                              theorem

                                              InformationTheory.Shannon.ShannonHartley.contAwgn_operational_converse_percoord

                                              source
                                              {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) :
                                              ∃ (P' : Fin c.k → ℝ), (∀ (i : Fin c.k), 0 ≤ P' i) ∧ (∀ (i : Fin c.k), P' i ≤ ∫ (x : Fin c.k → ℝ), x i ^ 2 ∂contAwgnSignalLaw c N₀) ∧ Real.log ↑M ≤ ∑ i : Fin c.k, 1 / 2 * Real.log (1 + P' i / (N₀ / 2)) + Real.binEntropy Pe + Pe * Real.log (↑M - 1)

                                              The operational parallel-Gaussian converse in per-coordinate form. It strengthens contAwgn_operational_converse by exposing the per-coordinate second-moment ellipsoid P'ᵢ ≤ ∫ (xᵢ)² ∂(contAwgnSignalLaw c N₀) in place of the plain-sum budget ∑ P'ᵢ ≤ T·P. Water-filling needs the per-coordinate constraint; the plain-sum version is the corollary contAwgn_operational_converse directly below.

                                              Used by
                                                theorem

                                                InformationTheory.Shannon.ShannonHartley.contAwgn_operational_converse

                                                source
                                                {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) :
                                                ∃ (P' : Fin c.k → ℝ), (∀ (i : Fin c.k), 0 ≤ P' i) ∧ ∑ i : Fin c.k, P' i ≤ T * P ∧ Real.log ↑M ≤ ∑ i : Fin c.k, 1 / 2 * Real.log (1 + P' i / (N₀ / 2)) + Real.binEntropy Pe + Pe * Real.log (↑M - 1)

                                                The operational parallel-Gaussian converse in equal-noise form (the Gram/prolate gains νᵢ enter downstream at water-filling). For a ContAwgnCode with 2 ≤ M and average error Pe, the log message count is bounded by the per-coordinate parallel-Gaussian sum plus the Fano terms. Plain-sum corollary of contAwgn_operational_converse_percoord: the per-coordinate ellipsoid P'ᵢ ≤ ∫ (xᵢ)² ∂p summed against the total power budget ∑ᵢ ∫ (xᵢ)² ∂p ≤ T·P yields ∑ P'ᵢ ≤ T·P.

                                                Used by