InformationTheory

InformationTheory.Shannon.AWGN.MutualInfoDecomposition

source

Imports 3

AWGN mutual-information decomposition #

The AWGN mutual-information bridge (Cover–Thomas) states the channel MI decomposition I(X;Y) = h(Y) − h(Y∣X), with the conditional differential entropy h(Y∣X) realized as the integral of the fibrewise differential entropies. The AWGN-specific form is IsAwgnMIDecomp.

Main definitions #

  • IsContChannelMIDecompHyp p W — the AWGN-independent, density-level mutual-information chain rule I(X;Y) = h(Y) − h(Y∣X) for an arbitrary Markov channel W and input law p.

Main statements #

Implementation notes #

The chain identity I(X;Y) = h(Y) − h(Y∣X) is not AWGN-specific: it holds for any Markov channel whose joint, output, and fibre laws are absolutely continuous w.r.t. Lebesgue volume (so all differential entropies are density integrals). It is a density-level identity obtained from the Radon–Nikodym / Bayes split rnDeriv (p ⊗ₘ W) (p.prod q) = W(y∣x) / q(y) together with the differential-entropy definition. The continuous form is captured by the single AWGN-independent predicate IsContChannelMIDecompHyp, which is strictly more primitive and reusable than the AWGN-specific IsAwgnMIDecomp; the AWGN-specific absolute-continuity side conditions are discharged here directly from gaussianReal_absolutelyContinuous.

Absolute-continuity facts #

theorem

InformationTheory.Shannon.AWGN.awgnChannel_apply_absolutelyContinuous

source
(N : NNReal) (hN : N ≠ 0) (h_meas : IsAwgnChannelMeasurable N) (x : ℝ) :
((awgnChannel N h_meas) x).AbsolutelyContinuous MeasureTheory.volume

Each AWGN fibre is absolutely continuous w.r.t. Lebesgue volume: gaussianReal x N ≪ volume for N ≠ 0.

Used by
    theorem

    InformationTheory.Shannon.AWGN.awgn_output_absolutelyContinuous_of_outputGaussian

    source
    (P : ℝ) (N : NNReal) (hPN : P.toNNReal + N ≠ 0) (h_meas : IsAwgnChannelMeasurable N) (h_out : IsAwgnOutputGaussian P N h_meas) :
    (ChannelCoding.outputDistribution (ProbabilityTheory.gaussianReal 0 P.toNNReal) (awgnChannel N h_meas)).AbsolutelyContinuous MeasureTheory.volume

    Given the output-Gaussian fact IsAwgnOutputGaussian, the output marginal is gaussianReal 0 (P.toNNReal + N), hence absolutely continuous w.r.t. Lebesgue volume.

    Used by

      Continuous-channel mutual-information chain rule predicate #

      def

      InformationTheory.Shannon.AWGN.IsContChannelMIDecompHyp

      source
      (p : MeasureTheory.Measure ℝ) (W : ChannelCoding.Channel ℝ ℝ) :
      Prop

      The continuous-channel mutual-information chain rule (mutualInfoOfChannel p W).toReal = differentialEntropy (outputDistribution p W) − ∫ x, differentialEntropy (W x) ∂p, i.e. I(X;Y) = h(Y) − h(Y∣X), for an input law p on ℝ and a Markov channel W. This is the density-based analogue of the discrete mutualInfo_eq_entropy_add_entropy_sub_jointEntropy; it requires the joint, output, and fibre laws to be absolutely continuous w.r.t. Lebesgue volume plus the relevant integrability, and makes no reference to the AWGN or Gaussian structure.

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

          Combinator: abstract chain rule → IsAwgnMIDecomp #

          theorem

          InformationTheory.Shannon.AWGN.awgn_midecomp_of_cont_chain

          source
          (P : ℝ) (N : NNReal) (h_meas : IsAwgnChannelMeasurable N) (h_chain : IsContChannelMIDecompHyp (ProbabilityTheory.gaussianReal 0 P.toNNReal) (awgnChannel N h_meas)) :
          IsAwgnMIDecomp P N h_meas

          IsAwgnMIDecomp follows from the abstract continuous MI chain rule. At the AWGN instance p := gaussianReal 0 P.toNNReal, W := awgnChannel N h_meas, the abstract predicate IsContChannelMIDecompHyp is definitionally the AWGN predicate IsAwgnMIDecomp, so the discharge is an exact.

          Used by
            theorem

            InformationTheory.Shannon.AWGN.cont_chain_of_awgn_midecomp

            source
            (P : ℝ) (N : NNReal) (h_meas : IsAwgnChannelMeasurable N) (h_decomp : IsAwgnMIDecomp P N h_meas) :
            IsContChannelMIDecompHyp (ProbabilityTheory.gaussianReal 0 P.toNNReal) (awgnChannel N h_meas)

            The reverse direction also holds definitionally — the AWGN predicate is just the abstract chain rule at the AWGN instance. Confirms the two predicates carry identical content (no information lost in the abstraction).

            Used by