InformationTheory.Shannon.AWGN.MIClosedForm

Imports 3

AWGN Gaussian-input MI closed form #

The hypothesis-free Gaussian-input mutual-information closed form I = (1/2)·log(1 + P/N) (no opaque h_bridge hypothesis for the textbook identity I = h(P+N) − h(N)), assembled from the MI decomposition (mutualInfoOfChannel_toReal_eq_diffEntropy_sub, ContChannelMIDecomp.lean) and the output-Gaussian bind/conv bridge (AWGN/BindConvolution.lean).

ContChannelMIDecomp.lean's own closed-form producer awgn_mi_gaussian_closed_form_of_out still leaves IsAwgnOutputGaussian standing as a hypothesis; this file discharges it inline from the AWGN-specialized, hypothesis-free bind/conv fact isAwgnBindEqConv (BindConvolution.lean), so it is the join point where the fully hypothesis-free wrapper is assembled.

theorem

InformationTheory.Shannon.AWGN.mutualInfoOfChannel_gaussianInput_closed_form'

source

(P : ℝ) (hP : 0 < P) (N : NNReal) (hN : ↑N ≠ 0) (h_meas : IsAwgnChannelMeasurable N) :

(ChannelCoding.mutualInfoOfChannel (ProbabilityTheory.gaussianReal 0 P.toNNReal) (awgnChannel N h_meas)).toReal = 1 / 2 * Real.log (1 + P / ↑N)

AWGN channel mutual information, Gaussian input, closed form I = (1/2)·log(1 + P/N), fully hypothesis-free (takes no h_bridge). The log-algebra is awgn_mi_gaussian_closed_form_of_primitives (MIBridge.lean).

Used by