InformationTheory

InformationTheory.Shannon.EPI.Conv.DensityGaussianGateway

source

Imports 3

Convolution density gateway — pX integrable-only + Gaussian-kernel-smooth variant #

convDensityAdd_hasDerivAt_of_integrable_smoothKernel is the fX-integrable-only variant of convDensityAdd_hasDerivAt_of_regular (InformationTheory/Shannon/EPI/Conv/Density.lean). The smoothness regularity on fX is dropped: differentiation is carried entirely by the Gaussian kernel fY (hregY : IsRegularDensityV2 fY + bounded fY / deriv fY). fX only needs Integrable fX volume, used for aestronglyMeasurable (via Integrable.aestronglyMeasurable) and the bound integrability.

This is the common foundation for the A-5 producer group: an arbitrary input density pX (no smoothness) convolved with the Gaussian heat kernel.

All hypotheses are honest regularity preconditions (integrability / boundedness); the differentiability conclusion is derived via the @audit:ok gateway convDensityAdd_hasDerivAt, NOT assumed (no load-bearing bundling).

theorem

InformationTheory.Shannon.EPIConvDensityGaussianGateway.convDensityAdd_hasDerivAt_of_integrable_smoothKernel

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

pX integrable-only variant of convDensityAdd_hasDerivAt_of_regular. fX smoothness is dropped; the derivative is carried by the Gaussian kernel fY. fX enters only through Integrable fX volume (ae-measurability + bound integrability). All hyps are regularity preconditions; the differentiability is derived via the gateway, not assumed. @audit:ok

Used by
    theorem

    InformationTheory.Shannon.EPIConvDensityGaussianGateway.convDensityAdd_differentiable_of_integrable_smoothKernel

    source
    (fX fY : ℝ → ℝ) (hX_int : MeasureTheory.Integrable fX MeasureTheory.volume) (hregY : FisherInfo.IsRegularDensityV2 fY) (hY_bdd : ∃ (M : ℝ), ∀ (w : ℝ), |fY w| ≤ M) (hY'_bdd : ∃ (M : ℝ), ∀ (w : ℝ), |deriv fY w| ≤ M) :
    Differentiable ℝ (EPIConvDensity.convDensityAdd fX fY)

    Differentiable corollary of convDensityAdd_hasDerivAt_of_integrable_smoothKernel, for the diff field of downstream regular-density witnesses. @audit:ok

    Used by