InformationTheory

InformationTheory.Shannon.EPI.Conv.DensityRegular

source

Imports 7

IsRegularDensityV2 (convDensityAdd pX g_t) producer — EPI A-5 precondition (1) #

For an arbitrary probability density pX (nonnegativity + measurability + integrability + positive mass) and the Gaussian heat kernel g_t = gaussianPDFReal 0 ⟨t, _⟩ (t > 0), the convolution density convDensityAdd pX g_t is a regular density in the V2 sense (InformationTheory.Shannon.FisherInfo.IsRegularDensityV2).

All six fields are discharged from existing @audit:ok infrastructure:

  • diff — convDensityAdd_differentiable_of_integrable_smoothKernel (gateway), differentiation carried by the smooth Gaussian kernel.
  • pos — convDensityAdd_pos (positive mass ⇒ strictly positive convolution).
  • integrable_deriv — deriv f = convDensityAdd pX (deriv g_t) (gateway HasDerivAt .deriv) + convKernel_envelope_integrable' (Tonelli envelope).
  • integral_deriv_eq_zero — Fubini swap of the same envelope + ∫ deriv g_t = 0.
  • tail_bot / tail_top — convolution with the Gaussian kernel vanishes at ±∞.

All hypotheses on pX are regularity preconditions (no load-bearing core).

theorem

InformationTheory.Shannon.EPIConvDensityRegular.gaussianPDFReal_abs_le

source
(v : NNReal) (w : ℝ) :
|ProbabilityTheory.gaussianPDFReal 0 v w| ≤ (√(2 * Real.pi * ↑v))⁻¹

Global sup bound of gaussianPDFReal 0 v: g(x) ≤ (√(2πv))⁻¹ since exp(-x²/(2v)) ≤ 1. @audit:ok

Used by
    theorem

    InformationTheory.Shannon.EPIConvDensityRegular.deriv_gaussianPDFReal_abs_le

    source
    {v : NNReal} (hv : v ≠ 0) :
    ∃ (M : ℝ), ∀ (w : ℝ), |deriv (ProbabilityTheory.gaussianPDFReal 0 v) w| ≤ M

    Global sup bound of deriv (gaussianPDFReal 0 v). With deriv g v x = -x/v · g v x and |x|·exp(-x²/(2v)) ≤ √(v)·exp(-1/2)·…, the derivative is globally bounded. @audit:ok

    Used by
      theorem

      InformationTheory.Shannon.EPIConvDensityRegular.deriv_convDensityAdd_eq

      source
      {pX : ℝ → ℝ} {t : ℝ} (ht : 0 < t) (hpX_int : MeasureTheory.Integrable pX MeasureTheory.volume) :
      deriv (EPIConvDensity.convDensityAdd pX (ProbabilityTheory.gaussianPDFReal 0 ⟨t, ⋯⟩)) = EPIConvDensity.convDensityAdd pX (deriv (ProbabilityTheory.gaussianPDFReal 0 ⟨t, ⋯⟩))

      The derivative of convDensityAdd pX g_t is the convolution of pX against deriv g_t: deriv (convDensityAdd pX g_t) z = convDensityAdd pX (deriv g_t) z. @audit:ok

      Used by
        theorem

        InformationTheory.Shannon.EPIConvDensityRegular.tendsto_convDensityAdd_gaussian_zero

        source
        {pX : ℝ → ℝ} {v : NNReal} (hv : v ≠ 0) (hpX_nn : ∀ (x : ℝ), 0 ≤ pX x) (hpX_int : MeasureTheory.Integrable pX MeasureTheory.volume) {l : Filter ℝ} [l.IsCountablyGenerated] (hl : Filter.Tendsto (fun (z : ℝ) => z) l Filter.atTop ∨ Filter.Tendsto (fun (z : ℝ) => z) l Filter.atBot) :
        Filter.Tendsto (EPIConvDensity.convDensityAdd pX (ProbabilityTheory.gaussianPDFReal 0 v)) l (nhds 0)

        Convolution-with-Gaussian tail vanishing (filter-generic). For an integrable nonnegative pX and the Gaussian kernel g = gaussianPDFReal 0 v that is globally bounded by M and vanishes (after the z - x shift) along the filter l, the convolution convDensityAdd pX g vanishes along l. Dominated convergence with bound pX · M. @audit:ok

        Used by
          theorem

          InformationTheory.Shannon.EPIConvDensityRegular.isRegularDensityV2_convDensityAdd_gaussian

          source
          (pX : ℝ → ℝ) {t : ℝ} (ht : 0 < t) (hpX_nn : ∀ (x : ℝ), 0 ≤ pX x) (hpX_meas : Measurable pX) (hpX_int : MeasureTheory.Integrable pX MeasureTheory.volume) (hpX_mass : 0 < ∫ (x : ℝ), pX x) :
          FisherInfo.IsRegularDensityV2 (EPIConvDensity.convDensityAdd pX (ProbabilityTheory.gaussianPDFReal 0 ⟨t, ⋯⟩))

          A-5 precondition (1) producer. convDensityAdd pX g_t is a regular V2 density for t > 0 and any probability density pX. @audit:ok

          Used by
            theorem

            InformationTheory.Shannon.EPIConvDensityRegular.fisherInfoOfDensityReal_convDensityAdd_pos

            source
            (pX : ℝ → ℝ) {t : ℝ} (ht : 0 < t) (hpX_nn : ∀ (x : ℝ), 0 ≤ pX x) (hpX_meas : Measurable pX) (hpX_int : MeasureTheory.Integrable pX MeasureTheory.volume) (hpX_norm : ∫ (x : ℝ), pX x = 1) :
            0 < FisherInfo.fisherInfoOfDensityReal (EPIConvDensity.convDensityAdd pX (ProbabilityTheory.gaussianPDFReal 0 ⟨t, ⋯⟩))

            Fisher non-degeneracy for a conv-with-Gaussian density (Gap 1 closure). 0 < J(convDensityAdd pX g_t) for t > 0 and any normalized probability density pX (nonneg / measurable / integrable / ∫ pX = 1).

            Route: J(f).toReal > 0 requires J(f) ≠ 0 and J(f) < ⊤.

            • Finiteness: gaussianConv_fisher_le_inv_var gives J(f) ≤ 1/t < ⊤.
            • Non-vanishing: if J(f) = 0 then the lintegrand ofReal((logDeriv f)²)·ofReal(f) vanishes a.e.; since f > 0 everywhere (convDensityAdd_pos), logDeriv f = 0 a.e., hence deriv f = 0 a.e. But deriv f = convDensityAdd pX (deriv g) is continuous (BddAbove.continuous_convolution_right_of_integrable), so it is 0 everywhere, making f constant (is_const_of_deriv_eq_zero). A constant contradicts the tail_bot field (f → 0 at -∞) together with f 0 > 0.

            All pX hypotheses are regularity preconditions (probability-density normalization ∫ pX = 1); the Fisher positivity conclusion is derived, not assumed.

            Used by