InformationTheory

InformationTheory.Shannon.EntropyPower.Ext

source

Imports 9

Extended entropy power #

A two-layer redefinition of entropy power on EReal that removes the degeneracy of the real-valued entropyPower (under which a singular measure satisfies entropyPower = exp 0 = 1).

  • differentialEntropyExt : Measure ℝ → EReal returns ⊥ for a singular measure and, for μ ≪ volume, the genuine extended differential entropy as the EReal difference of the positive and negative parts. It evaluates to ⊤ for an infinite-entropy a.c. density (h = +∞), to ⊥ for a tall peaked density (h = −∞), and to the workhorse differentialEntropy value when finite.
  • entropyPowerExt : Measure ℝ → ℝ≥0∞ is the non-branching EReal.exp (2 * differentialEntropyExt μ), with EReal.exp absorbing exp ⊥ = 0, exp ⊤ = ∞, and exp ↑x = ofReal (exp x) in one function.

Main definitions #

Implementation notes #

The a.c. branch must distinguish signs: coercing differentialEntropy μ directly is false as stated for infinite-entropy inputs, because the Bochner integral returns 0 when the integrand is non-integrable, collapsing h = ±∞ to entropyPowerExt = 1. Taking the EReal difference of the positive part ∫⁻ ofReal(negMulLog f) and the negative part ∫⁻ ofReal(-(negMulLog f)) produces +∞ / −∞ / a finite value correctly. Following klDiv, the a.c. test is made definitional via open Classical in together with irreducible_def.

noncomputable def

InformationTheory.Shannon.differentialEntropyExt

source
@[irreducible]
(μ : MeasureTheory.Measure ℝ) :
EReal

The extended differential entropy: ⊥ for a singular measure and, for μ ≪ volume, the EReal difference A − B of the positive part A := ∫⁻ ofReal(negMulLog f) and the negative part B := ∫⁻ ofReal(-(negMulLog f)) of negMulLog ∘ f, where f is the density. When both A and B are finite this equals the workhorse differentialEntropy μ; A = ⊤ (heavy tail) gives ⊤, B = ⊤ (tall peak) gives ⊥, and A = B = ⊤ gives ⊥ (the EPI-safe side of ⊤ − ⊤).

@audit:ok

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

      InformationTheory.Shannon.differentialEntropyExt_def

      source
      (μ : MeasureTheory.Measure ℝ) :
      differentialEntropyExt μ = if μ.AbsolutelyContinuous MeasureTheory.volume then ↑(∫⁻ (x : ℝ), ENNReal.ofReal (μ.rnDeriv MeasureTheory.volume x).toReal.negMulLog) - ↑(∫⁻ (x : ℝ), ENNReal.ofReal (-(μ.rnDeriv MeasureTheory.volume x).toReal.negMulLog)) else ⊥
      Used by
        noncomputable def

        InformationTheory.Shannon.entropyPowerExt

        source
        (μ : MeasureTheory.Measure ℝ) :
        ENNReal

        The extended entropy power valued in ℝ≥0∞: 0 for a singular measure or h = −∞, ∞ for h = +∞, and ofReal (exp (2h)) for a finite a.c. entropy, via the non-branching EReal.exp (2 * differentialEntropyExt μ).

        Equations
        Instances For
          Used by
            theorem

            InformationTheory.Shannon.differentialEntropyExt_of_ac

            source
            {μ : MeasureTheory.Measure ℝ} (h : μ.AbsolutelyContinuous MeasureTheory.volume) :
            differentialEntropyExt μ = ↑(∫⁻ (x : ℝ), ENNReal.ofReal (μ.rnDeriv MeasureTheory.volume x).toReal.negMulLog) - ↑(∫⁻ (x : ℝ), ENNReal.ofReal (-(μ.rnDeriv MeasureTheory.volume x).toReal.negMulLog))

            The a.c.-branch value of differentialEntropyExt as the EReal difference of positive and negative parts. @audit:ok

            Used by
              theorem

              InformationTheory.Shannon.differentialEntropyExt_of_ac_integrable

              source
              {μ : MeasureTheory.Measure ℝ} (hac : μ.AbsolutelyContinuous MeasureTheory.volume) (hint : MeasureTheory.Integrable (fun (x : ℝ) => (μ.rnDeriv MeasureTheory.volume x).toReal.negMulLog) MeasureTheory.volume) :
              differentialEntropyExt μ = ↑(differentialEntropy μ)

              When μ ≪ volume and negMulLog ∘ density is integrable (finite differential entropy), differentialEntropyExt equals the workhorse differentialEntropy. @audit:ok

              Used by
                theorem

                InformationTheory.Shannon.differentialEntropyExt_singular

                source
                {μ : MeasureTheory.Measure ℝ} (h : ¬μ.AbsolutelyContinuous MeasureTheory.volume) :
                differentialEntropyExt μ = ⊥

                The singular-branch value of differentialEntropyExt is ⊥. @audit:ok

                Used by
                  theorem

                  InformationTheory.Shannon.entropyPowerExt_of_ac_integrable

                  source
                  {μ : MeasureTheory.Measure ℝ} (hac : μ.AbsolutelyContinuous MeasureTheory.volume) (hint : MeasureTheory.Integrable (fun (x : ℝ) => (μ.rnDeriv MeasureTheory.volume x).toReal.negMulLog) MeasureTheory.volume) :
                  entropyPowerExt μ = ENNReal.ofReal (Real.exp (2 * differentialEntropy μ))

                  The finite a.c.-branch value of entropyPowerExt is ENNReal.ofReal (exp (2h)). @audit:ok

                  Used by
                    theorem

                    InformationTheory.Shannon.entropyPowerExt_eq_top_of_diffEntExt_top

                    source
                    {μ : MeasureTheory.Measure ℝ} (h : differentialEntropyExt μ = ⊤) :
                    entropyPowerExt μ = ⊤

                    If differentialEntropyExt μ = ⊤ (i.e. h = +∞) then entropyPowerExt μ = ⊤. @audit:ok

                    Used by
                      theorem

                      InformationTheory.Shannon.entropyPowerExt_singular

                      source
                      {μ : MeasureTheory.Measure ℝ} (h : ¬μ.AbsolutelyContinuous MeasureTheory.volume) :
                      entropyPowerExt μ = 0

                      The singular-branch (and h = −∞) value of entropyPowerExt is 0. @audit:ok

                      Used by
                        theorem

                        InformationTheory.Shannon.entropyPowerExt_dirac

                        source
                        (m : ℝ) :
                        entropyPowerExt (MeasureTheory.Measure.dirac m) = 0

                        The entropy power of a Dirac measure is 0 (where the real-valued entropyPower degenerates to 1). @audit:ok

                        Used by
                          theorem

                          InformationTheory.Shannon.integrable_negMulLog_gaussianReal_density

                          source
                          (m : ℝ) {v : NNReal} (hv : v ≠ 0) :
                          MeasureTheory.Integrable (fun (x : ℝ) => ((ProbabilityTheory.gaussianReal m v).rnDeriv MeasureTheory.volume x).toReal.negMulLog) MeasureTheory.volume

                          negMulLog of a Gaussian density is volume-integrable (finite differential entropy), via the a.e. identity negMulLog(gaussianPDF) = gaussianPDF · c₁ + gaussianPDF · (x-m)²/(2v) with the density integrable and the second moment finite. @audit:ok

                          Used by
                            theorem

                            InformationTheory.Shannon.entropyPowerExt_gaussianReal

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

                            The entropy power of a Gaussian (v ≠ 0, a.c.) is 2πe·v, hence does not collapse to 0. @audit:ok

                            Used by