InformationTheory.Shannon.EPI.Case1.RatioLimit.Assembly

Imports 11

§4 — Main analytic deliverable #

csiszarLogRatioGap_tendsto_zero_atTop: composing §2 (cancellation), §3 (per-path limits), and Gaussian additivity yields R t → 0.

theorem

InformationTheory.Shannon.EPICase1RatioLimit.csiszarLogRatioGap_tendsto_zero_atTop

source

{Ω : Type u_1} {mΩ : MeasurableSpace Ω} (X Y Z_X Z_Y : Ω → ℝ) (P : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure P] (hX : Measurable X) (hY : Measurable Y) (hZX : Measurable Z_X) (hZY : Measurable Z_Y) (v_X v_Y : NNReal) (hv_X : v_X ≠ 0) (hv_Y : v_Y ≠ 0) (hZX_law : MeasureTheory.Measure.map Z_X P = ProbabilityTheory.gaussianReal 0 v_X) (hZY_law : MeasureTheory.Measure.map Z_Y P = ProbabilityTheory.gaussianReal 0 v_Y) (hZXZY_indep : ProbabilityTheory.IndepFun Z_X Z_Y P) (h_scale_X : ∀ (t : ℝ), 0 < t → (MeasureTheory.Measure.map (fun (ω : Ω) => X ω / √t + Z_X ω) P).AbsolutelyContinuous MeasureTheory.volume ∧ MeasureTheory.Integrable (fun (x : ℝ) => ((MeasureTheory.Measure.map (fun (ω : Ω) => X ω / √t + Z_X ω) P).rnDeriv MeasureTheory.volume x).toReal.negMulLog) MeasureTheory.volume) (h_scale_Y : ∀ (t : ℝ), 0 < t → (MeasureTheory.Measure.map (fun (ω : Ω) => Y ω / √t + Z_Y ω) P).AbsolutelyContinuous MeasureTheory.volume ∧ MeasureTheory.Integrable (fun (x : ℝ) => ((MeasureTheory.Measure.map (fun (ω : Ω) => Y ω / √t + Z_Y ω) P).rnDeriv MeasureTheory.volume x).toReal.negMulLog) MeasureTheory.volume) (h_scale_sum : ∀ (t : ℝ), 0 < t → (MeasureTheory.Measure.map (fun (ω : Ω) => (X ω + Y ω) / √t + (Z_X ω + Z_Y ω)) P).AbsolutelyContinuous MeasureTheory.volume ∧ MeasureTheory.Integrable (fun (x : ℝ) => ((MeasureTheory.Measure.map (fun (ω : Ω) => (X ω + Y ω) / √t + (Z_X ω + Z_Y ω)) P).rnDeriv MeasureTheory.volume x).toReal.negMulLog) MeasureTheory.volume) (hZX_ac : (MeasureTheory.Measure.map Z_X P).AbsolutelyContinuous MeasureTheory.volume) (hZY_ac : (MeasureTheory.Measure.map Z_Y P).AbsolutelyContinuous MeasureTheory.volume) (hZXZY_ac : (MeasureTheory.Measure.map (fun (ω : Ω) => Z_X ω + Z_Y ω) P).AbsolutelyContinuous MeasureTheory.volume) (varX varY varS : ℝ) (h_varX_nn : 0 ≤ varX) (h_varY_nn : 0 ≤ varY) (h_varS_nn : 0 ≤ varS) (h_reg_X : IsRescaledPathRegular X Z_X P varX v_X) (h_reg_Y : IsRescaledPathRegular Y Z_Y P varY v_Y) (h_reg_S : IsRescaledPathRegular (fun (ω : Ω) => X ω + Y ω) (fun (ω : Ω) => Z_X ω + Z_Y ω) P varS (v_X + v_Y)) :

Filter.Tendsto (fun (t : ℝ) => EPIL3Integration.csiszarLogRatioGap X Y Z_X Z_Y P t) Filter.atTop (nhds 0)

