InformationTheory

InformationTheory.Shannon.FisherConvBound

source

Imports 10

Stam convolution Fisher information bound J(pX ∗ g_s) ≤ 1/s #

For any probability density pX and Gaussian kernel g_s of variance s, the Fisher information of the convolution pX ∗ g_s satisfies J(pX ∗ g_s) ≤ 1/s.

Main statements #

Implementation notes #

The proof follows a pointwise Cauchy-Schwarz route: the derivative formula convDensityAdd_deriv1_gaussian_eq gives (deriv p_s x) as an integral, Hölder's inequality with p = q = 2 bounds (logDeriv p_s x)² · p_s x pointwise, and Tonelli's theorem plus the Gaussian second moment ∫ u² g_s u du = s closes the bound.

theorem

InformationTheory.Shannon.FisherInfo.integral_sq_mul_gaussianPDFReal

source
{s : ℝ} (hs : 0 < s) :
∫ (u : ℝ), u ^ 2 * ProbabilityTheory.gaussianPDFReal 0 ⟨s, ⋯⟩ u = s

∫ u, u ^ 2 * gaussianPDFReal 0 ⟨s, _⟩ u ∂volume = s. @audit:ok

Used by
    theorem

    InformationTheory.Shannon.FisherInfo.integrable_sq_mul_gaussianPDFReal

    source
    {s : ℝ} (hs : 0 < s) :
    MeasureTheory.Integrable (fun (u : ℝ) => u ^ 2 * ProbabilityTheory.gaussianPDFReal 0 ⟨s, ⋯⟩ u) MeasureTheory.volume

    u ↦ u ^ 2 * gaussianPDFReal 0 ⟨s, _⟩ u is integrable over volume. @audit:ok

    Used by
      theorem

      InformationTheory.Shannon.FisherInfo.convSecondMoment_integrand_integrable

      source
      (pX : ℝ → ℝ) (_hpX_meas : Measurable pX) (hpX_int : MeasureTheory.Integrable pX MeasureTheory.volume) {s : ℝ} (hs : 0 < s) (x : ℝ) :
      MeasureTheory.Integrable (fun (y : ℝ) => (x - y) ^ 2 * (pX y * ProbabilityTheory.gaussianPDFReal 0 ⟨s, ⋯⟩ (x - y))) MeasureTheory.volume

      y ↦ (x - y) ^ 2 * (pX y * g_s(x - y)) is integrable over volume for each x. @audit:ok

      Used by
        theorem

        InformationTheory.Shannon.FisherInfo.convScore_sq_le_pointwise

        source
        (pX : ℝ → ℝ) (hpX_nn : ∀ (x : ℝ), 0 ≤ pX x) (hpX_meas : Measurable pX) (hpX_int : MeasureTheory.Integrable pX MeasureTheory.volume) {s : ℝ} (hs : 0 < s) (x : ℝ) :
        (∫ (y : ℝ), pX y * (x - y) * ProbabilityTheory.gaussianPDFReal 0 ⟨s, ⋯⟩ (x - y)) ^ 2 ≤ EPIConvDensity.convDensityAdd pX (ProbabilityTheory.gaussianPDFReal 0 ⟨s, ⋯⟩) x * ∫ (y : ℝ), (x - y) ^ 2 * (pX y * ProbabilityTheory.gaussianPDFReal 0 ⟨s, ⋯⟩ (x - y))

        Pointwise Cauchy-Schwarz: (∫ pX y (x-y) g_s(x-y))² ≤ p_s(x) · ∫ pX y (x-y)² g_s(x-y). @audit:ok

        Used by
          theorem

          InformationTheory.Shannon.FisherInfo.convDensityAdd_deriv_eq

          source
          (pX : ℝ → ℝ) (hpX_meas : Measurable pX) (hpX_int : MeasureTheory.Integrable pX MeasureTheory.volume) {s : ℝ} (hs : 0 < s) :
          deriv (EPIConvDensity.convDensityAdd pX (ProbabilityTheory.gaussianPDFReal 0 ⟨s, ⋯⟩)) = fun (ζ : ℝ) => ∫ (y : ℝ), pX y * (ProbabilityTheory.gaussianPDFReal 0 ⟨s, ⋯⟩ (ζ - y) * -((ζ - y) / s))

          deriv (convDensityAdd pX g_s) x = ∫ y, pX y * g_s(x-y) * (-(x-y)/s) ∂volume. @audit:ok

          Used by
            theorem

            InformationTheory.Shannon.FisherInfo.convLogDeriv_sq_mul_le

            source
            (pX : ℝ → ℝ) (hpX_nn : ∀ (x : ℝ), 0 ≤ pX x) (hpX_meas : Measurable pX) (hpX_int : MeasureTheory.Integrable pX MeasureTheory.volume) (hpX_mass : ∫ (y : ℝ), pX y = 1) {s : ℝ} (hs : 0 < s) (x : ℝ) :
            logDeriv (EPIConvDensity.convDensityAdd pX (ProbabilityTheory.gaussianPDFReal 0 ⟨s, ⋯⟩)) x ^ 2 * EPIConvDensity.convDensityAdd pX (ProbabilityTheory.gaussianPDFReal 0 ⟨s, ⋯⟩) x ≤ 1 / s ^ 2 * ∫ (y : ℝ), (x - y) ^ 2 * (pX y * ProbabilityTheory.gaussianPDFReal 0 ⟨s, ⋯⟩ (x - y))

            (logDeriv p_s x) ^ 2 * p_s x ≤ (1/s²) * ∫ (x-y)² * (pX y * g_s(x-y)) ∂volume. @audit:ok

            Used by
              theorem

              InformationTheory.Shannon.FisherInfo.gaussianConv_fisher_le_inv_var

              source
              (pX : ℝ → ℝ) (hpX_nn : ∀ (x : ℝ), 0 ≤ pX x) (hpX_meas : Measurable pX) (hpX_int : MeasureTheory.Integrable pX MeasureTheory.volume) (hpX_mass : ∫ (y : ℝ), pX y = 1) {s : ℝ} (hs : 0 < s) :
              fisherInfoOfDensity (EPIConvDensity.convDensityAdd pX (ProbabilityTheory.gaussianPDFReal 0 ⟨s, ⋯⟩)) ≤ ENNReal.ofReal (1 / s)

              Stam convolution Fisher information bound: J(pX ∗ g_s) ≤ 1/s for any probability density pX and Gaussian kernel g_s of variance s > 0. @audit:ok

              Used by