InformationTheory.Shannon.EPI.G2.ConvEntropyDensity

Imports 12

EPI G2 — (β) density-only lower bound #

This file packages the Ω-level (β) lower bound negMulLog_convDensity_entropy_ge (EPI/G2/ConvEntropyMonotone.lean) into a density-only wrapper: given just a probability density pX (plus minimal regularity), no abstract independent pair is required.

∫ negMulLog pX ≤ ∫ negMulLog (pX ∗ g_{u n}).

The Ω-level theorem requires an independent pair X ⊥ Z (with Z ∼ 𝒩(0, v_Z)) on some probability space together with 8 per-n regularity/integrability preconditions. We instantiate the canonical product space Ω := ℝ × ℝ, μ := (volume.withDensity (ofReal ∘ pX)).prod (gaussianReal 0 v_Z), X := Prod.fst, Z := Prod.snd. Then X ⊥ Z (product independence), μ.map X = withDensity pX, μ.map Z = gaussianReal 0 v_Z, and the 8 preconditions are discharged here.

Status — proof done (0 sorry / 0 residual) #

All 8 per-n preconditions of the Ω-level (β) lower bound are discharged here from the canonical construction:

per-fiber absolute continuity, p log p integrability, fiber-entropy integrability (translation invariance: each fiber is a translate pX(· − √s·z) of μ.map X);
joint absolute continuity (per-fiber ≪ volume ≪ μ.map W, the marginal having a strictly positive density);
the two cross terms (per-fiber (5) + outer (7)): closed via the s-uniform polynomial majorant |log p_t| ≤ A + B·x² (convDensityAdd_logFactor_poly_majorant, made public in FisherInfoDeBruijnAssembly) integrated against pX's translate moments (the standalone convCrossEntropy_perFibre_integrable / convCrossEntropy_zAvg_integrable, fed the a.e. identifications hLog / hfib_eq in the proof body);
marginal log-density integrability (∫ negMulLog p_t < ∞, the convDensityAdd_negMulLog_integrable);
joint llr integrability h_int (= KL finiteness D(joint ‖ product) < ∞): closed via MeasureTheory.Measure.integrable_compProd_iff. The slice identity rnDeriv_compProd_eq_kernel_rnDeriv + Kernel.rnDeriv_eq_rnDeriv_measure identify the joint llr a.e. with the per-fiber llr (κ_z) (μ.map W), which the density split llr_eq_log_density_sub_log_density rewrites as log p_z − log p_t. The per-fiber branch reuses the fiber-entropy + cross-term integrabilities (via integrable_toReal_rnDeriv_mul_iff); the outer branch dominates ∫ ‖log p_z − log p_t‖ ∂κ_z by C0 + (A+1) + 2B·M2 + 2B·s·z² (Gaussian-integrable), using ∫ pX·|log pX| < ∞ (from Integrable f ↔ Integrable ‖f‖ on hpX_ent) plus the s-uniform majorant.

#print axioms negMulLog_convDensity_entropy_ge_density = [propext, Classical.choice, Quot.sound] (sorryAx-free). This completes the EPI G2 (β) density-only lower bound.

theorem

InformationTheory.Shannon.fibre_rnDeriv_integrable_iff

source

(ν : MeasureTheory.Measure ℝ) [MeasureTheory.SigmaFinite ν] (c : ℝ) (Φ : ℝ → ℝ) :

MeasureTheory.Integrable (fun (x : ℝ) => Φ ((MeasureTheory.Measure.map (fun (y : ℝ) => y + c) ν).rnDeriv MeasureTheory.volume x).toReal) MeasureTheory.volume ↔ MeasureTheory.Integrable (fun (x : ℝ) => Φ (ν.rnDeriv MeasureTheory.volume x).toReal) MeasureTheory.volume

Translation transport for fiber integrability: if κ z = ν.map (· + c·z) (with ν ≪ volume), then Integrable (fun x ↦ Φ ((κ z).rnDeriv volume x).toReal) volume holds iff Integrable (fun x ↦ Φ (ν.rnDeriv volume x).toReal) volume.

Used by

Standalone cross-entropy integrability lemmas (extract of the template above) #

The 3 have blocks hκ_cross_int / h_cross_int / h_int inside negMulLog_convDensity_entropy_ge_density are extracted into standalone lemmas parametrized over an arbitrary fiber density q (with mass 1, finite second moment, finite absolute entropy) and a target convolution log-density g := convDensityAdd pX (gaussianPDFReal 0 v). Unlike the template (where fiber and target share the same pX), these admit two distinct densities, so they cover the EPI case-1 framing where the fiber is the Gaussian q = gaussianPDFReal 0 v_B (translated by z) and the target is the input-convolution density g.

The polynomial majorant |log g| ≤ (A+1) + B·x² (a.e.) comes from convDensityAdd_logFactor_poly_majorant pX …; the fiber q supplies the dominating moments, reusing the template's domination structure (no sorry).

theorem

