InformationTheory.Shannon.EPI.Unconditional.MixedCase
Entropy power inequality — singular and mixed cases #
The entropy power inequality for the singular and mixed cases of the absolute-continuity split:
case 3 (both push-forwards singular) and case 2 (X a.c., Y singular).
Main statements #
entropyPowerExt_singular_add_ge— case 3 (both singular): RHS= 0, closed byzero_le.map_add_absolutelyContinuous—Xa.c. andX ⊥ Y ⟹ X+Ya.c. (convolution).differentialEntropy_add_ge_of_indep— the real coreh(X) ≤ h(X+Y).entropyPowerExt_mixed_add_ge_of_regular/_symm_of_regular— case 2 lifted toℝ≥0∞.
Implementation notes #
- The integrability hypotheses of the mixed-case lemmas are regularity preconditions (a.c. density
of
X+Yand fiber regularity), passed explicitly rather than bundled into a predicate. - In case 3,
RHS = 0is the genuine value: the entropy power of a singular measure is0.
InformationTheory.Shannon.entropyPowerExt_singular_add_ge
source{Ω : Type u_1}
[MeasurableSpace Ω]
(X Y : Ω → ℝ)
(P : MeasureTheory.Measure Ω)
(hX_sing : ¬(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 3 (both singular): if X and Y are both singular, then N(X+Y) ≥ N(X) + N(Y) = 0. The
RHS is 0 (the genuine entropy-power value of a singular measure), so the inequality holds by
zero_le regardless of whether X+Y is a.c.
@audit:ok
Used by
InformationTheory.Shannon.map_add_absolutelyContinuous
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)
:
(MeasureTheory.Measure.map (fun (ω : Ω) => X ω + Y ω) P).AbsolutelyContinuous MeasureTheory.volume
Convolution preserves absolute continuity: X a.c. and X ⊥ Y ⟹ X+Y a.c. The sum law factors
as the convolution μ.map X ∗ μ.map Y (independence), and conv_absolutelyContinuous propagates
absolute continuity of the a.c. factor.
@audit:ok
Used by
InformationTheory.Shannon.differentialEntropy_add_ge_of_indep
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)
(hW_ac : (MeasureTheory.Measure.map (fun (ω : Ω) => X ω + Y ω) P).AbsolutelyContinuous MeasureTheory.volume)
(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))
:
differentialEntropy (MeasureTheory.Measure.map X P) ≤ differentialEntropy (MeasureTheory.Measure.map (fun (ω : Ω) => X ω + Y ω) P)
The real core of case 2: h(X) ≤ h(X+Y). Combines the fiber identification
condDifferentialEntropy (X+Y) Y P = h(X) (condDifferentialEntropy_indep_add_eq at c = 1) with
the conditioning bound h(X+Y | Y) ≤ h(X+Y) (condDifferentialEntropy_le). The integrability
hypotheses are regularity preconditions (a.c. density of X+Y and fiber regularity).
@audit:ok
Used by
InformationTheory.Shannon.entropyPowerExt_mixed_add_ge_of_regular
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)
(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))
(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)
:
entropyPowerExt (MeasureTheory.Measure.map (fun (ω : Ω) => X ω + Y ω) P) ≥ entropyPowerExt (MeasureTheory.Measure.map X P) + entropyPowerExt (MeasureTheory.Measure.map Y P)
Case 2 lifted to ℝ≥0∞ (X a.c., Y singular): N(X+Y) ≥ N(X) + N(Y). Since N(Y) = 0, the
RHS is N(X); both X and X+Y are a.c. with finite differential entropy, so
entropyPowerExt_of_ac_integrable writes each as ofReal (exp (2h)), and the real core
h(X) ≤ h(X+Y) lifts via Real.exp_le_exp. The integrability and finite-entropy hypotheses are
regularity preconditions.
@audit:superseded-by(entropyPowerExt_add_ge) Replaced by the unconditional
entropyPowerExt_mixed_add_ge; retained as a proof-done leaf reachable only from the dead
dispatch skeleton.
@audit:ok
Used by
InformationTheory.Shannon.entropyPowerExt_mixed_add_ge_symm_of_regular
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)
(h_ac :
((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 :
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 :
∀ᵐ (z : ℝ) ∂MeasureTheory.Measure.map X P, ((ProbabilityTheory.condDistrib (fun (ω : Ω) => Y ω + X ω) X P) z).AbsolutelyContinuous MeasureTheory.volume)
(hκ_logp_int :
∀ᵐ (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 :
∀ᵐ (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 :
MeasureTheory.Integrable
(fun (z : ℝ) => differentialEntropy ((ProbabilityTheory.condDistrib (fun (ω : Ω) => Y ω + X ω) X P) z))
(MeasureTheory.Measure.map X P))
(h_cross_int :
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 :
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))
(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)
Case 2 symmetric (Y a.c., X singular): N(X+Y) ≥ N(X) + N(Y). Re-applies
entropyPowerExt_mixed_add_ge_of_regular with X and Y swapped via X + Y = Y + X, passing
hY_ent / hWyx_ent into the X-role positions. The integrability and finite-entropy hypotheses
are regularity preconditions for the Y+X path.
@audit:superseded-by(entropyPowerExt_add_ge) Replaced by the unconditional
entropyPowerExt_mixed_add_ge_symm; retained as a proof-done leaf reachable only from the
dead dispatch skeleton.
@audit:ok