InformationTheory.Shannon.EPI.Blachman.GeneralDensity
Non-Gaussian IsBlachmanConvReady producer — EPI A-5 precondition (4) #
This file supplies a producer for
IsBlachmanConvReady (convDensityAdd pX g_t) (convDensityAdd pY g_t) where pX/pY
are arbitrary probability densities and g_t = gaussianPDFReal 0 ⟨t, ht.le⟩ is the
heat kernel (t > 0). The existing producer
(isBlachmanConvReady_gaussianPDFReal) is Gaussian-only; the A-5 chain apex needs the
conv-with-Gaussian (general density) version.
Set fX := convDensityAdd pX g_t, fY := convDensityAdd pY g_t. Both are
conv-with-Gaussian densities. All 19 IsBlachmanConvReady fields are closed genuinely
(19/19, no retreat).
- The 18 conv-with-Gaussian fields
int_fX/fY,bdd_*,pos_pZ,int_X/int_Y,cond_int,int_W,int_Wsq,int_inner,int_fisherX/int_fisherY,int_prod1/2/3are closed genuinely from the conv-with-Gaussian regularity assets (isRegularDensityV2_convDensityAdd_gaussian,convDensityAdd_gaussian_bdd/_deriv_bdd/_integrable,convDensityAdd_pos_of_pos_cont, the Fisher-finiteness boundgaussianConv_fisher_le_inv_varviaconvDensityAdd_fisher_integrand_integrable, and the shearmeasurePreserving_prod_sub_swapfor the Tonelli product-measure terms). The key reduction islogDeriv fX · fX = deriv fX(strict positivity offX), turning the linear-score fields into integrable·bounded products and the Fisher fields into shifted/sheared copies ofint_fisherX/int_fisherY. - The
int_fisherZfield is closed genuinely from Fisher integrability of the conv-of-convconvDensityAdd fX fY. The 4-fold interchange bridgeconvDensityAdd_convGaussian_interchange(EPI/Conv/DensityAssoc.lean) identifies it withconvDensityAdd (convDensityAdd pX pY) g_{2t}(convolution associativity via Mathlibconvolution_assoc+convDensityAdd_comm+ variance-doublingg_t ∗ g_t = g_{2t}), which is conv-with-Gaussian (variance2t) and closes viaconvDensityAdd_fisher_integrand_integrable (pX∗pY) … (2t). ThepX∗pYarm needspX∗pYto be a normalized probability density (nonneg / measurable / integrable / mass 1), supplied by theconvDensityAdd_pXpY_*helpers inEPI/Conv/DensityAssoc.lean.
hpX_norm : ∫ pX = 1 / hpY_norm are added beyond the bare hpX_mass of the brief
target signature: they are A-5-suppliable regularity (from pX_law's probability
measure pushforward) and needed by gaussianConv_fisher_le_inv_var.
InformationTheory.Shannon.EPIBlachmanGeneralDensity.convDensityAdd_fisher_integrand_integrable
source(pX : ℝ → ℝ)
(hpX_nn : ∀ (x : ℝ), 0 ≤ pX x)
(hpX_meas : Measurable pX)
(hpX_int : MeasureTheory.Integrable pX MeasureTheory.volume)
(hpX_norm : ∫ (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
Fisher integrand integrability for a conv-with-Gaussian density (public form).
Integrable ((logDeriv (convDensityAdd pX g_t))² · convDensityAdd pX g_t) — the
int_fisherX shape. Reconstructed from the public Fisher-finiteness bound
gaussianConv_fisher_le_inv_var (J(p_t) ≤ 1/t < ⊤), exactly mirroring the private
convDensityAdd_fisher_integrable body.
@audit:ok. Hypotheses are all regularity
(nonneg / Measurable / Integrable / mass = 1 normalization); the Fisher-integrand
integrability follows genuinely from the existing @audit:ok bound
gaussianConv_fisher_le_inv_var (J(p_t) < ⊤) + lintegral_ofReal_ne_top_iff_integrable.
No bundled core (the Fisher inequality is imported from a proved lemma, not a hypothesis).
#print axioms = [propext, Classical.choice, Quot.sound] (sorryAx-free, machine-confirmed).
Used by
InformationTheory.Shannon.EPIBlachmanGeneralDensity.convDensityAdd_gaussian_bdd
source(pX : ℝ → ℝ)
(hpX_nn : ∀ (x : ℝ), 0 ≤ pX x)
(hpX_int : MeasureTheory.Integrable pX MeasureTheory.volume)
{t : ℝ}
(ht : 0 < t)
:
∃ (M : ℝ), ∀ (z : ℝ), |EPIConvDensity.convDensityAdd pX (ProbabilityTheory.gaussianPDFReal 0 ⟨t, ⋯⟩) z| ≤ M
Global boundedness of a conv-with-Gaussian density:
|convDensityAdd pX g_t z| ≤ (sup g_t) · ∫ pX.
@audit:ok
Used by
InformationTheory.Shannon.EPIBlachmanGeneralDensity.convDensityAdd_gaussian_integrable
source(pX : ℝ → ℝ)
(hpX_meas : Measurable pX)
(hpX_int : MeasureTheory.Integrable pX MeasureTheory.volume)
{t : ℝ}
(ht : 0 < t)
:
convDensityAdd pX g_t is Lebesgue-integrable (envelope).
@audit:ok
Used by
InformationTheory.Shannon.EPIBlachmanGeneralDensity.convDensityAdd_gaussian_deriv_bdd
source(pX : ℝ → ℝ)
(hpX_nn : ∀ (x : ℝ), 0 ≤ pX x)
(hpX_int : MeasureTheory.Integrable pX MeasureTheory.volume)
{t : ℝ}
(ht : 0 < t)
:
∃ (M : ℝ), ∀ (z : ℝ), |deriv (EPIConvDensity.convDensityAdd pX (ProbabilityTheory.gaussianPDFReal 0 ⟨t, ⋯⟩)) z| ≤ M
deriv (convDensityAdd pX g_t) is globally bounded:
|deriv (convDensityAdd pX g_t) z| = |convDensityAdd pX (deriv g_t) z| ≤ (sup|deriv g_t|)·∫pX.
@audit:ok
Used by
InformationTheory.Shannon.EPIBlachmanGeneralDensity.convDensityAdd_pos_of_pos_cont
source(fX fY : ℝ → ℝ)
(hfX_cont : Continuous fX)
(hfY_cont : Continuous fY)
(hfX_pos : ∀ (x : ℝ), 0 < fX x)
(hfY_pos : ∀ (x : ℝ), 0 < fY x)
(z : ℝ)
(hint : MeasureTheory.Integrable (fun (x : ℝ) => fX x * fY (z - x)) MeasureTheory.volume)
:
General convolution positivity: if fX, fY are continuous, strictly
positive everywhere, and the integrand x ↦ fX x · fY (z - x) is integrable, then the
convolution density convDensityAdd fX fY z is strictly positive.
@audit:ok
Used by
InformationTheory.Shannon.EPIBlachmanGeneralDensity.convDensityAdd_gaussian_convDensityAdd_pos
source(pX pY : ℝ → ℝ)
{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)
(hpY_nn : ∀ (x : ℝ), 0 ≤ pY x)
(hpY_meas : Measurable pY)
(hpY_int : MeasureTheory.Integrable pY MeasureTheory.volume)
(hpY_mass : 0 < ∫ (x : ℝ), pY x)
(z : ℝ)
:
Used by
InformationTheory.Shannon.EPIBlachmanGeneralDensity.convDensityAdd_gaussian_integrable_deriv_mul
source(pX pY : ℝ → ℝ)
{t : ℝ}
(ht : 0 < t)
(hpX_nn : ∀ (x : ℝ), 0 ≤ pX x)
(hpX_int : MeasureTheory.Integrable pX MeasureTheory.volume)
(hpY_meas : Measurable pY)
(hpY_int : MeasureTheory.Integrable pY MeasureTheory.volume)
(z : ℝ)
:
MeasureTheory.Integrable
(fun (x : ℝ) =>
deriv (EPIConvDensity.convDensityAdd pX (ProbabilityTheory.gaussianPDFReal 0 ⟨t, ⋯⟩)) x * EPIConvDensity.convDensityAdd pY (ProbabilityTheory.gaussianPDFReal 0 ⟨t, ⋯⟩) (z - x))
MeasureTheory.volume
Used by
InformationTheory.Shannon.EPIBlachmanGeneralDensity.convDensityAdd_gaussian_integrable_mul_deriv
source(pX pY : ℝ → ℝ)
{t : ℝ}
(ht : 0 < t)
(hpX_meas : Measurable pX)
(hpX_int : MeasureTheory.Integrable pX MeasureTheory.volume)
(hpY_nn : ∀ (x : ℝ), 0 ≤ pY x)
(hpY_int : MeasureTheory.Integrable pY MeasureTheory.volume)
(z : ℝ)
:
MeasureTheory.Integrable
(fun (x : ℝ) =>
EPIConvDensity.convDensityAdd pX (ProbabilityTheory.gaussianPDFReal 0 ⟨t, ⋯⟩) x * deriv (EPIConvDensity.convDensityAdd pY (ProbabilityTheory.gaussianPDFReal 0 ⟨t, ⋯⟩)) (z - x))
MeasureTheory.volume
Used by
InformationTheory.Shannon.EPIBlachmanGeneralDensity.convDensityAdd_gaussian_condDensityX_integrable
source(pX pY : ℝ → ℝ)
{t : ℝ}
(ht : 0 < t)
(hpX_meas : Measurable pX)
(hpX_int : MeasureTheory.Integrable pX MeasureTheory.volume)
(hpY_nn : ∀ (x : ℝ), 0 ≤ pY x)
(hpY_meas : Measurable pY)
(hpY_int : MeasureTheory.Integrable pY MeasureTheory.volume)
(hpY_mass : 0 < ∫ (x : ℝ), pY x)
(z : ℝ)
:
Used by
InformationTheory.Shannon.EPIBlachmanGeneralDensity.convDensityAdd_gaussian_integrable_scoreWeight_mul_condDensityX
source(pX pY : ℝ → ℝ)
{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)
(hpY_nn : ∀ (x : ℝ), 0 ≤ pY x)
(hpY_meas : Measurable pY)
(hpY_int : MeasureTheory.Integrable pY MeasureTheory.volume)
(hpY_mass : 0 < ∫ (x : ℝ), pY x)
(lam z : ℝ)
:
MeasureTheory.Integrable
(fun (x : ℝ) =>
EPIBlachmanDensity.scoreWeight (EPIConvDensity.convDensityAdd pX (ProbabilityTheory.gaussianPDFReal 0 ⟨t, ⋯⟩))
(EPIConvDensity.convDensityAdd pY (ProbabilityTheory.gaussianPDFReal 0 ⟨t, ⋯⟩)) lam z x * EPIBlachmanDensity.condDensityX (EPIConvDensity.convDensityAdd pX (ProbabilityTheory.gaussianPDFReal 0 ⟨t, ⋯⟩))
(EPIConvDensity.convDensityAdd pY (ProbabilityTheory.gaussianPDFReal 0 ⟨t, ⋯⟩)) z x)
MeasureTheory.volume
Used by
InformationTheory.Shannon.EPIBlachmanGeneralDensity.convDensityAdd_gaussian_integrable_scoreWeight_sq_mul_condDensityX
source(pX pY : ℝ → ℝ)
{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)
(hpX_norm : ∫ (x : ℝ), pX x = 1)
(hpY_nn : ∀ (x : ℝ), 0 ≤ pY x)
(hpY_meas : Measurable pY)
(hpY_int : MeasureTheory.Integrable pY MeasureTheory.volume)
(hpY_mass : 0 < ∫ (x : ℝ), pY x)
(hpY_norm : ∫ (x : ℝ), pY x = 1)
(lam z : ℝ)
:
MeasureTheory.Integrable
(fun (x : ℝ) =>
EPIBlachmanDensity.scoreWeight (EPIConvDensity.convDensityAdd pX (ProbabilityTheory.gaussianPDFReal 0 ⟨t, ⋯⟩))
(EPIConvDensity.convDensityAdd pY (ProbabilityTheory.gaussianPDFReal 0 ⟨t, ⋯⟩)) lam z x ^ 2 * EPIBlachmanDensity.condDensityX (EPIConvDensity.convDensityAdd pX (ProbabilityTheory.gaussianPDFReal 0 ⟨t, ⋯⟩))
(EPIConvDensity.convDensityAdd pY (ProbabilityTheory.gaussianPDFReal 0 ⟨t, ⋯⟩)) z x)
MeasureTheory.volume
Used by
InformationTheory.Shannon.EPIBlachmanGeneralDensity.convDensityAdd_gaussian_integrable_inner_scoreWeight_sq
source(pX pY : ℝ → ℝ)
{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)
(hpX_norm : ∫ (x : ℝ), pX x = 1)
(hpY_nn : ∀ (x : ℝ), 0 ≤ pY x)
(hpY_meas : Measurable pY)
(hpY_int : MeasureTheory.Integrable pY MeasureTheory.volume)
(hpY_mass : 0 < ∫ (x : ℝ), pY x)
(hpY_norm : ∫ (x : ℝ), pY x = 1)
(lam : ℝ)
:
MeasureTheory.Integrable
(fun (z : ℝ) =>
(∫ (x : ℝ), EPIBlachmanDensity.scoreWeight (EPIConvDensity.convDensityAdd pX (ProbabilityTheory.gaussianPDFReal 0 ⟨t, ⋯⟩))
(EPIConvDensity.convDensityAdd pY (ProbabilityTheory.gaussianPDFReal 0 ⟨t, ⋯⟩)) lam z x ^ 2 * EPIBlachmanDensity.condDensityX
(EPIConvDensity.convDensityAdd pX (ProbabilityTheory.gaussianPDFReal 0 ⟨t, ⋯⟩))
(EPIConvDensity.convDensityAdd pY (ProbabilityTheory.gaussianPDFReal 0 ⟨t, ⋯⟩)) z x) * EPIConvDensity.convDensityAdd (EPIConvDensity.convDensityAdd pX (ProbabilityTheory.gaussianPDFReal 0 ⟨t, ⋯⟩))
(EPIConvDensity.convDensityAdd pY (ProbabilityTheory.gaussianPDFReal 0 ⟨t, ⋯⟩)) z)
MeasureTheory.volume
Used by
InformationTheory.Shannon.EPIBlachmanGeneralDensity.convDensityAdd_gaussian_fisher_integrand_integrable
source(pX pY : ℝ → ℝ)
{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)
(hpY_nn : ∀ (x : ℝ), 0 ≤ pY x)
(hpY_meas : Measurable pY)
(hpY_int : MeasureTheory.Integrable pY MeasureTheory.volume)
(hpY_norm : ∫ (x : ℝ), pY x = 1)
:
MeasureTheory.Integrable
(fun (z : ℝ) =>
logDeriv
(EPIConvDensity.convDensityAdd (EPIConvDensity.convDensityAdd pX (ProbabilityTheory.gaussianPDFReal 0 ⟨t, ⋯⟩))
(EPIConvDensity.convDensityAdd pY (ProbabilityTheory.gaussianPDFReal 0 ⟨t, ⋯⟩)))
z ^ 2 * EPIConvDensity.convDensityAdd (EPIConvDensity.convDensityAdd pX (ProbabilityTheory.gaussianPDFReal 0 ⟨t, ⋯⟩))
(EPIConvDensity.convDensityAdd pY (ProbabilityTheory.gaussianPDFReal 0 ⟨t, ⋯⟩)) z)
MeasureTheory.volume
Used by
InformationTheory.Shannon.EPIBlachmanGeneralDensity.convDensityAdd_gaussian_integrable_prod_logDeriv_sq_mul
source(pX pY : ℝ → ℝ)
{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)
(hpY_meas : Measurable pY)
(hpY_int : MeasureTheory.Integrable pY MeasureTheory.volume)
:
MeasureTheory.Integrable
(Function.uncurry fun (z x : ℝ) =>
logDeriv (EPIConvDensity.convDensityAdd pX (ProbabilityTheory.gaussianPDFReal 0 ⟨t, ⋯⟩)) x ^ 2 * EPIConvDensity.convDensityAdd pX (ProbabilityTheory.gaussianPDFReal 0 ⟨t, ⋯⟩) x * EPIConvDensity.convDensityAdd pY (ProbabilityTheory.gaussianPDFReal 0 ⟨t, ⋯⟩) (z - x))
(MeasureTheory.volume.prod MeasureTheory.volume)
Used by
InformationTheory.Shannon.EPIBlachmanGeneralDensity.convDensityAdd_gaussian_integrable_prod_logDeriv_sq_shift_mul
source(pX pY : ℝ → ℝ)
{t : ℝ}
(ht : 0 < t)
(hpX_meas : Measurable pX)
(hpX_int : MeasureTheory.Integrable pX MeasureTheory.volume)
(hpY_nn : ∀ (x : ℝ), 0 ≤ pY x)
(hpY_meas : Measurable pY)
(hpY_int : MeasureTheory.Integrable pY MeasureTheory.volume)
(hpY_norm : ∫ (x : ℝ), pY x = 1)
:
MeasureTheory.Integrable
(Function.uncurry fun (z x : ℝ) =>
logDeriv (EPIConvDensity.convDensityAdd pY (ProbabilityTheory.gaussianPDFReal 0 ⟨t, ⋯⟩)) (z - x) ^ 2 * EPIConvDensity.convDensityAdd pX (ProbabilityTheory.gaussianPDFReal 0 ⟨t, ⋯⟩) x * EPIConvDensity.convDensityAdd pY (ProbabilityTheory.gaussianPDFReal 0 ⟨t, ⋯⟩) (z - x))
(MeasureTheory.volume.prod MeasureTheory.volume)
Used by
InformationTheory.Shannon.EPIBlachmanGeneralDensity.convDensityAdd_gaussian_integrable_prod_deriv_mul
source(pX pY : ℝ → ℝ)
{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)
(hpY_nn : ∀ (x : ℝ), 0 ≤ pY x)
(hpY_meas : Measurable pY)
(hpY_int : MeasureTheory.Integrable pY MeasureTheory.volume)
(hpY_mass : 0 < ∫ (x : ℝ), pY x)
:
MeasureTheory.Integrable
(Function.uncurry fun (z x : ℝ) =>
logDeriv (EPIConvDensity.convDensityAdd pX (ProbabilityTheory.gaussianPDFReal 0 ⟨t, ⋯⟩)) x * EPIConvDensity.convDensityAdd pX (ProbabilityTheory.gaussianPDFReal 0 ⟨t, ⋯⟩) x * (logDeriv (EPIConvDensity.convDensityAdd pY (ProbabilityTheory.gaussianPDFReal 0 ⟨t, ⋯⟩)) (z - x) * EPIConvDensity.convDensityAdd pY (ProbabilityTheory.gaussianPDFReal 0 ⟨t, ⋯⟩) (z - x)))
(MeasureTheory.volume.prod MeasureTheory.volume)
Used by
InformationTheory.Shannon.EPIBlachmanGeneralDensity.isBlachmanConvReady_convDensityAdd_gaussian
source(pX pY : ℝ → ℝ)
{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)
(hpX_norm : ∫ (x : ℝ), pX x = 1)
(hpY_nn : ∀ (x : ℝ), 0 ≤ pY x)
(hpY_meas : Measurable pY)
(hpY_int : MeasureTheory.Integrable pY MeasureTheory.volume)
(hpY_mass : 0 < ∫ (x : ℝ), pY x)
(hpY_norm : ∫ (x : ℝ), pY x = 1)
:
A non-Gaussian IsBlachmanConvReady producer for EPI A-5 precondition (4).
fX := convDensityAdd pX g_t, fY := convDensityAdd pY g_t.
@audit:ok