InformationTheory.Shannon.EPI.Unconditional.TruncationLimit.Mono

Imports 13

TruncationLimit — monotonicity part #

Fatou lift of the positive-part lintegral, finite-entropy monotonicity via per-fibre translate Gibbs, and per-n truncation monotonicity. Depends on the Core part (truncW, convolution density, per-fibre absolute continuity, cross-entropy); re-exported by the umbrella InformationTheory.Shannon.EPI.Unconditional.TruncationLimit.

theorem

InformationTheory.Shannon.lintegral_ofReal_neg_ne_top_of_integrable

source

{α : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {g : α → ℝ} (hg : MeasureTheory.Integrable g μ) :

∫⁻ (x : α), ENNReal.ofReal (-g x) ∂μ ≠ ⊤

Used by

theorem

InformationTheory.Shannon.mul_abs_log_eq_abs_negMulLog_of_nonneg

source

{r : ℝ} (hr : 0 ≤ r) :

r * |Real.log r| = |r.negMulLog|

Used by

theorem

InformationTheory.Shannon.lintegral_enorm_eq_lintegral_ofReal_add_ofReal_neg

source

{α : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {g : α → ℝ} (hg : Measurable g) :

∫⁻ (x : α), ‖g x‖ₑ ∂μ = ∫⁻ (x : α), ENNReal.ofReal (g x) ∂μ + ∫⁻ (x : α), ENNReal.ofReal (-g x) ∂μ

Used by

theorem

InformationTheory.Shannon.lintegral_ofReal_eq_top_of_not_hasFiniteIntegral

source

{α : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {g : α → ℝ} (hg : Measurable g) (hnotfin : ¬MeasureTheory.HasFiniteIntegral g μ) (hneg : ∫⁻ (x : α), ENNReal.ofReal (-g x) ∂μ ≠ ⊤) :

∫⁻ (x : α), ENNReal.ofReal (g x) ∂μ = ⊤

Used by

theorem

InformationTheory.Shannon.differentialEntropy_eq_neg_integral_mul_log

source

(μ : MeasureTheory.Measure ℝ) :

differentialEntropy μ = -∫ (x : ℝ), (μ.rnDeriv MeasureTheory.volume x).toReal * Real.log (μ.rnDeriv MeasureTheory.volume x).toReal

Used by

theorem

InformationTheory.Shannon.differentialEntropyExt_eq_top_of_not_integrable

source

{μ : MeasureTheory.Measure ℝ} (hac : μ.AbsolutelyContinuous MeasureTheory.volume) (hnotint : ¬MeasureTheory.Integrable (fun (x : ℝ) => (μ.rnDeriv MeasureTheory.volume x).toReal.negMulLog) MeasureTheory.volume) (hBfin : ∫⁻ (x : ℝ), ENNReal.ofReal (-(μ.rnDeriv MeasureTheory.volume x).toReal.negMulLog) ≠ ⊤) :

differentialEntropyExt μ = ⊤

Used by

theorem

InformationTheory.Shannon.differentialEntropyExt_posPart_le_liminf_of_ae_tendsto

source

(μ : MeasureTheory.Measure ℝ) (μ_n : ℕ → MeasureTheory.Measure ℝ) (h_ae : ∀ᵐ (x : ℝ), Filter.Tendsto (fun (n : ℕ) => ((μ_n n).rnDeriv MeasureTheory.volume x).toReal) Filter.atTop (nhds (μ.rnDeriv MeasureTheory.volume x).toReal)) :

∫⁻ (x : ℝ), ENNReal.ofReal (μ.rnDeriv MeasureTheory.volume x).toReal.negMulLog ≤ Filter.liminf (fun (n : ℕ) => ∫⁻ (x : ℝ), ENNReal.ofReal ((μ_n n).rnDeriv MeasureTheory.volume x).toReal.negMulLog) Filter.atTop

Fatou lift of the positive-part lintegral A μ = ∫⁻ x, ofReal (negMulLog (rnDeriv μ vol x)): from a.e. convergence of the densities (μ_n).rnDeriv vol → μ.rnDeriv vol, the lower bound A μ ≤ liminf (A μ_n). Built from lintegral_liminf_le with continuity of negMulLog and ENNReal.ofReal.

@audit:ok

Used by

theorem

InformationTheory.Shannon.integral_map_add_const_eq_integral_translate_mul

source

(μW : MeasureTheory.Measure ℝ) [MeasureTheory.SigmaFinite μW] (hμW_ac : μW.AbsolutelyContinuous MeasureTheory.volume) (z : ℝ) (g : ℝ → ℝ) :

∫ (x : ℝ), g x ∂MeasureTheory.Measure.map (fun (x : ℝ) => x + z) μW = ∫ (x : ℝ), (μW.rnDeriv MeasureTheory.volume (x - z)).toReal * g x

Used by

theorem

InformationTheory.Shannon.rnDeriv_conv_toReal_aeeq_integral_translate

source

(μW μV : MeasureTheory.Measure ℝ) [MeasureTheory.IsProbabilityMeasure μW] [MeasureTheory.IsProbabilityMeasure μV] (hμW_ac : μW.AbsolutelyContinuous MeasureTheory.volume) :

(fun (x : ℝ) => ((μW.conv μV).rnDeriv MeasureTheory.volume x).toReal) =ᵐ[MeasureTheory.volume ] fun (x : ℝ) => ∫ (z : ℝ), (μW.rnDeriv MeasureTheory.volume (x - z)).toReal ∂μV

Used by

theorem

InformationTheory.Shannon.lintegral_ofReal_translate_density_aeeq

source

(μW μV : MeasureTheory.Measure ℝ) [MeasureTheory.IsProbabilityMeasure μW] [MeasureTheory.IsProbabilityMeasure μV] (hμW_ac : μW.AbsolutelyContinuous MeasureTheory.volume) :

∀ᵐ (x : ℝ), ∫⁻ (z : ℝ), ENNReal.ofReal (μW.rnDeriv MeasureTheory.volume (x - z)).toReal ∂μV = ENNReal.ofReal ((μW.conv μV).rnDeriv MeasureTheory.volume x).toReal

Used by

theorem

InformationTheory.Shannon.lintegral_translate_mul_abs_log_ne_top

source

(μW μV : MeasureTheory.Measure ℝ) [MeasureTheory.IsProbabilityMeasure μW] [MeasureTheory.IsProbabilityMeasure μV] (hμW_ac : μW.AbsolutelyContinuous MeasureTheory.volume) (hent_sum : MeasureTheory.Integrable (fun (x : ℝ) => ((μW.conv μV).rnDeriv MeasureTheory.volume x).toReal.negMulLog) MeasureTheory.volume) :

∫⁻ (p : ℝ × ℝ), ENNReal.ofReal ((μW.rnDeriv MeasureTheory.volume (p.2 - p.1)).toReal * |Real.log ((μW.conv μV).rnDeriv MeasureTheory.volume p.2).toReal|) ∂μV.prod MeasureTheory.volume ≠ ⊤

Used by

theorem

InformationTheory.Shannon.integrable_translate_mul_log

source

MeasureTheory.Integrable (fun (p : ℝ × ℝ) => (μW.rnDeriv MeasureTheory.volume (p.2 - p.1)).toReal * Real.log ((μW.conv μV).rnDeriv MeasureTheory.volume p.2).toReal) (μV.prod MeasureTheory.volume)

Used by

theorem

InformationTheory.Shannon.integral_neg_translate_log_eq_differentialEntropy

source

∫ (z : ℝ), -∫ (x : ℝ), Real.log ((μW.conv μV).rnDeriv MeasureTheory.volume x).toReal ∂MeasureTheory.Measure.map (fun (x : ℝ) => x + z) μW ∂μV = differentialEntropy (μW.conv μV)

Used by

theorem

InformationTheory.Shannon.differentialEntropyExt_mono_add_of_integrable

source

{Ω : Type u_1} [MeasurableSpace Ω] (W V : Ω → ℝ) (Q : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure Q] (hW : Measurable W) (hV : Measurable V) (hWV : ProbabilityTheory.IndepFun W V Q) (hW_ac : (MeasureTheory.Measure.map W Q).AbsolutelyContinuous MeasureTheory.volume) (hW_ent : MeasureTheory.Integrable (fun (x : ℝ) => ((MeasureTheory.Measure.map W Q).rnDeriv MeasureTheory.volume x).toReal.negMulLog) MeasureTheory.volume) :

differentialEntropyExt (MeasureTheory.Measure.map W Q) ≤ differentialEntropyExt (MeasureTheory.Measure.map (fun (ω : Ω) => W ω + V ω) Q)

Finite-entropy monotonicity of differential entropy under independent addition: for W a.c., W ⊥ V, and Q.map W of finite differential entropy (hW_ent), h(W) ≤ h(W+V). The proof uses per-fibre translate Gibbs and splits on finiteness of ν = W+V (finite branch: real-valued Gibbs; ⊤ branch: le_top). It requires no truncation, so it applies directly to an un-truncated W.

@audit:ok

Used by

theorem

InformationTheory.Shannon.truncW_indepFun_of_indepFun

source

{Ω : Type u_1} [MeasurableSpace Ω] (W V : Ω → ℝ) (P : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure P] (hW : Measurable W) (_hV : Measurable V) (hWV : ProbabilityTheory.IndepFun W V P) (n : ℕ) (hn : P {ω : Ω | |W ω| ≤ ↑n} ≠ 0) :

ProbabilityTheory.IndepFun W V (truncW P W n)

Used by

theorem

InformationTheory.Shannon.truncW_map_negMulLog_negPart_lintegral_ne_top

source

{Sn : Set ℝ} (_hSn_meas : MeasurableSet Sn) {ρ : ℝ → ENNReal} (hρ_meas : Measurable ρ) (hρ_lint : ∫⁻ (x : ℝ), ENNReal.ofReal (ρ x).toReal = 1) {c : ENNReal} (_hc_top : c ≠ ⊤) {fn : ℝ → ℝ} (h_fn_ae : ∀ᵐ (x : ℝ), fn x = (c⁻¹ * Sn.indicator ρ x).toReal) (hρ_negPart_fin : ∫⁻ (x : ℝ), ENNReal.ofReal (-(ρ x).toReal.negMulLog) ≠ ⊤) :

∫⁻ (x : ℝ), ENNReal.ofReal (-(fn x).negMulLog) ≠ ⊤

Used by

theorem

InformationTheory.Shannon.differentialEntropyExt_mono_add_truncW

source

{Ω : Type u_1} [MeasurableSpace Ω] (W V : Ω → ℝ) (P : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure P] (hW : Measurable W) (hV : Measurable V) (hWV : ProbabilityTheory.IndepFun W V P) (hW_ac : (MeasureTheory.Measure.map W P).AbsolutelyContinuous MeasureTheory.volume) (hW_negPart_fin : ∫⁻ (x : ℝ), ENNReal.ofReal (-((MeasureTheory.Measure.map W P).rnDeriv MeasureTheory.volume x).toReal.negMulLog) ≠ ⊤) (n : ℕ) (hn : P {ω : Ω | |W ω| ≤ ↑n} ≠ 0) :

differentialEntropyExt (MeasureTheory.Measure.map W (truncW P W n)) ≤ differentialEntropyExt (MeasureTheory.Measure.map (fun (ω : Ω) => W ω + V ω) (truncW P W n))

Per-n monotonicity h(W_n) ≤ h(W_n + V), where W_n := truncW P W n is the compact-support approximation obtained by conditioning P on the W-event {|W| ≤ n}. The preamble supplies the truncation-specific regularity (a.c., independence, and finite entropy preserved under conditioning), then delegates to the truncation-free core differentialEntropyExt_mono_add_of_integrable.

@audit:ok

Used by