InformationTheory.Shannon.EPI.Case1.TwoTime.EntropyPowerInequality

Imports 23

EPI case-1 two-time object — entropy power inequality bridge (§4 terminal) #

The entropy power inequality bridge for the two-time object: epi_of_twoTimeLogRatioGap_zero_nonneg / epi_of_twoTimeLogRatioGap_tendsto turn the gap's nonnegativity at 0 (delivered by antitonicity plus the saturation limit) into N(X + Y) ≥ N(X) + N(Y), and the terminal entropyPower_add_ge_case1_of_regular_twotime assembles the matched-path producer with the three genuine pillars. Verbatim split of TwoTime.lean §4 (EPI bridge / terminal part); proofs unchanged. Builds on TwoTime.GapDerivative (gap object) and TwoTime.MonotonicityAndSaturation (antitonicity / saturation). Umbrella: TwoTime.lean.

theorem

InformationTheory.Shannon.EPICase1TwoTime.epi_of_twoTimeLogRatioGap_zero_nonneg

source

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

Nonnegativity of the two-time log-ratio gap at 0 gives the entropy power inequality N(X + Y) ≥ N(X) + N(Y).

twoTimeLogRatioGap_at_zero rewrites R 0 to the EPI bridge form, so R 0 ≥ 0 ⟺ entropyPower (X+Y) ≥ entropyPower X + entropyPower Y. Mirrors epi_of_csiszarLogRatioGap_zero_nonneg (EPI/Stam/ToBridge.lean). @audit:ok

Used by

theorem

InformationTheory.Shannon.EPICase1TwoTime.epi_of_twoTimeLogRatioGap_tendsto

source

{Ω : Type u_1} {mΩ : MeasurableSpace Ω} (X Y Z_X Z_Y : Ω → ℝ) (P : MeasureTheory.Measure Ω) {J_X J_Y s r : ℝ → ℝ} (h_path_X : IsMatchedTimePath X Z_X P J_X s) (h_path_Y : IsMatchedTimePath Y Z_Y P J_Y r) (h_anti : AntitoneOn (fun (t : ℝ) => twoTimeLogRatioGap X Y Z_X Z_Y P s r t) (Set.Ici 0)) (h_lim : Filter.Tendsto (fun (t : ℝ) => twoTimeLogRatioGap X Y Z_X Z_Y P s r t) Filter.atTop (nhds 0)) :

TT EPI via tendsto — antitonicity + R(t) → 0 give R(0) ≥ 0, hence EPI.

Order-limit bridge (le_of_tendsto) over twoTimeLogRatioGap_antitoneOn_Ici_zero

twoTimeLogRatioGap_tendsto_zero_atTop, then epi_of_twoTimeLogRatioGap_zero_nonneg. Mirrors epi_of_csiszarLogRatioGap_tendsto (EPI/Case1/RatioLimit/PathRegular.lean). @audit:ok

Used by

theorem

InformationTheory.Shannon.EPICase1TwoTime.heatFlowEP_hasDerivAt_of_regular

source

{Ω : Type u_1} {mΩ : MeasurableSpace Ω} (X Z : Ω → ℝ) (P : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure P] (hX : Measurable X) (hZ : Measurable Z) (hXZ : ProbabilityTheory.IndepFun X Z P) {σ : ℝ} (hσ : 0 < σ) (h_reg : FisherInfo.IsRegularDeBruijnHypV2 X Z P σ) :

HasDerivAt (fun (u : ℝ) => heatFlowEP X Z P u) (heatFlowEP X Z P σ * FisherInfo.fisherInfoOfDensityReal h_reg.density_t) σ

Used by

theorem

InformationTheory.Shannon.EPICase1TwoTime.heatFlowEP_tendsto_atTop

source

{Ω : Type u_1} {mΩ : MeasurableSpace Ω} (X Z : Ω → ℝ) (P : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure P] (hX : Measurable X) (hZ : Measurable Z) (hZ_law : MeasureTheory.Measure.map Z P = ProbabilityTheory.gaussianReal 0 1) (hZ_ac : (MeasureTheory.Measure.map Z P).AbsolutelyContinuous MeasureTheory.volume) (h_scale : ∀ (σ : ℝ), 0 < σ → (MeasureTheory.Measure.map (fun (ω : Ω) => X ω / √σ + Z ω) P).AbsolutelyContinuous MeasureTheory.volume ∧ MeasureTheory.Integrable (fun (x : ℝ) => ((MeasureTheory.Measure.map (fun (ω : Ω) => X ω / √σ + Z ω) P).rnDeriv MeasureTheory.volume x).toReal.negMulLog) MeasureTheory.volume) (var : ℝ) (h_var_nn : 0 ≤ var) (h_rescale : EPICase1RatioLimit.IsRescaledPathRegular X Z P var 1) :

Filter.Tendsto (fun (s : ℝ) => heatFlowEP X Z P s) Filter.atTop Filter.atTop

Used by

theorem

InformationTheory.Shannon.EPICase1TwoTime.entropyPower_add_ge_case1_of_regular_twotime

source

The case-1 entropy power inequality in two-time form, the two-time analog of the single-t entropyPower_add_ge_case1_of_regular (EPI/Case1/RatioLimit/Assembly.lean).

N(X+Y) ≥ N(X) + N(Y), assembled from the three GENUINE two-time pillars (twoTimeLogRatioGap_antitoneOn_Ici_zero, twoTimeLogRatioGap_tendsto_zero_atTop, epi_of_twoTimeLogRatioGap_tendsto) + the path producer matchedTimePath_exists. Unlike the single-t route (whose sum derivative is the variance-2 2·J_sum that does NOT close from harmonic Stam), the two-time object perturbs X/Y at independent matched times s(t)/r(t) and closes from the genuine harmonic Stam producer.

J_X/J_Y Fisher pin (honesty-load-bearing). The Fisher infos are NOT free variables: J_X/J_Y are defined as the total-domain functions fun σ ↦ if 0 < σ then fisherInfoOfDensityReal ((h_reg_*.reg_at σ _).density_t) else 0. The same quantity supplies both (a) matchedTimePath_exists's entropy-power HasDerivAt (via deBruijn_identity_v2 → entropyPower_hasDerivAt_of_diffEnt_hasDerivAt) and (b) Pillar B's per-t density-pin (dif_pos under s t > 0). density_t is pointwise-pinned by IsRegularDeBruijnHypV2.density_t_eq (∀ x, NOT a.e.), so a representative escape is structurally impossible — the same honest mechanism as twoTimeLogRatioGap_hasDerivAt.

Preconditions are the union of matchedTimePath_exists (×2) + Pillar B + Pillar C regularity, deduplicated. None encode the EPI conclusion (the same precondition union as the single-t form in EPI/Case1/RatioLimit/Assembly.lean, itself @audit:ok):

h_endpt_X/h_endpt_Y (path-producer endpoint continuity), h_endpt_sum (Pillar B);
h_reg_X/h_reg_Y/h_reg_sum : IsDeBruijnRegularityHyp (de Bruijn + J pin);
h_scale_* per-σ a.c.+integrability (consumed by entropyPower_path_scaling, used both for the path-producer hN_tendsto and Pillar C);
h_rescale_* (IsRescaledPathRegular) + varX/varY/varS (Pillar C squeeze and the path-producer divergence);
h_stam_supply the per-time harmonic-Stam + positivity supply (genuine producer isStamInequalityHyp_of_indepFun, NOT a bundled conclusion — 1/J_S ≥ 1/J_X+1/J_Y is the Fisher form, a different statement from the EPI inequality). @audit:ok

Used by