InformationTheory

InformationTheory.Shannon.EPI.Conv.Density

source

Imports 6

Convolution density apparatus #

p_Z(z) = ∫ x, p_X(x) · p_Y(z - x) ∂volume (sum density of independent X, Y), its pointwise differentiability, and the logDeriv p_Z representation. This is the common foundational helper for the density-route Stam and de Bruijn arguments.

Implementation notes #

The 6 Mathlib HasCompactSupport.*_convolution_* lemmas require the smooth factor to have compact support, which the Gaussian heat kernel does not have. We go through hasDerivAt_integral_of_dominated_loc_of_deriv_le (Mathlib/Analysis/Calculus/ParametricIntegral.lean): differentiation under the integral sign, with the Gaussian-tail domination supplied as regularity preconditions.

convDensityAdd is defined as a Bochner ∫ (not ⋆ₗ / ⋆[L,μ]), matching the conclusion shape of the parametric-integral gateway HasDerivAt (fun z ↦ ∫ a, F z a ∂μ) (∫ a, F' x₀ a ∂μ) x₀.

noncomputable def

InformationTheory.Shannon.EPIConvDensity.convDensityAdd

source
(pX pY : ℝ → ℝ) :
ℝ → ℝ

Convolution density (sum density of independent X, Y): p_Z(z) = ∫ x, p_X(x) · p_Y(z - x) ∂volume. Bochner-∫ form to match the hasDerivAt_integral_of_dominated_loc_of_deriv_le conclusion shape.

Equations
Instances For
    Used by
      theorem

      InformationTheory.Shannon.EPIConvDensity.convDensityAdd_comm

      source
      (pX pY : ℝ → ℝ) :
      convDensityAdd pX pY = convDensityAdd pY pX

      The convolution density is commutative: pX ⋆ pY = pY ⋆ pX. Genuine fact via the reflection substitution x ↦ z - x (volume-preserving).

      Used by
        noncomputable def

        InformationTheory.Shannon.EPIConvDensity.convDensityAddDeriv

        source
        (pX pY : ℝ → ℝ) :
        ℝ → ℝ → ℝ

        The z-partial-derivative integrand: ∂_z (p_X x · p_Y (z - x)) = p_X x · p_Y' (z - x).

        Equations
        Instances For
          Used by
            theorem

            InformationTheory.Shannon.EPIConvDensity.convDensityAdd_hasDerivAt

            source
            (pX pY : ℝ → ℝ) (z₀ : ℝ) {s : Set ℝ} {bound : ℝ → ℝ} (hs : s ∈ nhds z₀) (hF_meas : ∀ᶠ (z : ℝ) in nhds z₀, MeasureTheory.AEStronglyMeasurable (fun (x : ℝ) => pX x * pY (z - x)) MeasureTheory.volume) (hF_int : MeasureTheory.Integrable (fun (x : ℝ) => pX x * pY (z₀ - x)) MeasureTheory.volume) (hF'_meas : MeasureTheory.AEStronglyMeasurable (fun (x : ℝ) => convDensityAddDeriv pX pY z₀ x) MeasureTheory.volume) (h_bound : ∀ᵐ (x : ℝ), ∀ z ∈ s, ‖convDensityAddDeriv pX pY z x‖ ≤ bound x) (bound_integrable : MeasureTheory.Integrable bound MeasureTheory.volume) (h_diff : ∀ᵐ (x : ℝ), ∀ z ∈ s, HasDerivAt (fun (z : ℝ) => pX x * pY (z - x)) (convDensityAddDeriv pX pY z x) z) :
            HasDerivAt (convDensityAdd pX pY) (∫ (x : ℝ), convDensityAddDeriv pX pY z₀ x) z₀

            Under Gaussian-tail / integrability regularity preconditions, convDensityAdd pX pY is differentiable at z₀ with derivative ∫ x, p_X x · p_Y' (z₀ - x).

            All hypotheses are regularity preconditions (integrability, ae-measurability, the domination bound, pointwise differentiability of the integrand), pinned in the shape hasDerivAt_integral_of_dominated_loc_of_deriv_le consumes. The differentiability of convDensityAdd is derived, not assumed.

            • s is a neighborhood of z₀.
            • bound is the integrable Gaussian-tail dominating function. @audit:ok
            Used by
              theorem

              InformationTheory.Shannon.EPIConvDensity.convDensityAdd_logDeriv

              source
              (pX pY : ℝ → ℝ) (z₀ : ℝ) {s : Set ℝ} {bound : ℝ → ℝ} (hs : s ∈ nhds z₀) (hF_meas : ∀ᶠ (z : ℝ) in nhds z₀, MeasureTheory.AEStronglyMeasurable (fun (x : ℝ) => pX x * pY (z - x)) MeasureTheory.volume) (hF_int : MeasureTheory.Integrable (fun (x : ℝ) => pX x * pY (z₀ - x)) MeasureTheory.volume) (hF'_meas : MeasureTheory.AEStronglyMeasurable (fun (x : ℝ) => convDensityAddDeriv pX pY z₀ x) MeasureTheory.volume) (h_bound : ∀ᵐ (x : ℝ), ∀ z ∈ s, ‖convDensityAddDeriv pX pY z x‖ ≤ bound x) (bound_integrable : MeasureTheory.Integrable bound MeasureTheory.volume) (h_diff : ∀ᵐ (x : ℝ), ∀ z ∈ s, HasDerivAt (fun (z : ℝ) => pX x * pY (z - x)) (convDensityAddDeriv pX pY z x) z) :
              logDeriv (convDensityAdd pX pY) z₀ = (∫ (x : ℝ), convDensityAddDeriv pX pY z₀ x) / convDensityAdd pX pY z₀

              logDeriv p_Z representation at z₀ (score of the convolution density): logDeriv (convDensityAdd pX pY) z₀ = (∫ x, p_X x · p_Y'(z₀ - x)) / p_Z(z₀). This is the Blachman / Fisher connection point. @audit:ok

              Used by
                theorem

                InformationTheory.Shannon.EPIConvDensity.convDensity_add_differentiable

                source
                (pX pY : ℝ → ℝ) (z₀ : ℝ) {s : Set ℝ} {bound : ℝ → ℝ} (hs : s ∈ nhds z₀) (hF_meas : ∀ᶠ (z : ℝ) in nhds z₀, MeasureTheory.AEStronglyMeasurable (fun (x : ℝ) => pX x * pY (z - x)) MeasureTheory.volume) (hF_int : MeasureTheory.Integrable (fun (x : ℝ) => pX x * pY (z₀ - x)) MeasureTheory.volume) (hF'_meas : MeasureTheory.AEStronglyMeasurable (fun (x : ℝ) => convDensityAddDeriv pX pY z₀ x) MeasureTheory.volume) (h_bound : ∀ᵐ (x : ℝ), ∀ z ∈ s, ‖convDensityAddDeriv pX pY z x‖ ≤ bound x) (bound_integrable : MeasureTheory.Integrable bound MeasureTheory.volume) (h_diff : ∀ᵐ (x : ℝ), ∀ z ∈ s, HasDerivAt (fun (z : ℝ) => pX x * pY (z - x)) (convDensityAddDeriv pX pY z x) z) :
                HasDerivAt (convDensityAdd pX pY) (∫ (x : ℝ), convDensityAddDeriv pX pY z₀ x) z₀ ∧ logDeriv (convDensityAdd pX pY) z₀ = (∫ (x : ℝ), convDensityAddDeriv pX pY z₀ x) / convDensityAdd pX pY z₀

                The convolution density is differentiable at z₀, with the logDeriv (score) given by the score-of-convolution formula. Bundles the two atoms above for the downstream Blachman and de Bruijn arguments. The public gateway for those consumers. @audit:ok

                Used by

                  Discharging the gateway hypotheses from IsRegularDensityV2 #

                  convDensityAdd_hasDerivAt_of_regular: the wrapper that supplies all parametric-integral regularity hypotheses from the density preconditions IsRegularDensityV2 fX/fY plus three genuine regularity preconditions:

                  • hX_int : Integrable fX — fX is a probability density.
                  • hY_bdd : fY is bounded (the Gaussian PDF is, since exp(-x²) is bounded).
                  • hY'_bdd : deriv fY is bounded (Gaussian deriv = -(x-m)/v · pdf, polynomial × Gaussian decay → bounded).

                  These are per-factor regularity preconditions on fX/fY individually, not on the convolution; the differentiability of convDensityAdd is derived via the gateway, not assumed. The Gaussian instance satisfies all three.

                  theorem

                  InformationTheory.Shannon.EPIConvDensity.convDensityAdd_hasDerivAt_of_regular

                  source
                  (fX fY : ℝ → ℝ) (z₀ : ℝ) (hregX : FisherInfo.IsRegularDensityV2 fX) (hregY : FisherInfo.IsRegularDensityV2 fY) (hX_int : MeasureTheory.Integrable fX MeasureTheory.volume) (hY_bdd : ∃ (M : ℝ), ∀ (w : ℝ), |fY w| ≤ M) (hY'_bdd : ∃ (M : ℝ), ∀ (w : ℝ), |deriv fY w| ≤ M) :
                  HasDerivAt (convDensityAdd fX fY) (∫ (x : ℝ), convDensityAddDeriv fX fY z₀ x) z₀

                  Discharges the gateway hypotheses of convDensityAdd_hasDerivAt from IsRegularDensityV2 fX/fY plus per-factor boundedness/integrability preconditions. @audit:ok

                  Used by