InformationTheory.Shannon.EPI.Conv.DensitySecondDeriv

Imports 4

Convolution density — spatial 2nd derivative identification (STEP D bridge) #

The genuine spatial-second-derivative closed form of the heat-flow convolution density p_s(z) = ∫ y, pX y · g_s(z - y) ∂volume (g_s = gaussianPDFReal 0 ⟨s,_⟩, variance s):

deriv (deriv (convDensityAdd pX g_s)) z
  = ∫ y, pX y · (g_s(z - y) · ((z - y)²/s² - 1/s)) ∂volume.

This is the upstream block of GAP② (convDensityAdd_deriv2_poly_moment_majorant): once the second derivative is identified as this integral, GAP② majorizes it by ∫ pX y · g_s(z-y) · |(z-y)²/s² - 1/s| dy via a triangle bound.

Mathlib-shape-driven #

The conclusion is an equality (not a HasDerivAt) so that the triangle bound in GAP② can rw it directly. We reach it by applying the parametric-integral gateway hasDerivAt_integral_of_dominated_loc_of_deriv_le twice (1st then 2nd spatial derivative), mirroring the genuine STEP D code in heatFlow_density_heat_equation (FisherInfo/DeBruijnPerTime.lean). The Gaussian-tail domination of the polynomial×Gaussian integrand is supplied as honest regularity preconditions in the exact shape the gateway consumes — NOT a load-bearing bundling of the second-derivative conclusion, which is derived.

The per-y kernel derivative closed forms are the @audit:ok atoms heatFlow_density_heat_equation_kernel_x_deriv1 / _x_deriv2 (FisherInfo/DeBruijnPerTime.lean), and heatFlow_density_heat_equation_kernel_eq bridges them to gaussianPDFReal.

theorem

InformationTheory.Shannon.EPIConvDensitySecondDeriv.convDensityAdd_deriv1_gaussian_eq

source