InformationTheory.Shannon.integrable_sq_mul_gaussianPDFReal

source

{v : NNReal} (hv : v ≠ 0) :

MeasureTheory.Integrable (fun (y : ℝ) => y ^ 2 * ProbabilityTheory.gaussianPDFReal 0 v y) MeasureTheory.volume

Second-moment integrability of the centered Gaussian density: y²·g_v(y) is volume-integrable. Via ∫ y²·g_v = ∫ y² ∂(gaussianReal 0 v) (finite by memLp_id_gaussianReal 2). @audit:ok

Used by

theorem

InformationTheory.Shannon.convCrossEntropy_perFibre_integrable

source

(q pX : ℝ → ℝ) (hq_nn : ∀ (x : ℝ), 0 ≤ q x) (hq_meas : Measurable q) (hq_int : MeasureTheory.Integrable q MeasureTheory.volume) (hq_mom : MeasureTheory.Integrable (fun (y : ℝ) => y ^ 2 * q y) MeasureTheory.volume) (hpX_nn : ∀ (x : ℝ), 0 ≤ pX x) (hpX_meas : Measurable pX) (hpX_int : MeasureTheory.Integrable pX MeasureTheory.volume) (hpX_mass : ∫ (y : ℝ), pX y = 1) {v : NNReal} (hv : 0 < v) (c : ℝ) :

MeasureTheory.Integrable (fun (x : ℝ) => q (x - c) * Real.log (EPIConvDensity.convDensityAdd pX (ProbabilityTheory.gaussianPDFReal 0 v) x)) MeasureTheory.volume

Per-fiber cross-term integrability: the (shifted) fiber density q(·−c) times the log of the convolution target g = convDensityAdd pX g_v is volume-integrable. Dominated by q(x−c)·((A+1)+B·x²) via the polynomial majorant of log g. @audit:ok

Used by

theorem

InformationTheory.Shannon.convCrossEntropy_zAvg_integrable

source

(q pX : ℝ → ℝ) (hq_nn : ∀ (x : ℝ), 0 ≤ q x) (hq_meas : Measurable q) (hq_int : MeasureTheory.Integrable q MeasureTheory.volume) (hq_mass : ∫ (y : ℝ), q y = 1) (hq_mom : MeasureTheory.Integrable (fun (y : ℝ) => y ^ 2 * q y) MeasureTheory.volume) (hpX_nn : ∀ (x : ℝ), 0 ≤ pX x) (hpX_meas : Measurable pX) (hpX_int : MeasureTheory.Integrable pX MeasureTheory.volume) (hpX_mass : ∫ (y : ℝ), pX y = 1) {v : NNReal} (hv : 0 < v) {s : ℝ} (hs : 0 < s) (νZ : MeasureTheory.Measure ℝ) [MeasureTheory.IsFiniteMeasure νZ] (hνZ_sq : MeasureTheory.Integrable (fun (z : ℝ) => z ^ 2) νZ) :

MeasureTheory.Integrable (fun (z : ℝ) => ∫ (x : ℝ), q (x - √s * z) * Real.log (EPIConvDensity.convDensityAdd pX (ProbabilityTheory.gaussianPDFReal 0 v) x)) νZ

z-averaged cross-term integrability: averaging the per-fiber cross integral over a measure νZ with finite second moment yields an integrable function of z. The shift is c(z) = √s·z; bounded by (A+1) + 2B·M2q + 2B·s·z² (gaussian-style moment control). @audit:ok

Used by

theorem

InformationTheory.Shannon.convJointLlr_integrable

source

MeasureTheory.Integrable (MeasureTheory.llr ((MeasureTheory.Measure.map Z μ).compProd (ProbabilityTheory.condDistrib W Z μ)) ((MeasureTheory.Measure.map Z μ).compProd (ProbabilityTheory.Kernel.const ℝ (MeasureTheory.Measure.map W μ)))) ((MeasureTheory.Measure.map Z μ).compProd (ProbabilityTheory.condDistrib W Z μ))

Joint llr (conditional-KL divergence integrand) integrability, extracted from the template h_int block. Given a probability space μ with coordinates Z W, a fiber kernel κ = condDistrib W Z μ whose fibers a.e.-equal the (shifted) density q(·−√s·z) and whose marginal μ.map W has density g, with the polynomial majorant |log g| ≤ (A+1)+B·x², the joint llr of the compProd vs. the product-with-const is (μ.map Z) ⊗ₘ κ-integrable. All hypotheses are regularity/integrability obligations (none encodes the EPI conclusion). @audit:ok

Used by

theorem

InformationTheory.Shannon.integrable_sq_gaussianReal

source

{v : NNReal} :

MeasureTheory.Integrable (fun (z : ℝ) => z ^ 2) (ProbabilityTheory.gaussianReal 0 v)

@audit:ok

Used by

theorem

InformationTheory.Shannon.condDistrib_fibre_rnDeriv_eq_translate

source

