InformationTheory.Shannon.EPI.DensityForm

Imports 11

Density-form entropy power inequality #

entropy_power_inequality_of_density: EPI for absolutely continuous distributions with finite second moment and regular densities, proved via a 3-noise lift and two-time terminal.

Main statements #

entropy_power_inequality_of_density: EPI under explicit density regularity hypotheses.

Implementation notes #

The proof lifts the base space (Ω, P) to (Ω × ℝ × ℝ × ℝ, liftMeasure3 P) and introduces three independent unit-noise variables Z_X, Z_Y, Z. Smoothing the sum with a separate unit noise Z (rather than using Z_X + Z_Y ~ 𝒩(0,2)) ensures that isDeBruijnRegularityHyp_of_methodX_unitnoise (which requires gaussianReal 0 1) applies to the sum-instance as well.

noncomputable def

InformationTheory.Shannon.EPIDensityForm.isHeatFlowEndpointRegular_of_canonical_rnDeriv

source

{Ω : Type u_1} {mΩ : MeasurableSpace Ω} (P : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure P] {α : Type u_2} {mα : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure μ] (W : Ω → ℝ) (W' Zw : α → ℝ) (hW : Measurable W) (hW' : Measurable W') (hZw : Measurable Zw) (hWZ : ProbabilityTheory.IndepFun W' Zw μ) (hZw_law : MeasureTheory.Measure.map Zw μ = ProbabilityTheory.gaussianReal 0 1) (hmap : MeasureTheory.Measure.map W' μ = MeasureTheory.Measure.map W P) (hac : (MeasureTheory.Measure.map W P).AbsolutelyContinuous MeasureTheory.volume) (hmom : MeasureTheory.Integrable (fun (ω : Ω) => W ω ^ 2) P) (hent : MeasureTheory.Integrable (fun (x : ℝ) => ((MeasureTheory.Measure.map W P).rnDeriv MeasureTheory.volume x).toReal.negMulLog) MeasureTheory.volume) :

IsHeatFlowEndpointRegular W' Zw μ

Equations

One or more equations did not get rendered due to their size.

Instances For

Used by

theorem

InformationTheory.Shannon.EPIDensityForm.integral_sub_integral_sq_rescaled_path_le

source

{α : Type u_1} {mα : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure μ] (A B : α → ℝ) (hA : Measurable A) (hB : Measurable B) (hAB : ProbabilityTheory.IndepFun A B μ) (h_mom_A : MeasureTheory.Integrable (fun (p : α) => A p ^ 2) μ) (v_B : NNReal) (hB_law : MeasureTheory.Measure.map B μ = ProbabilityTheory.gaussianReal 0 v_B) {t : ℝ} (ht : 0 < t) :

∫ (x : ℝ), (x - ∫ (y : ℝ), y ∂MeasureTheory.Measure.map (fun (p : α) => A p / √t + B p) μ) ^ 2 ∂MeasureTheory.Measure.map (fun (p : α) => A p / √t + B p) μ ≤ ProbabilityTheory.variance A μ / t + ↑v_B

Used by

theorem

InformationTheory.Shannon.EPIDensityForm.rescaled_path_absolutelyContinuous_and_negMulLog_integrable

source

{α : Type u_1} {mα : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure μ] (A B : α → ℝ) (hA : Measurable A) (hB : Measurable B) (hAB : ProbabilityTheory.IndepFun A B μ) (hA_ac : (MeasureTheory.Measure.map A μ).AbsolutelyContinuous MeasureTheory.volume) (h_mom_A : MeasureTheory.Integrable (fun (p : α) => A p ^ 2) μ) (v_B : NNReal) (hv_B : v_B ≠ 0) (hB_law : MeasureTheory.Measure.map B μ = ProbabilityTheory.gaussianReal 0 v_B) {t : ℝ} (ht : 0 < t) :

(MeasureTheory.Measure.map (fun (p : α) => A p / √t + B p) μ).AbsolutelyContinuous MeasureTheory.volume ∧ MeasureTheory.Integrable (fun (x : ℝ) => ((MeasureTheory.Measure.map (fun (p : α) => A p / √t + B p) μ).rnDeriv MeasureTheory.volume x).toReal.negMulLog) MeasureTheory.volume

Used by

theorem

InformationTheory.Shannon.EPIDensityForm.liftMeasure3_map_fst_eq

source

{Ω : Type u_1} {mΩ : MeasurableSpace Ω} (P : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure P] (X Y : Ω → ℝ) (hX : Measurable X) (hY : Measurable Y) :

MeasureTheory.Measure.map (fun (p : Ω × ℝ × ℝ × ℝ) => X p.1) (EPINoiseExtension.liftMeasure3 P) = MeasureTheory.Measure.map X P ∧ MeasureTheory.Measure.map (fun (p : Ω × ℝ × ℝ × ℝ) => Y p.1) (EPINoiseExtension.liftMeasure3 P) = MeasureTheory.Measure.map Y P ∧ MeasureTheory.Measure.map (fun (p : Ω × ℝ × ℝ × ℝ) => X p.1 + Y p.1) (EPINoiseExtension.liftMeasure3 P) = MeasureTheory.Measure.map (fun (ω : Ω) => X ω + Y ω) P

Used by

theorem

InformationTheory.Shannon.EPIDensityForm.liftMeasure3_noise_laws

source

{Ω : Type u_1} {mΩ : MeasurableSpace Ω} (P : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure P] :

MeasureTheory.Measure.map (fun (p : Ω × ℝ × ℝ × ℝ) => p.2.1) (EPINoiseExtension.liftMeasure3 P) = ProbabilityTheory.gaussianReal 0 1 ∧ MeasureTheory.Measure.map (fun (p : Ω × ℝ × ℝ × ℝ) => p.2.2.1) (EPINoiseExtension.liftMeasure3 P) = ProbabilityTheory.gaussianReal 0 1 ∧ MeasureTheory.Measure.map (fun (p : Ω × ℝ × ℝ × ℝ) => p.2.2.2) (EPINoiseExtension.liftMeasure3 P) = ProbabilityTheory.gaussianReal 0 1

Used by

theorem

InformationTheory.Shannon.EPIDensityForm.liftMeasure3_moment_transport

source

{Ω : Type u_1} {mΩ : MeasurableSpace Ω} (P : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure P] (X Y : Ω → ℝ) (hX : Measurable X) (hY : Measurable Y) (h_mom_X : MeasureTheory.Integrable (fun (ω : Ω) => X ω ^ 2) P) (h_mom_Y : MeasureTheory.Integrable (fun (ω : Ω) => Y ω ^ 2) P) :

MeasureTheory.Integrable (fun (ω : Ω) => (X ω + Y ω) ^ 2) P ∧ MeasureTheory.Integrable (fun (p : Ω × ℝ × ℝ × ℝ) => X p.1 ^ 2) (EPINoiseExtension.liftMeasure3 P) ∧ MeasureTheory.Integrable (fun (p : Ω × ℝ × ℝ × ℝ) => Y p.1 ^ 2) (EPINoiseExtension.liftMeasure3 P) ∧ MeasureTheory.Integrable (fun (p : Ω × ℝ × ℝ × ℝ) => (X p.1 + Y p.1) ^ 2) (EPINoiseExtension.liftMeasure3 P)

Used by

theorem

InformationTheory.Shannon.EPIDensityForm.iIndepFun_liftMeasure3_of_indep

source

ProbabilityTheory.iIndepFun ![fun (p : Ω × ℝ × ℝ × ℝ) => X p.1, fun (p : Ω × ℝ × ℝ × ℝ) => Y p.1, fun (p : Ω × ℝ × ℝ × ℝ) => p.2.1, fun (p : Ω × ℝ × ℝ × ℝ) => p.2.2.1, fun (p : Ω × ℝ × ℝ × ℝ) => p.2.2.2] (EPINoiseExtension.liftMeasure3 P)

Used by

theorem

InformationTheory.Shannon.EPIDensityForm.liftMeasure3_pairwise_indep

source

{Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X' Y' ZX ZY Z : Ω × ℝ × ℝ × ℝ → ℝ} (hX'_meas : Measurable X') (hY'_meas : Measurable Y') (hZX_meas : Measurable ZX) (hZY_meas : Measurable ZY) (hZ_meas : Measurable Z) (h_iIndep : ProbabilityTheory.iIndepFun ![X', Y', ZX, ZY, Z] (EPINoiseExtension.liftMeasure3 P)) :

ProbabilityTheory.IndepFun X' ZX (EPINoiseExtension.liftMeasure3 P) ∧ ProbabilityTheory.IndepFun Y' ZY (EPINoiseExtension.liftMeasure3 P) ∧ ProbabilityTheory.IndepFun X' Y' (EPINoiseExtension.liftMeasure3 P) ∧ ProbabilityTheory.IndepFun ZX ZY (EPINoiseExtension.liftMeasure3 P) ∧ ProbabilityTheory.IndepFun (fun (p : Ω × ℝ × ℝ × ℝ) => (X' p, ZX p)) (fun (p : Ω × ℝ × ℝ × ℝ) => (Y' p, ZY p)) (EPINoiseExtension.liftMeasure3 P) ∧ ProbabilityTheory.IndepFun (fun (p : Ω × ℝ × ℝ × ℝ) => X' p + Y' p) Z (EPINoiseExtension.liftMeasure3 P) ∧ ProbabilityTheory.IndepFun (fun (p : Ω × ℝ × ℝ × ℝ) => X' p + Y' p) (fun (p : Ω × ℝ × ℝ × ℝ) => (ZX p, ZY p)) (EPINoiseExtension.liftMeasure3 P)

Used by

theorem

InformationTheory.Shannon.EPIDensityForm.entropy_power_inequality_of_density

source

EntropyPowerInequality.entropyPower (MeasureTheory.Measure.map (fun (ω : Ω) => X ω + Y ω) P) ≥ EntropyPowerInequality.entropyPower (MeasureTheory.Measure.map X P) + EntropyPowerInequality.entropyPower (MeasureTheory.Measure.map Y P)

Entropy power inequality for absolutely continuous distributions with regular densities.

All 16 hypotheses are regularity preconditions (measurability, independence, absolute continuity, finite second moment, IsRegularDensityV2, normalization, IsBlachmanConvReady, finite Fisher information, finite entropy) for X, Y, and X + Y; they do not encode the EPI inequality core. The proof derives EPI via a 3-noise lift and two-time terminal.

Used by