R t → 0 as t → ∞ (entropic-CLT-free). Combining the scaling cancellation (entropyPower_path_scaling), the three per-path limits (entropyPower_rescaled_path_tendsto), Gaussian additivity of the noise (entropyPower_gaussian_additivity), and continuity of log on positive reals.

The per-t regularity (a.c. + entropy integrability of the three W-path laws for the scaling step; the §3 squeeze regularity bundles IsRescaledPathRegular for the three paths) is threaded as preconditions; the noise Gaussian laws + independence are regularity. No EPI / Stam core is bundled. @audit:ok

Used by

§5 — End-to-end case-1 assembly (with-noise) #

entropyPower_add_ge_case1_of_regular: combine the ratio antitonicity (csiszarLogRatioGap_antitoneOn_Ici_zero, EPI/Stam/ToBridge.lean) and the saturation (csiszarLogRatioGap_tendsto_zero_atTop, §4) through the order-limit bridge (§1 epi_of_csiszarLogRatioGap_tendsto) to obtain the classical (case-1, a.c. inputs) entropy power inequality. Pure assembly — no new analytic content, no sorry.

theorem

InformationTheory.Shannon.EPICase1RatioLimit.entropyPower_add_ge_case1_of_regular

source

{Ω : Type u_1} {mΩ : MeasurableSpace Ω} (X Y Z_X Z_Y : Ω → ℝ) (P : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure P] (hX : Measurable X) (hY : Measurable Y) (hZX : Measurable Z_X) (hZY : Measurable Z_Y) (hXZX : ProbabilityTheory.IndepFun X Z_X P) (hYZY : ProbabilityTheory.IndepFun Y Z_Y P) (hXYZXY : ProbabilityTheory.IndepFun (fun (ω : Ω) => X ω + Y ω) (fun (ω : Ω) => Z_X ω + Z_Y ω) P) (hZXZY_indep : ProbabilityTheory.IndepFun Z_X Z_Y P) (v_X v_Y : NNReal) (hv_X : v_X ≠ 0) (hv_Y : v_Y ≠ 0) (hZX_law : MeasureTheory.Measure.map Z_X P = ProbabilityTheory.gaussianReal 0 v_X) (hZY_law : MeasureTheory.Measure.map Z_Y P = ProbabilityTheory.gaussianReal 0 v_Y) (hZX_ac : (MeasureTheory.Measure.map Z_X P).AbsolutelyContinuous MeasureTheory.volume) (hZY_ac : (MeasureTheory.Measure.map Z_Y P).AbsolutelyContinuous MeasureTheory.volume) (hZXZY_ac : (MeasureTheory.Measure.map (fun (ω : Ω) => Z_X ω + Z_Y ω) P).AbsolutelyContinuous MeasureTheory.volume) (h_reg_sum : StamEPIBridge.IsDeBruijnRegularityHyp (fun (ω : Ω) => X ω + Y ω) (fun (ω : Ω) => Z_X ω + Z_Y ω) P) (h_reg_X' : StamEPIBridge.IsDeBruijnRegularityHyp X Z_X P) (h_reg_Y' : StamEPIBridge.IsDeBruijnRegularityHyp Y Z_Y P) (h_endpt_sum : IsHeatFlowEndpointRegular (fun (ω : Ω) => X ω + Y ω) (fun (ω : Ω) => Z_X ω + Z_Y ω) P) (h_endpt_X : IsHeatFlowEndpointRegular X Z_X P) (h_endpt_Y : IsHeatFlowEndpointRegular Y Z_Y P) (h_pos_stam : ∀ (t : ℝ) (ht : 0 < t), 0 < FisherInfo.fisherInfoOfDensityReal (h_reg_X'.reg_at t ht).density_t ∧ 0 < FisherInfo.fisherInfoOfDensityReal (h_reg_Y'.reg_at t ht).density_t ∧ 0 < FisherInfo.fisherInfoOfDensityReal (h_reg_sum.reg_at t ht).density_t ∧ StamEPIBridge.IsStamInequalityHyp (fun (ω : Ω) => X ω + √t * Z_X ω) (fun (ω : Ω) => Y ω + √t * Z_Y ω) P ∧ FisherInfo.IsRegularDensityV2 (h_reg_X'.reg_at t ht).density_t ∧ FisherInfo.IsRegularDensityV2 (h_reg_Y'.reg_at t ht).density_t ∧ ∫ (x : ℝ), (h_reg_X'.reg_at t ht).density_t x = 1 ∧ ∫ (x : ℝ), (h_reg_Y'.reg_at t ht).density_t x = 1 ∧ (∀ (x : ℝ), (h_reg_sum.reg_at t ht).density_t x = EPIConvDensity.convDensityAdd (h_reg_X'.reg_at t ht).density_t (h_reg_Y'.reg_at t ht).density_t x) ∧ EPIBlachmanDensity.IsBlachmanConvReady (h_reg_X'.reg_at t ht).density_t (h_reg_Y'.reg_at t ht).density_t) (h_scale_X : ∀ (t : ℝ), 0 < t → (MeasureTheory.Measure.map (fun (ω : Ω) => X ω / √t + Z_X ω) P).AbsolutelyContinuous MeasureTheory.volume ∧ MeasureTheory.Integrable (fun (x : ℝ) => ((MeasureTheory.Measure.map (fun (ω : Ω) => X ω / √t + Z_X ω) P).rnDeriv MeasureTheory.volume x).toReal.negMulLog) MeasureTheory.volume) (h_scale_Y : ∀ (t : ℝ), 0 < t → (MeasureTheory.Measure.map (fun (ω : Ω) => Y ω / √t + Z_Y ω) P).AbsolutelyContinuous MeasureTheory.volume ∧ MeasureTheory.Integrable (fun (x : ℝ) => ((MeasureTheory.Measure.map (fun (ω : Ω) => Y ω / √t + Z_Y ω) P).rnDeriv MeasureTheory.volume x).toReal.negMulLog) MeasureTheory.volume) (h_scale_sum : ∀ (t : ℝ), 0 < t → (MeasureTheory.Measure.map (fun (ω : Ω) => (X ω + Y ω) / √t + (Z_X ω + Z_Y ω)) P).AbsolutelyContinuous MeasureTheory.volume ∧ MeasureTheory.Integrable (fun (x : ℝ) => ((MeasureTheory.Measure.map (fun (ω : Ω) => (X ω + Y ω) / √t + (Z_X ω + Z_Y ω)) P).rnDeriv MeasureTheory.volume x).toReal.negMulLog) MeasureTheory.volume) (varX varY varS : ℝ) (h_varX_nn : 0 ≤ varX) (h_varY_nn : 0 ≤ varY) (h_varS_nn : 0 ≤ varS) (h_reg_X : IsRescaledPathRegular X Z_X P varX v_X) (h_reg_Y : IsRescaledPathRegular Y Z_Y P varY v_Y) (h_reg_S : IsRescaledPathRegular (fun (ω : Ω) => X ω + Y ω) (fun (ω : Ω) => Z_X ω + Z_Y ω) P varS (v_X + v_Y)) :

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

