InformationTheory.Shannon.FisherInfo.DeBruijnAssembly.Domination
InformationTheory.Shannon.FisherInfo.debruijnIdentityV2_holds_assembled_chain_domination
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)
:
∃ (bound : ℝ → ℝ),
MeasureTheory.Integrable bound MeasureTheory.volume ∧ ∀ᵐ (x : ℝ), ∀ (s : ℝ) (hs : s ∈ Set.Ioo (t / 2) (2 * t)),
‖(-Real.log (EPIConvDensity.convDensityAdd pX (ProbabilityTheory.gaussianPDFReal 0 ⟨s, ⋯⟩) x) - 1) * (1 / 2 * deriv (deriv (EPIConvDensity.convDensityAdd pX (ProbabilityTheory.gaussianPDFReal 0 ⟨s, ⋯⟩))) x)‖ ≤ bound x
Produces an integrable majorant bound dominating the full entropy σ-derivand
(- log (pPath s x) - 1) · ((1/2) · ∂²_x pPath s x) uniformly over s ∈ Set.Ioo (t/2) (2*t).
The majorant is the product (A + B·x²) · ((1/2) · hessBound x) of an s-uniform polynomial
majorant for the log factor (convDensityAdd_logFactor_poly_majorant) and the s-uniform
integrable Hessian envelope (convDensityAdd_deriv2_poly_moment_majorant). Its integrability is
established by Tonelli against the Gaussian moments of the kernel, which collapses the outer
integral to the mass, first, and second moments of pX — all finite under hpX_mass and
hpX_mom.
@audit:ok