InformationTheory.Shannon.FisherInfo.DeBruijnAssembly.Derivatives

Imports 7

theorem

InformationTheory.Shannon.FisherInfo.convDensityAdd_fisher_integrable

(pX : ℝ → ℝ) (hpX_nn : ∀ (x : ℝ), 0 ≤ pX x) (hpX_meas : Measurable pX) (hpX_int : MeasureTheory.Integrable pX MeasureTheory.volume) (hpX_mass : ∫ (y : ℝ), pX y = 1) {t : ℝ} (ht : 0 < t) :

MeasureTheory.Integrable (fun (x : ℝ) => logDeriv (EPIConvDensity.convDensityAdd pX (ProbabilityTheory.gaussianPDFReal 0 ⟨t, ⋯⟩)) x ^ 2 * EPIConvDensity.convDensityAdd pX (ProbabilityTheory.gaussianPDFReal 0 ⟨t, ⋯⟩) x) MeasureTheory.volume

The square-score density (logDeriv p_t)² · p_t of the convolution density p_t = convDensityAdd pX g_t is Lebesgue-integrable, where g_t = gaussianPDFReal 0 ⟨t, _⟩. The Fisher information J(X + √t · Z) = ∫ (logDeriv p_t)² · p_t is bounded by 1 / t (gaussianConv_fisher_le_inv_var) and hence finite, so the integrand is integrable.

@audit:ok

Used by

theorem

InformationTheory.Shannon.FisherInfo.convDensityAdd_hasDerivAt_self

source

(pX : ℝ → ℝ) (_hpX_nn : ∀ (x : ℝ), 0 ≤ pX x) (hpX_meas : Measurable pX) (hpX_int : MeasureTheory.Integrable pX MeasureTheory.volume) {t : ℝ} (ht : 0 < t) (x : ℝ) :

HasDerivAt (EPIConvDensity.convDensityAdd pX (ProbabilityTheory.gaussianPDFReal 0 ⟨t, ⋯⟩)) (deriv (EPIConvDensity.convDensityAdd pX (ProbabilityTheory.gaussianPDFReal 0 ⟨t, ⋯⟩)) x) x

HasDerivAt p_t (deriv p_t x) x for p_t = convDensityAdd pX g_t at every x (t > 0): the spatial first derivative of the heat-flow convolution density exists, reconstructed via the parametric-integral gateway hasDerivAt_integral_of_dominated_loc_of_deriv_le with the domination supplied by kernel_x_deriv1_global_bound.

@audit:ok

Used by

theorem

InformationTheory.Shannon.FisherInfo.convDensityAdd_deriv_hasDerivAt_self

source

(pX : ℝ → ℝ) (_hpX_nn : ∀ (x : ℝ), 0 ≤ pX x) (hpX_meas : Measurable pX) (hpX_int : MeasureTheory.Integrable pX MeasureTheory.volume) {t : ℝ} (ht : 0 < t) (x : ℝ) :

HasDerivAt (deriv (EPIConvDensity.convDensityAdd pX (ProbabilityTheory.gaussianPDFReal 0 ⟨t, ⋯⟩))) (deriv (deriv (EPIConvDensity.convDensityAdd pX (ProbabilityTheory.gaussianPDFReal 0 ⟨t, ⋯⟩))) x) x

HasDerivAt (deriv p_t) (deriv (deriv p_t) x) x for p_t = convDensityAdd pX g_t at every x (t > 0): the spatial second derivative exists. The proof identifies deriv p_t as the kernel-form first-derivative function (convDensityAdd_deriv1_gaussian_eq) and differentiates it via the parametric-integral gateway with domination from kernel_x_deriv2_global_bound.

@audit:ok

Used by

Entropy-finiteness plumbing #

Three integrability lemmas for the entropy of the convolution density, with a uniform signature: pX nonnegative, measurable, integrable, mass 1, and finite second moment. They close from the Gaussian envelopes and the log-factor polynomial majorant in this file.

theorem

InformationTheory.Shannon.FisherInfo.convDensityAdd_logFactor_deriv2_integrable

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) (hpX_mom : MeasureTheory.Integrable (fun (y : ℝ) => y ^ 2 * pX y) MeasureTheory.volume) {t : ℝ} (ht : 0 < t) :

MeasureTheory.Integrable (fun (x : ℝ) => (-Real.log (EPIConvDensity.convDensityAdd pX (ProbabilityTheory.gaussianPDFReal 0 ⟨t, ⋯⟩) x) - 1) * deriv (deriv (EPIConvDensity.convDensityAdd pX (ProbabilityTheory.gaussianPDFReal 0 ⟨t, ⋯⟩))) x) MeasureTheory.volume

Integrable ((- log p_t - 1) · ∂²_x p_t) for p_t = convDensityAdd pX g_t, t > 0. Closes from the joint-domination envelope debruijnIdentityV2_holds_assembled_chain_domination instantiated at s = t.

@audit:ok

Used by

theorem

InformationTheory.Shannon.FisherInfo.convDensityAdd_logFactor_deriv_integrable

source

MeasureTheory.Integrable (fun (x : ℝ) => (-Real.log (EPIConvDensity.convDensityAdd pX (ProbabilityTheory.gaussianPDFReal 0 ⟨t, ⋯⟩) x) - 1) * deriv (EPIConvDensity.convDensityAdd pX (ProbabilityTheory.gaussianPDFReal 0 ⟨t, ⋯⟩)) x) MeasureTheory.volume

Integrable ((- log p_t - 1) · ∂_x p_t) for p_t = convDensityAdd pX g_t, t > 0. Closes from the log-factor polynomial majorant convDensityAdd_logFactor_poly_majorant and the gradient envelope gaussGradMaj.

@audit:ok

Used by

theorem

InformationTheory.Shannon.FisherInfo.convDensityAdd_negMulLog_integrable

source

MeasureTheory.Integrable (fun (x : ℝ) => (EPIConvDensity.convDensityAdd pX (ProbabilityTheory.gaussianPDFReal 0 ⟨t, ⋯⟩) x).negMulLog) MeasureTheory.volume

Integrable (negMulLog p_t) for p_t = convDensityAdd pX g_t, t > 0, so the entropy h(X + √t · Z) = -∫ negMulLog p_t is finite. Closes from the log-factor polynomial majorant (‖negMulLog p_t‖ = p_t · |log p_t| ≤ p_t · (A + 1 + B·x²)) and Integrable (x² · p_t).

@audit:ok

Used by