The classical entropy power inequality N(law(X+Y)) ≥ N(law X) + N(law Y) for absolutely continuous inputs, proved with auxiliary Gaussian noise and without an entropic CLT, under heat-flow and scaling regularity preconditions. It is assembled from the two pillars:

csiszarLogRatioGap_antitoneOn_Ici_zero (EPI/Stam/ToBridge.lean): the log-ratio gap R = csiszarLogRatioGap X Y Z_X Z_Y P is AntitoneOn (Set.Ici 0).
csiszarLogRatioGap_tendsto_zero_atTop (§4): R t → 0 as t → ∞.

By the order-limit bridge §1 epi_of_csiszarLogRatioGap_tendsto, antitonicity + R t → 0 force R 0 ≥ 0, hence EPI. No entropic CLT — the saturation R t → 0 is the scaling squeeze of §4.

All hypotheses are regularity preconditions, the union of the two pillars' preconditions: pairwise + joint independence (hXZX/hYZY/hXYZXY), the three IsDeBruijnRegularityHyp / IsHeatFlowEndpointRegular density-witness bundles, the per-t h_pos_stam Fisher/Stam/Blachman bundle (ratio antitone side), the noise Gaussian laws + a.c. (hZX_law/hZY_law/hZXZY_indep/hZX_ac/hZY_ac/hZXZY_ac), the per-t scaling regularity (h_scale_X/Y/sum), and the per-path variance data + three IsRescaledPathRegular bundles (§4 side). None is load-bearing: the EPI / Stam core is supplied inside the two pillars; the conclusion N(X+Y) ≥ N(X)+N(Y) is not encoded in any hypothesis. The _of_regular suffix records that those regularity preconditions are real and not removable here.