{mZ ν : MeasureTheory.Measure ℝ} [MeasureTheory.SigmaFinite ν] {κ : ProbabilityTheory.Kernel ℝ ℝ} {c : ℝ} {g : ℝ → ENNReal} (hae : ⇑κ =ᵐ[mZ] ⇑(affineShiftKernel ν c)) (hqν : ν.rnDeriv MeasureTheory.volume =ᵐ[MeasureTheory.volume ] g) :

∀ᵐ (z : ℝ) ∂mZ, (κ z).rnDeriv MeasureTheory.volume =ᵐ[MeasureTheory.volume ] fun (x : ℝ) => g (x - c * z)

@audit:ok

Used by

theorem

InformationTheory.Shannon.condDistrib_fibre_absolutelyContinuous

source

{mZ ν : MeasureTheory.Measure ℝ} [MeasureTheory.SFinite ν] {κ : ProbabilityTheory.Kernel ℝ ℝ} {c : ℝ} (hν_ac : ν.AbsolutelyContinuous MeasureTheory.volume) (hae : ⇑κ =ᵐ[mZ] ⇑(affineShiftKernel ν c)) :

∀ᵐ (z : ℝ) ∂mZ, (κ z).AbsolutelyContinuous MeasureTheory.volume

@audit:ok

Used by

theorem

InformationTheory.Shannon.condDistrib_fibre_pXlogpX_integrable

source

{mZ ν : MeasureTheory.Measure ℝ} [MeasureTheory.SigmaFinite ν] {κ : ProbabilityTheory.Kernel ℝ ℝ} {c : ℝ} (hae : ⇑κ =ᵐ[mZ] ⇑(affineShiftKernel ν c)) (h_pXlogpX : MeasureTheory.Integrable (fun (x : ℝ) => (ν.rnDeriv MeasureTheory.volume x).toReal * Real.log (ν.rnDeriv MeasureTheory.volume x).toReal) MeasureTheory.volume) :

∀ᵐ (z : ℝ) ∂mZ, MeasureTheory.Integrable (fun (x : ℝ) => ((κ z).rnDeriv MeasureTheory.volume x).toReal * Real.log ((κ z).rnDeriv MeasureTheory.volume x).toReal) MeasureTheory.volume

@audit:ok

Used by

theorem

InformationTheory.Shannon.condDistrib_fibre_entropy_integrable

source

{mZ ν : MeasureTheory.Measure ℝ} [MeasureTheory.SigmaFinite ν] [MeasureTheory.IsProbabilityMeasure mZ] {κ : ProbabilityTheory.Kernel ℝ ℝ} {c : ℝ} (hν_ac : ν.AbsolutelyContinuous MeasureTheory.volume) (hae : ⇑κ =ᵐ[mZ] ⇑(affineShiftKernel ν c)) :

MeasureTheory.Integrable (fun (z : ℝ) => differentialEntropy (κ z)) mZ

@audit:ok

Used by

theorem

InformationTheory.Shannon.abs_log_convDensityAdd_le_of_majorant

source

{pX : ℝ → ℝ} {A B un : ℝ} (hun : 0 < un) (hLog0 : ∀ᵐ (x : ℝ), ∀ (s : ℝ) (hs : s ∈ Set.Ioo (un / 2) (2 * un)), ‖-Real.log (EPIConvDensity.convDensityAdd pX (ProbabilityTheory.gaussianPDFReal 0 ⟨s, ⋯⟩) x) - 1‖ ≤ A + B * x ^ 2) :

∀ᵐ (x : ℝ), |Real.log (EPIConvDensity.convDensityAdd pX (ProbabilityTheory.gaussianPDFReal 0 ⟨un, ⋯⟩) x)| ≤ A + 1 + B * x ^ 2

@audit:ok

Used by

theorem

InformationTheory.Shannon.negMulLog_convDensity_entropy_ge_density

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) (hpX_ent : MeasureTheory.Integrable (fun (x : ℝ) => (pX x).negMulLog) MeasureTheory.volume) {v_Z : NNReal} (hv_Z_pos : 0 < v_Z) (u : ℕ → ℝ) (hu_pos : ∀ (n : ℕ), 0 < u n) (n : ℕ) :

∫ (x : ℝ), (pX x).negMulLog ≤ ∫ (x : ℝ), (EPIConvDensity.convDensityAdd pX (ProbabilityTheory.gaussianPDFReal 0 ⟨u n, ⋯⟩) x).negMulLog

The (β) density form, pX-only: convolution with a Gaussian does not decrease the negMulLog entropy integral: ∫ negMulLog pX ≤ ∫ negMulLog (pX ∗ g_{u n}).

pX is a probability density (non-negative, measurable, integrable, mass 1) with a finite second moment and integrable entropy integrand. v_Z is any fixed positive variance for the auxiliary Gaussian; it does not appear in the conclusion.

Proved by instantiating the Ω-level (β) lower bound negMulLog_convDensity_entropy_ge on the canonical product space ℝ × ℝ. @audit:ok

Used by