InformationTheory.Shannon.EPI.InfiniteVariance.Truncation.Convergence

theorem

InformationTheory.Shannon.EPIInfiniteVarianceTruncation.differentialEntropy_cond_decomp

(μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsProbabilityMeasure μ] {n : ℕ} (hpos : μ {r : ℝ | |r| ≤ ↑n} ≠ 0) (hac : μ.AbsolutelyContinuous MeasureTheory.volume) (hent : MeasureTheory.Integrable (fun (x : ℝ) => (μ.rnDeriv MeasureTheory.volume x).toReal.negMulLog) MeasureTheory.volume) :

differentialEntropy μ[|{r : ℝ | |r| ≤ ↑n}] = ((μ {r : ℝ | |r| ≤ ↑n}).toReal⁻¹ * ∫ (x : ℝ), {r : ℝ | |r| ≤ ↑n}.indicator (fun (x : ℝ) => (μ.rnDeriv MeasureTheory.volume x).toReal.negMulLog) x) + Real.log (μ {r : ℝ | |r| ≤ ↑n}).toReal

Differential entropy of a measure conditioned on a growing truncation set Sn := {|r| ≤ n} decomposes as h(cond μ Sn) = (m_n.toReal)⁻¹ · ∫ Sn.indicator (negMulLog ∘ q) ∂volume + log (m_n.toReal), where m_n := μ Sn and q x := (μ.rnDeriv volume x).toReal.

Used by

theorem

InformationTheory.Shannon.EPIInfiniteVarianceTruncation.differentialEntropy_map_condTrunc_tendsto

source

{Ω : Type u_1} {mΩ : MeasurableSpace Ω} (P : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure P] {X Y : Ω → ℝ} (hX : Measurable X) (hY : Measurable Y) (hXY : ProbabilityTheory.IndepFun X Y P) {Z : Ω → ℝ} (hZ : Z = X ∨ Z = Y) (hZ_ac : (MeasureTheory.Measure.map Z P).AbsolutelyContinuous MeasureTheory.volume) (hZ_ent : MeasureTheory.Integrable (fun (x : ℝ) => ((MeasureTheory.Measure.map Z P).rnDeriv MeasureTheory.volume x).toReal.negMulLog) MeasureTheory.volume) :

Filter.Tendsto (fun (n : ℕ) => differentialEntropy (MeasureTheory.Measure.map Z (condTrunc P X Y n))) Filter.atTop (nhds (differentialEntropy (MeasureTheory.Measure.map Z P)))

Per-component convergence of differential entropy under conditioning truncation: h((condTrunc P X Y n).map Z) → h(P.map Z) for Z = X or Z = Y. The decomposition -∫ p_n log p_n = -(1/m_n) ∫_{truncSet} p log p + log m_n converges by dominated convergence on the fixed integrable p log p (first term) and m_n → 1 (second term).

Used by

theorem

InformationTheory.Shannon.EPIInfiniteVarianceTruncation.entropyPowerExt_map_condTrunc_tendsto

source

{Ω : Type u_1} {mΩ : MeasurableSpace Ω} (P : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure P] {X Y : Ω → ℝ} (hX : Measurable X) (hY : Measurable Y) (hXY : ProbabilityTheory.IndepFun X Y P) {Z : Ω → ℝ} (hZ : Z = X ∨ Z = Y) (hZ_ac : (MeasureTheory.Measure.map Z P).AbsolutelyContinuous MeasureTheory.volume) (hZ_ent : MeasureTheory.Integrable (fun (x : ℝ) => ((MeasureTheory.Measure.map Z P).rnDeriv MeasureTheory.volume x).toReal.negMulLog) MeasureTheory.volume) :

Filter.Tendsto (fun (n : ℕ) => entropyPowerExt (MeasureTheory.Measure.map Z (condTrunc P X Y n))) Filter.atTop (nhds (entropyPowerExt (MeasureTheory.Measure.map Z P)))

Per-component convergence of the entropy power under conditioning truncation: Nₑ((condTrunc P X Y n).map Z) → Nₑ(P.map Z), obtained from the differential-entropy version by the continuous transform entropyPowerExt = exp (2 · h).

Used by

theorem

InformationTheory.Shannon.EPIInfiniteVarianceTruncation.differentialEntropy_condTrunc_sum_bddUnder

source

(Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) Filter.atTop fun (n : ℕ) => differentialEntropy (MeasureTheory.Measure.map (fun (ω : Ω) => X ω + Y ω) (condTrunc P X Y n))) ∧ Filter.IsCoboundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) Filter.atTop fun (n : ℕ) => differentialEntropy (MeasureTheory.Measure.map (fun (ω : Ω) => X ω + Y ω) (condTrunc P X Y n))

The sequence h((condTrunc P X Y n).map (X + Y)) is bounded above (IsBoundedUnder (≤)) and cobounded below (IsCoboundedUnder (≤)) along atTop. These supply the bddAbove / cobdd premises for the monotone-continuous limsup push in the entropy-power upper semicontinuity bound.

The upper bound comes from the per-n Gibbs bound h(μ_n) ≤ RHS_n plus convergence of RHS_n; the coboundedness comes from the per-n lower bound Nₑ(μ_n) ≥ Nₑ(X_n), taking logs to get h(μ_n) ≥ (1/2) log (Nₑ(X).toReal / 2) eventually. The entropy finiteness hypotheses are regularity preconditions. @audit:ok

Used by

theorem

InformationTheory.Shannon.EPIInfiniteVarianceTruncation.differentialEntropy_condTrunc_sum_limsup_le

source

Filter.limsup (fun (n : ℕ) => differentialEntropy (MeasureTheory.Measure.map (fun (ω : Ω) => X ω + Y ω) (condTrunc P X Y n))) Filter.atTop ≤ differentialEntropy (MeasureTheory.Measure.map (fun (ω : Ω) => X ω + Y ω) P)

Upper semicontinuity of differential entropy under conditioning truncation: limsupₙ h((condTrunc P X Y n).map (X + Y)) ≤ h(P.map (X + Y)).

Assembled from the per-n Gibbs bound h(μ_n) ≤ RHS_n, convergence RHS_n → h(ν), and boundedness, into limsup h(μ_n) ≤ limsup RHS_n = h(ν). The hypothesis hent_sum is a finite-differential-entropy regularity precondition. @audit:ok

Used by

theorem

InformationTheory.Shannon.EPIInfiniteVarianceTruncation.entropyPowerExt_condTrunc_sum_limsup_le

source

Filter.limsup (fun (n : ℕ) => entropyPowerExt (MeasureTheory.Measure.map (fun (ω : Ω) => X ω + Y ω) (condTrunc P X Y n))) Filter.atTop ≤ entropyPowerExt (MeasureTheory.Measure.map (fun (ω : Ω) => X ω + Y ω) P)

Upper semicontinuity of the entropy power under conditioning truncation: limsupₙ Nₑ((condTrunc P X Y n).map (X + Y)) ≤ Nₑ(P.map (X + Y)).

The differential-entropy version is lifted through the monotone continuous map g h := ENNReal.ofReal (exp (2 · h)), rewriting both sides as g ∘ h and pushing the limsup through g via Monotone.map_limsup_of_continuousAt. The hypothesis hent_sum is a regularity precondition. @audit:ok

Used by