@audit:ok @audit:superseded-by(entropyPowerExt_add_ge) Superseded by the unconditional EPI; the sole consumer entropyPower_add_ge_case1_of_methodX is a dead leaf. Retained as proof-done. The two-time variant entropyPower_add_ge_case1_of_regular_twotime is separate and live.

Used by

theorem

InformationTheory.Shannon.EPICase1RatioLimit.variance_rescaledPath_le

source

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

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

Used by

theorem

InformationTheory.Shannon.EPICase1RatioLimit.rescaledPath_ac_and_negMulLog_integrable

source

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

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

Used by

theorem

InformationTheory.Shannon.EPICase1RatioLimit.entropyPower_add_ge_case1_of_methodX

source

{Ω : Type u_1} {mΩ : MeasurableSpace Ω} (X Y Z_X Z_Y : Ω → ℝ) (P : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure P] (hX : Measurable X) (hY : Measurable Y) (hZX : Measurable Z_X) (hZY : Measurable Z_Y) (hX_ac : (MeasureTheory.Measure.map X P).AbsolutelyContinuous MeasureTheory.volume) (hY_ac : (MeasureTheory.Measure.map Y P).AbsolutelyContinuous MeasureTheory.volume) (hXY_ac : (MeasureTheory.Measure.map (fun (ω : Ω) => X ω + Y ω) P).AbsolutelyContinuous MeasureTheory.volume) (h_mom_X : MeasureTheory.Integrable (fun (ω : Ω) => X ω ^ 2) P) (h_mom_Y : MeasureTheory.Integrable (fun (ω : Ω) => Y ω ^ 2) P) (hZX_law : MeasureTheory.Measure.map Z_X P = ProbabilityTheory.gaussianReal 0 1) (hZY_law : MeasureTheory.Measure.map Z_Y P = ProbabilityTheory.gaussianReal 0 1) (h_iIndep : ProbabilityTheory.iIndepFun ![X, Y, Z_X, Z_Y] P) (h_reg_sum : StamEPIBridge.IsDeBruijnRegularityHyp (fun (ω : Ω) => X ω + Y ω) (fun (ω : Ω) => Z_X ω + Z_Y ω) P) (h_reg_X' : StamEPIBridge.IsDeBruijnRegularityHyp X Z_X P) (h_reg_Y' : StamEPIBridge.IsDeBruijnRegularityHyp Y Z_Y P) (h_endpt_sum : IsHeatFlowEndpointRegular (fun (ω : Ω) => X ω + Y ω) (fun (ω : Ω) => Z_X ω + Z_Y ω) P) (h_endpt_X : IsHeatFlowEndpointRegular X Z_X P) (h_endpt_Y : IsHeatFlowEndpointRegular Y Z_Y P) (h_pos_stam : ∀ (t : ℝ) (ht : 0 < t), 0 < FisherInfo.fisherInfoOfDensityReal (h_reg_X'.reg_at t ht).density_t ∧ 0 < FisherInfo.fisherInfoOfDensityReal (h_reg_Y'.reg_at t ht).density_t ∧ 0 < FisherInfo.fisherInfoOfDensityReal (h_reg_sum.reg_at t ht).density_t ∧ StamEPIBridge.IsStamInequalityHyp (fun (ω : Ω) => X ω + √t * Z_X ω) (fun (ω : Ω) => Y ω + √t * Z_Y ω) P ∧ FisherInfo.IsRegularDensityV2 (h_reg_X'.reg_at t ht).density_t ∧ FisherInfo.IsRegularDensityV2 (h_reg_Y'.reg_at t ht).density_t ∧ ∫ (x : ℝ), (h_reg_X'.reg_at t ht).density_t x = 1 ∧ ∫ (x : ℝ), (h_reg_Y'.reg_at t ht).density_t x = 1 ∧ (∀ (x : ℝ), (h_reg_sum.reg_at t ht).density_t x = EPIConvDensity.convDensityAdd (h_reg_X'.reg_at t ht).density_t (h_reg_Y'.reg_at t ht).density_t x) ∧ EPIBlachmanDensity.IsBlachmanConvReady (h_reg_X'.reg_at t ht).density_t (h_reg_Y'.reg_at t ht).density_t) :