(pX : ℝ → ℝ) {s : ℝ} (hs : 0 < s) (bound1 : ℝ → ℝ) (hbound1_int : MeasureTheory.Integrable bound1 MeasureTheory.volume) (hF1_meas : ∀ (ξ : ℝ), MeasureTheory.AEStronglyMeasurable (fun (y : ℝ) => pX y * FisherInfo.heatFlow_density_heat_equation_kernel s (ξ - y)) MeasureTheory.volume) (hF1_int : ∀ (ξ : ℝ), MeasureTheory.Integrable (fun (y : ℝ) => pX y * FisherInfo.heatFlow_density_heat_equation_kernel s (ξ - y)) MeasureTheory.volume) (hF1'_meas : ∀ (ξ : ℝ), MeasureTheory.AEStronglyMeasurable (fun (y : ℝ) => pX y * (FisherInfo.heatFlow_density_heat_equation_kernel s (ξ - y) * -((ξ - y) / s))) MeasureTheory.volume) (hb1 : ∀ᵐ (y : ℝ), ∀ ξ ∈ Set.univ, ‖pX y * (FisherInfo.heatFlow_density_heat_equation_kernel s (ξ - y) * -((ξ - y) / s))‖ ≤ bound1 y) :

deriv (EPIConvDensity.convDensityAdd pX (ProbabilityTheory.gaussianPDFReal 0 ⟨s, ⋯⟩)) = fun (ζ : ℝ) => ∫ (y : ℝ), pX y * (ProbabilityTheory.gaussianPDFReal 0 ⟨s, ⋯⟩ (ζ - y) * -((ζ - y) / s))

Spatial first-derivative identification (as a function). Under Gaussian-tail domination preconditions, the spatial first derivative of the convolution density is the integral of pX y · ∂_z g_s(z-y) = pX y · g_s(z-y)·(-(z-y)/s):

deriv (convDensityAdd pX g_s) = fun ζ => ∫ y, pX y · (g_s(ζ-y) · (-(ζ-y)/s)) ∂volume.

All hyps are integrand-level regularity (per-y integrability / ae-measurability / Gaussian-tail norm bound), 1:1 with the gateway lemma's argument group. NOT load-bearing: the derivative is derived via the gateway, not assumed.

Genuine, sorryAx-free (#print axioms = [propext, Classical.choice, Quot.sound]), 0 sorry / 0 residual.

Used by

theorem

InformationTheory.Shannon.EPIConvDensitySecondDeriv.convDensityAdd_deriv2_eq_gaussian

source

(pX : ℝ → ℝ) (_hpX_nn : ∀ (x : ℝ), 0 ≤ pX x) (_hpX_int : MeasureTheory.Integrable pX MeasureTheory.volume) {s : ℝ} (hs : 0 < s) (z : ℝ) (bound1 : ℝ → ℝ) (hbound1_int : MeasureTheory.Integrable bound1 MeasureTheory.volume) (hF1_meas : ∀ (ξ : ℝ), MeasureTheory.AEStronglyMeasurable (fun (y : ℝ) => pX y * FisherInfo.heatFlow_density_heat_equation_kernel s (ξ - y)) MeasureTheory.volume) (hF1_int : ∀ (ξ : ℝ), MeasureTheory.Integrable (fun (y : ℝ) => pX y * FisherInfo.heatFlow_density_heat_equation_kernel s (ξ - y)) MeasureTheory.volume) (hF1'_meas : ∀ (ξ : ℝ), MeasureTheory.AEStronglyMeasurable (fun (y : ℝ) => pX y * (FisherInfo.heatFlow_density_heat_equation_kernel s (ξ - y) * -((ξ - y) / s))) MeasureTheory.volume) (hb1 : ∀ᵐ (y : ℝ), ∀ ξ ∈ Set.univ, ‖pX y * (FisherInfo.heatFlow_density_heat_equation_kernel s (ξ - y) * -((ξ - y) / s))‖ ≤ bound1 y) (bound2 : ℝ → ℝ) (hbound2_int : MeasureTheory.Integrable bound2 MeasureTheory.volume) (hF2_int : MeasureTheory.Integrable (fun (y : ℝ) => pX y * (FisherInfo.heatFlow_density_heat_equation_kernel s (z - y) * -((z - y) / s))) MeasureTheory.volume) (hF2'_meas : MeasureTheory.AEStronglyMeasurable (fun (y : ℝ) => pX y * (FisherInfo.heatFlow_density_heat_equation_kernel s (z - y) * ((z - y) ^ 2 / s ^ 2 - 1 / s))) MeasureTheory.volume) (hb2 : ∀ᵐ (y : ℝ), ∀ ξ ∈ Set.univ, ‖pX y * (FisherInfo.heatFlow_density_heat_equation_kernel s (ξ - y) * ((ξ - y) ^ 2 / s ^ 2 - 1 / s))‖ ≤ bound2 y) :

deriv (deriv (EPIConvDensity.convDensityAdd pX (ProbabilityTheory.gaussianPDFReal 0 ⟨s, ⋯⟩))) z = ∫ (y : ℝ), pX y * (ProbabilityTheory.gaussianPDFReal 0 ⟨s, ⋯⟩ (z - y) * ((z - y) ^ 2 / s ^ 2 - 1 / s))

Spatial second-derivative closed form (STEP D bridge). Under Gaussian-tail domination preconditions, the spatial second derivative of the heat-flow convolution density is the integral of pX y · ∂²_z g_s(z-y):

deriv (deriv (convDensityAdd pX g_s)) z
  = ∫ y, pX y · (g_s(z-y) · ((z-y)²/s² - 1/s)) ∂volume.

hpX_nn / hpX_int are regularity preconditions on pX (carried for downstream GAP② consumers; not used by this pure differentiation identity). The bound1 / bound2 groups are Gaussian-tail domination preconditions in the exact gateway shape (integrand-level, NOT load-bearing). The closed form is derived via two gateway applications + the @audit:ok kernel derivative atoms _x_deriv1 / _x_deriv2. @audit:ok

Used by