InformationTheory.Shannon.EPI.Unconditional.Dispatch
Entropy power inequality — case-1 dispatch #
The two-a.c. classical entropy power inequality N(X+Y) ≥ N(X) + N(Y) (case 1 of the
absolute-continuity case split) together with the four-case dispatch skeleton that combines it
with the mixed and singular cases.
Main statements #
entropyPowerExt_add_ge_finite_ac— case 1 (both push-forwards a.c. with finite differential entropy): the extended-real entropy power inequality, split by finiteness of variance.entropy_power_inequality_of_ac— the real-valued entropy power inequality under absolute continuity and finite differential entropy.
Implementation notes #
- This file sits downstream of both
EPIUncondMixedCaseandEPICase1SmoothingLimitso that the case-1 lemma can delegate toEPICase1SmoothingLimit.entropyPowerExt_add_ge_of_finite_variance. Placing the dispatch in either of those files instead would introduce an import cycle, sinceEPICase1SmoothingLimitalready (transitively) importsEPIUncondMixedCase. - Case 1 is split by whether both inputs have finite variance: the finite-variance branch
delegates to the smoothing-limit closure, the infinite-variance branch to the conditioning
truncation (route T) closure. Both branches are
sorryAx-free.
InformationTheory.Shannon.entropyPowerExt_add_ge_finite_ac
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)
(hX_ent :
MeasureTheory.Integrable
(fun (x : ℝ) => ((MeasureTheory.Measure.map X P).rnDeriv MeasureTheory.volume x).toReal.negMulLog)
MeasureTheory.volume)
(hY_ent :
MeasureTheory.Integrable
(fun (x : ℝ) => ((MeasureTheory.Measure.map Y P).rnDeriv MeasureTheory.volume x).toReal.negMulLog)
MeasureTheory.volume)
(hW_ent :
MeasureTheory.Integrable
(fun (x : ℝ) =>
((MeasureTheory.Measure.map (fun (ω : Ω) => X ω + Y ω) P).rnDeriv MeasureTheory.volume x).toReal.negMulLog)
MeasureTheory.volume)
:
entropyPowerExt (MeasureTheory.Measure.map (fun (ω : Ω) => X ω + Y ω) P) ≥ entropyPowerExt (MeasureTheory.Measure.map X P) + entropyPowerExt (MeasureTheory.Measure.map Y P)
The classical entropy power inequality N(X+Y) ≥ N(X) + N(Y) when both P.map X and
P.map Y are absolutely continuous and have finite differential entropy. The proof splits on
whether both inputs have finite variance: the finite-variance branch delegates to the
smoothing-limit closure, the infinite-variance branch to the conditioning-truncation (route T)
closure. The hypotheses hX_ent/hY_ent/hW_ent are finite-differential-entropy regularity
preconditions.
@audit:ok
Used by
InformationTheory.Shannon.entropyPowerExt_add_ge_dispatch_skeleton
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)
(h_ac :
((MeasureTheory.Measure.map Y P).compProd
(ProbabilityTheory.condDistrib (fun (ω : Ω) => X ω + Y ω) Y P)).AbsolutelyContinuous
((MeasureTheory.Measure.map Y P).compProd
(ProbabilityTheory.Kernel.const ℝ (MeasureTheory.Measure.map (fun (ω : Ω) => X ω + Y ω) P))))
(h_int :
MeasureTheory.Integrable
(MeasureTheory.llr
((MeasureTheory.Measure.map Y P).compProd (ProbabilityTheory.condDistrib (fun (ω : Ω) => X ω + Y ω) Y P))
((MeasureTheory.Measure.map Y P).compProd
(ProbabilityTheory.Kernel.const ℝ (MeasureTheory.Measure.map (fun (ω : Ω) => X ω + Y ω) P))))
((MeasureTheory.Measure.map Y P).compProd (ProbabilityTheory.condDistrib (fun (ω : Ω) => X ω + Y ω) Y P)))
(hκ_v :
∀ᵐ (z : ℝ) ∂MeasureTheory.Measure.map Y P, ((ProbabilityTheory.condDistrib (fun (ω : Ω) => X ω + Y ω) Y P) z).AbsolutelyContinuous MeasureTheory.volume)
(hκ_logp_int :
∀ᵐ (z : ℝ) ∂MeasureTheory.Measure.map Y P, MeasureTheory.Integrable
(fun (x : ℝ) =>
(((ProbabilityTheory.condDistrib (fun (ω : Ω) => X ω + Y ω) Y P) z).rnDeriv MeasureTheory.volume x).toReal * Real.log
(((ProbabilityTheory.condDistrib (fun (ω : Ω) => X ω + Y ω) Y P) z).rnDeriv MeasureTheory.volume x).toReal)
MeasureTheory.volume)
(hκ_cross_int :
∀ᵐ (z : ℝ) ∂MeasureTheory.Measure.map Y P, MeasureTheory.Integrable
(fun (x : ℝ) =>
(((ProbabilityTheory.condDistrib (fun (ω : Ω) => X ω + Y ω) Y P) z).rnDeriv MeasureTheory.volume x).toReal * Real.log ((MeasureTheory.Measure.map (fun (ω : Ω) => X ω + Y ω) P).rnDeriv MeasureTheory.volume x).toReal)
MeasureTheory.volume)
(h_fibreEnt_int :
MeasureTheory.Integrable
(fun (z : ℝ) => differentialEntropy ((ProbabilityTheory.condDistrib (fun (ω : Ω) => X ω + Y ω) Y P) z))
(MeasureTheory.Measure.map Y P))
(h_cross_int :
MeasureTheory.Integrable
(fun (z : ℝ) =>
∫ (x : ℝ), (((ProbabilityTheory.condDistrib (fun (ω : Ω) => X ω + Y ω) Y P) z).rnDeriv MeasureTheory.volume x).toReal * Real.log ((MeasureTheory.Measure.map (fun (ω : Ω) => X ω + Y ω) P).rnDeriv MeasureTheory.volume x).toReal)
(MeasureTheory.Measure.map Y P))
(h_logq_int :
MeasureTheory.Integrable
(fun (x : ℝ) =>
Real.log ((MeasureTheory.Measure.map (fun (ω : Ω) => X ω + Y ω) P).rnDeriv MeasureTheory.volume x).toReal)
(MeasureTheory.Measure.map (fun (ω : Ω) => X ω + Y ω) P))
(h_ac_symm :
((MeasureTheory.Measure.map X P).compProd
(ProbabilityTheory.condDistrib (fun (ω : Ω) => Y ω + X ω) X P)).AbsolutelyContinuous
((MeasureTheory.Measure.map X P).compProd
(ProbabilityTheory.Kernel.const ℝ (MeasureTheory.Measure.map (fun (ω : Ω) => Y ω + X ω) P))))
(h_int_symm :
MeasureTheory.Integrable
(MeasureTheory.llr
((MeasureTheory.Measure.map X P).compProd (ProbabilityTheory.condDistrib (fun (ω : Ω) => Y ω + X ω) X P))
((MeasureTheory.Measure.map X P).compProd
(ProbabilityTheory.Kernel.const ℝ (MeasureTheory.Measure.map (fun (ω : Ω) => Y ω + X ω) P))))
((MeasureTheory.Measure.map X P).compProd (ProbabilityTheory.condDistrib (fun (ω : Ω) => Y ω + X ω) X P)))
(hκ_v_symm :
∀ᵐ (z : ℝ) ∂MeasureTheory.Measure.map X P, ((ProbabilityTheory.condDistrib (fun (ω : Ω) => Y ω + X ω) X P) z).AbsolutelyContinuous MeasureTheory.volume)
(hκ_logp_int_symm :
∀ᵐ (z : ℝ) ∂MeasureTheory.Measure.map X P, MeasureTheory.Integrable
(fun (x : ℝ) =>
(((ProbabilityTheory.condDistrib (fun (ω : Ω) => Y ω + X ω) X P) z).rnDeriv MeasureTheory.volume x).toReal * Real.log
(((ProbabilityTheory.condDistrib (fun (ω : Ω) => Y ω + X ω) X P) z).rnDeriv MeasureTheory.volume x).toReal)
MeasureTheory.volume)
(hκ_cross_int_symm :
∀ᵐ (z : ℝ) ∂MeasureTheory.Measure.map X P, MeasureTheory.Integrable
(fun (x : ℝ) =>
(((ProbabilityTheory.condDistrib (fun (ω : Ω) => Y ω + X ω) X P) z).rnDeriv MeasureTheory.volume x).toReal * Real.log ((MeasureTheory.Measure.map (fun (ω : Ω) => Y ω + X ω) P).rnDeriv MeasureTheory.volume x).toReal)
MeasureTheory.volume)
(h_fibreEnt_int_symm :
MeasureTheory.Integrable
(fun (z : ℝ) => differentialEntropy ((ProbabilityTheory.condDistrib (fun (ω : Ω) => Y ω + X ω) X P) z))
(MeasureTheory.Measure.map X P))
(h_cross_int_symm :
MeasureTheory.Integrable
(fun (z : ℝ) =>
∫ (x : ℝ), (((ProbabilityTheory.condDistrib (fun (ω : Ω) => Y ω + X ω) X P) z).rnDeriv MeasureTheory.volume x).toReal * Real.log ((MeasureTheory.Measure.map (fun (ω : Ω) => Y ω + X ω) P).rnDeriv MeasureTheory.volume x).toReal)
(MeasureTheory.Measure.map X P))
(h_logq_int_symm :
MeasureTheory.Integrable
(fun (x : ℝ) =>
Real.log ((MeasureTheory.Measure.map (fun (ω : Ω) => Y ω + X ω) P).rnDeriv MeasureTheory.volume x).toReal)
(MeasureTheory.Measure.map (fun (ω : Ω) => Y ω + X ω) P))
(hX_ent :
MeasureTheory.Integrable
(fun (x : ℝ) => ((MeasureTheory.Measure.map X P).rnDeriv MeasureTheory.volume x).toReal.negMulLog)
MeasureTheory.volume)
(hW_ent :
MeasureTheory.Integrable
(fun (x : ℝ) =>
((MeasureTheory.Measure.map (fun (ω : Ω) => X ω + Y ω) P).rnDeriv MeasureTheory.volume x).toReal.negMulLog)
MeasureTheory.volume)
(hY_ent :
MeasureTheory.Integrable
(fun (x : ℝ) => ((MeasureTheory.Measure.map Y P).rnDeriv MeasureTheory.volume x).toReal.negMulLog)
MeasureTheory.volume)
(hWyx_ent :
MeasureTheory.Integrable
(fun (x : ℝ) =>
((MeasureTheory.Measure.map (fun (ω : Ω) => Y ω + X ω) P).rnDeriv MeasureTheory.volume x).toReal.negMulLog)
MeasureTheory.volume)
:
entropyPowerExt (MeasureTheory.Measure.map (fun (ω : Ω) => X ω + Y ω) P) ≥ entropyPowerExt (MeasureTheory.Measure.map X P) + entropyPowerExt (MeasureTheory.Measure.map Y P)
Four-case dispatch for the extended-real entropy power inequality, splitting on absolute
continuity of P.map X and P.map Y: both a.c. delegates to entropyPowerExt_add_ge_finite_ac,
the mixed cases to entropyPowerExt_mixed_add_ge_of_regular / _symm_of_regular, and the
doubly-singular case to entropyPowerExt_singular_add_ge. The integrability and finite-entropy
hypotheses are path-dependent regularity preconditions threaded into the mixed-case lemmas.
@audit:superseded-by(entropyPowerExt_add_ge) The fully unconditional version
entropyPowerExt_add_ge (in EPI.Unconditional.DispatchFull, taking only hX hY hXY) is the
canonical headline; this skeleton is retained as a proof-done leaf with no consumers.
@audit:ok
Used by
InformationTheory.Shannon.entropy_power_inequality_of_ac
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)
(hX_ent :
MeasureTheory.Integrable
(fun (x : ℝ) => ((MeasureTheory.Measure.map X P).rnDeriv MeasureTheory.volume x).toReal.negMulLog)
MeasureTheory.volume)
(hY_ent :
MeasureTheory.Integrable
(fun (x : ℝ) => ((MeasureTheory.Measure.map Y P).rnDeriv MeasureTheory.volume x).toReal.negMulLog)
MeasureTheory.volume)
(hW_ent :
MeasureTheory.Integrable
(fun (x : ℝ) =>
((MeasureTheory.Measure.map (fun (ω : Ω) => X ω + Y ω) P).rnDeriv MeasureTheory.volume x).toReal.negMulLog)
MeasureTheory.volume)
:
EntropyPowerInequality.entropyPower (MeasureTheory.Measure.map (fun (ω : Ω) => X ω + Y ω) P) ≥ EntropyPowerInequality.entropyPower (MeasureTheory.Measure.map X P) + EntropyPowerInequality.entropyPower (MeasureTheory.Measure.map Y P)
The real-valued entropy power inequality N(X+Y) ≥ N(X) + N(Y) (with entropyPower μ = exp (2 · h μ)) for independent X, Y whose push-forwards are absolutely continuous with finite
differential entropy. The inequality is supplied by the extended-real version
entropyPowerExt_add_ge_finite_ac; this lemma only transports it across ℝ≥0∞ → ℝ via
entropyPowerExt_of_ac_integrable.
@audit:ok