Case-1 EPI under method-X regularity (entropic-CLT-free, unit-noise form). N(P.map(X+Y)) ≥ N(P.map X) + N(P.map Y) for a.c. inputs, reduced to method-X regularity (a.c. inputs + finite second moments + standard-normal 𝒩(0,1) noise laws + 4-tuple independence) plus de Bruijn per-time regularity.

On the unit-noise restriction and non-vacuity: the conclusion N(X+Y) ≥ N(X)+N(Y) does not mention the noise, so the noise is an auxiliary variable and fixing its law to 𝒩(0,1) loses no generality. Unit variance is what makes the threaded IsDeBruijnRegularityHyp group supplyable at all: its reg_at t ht .Z_law (= IsRegularDeBruijnHypV2.Z_law, FisherInfo/DeBruijn.lean) hardcodes P.map Z_X = gaussianReal 0 1, so under any other noise variance that field and hZX_law are mutually unsatisfiable and the premises are never jointly inhabitable. The body re-introduces v_X v_Y := (1 : ℝ≥0) existentially to keep the _of_regular plumbing (general v_B on the §4 saturation side) unchanged, and that step is honest (not circular := h, not :True): the obtain supplying ∃ v : ℝ≥0, v ≠ 0 ∧ P.map Z_X = gaussianReal 0 v re-derives that shape at the witness v = 1 carried by the unit hypothesis. The threaded IsDeBruijnRegularityHyp / h_reg_* are preconditions (residuals live in the producer's integrable_deriv, see isDeBruijnRegularityHyp_of_methodX_unitnoise). Not @audit:ok only because it threads residual-carrying regularity hyps.

This wrapper supplies the derivable preconditions of entropyPower_add_ge_case1_of_regular from clean method-X data:

noise a.c. (hZX_ac/hZY_ac/hZXZY_ac) via gaussianReal_absolutelyContinuous
- map_add_absolutelyContinuous;
the four individual independences from the single 4-tuple iIndepFun ![X,Y,Z_X,Z_Y] P (pairwise via iIndepFun.indepFun, joint via iIndepFun.indepFun_prodMk_prodMk + IndepFun.comp);
the three IsRescaledPathRegular bundles via isRescaledPathRegular_of_methodX;
the per-t scaling regularity (h_scale_*) via the B(i)-identical density-witness plumbing (rescaledInput_density_witness + pPath_eq_convDensityAdd + convDensityAdd_negMulLog_integrable_pub);
the variance bounds (varX/Y/S := Var[·;P]) via IndepFun.variance_fun_add + variance scaling, which hold with equality.

The de Bruijn per-time regularity group (h_reg_*' / h_endpt_* / h_pos_stam) is not supplied from method-X (it depends on epi-debruijn-pertime-closure) and is threaded as a precondition.

@audit:superseded-by(entropyPowerExt_add_ge) No consumers, and the de Bruijn per-time regularity group is still open (@residual below). Superseded by the unconditional EPI. The de Bruijn closure epi-debruijn-pertime-closure remains a valid standalone goal independently of this supersession. @residual(plan:epi-debruijn-pertime-closure)

Used by