InformationTheory

InformationTheory.Shannon.EntropyPower.Inequality

source

Imports 11

Entropy power inequality (Cover–Thomas) #

The entropy power inequality (EPI) for independent real-valued random variables X, Y:

exp(2 h(X + Y)) ≥ exp(2 h(X)) + exp(2 h(Y)),

stated through the named EPI-conclusion predicate IsEntropyPowerInequalityHypothesis, together with the Gaussian saturation case where the inequality holds with equality.

Main definitions #

Main statements #

Implementation notes #

entropyPower is defined as exp (2 h(μ)), directly matching the conclusion forms of Real.exp_pos / Real.exp_log; the Cover–Thomas normalization N(μ) = (2πe)⁻¹ · exp(2 h(μ)) is recovered by a scaling corollary. The Gaussian saturation case is discharged from Mathlib's gaussianReal_add_gaussianReal_of_indepFun together with differentialEntropy_gaussianReal.

entropyPower: definition and basic properties #

noncomputable def

InformationTheory.Shannon.EntropyPowerInequality.entropyPower

source
(μ : MeasureTheory.Measure ℝ) :
ℝ

The entropy power of a measure μ on ℝ: entropyPower μ := exp (2 · h(μ)), where h is InformationTheory.Shannon.differentialEntropy. This differs from the Cover–Thomas normalization N(X) := (2πe)⁻¹ · exp(2 h(X)) only by the constant (2πe), recovered by a scaling corollary.

