InformationTheory.Shannon.EPI.Unconditional.DispatchFull

Imports 3

Entropy power inequality — fully unconditional dispatch #

The fully unconditional entropy power inequality entropyPowerExt_add_ge, taking only (hX hY : Measurable) (hXY : IndepFun X Y P), built from the unconditional gateway lemmas.

Main statements #

entropyPowerExt_add_ge — the unconditional ℝ≥0∞ entropy power inequality.
entropyPowerExt_mixed_add_ge / _symm — the mixed cases (one factor a.c., the other singular), via gateway monotonicity.
entropyPowerExt_add_ge_case1 — case 1 (both a.c.), splitting on ⊤/⊥/finite of the three differential entropies and delegating to entropyPowerExt_add_ge_finite_ac.

Implementation notes #

The 21-precondition dispatch entropyPowerExt_add_ge_dispatch_skeleton is a separate route; this file builds the gateway-based unconditional version independently of it.
Every declaration delegates to an existing gateway lemma or bridge; the only work is plumbing (order lemmas, EReal.exp expansion, add_comm reshaping).

theorem

InformationTheory.Shannon.entropyPowerExt_mixed_add_ge

source

{Ω : Type u_1} [MeasurableSpace Ω] (X Y : Ω → ℝ) (P : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure P] (hX : Measurable X) (hY : Measurable Y) (hXY : ProbabilityTheory.IndepFun X Y P) (hX_ac : (MeasureTheory.Measure.map X P).AbsolutelyContinuous MeasureTheory.volume) (hY_sing : ¬(MeasureTheory.Measure.map Y P).AbsolutelyContinuous MeasureTheory.volume) :

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

Case 2 (X a.c., Y singular): since N(Y) = 0, the RHS is N(X), and gateway monotonicity gives N(X+Y) ≥ N(X). The only hypotheses are hX hY hXY hX_ac hY_sing.

@audit:ok

Used by

theorem

InformationTheory.Shannon.entropyPowerExt_mixed_add_ge_symm

source

{Ω : Type u_1} [MeasurableSpace Ω] (X Y : Ω → ℝ) (P : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure P] (hX : Measurable X) (hY : Measurable Y) (hXY : ProbabilityTheory.IndepFun X Y P) (hY_ac : (MeasureTheory.Measure.map Y P).AbsolutelyContinuous MeasureTheory.volume) (hX_sing : ¬(MeasureTheory.Measure.map X P).AbsolutelyContinuous MeasureTheory.volume) :

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

Case 2 symmetric (Y a.c., X singular): since N(X) = 0, the RHS is N(Y), and gateway monotonicity (W = Y, V = X) gives N(Y+X) ≥ N(Y), reshaped to X+Y by add_comm. The only hypotheses are hX hY hXY hY_ac hX_sing.

@audit:ok

Used by

theorem

InformationTheory.Shannon.entropyPowerExt_add_ge_case1

source

{Ω : Type u_1} [MeasurableSpace Ω] (X Y : Ω → ℝ) (P : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure P] (hX : Measurable X) (hY : Measurable Y) (hXY : ProbabilityTheory.IndepFun X Y P) (hX_ac : (MeasureTheory.Measure.map X P).AbsolutelyContinuous MeasureTheory.volume) (hY_ac : (MeasureTheory.Measure.map Y P).AbsolutelyContinuous MeasureTheory.volume) :

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

Case 1 (both a.c.), with no finite-entropy hypotheses. Splits on ⊤/⊥/finite of h(X+Y), h(X), h(Y): the ⊤/⊥ branches collapse one RHS term via gateway monotonicity, and the all-finite branch supplies the three integrability hypotheses through the bridge differentialEntropyExt_integrable_of_finite and delegates to entropyPowerExt_add_ge_finite_ac. The only hypotheses are hX hY hXY hX_ac hY_ac.

@audit:ok

Used by

theorem

InformationTheory.Shannon.entropyPowerExt_add_ge

source

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

The fully unconditional extended-real entropy power inequality N(X+Y) ≥ N(X) + N(Y), taking only hX hY hXY. The four-case split on absolute continuity of P.map X and P.map Y delegates to entropyPowerExt_add_ge_case1 (both a.c.), entropyPowerExt_mixed_add_ge / _symm (mixed), and entropyPowerExt_singular_add_ge (both singular).

@audit:ok

Used by