Equations
Instances For
    Used by
      theorem

      InformationTheory.Shannon.EntropyPowerInequality.entropyPower_pos

      source
      (μ : MeasureTheory.Measure ℝ) :
      0 < entropyPower μ

      Entropy power is strictly positive.

      @audit:ok

      Used by
        theorem

        InformationTheory.Shannon.EntropyPowerInequality.entropyPower_nonneg

        source
        (μ : MeasureTheory.Measure ℝ) :
        0 ≤ entropyPower μ

        Entropy power is non-negative.

        @audit:ok

        Used by
          theorem

          InformationTheory.Shannon.EntropyPowerInequality.entropyPower_gaussianReal

          source
          (m : ℝ) {v : NNReal} (hv : v ≠ 0) :
          entropyPower (ProbabilityTheory.gaussianReal m v) = 2 * Real.pi * Real.exp 1 * ↑v

          Closed form for Gaussian entropy power: entropyPower (gaussianReal m v) = 2πe v. This is the Gaussian saturation reference value that drives the saturating case of EPI.

          Computation: by differentialEntropy_gaussianReal, h(𝒩(m,v)) = (1/2) log(2πe v), so entropyPower (𝒩(m,v)) = exp(2 · (1/2) log(2πe v)) = exp(log(2πe v)) = 2πe v.

          @audit:ok

          Used by

            EPI conclusion predicate #

            def

            InformationTheory.Shannon.EntropyPowerInequality.IsEntropyPowerInequalityHypothesis

            source
            {Ω : Type u_1} [MeasurableSpace Ω] (X Y : Ω → ℝ) (P : MeasureTheory.Measure Ω) :
            Prop

            The EPI conclusion named as a Prop:

            entropyPower (P.map (X+Y)) ≥ entropyPower (P.map X) + entropyPower (P.map Y).

            This is the conclusion itself and is not used as a hypothesis (that would be circular); it names the output of the Gaussian saturation case and downstream intermediate results.

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

                Gaussian saturation case #

                theorem

                InformationTheory.Shannon.EntropyPowerInequality.entropyPower_gaussian_additivity

                source
                {Ω : Type u_1} {mΩ : MeasurableSpace Ω} (P : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure P] (X Y : Ω → ℝ) (hX : Measurable X) (hY : Measurable Y) (hXY : ProbabilityTheory.IndepFun X Y P) (m₁ m₂ : ℝ) (v₁ v₂ : NNReal) (hv₁ : v₁ ≠ 0) (hv₂ : v₂ ≠ 0) (hLawX : MeasureTheory.Measure.map X P = ProbabilityTheory.gaussianReal m₁ v₁) (hLawY : MeasureTheory.Measure.map Y P = ProbabilityTheory.gaussianReal m₂ v₂) :
                entropyPower (MeasureTheory.Measure.map (fun (ω : Ω) => X ω + Y ω) P) = entropyPower (MeasureTheory.Measure.map X P) + entropyPower (MeasureTheory.Measure.map Y P)

                For independent Gaussians X, Y with nonzero variance, EPI holds with equality: exp(2 h(X+Y)) = exp(2 h(X)) + exp(2 h(Y)). This follows from gaussianReal_add_gaussianReal_of_indepFun identifying the law of the sum as Gaussian, together with the closed form differentialEntropy_gaussianReal.

                @audit:ok

                Used by
                  theorem

                  InformationTheory.Shannon.EntropyPowerInequality.isEntropyPowerInequalityHypothesis_of_gaussian

                  source
                  {Ω : Type u_1} {mΩ : MeasurableSpace Ω} (P : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure P] (X Y : Ω → ℝ) (hX : Measurable X) (hY : Measurable Y) (hXY : ProbabilityTheory.IndepFun X Y P) (m₁ m₂ : ℝ) (v₁ v₂ : NNReal) (hv₁ : v₁ ≠ 0) (hv₂ : v₂ ≠ 0) (hLawX : MeasureTheory.Measure.map X P = ProbabilityTheory.gaussianReal m₁ v₁) (hLawY : MeasureTheory.Measure.map Y P = ProbabilityTheory.gaussianReal m₂ v₂) :
                  IsEntropyPowerInequalityHypothesis X Y P

                  The entropy-power-inequality hypothesis is satisfied (with equality) whenever both X and Y are independent Gaussians.

                  @audit:ok

                  Used by

                    Corollaries #

                    theorem

                    InformationTheory.Shannon.EntropyPowerInequality.entropyPower_map_add_const

                    source
                    {μ : MeasureTheory.Measure ℝ} (hμ : μ.AbsolutelyContinuous MeasureTheory.volume) [MeasureTheory.SigmaFinite μ] (a : ℝ) :
                    entropyPower (MeasureTheory.Measure.map (fun (x : ℝ) => x + a) μ) = entropyPower μ

                    Translation invariance of entropy power: for μ ≪ volume and σ-finite μ, entropyPower (μ.map (· + a)) = entropyPower μ.

                    @audit:ok

                    Used by
                      theorem

                      InformationTheory.Shannon.EntropyPowerInequality.entropy_power_inequality_three_arg

                      source
                      {Ω : Type u_1} {mΩ : MeasurableSpace Ω} (P : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure P] (X Y Z : Ω → ℝ) (h_xy_z_epi : IsEntropyPowerInequalityHypothesis (fun (ω : Ω) => X ω + Y ω) Z P) (h_x_y_epi : IsEntropyPowerInequalityHypothesis X Y P) :
                      entropyPower (MeasureTheory.Measure.map (fun (ω : Ω) => X ω + Y ω + Z ω) P) ≥ entropyPower (MeasureTheory.Measure.map X P) + entropyPower (MeasureTheory.Measure.map Y P) + entropyPower (MeasureTheory.Measure.map Z P)

                      The three-variable EPI obtained by chaining the two-variable form: for independent X, Y, Z, exp(2 h(X+Y+Z)) ≥ exp(2 h(X)) + exp(2 h(Y)) + exp(2 h(Z)), from two lower-arity EPI conclusions (the X+Y vs Z pair and the X vs Y pair).

                      The body is a structural composition (associativity plus transitivity via linarith) with no internal sorry: the supplied h_xy_z_epi / h_x_y_epi carry lower-arity EPI conclusions IsEntropyPowerInequalityHypothesis _ _ P transparently, and this wrapper holds no core itself — the load-bearing content lives at the definition site of the IsEntropyPowerInequalityHypothesis predicate. The sister entropy_power_inequality_four_arg (EPI/Plumbing.lean) carries @audit:ok for the same reason.

                      @audit:ok

                      Used by