InformationTheory.Probability.TwoSidedExtension.LogCondIntegral

Imports 20

Integrability of `pmfLogCondPast` and `pmfLogCondInfty` #

The integrand has the pointwise decomposition pmfLogCondPast μ p k x = ∑ a, 1_{coord0=a}(x) * (-log condProbPast a k x) (indicators partition unity on the singleton {coord0=a}, so the inner sum has a single nonzero summand at a = coord0 x).

For each a, the summand 1_{coord0=a} * (-log condProbPast a k) is integrable via the L¹ tower (condExp_stronglyMeasurable_mul_of_bound with a truncated -log factor) + monotone convergence. The truncated bound F_M := min(M, (-log g)⁺) satisfies ∫ (1_{coord0=a}) * F_M = ∫ g * F_M ≤ ∫ negMulLog g ≤ 1, uniformly in M, so by MCT ∫ (1_{coord0=a}) * (-log g)⁺ ≤ 1.

theorem

InformationTheory.Shannon.TwoSided.tendsto_min_posPart_natCast

source

(t : ℝ) :

Filter.Tendsto (fun (M : ℕ) => min t⁺ ↑M) Filter.atTop (nhds t⁺)

Used by

theorem

InformationTheory.Shannon.TwoSided.norm_min_posPart_natCast_le

source

(t : ℝ) (M : ℕ) :

‖min t⁺ ↑M‖ ≤ ↑M

Used by

theorem

InformationTheory.Shannon.TwoSided.min_posPart_neg_log_mul_le_negMulLog

source

{y : ℝ} (hy_nn : 0 ≤ y) (hy_le : y ≤ 1) (M : ℕ) :

min (-Real.log y)⁺ ↑M * y ≤ y.negMulLog

Used by

theorem

InformationTheory.Shannon.TwoSided.enorm_mul_neg_log_eq_ofReal

source

{c y : ℝ} (hc : 0 ≤ c) (hy_nn : 0 ≤ y) (hy_le : y ≤ 1) :

‖c * -Real.log y‖ₑ = ENNReal.ofReal (c * (-Real.log y)⁺)

Used by

theorem

InformationTheory.Shannon.TwoSided.integrable_negMulLog_of_mem_Icc

source

{β : Type u_3} {mβ : MeasurableSpace β} {ν : MeasureTheory.Measure β} [MeasureTheory.IsFiniteMeasure ν] {g : β → ℝ} (hg_meas : MeasureTheory.AEStronglyMeasurable g ν) (hg_nn : 0 ≤ᵐ[ν] g) (hg_le : g ≤ᵐ[ν] fun (x : β) => 1) :

MeasureTheory.Integrable (fun (x : β) => (g x).negMulLog) ν

Used by

theorem

InformationTheory.Shannon.TwoSided.integral_negMulLog_le_one

source

{β : Type u_3} {mβ : MeasurableSpace β} {ν : MeasureTheory.Measure β} [MeasureTheory.IsProbabilityMeasure ν] {g : β → ℝ} (hg_meas : MeasureTheory.AEStronglyMeasurable g ν) (hg_nn : 0 ≤ᵐ[ν] g) (hg_le : g ≤ᵐ[ν] fun (x : β) => 1) :

∫ (x : β), (g x).negMulLog ∂ν ≤ 1

Used by

theorem

InformationTheory.Shannon.TwoSided.lintegral_ofReal_le_one_of_integral_le_one

source

{β : Type u_3} {mβ : MeasurableSpace β} {ν : MeasureTheory.Measure β} {φ : β → ℝ} (hφ_int : MeasureTheory.Integrable φ ν) (hφ_nn : 0 ≤ᵐ[ν] φ) (hφ_le : ∫ (x : β), φ x ∂ν ≤ 1) :

∫⁻ (x : β), ENNReal.ofReal (φ x) ∂ν ≤ 1

Used by

theorem

InformationTheory.Shannon.TwoSided.lintegral_lt_top_of_monotone_tendsto_le

source

{β : Type u_3} {mβ : MeasurableSpace β} {ν : MeasureTheory.Measure β} {f : ℕ → β → ENNReal} {ψ : β → ENNReal} {C : ENNReal} (hf_meas : ∀ (M : ℕ), Measurable (f M)) (hf_mono : ∀ (x : β), Monotone fun (M : ℕ) => f M x) (hf_tendsto : ∀ (x : β), Filter.Tendsto (fun (M : ℕ) => f M x) Filter.atTop (nhds (ψ x))) (hf_bound : ∀ (M : ℕ), ∫⁻ (x : β), f M x ∂ν ≤ C) (hC : C < ⊤) :

∫⁻ (x : β), ψ x ∂ν < ⊤

Used by

theorem

InformationTheory.Shannon.TwoSided.integrable_pmfLogCondPast

source

{Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (p : StationaryProcess μ α) (k : ℕ) :

MeasureTheory.Integrable (pmfLogCondPast μ p k) (μZ μ p)

Integrability of pmfLogCondPast k.

The integrand -log(condProbPast (coord0 x) k x) decomposes as `∑a 1{coord0=a}(x)

(-log condProbPast a k x). Each summand is integrable via integrable_indicator_mul_negLog_of_condExpapplied atm := pastFiltration k, using the defining identity condProbPast a k = μZ[1_{coord0=a} | pastFiltration k]and the[0,1]` bound. The sum of finitely many integrable functions is integrable.

Used by

theorem

InformationTheory.Shannon.TwoSided.integrable_pmfLogCondInfty

source

MeasureTheory.Integrable (pmfLogCondInfty μ p) (μZ μ p)

Integrability of pmfLogCondInfty.

Same argument as integrable_pmfLogCondPast, but applied to the infinite-past limit condProbInfty a, which is by definition the condExp of the indicator w.r.t. the σ-algebra ⨆ k, pastFiltration k of the infinite past.

Used by

theorem

InformationTheory.Shannon.TwoSided.ae_condProbInfty_coord0_pos

source

∀ᵐ (x : ℤ → α) ∂μZ μ p, 0 < condProbInfty μ p (coord0 x) x

AE positivity of the realized conditional probability.

Almost surely under μZ, the infinite-past conditional probability of the realized coord0 value is strictly positive. This is a standard fact: the indicator 1_{coord0 = coord0 x} is exactly 1 at x, and the conditional expectation w.r.t. ⨆ k, pastFiltration k of an indicator-of-a-set has total mass equal to that set's measure. Positivity on a full-measure set follows from the integral identity ∫_E condProbInfty (coord0 x) = (μZ μ p)({coord0 = a} ∩ E).

Used inside pmfLogCondPast_tendsto_pmfLogCondInfty to handle Real.log discontinuity at 0.

Used by

theorem

InformationTheory.Shannon.TwoSided.pmfLogCondPast_tendsto_pmfLogCondInfty

source

∀ᵐ (x : ℤ → α) ∂μZ μ p, Filter.Tendsto (fun (k : ℕ) => pmfLogCondPast μ p k x) Filter.atTop (nhds (pmfLogCondInfty μ p x))

Forward Lévy upward convergence: per-step conditional log-likelihood on longer-and-longer finite past converges to pmfLogCondInfty. Application of MeasureTheory.tendsto_ae_condExp (one application per a : α, combined by continuity of -log and the inner-sum identity ∑ a, indicator(coord0=a) * f a = f (coord0 x)).

Caveat: convergence holds on the AE set where condProbInfty (coord0 x) x > 0 (provided by ae_condProbInfty_coord0_pos); on the null set where the conditional probability of the realized coord0 value is 0, Real.log is discontinuous, and we report pmfLogCondPast/pmfLogCondInfty as 0 by convention (Real.log 0 = 0).

Used by

Integral identity proof #

theorem

InformationTheory.Shannon.TwoSided.integral_pmfLogCondPast_eq_conditionalEntropyTail

source

{Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (p : StationaryProcess μ α) (k : ℕ) :

∫ (x : ℤ → α), pmfLogCondPast μ p k x ∂μZ μ p = conditionalEntropyTail μ p k

Per-step integral identity: integrating pmfLogCondPast k against μZ gives conditionalEntropyTail μ p k.

The proof structure:

Decompose ∫ pmfLogCondPast k dμZ into a finite sum of ∫ negMulLog(condProbPast a k) dμZ (via integral_pmfLogCondPast_eq_sum).
Identify each condProbPast a k with the condDistrib-form regular conditional probability (via condProbPast_ae_eq_condDistrib).
Bridge the sum to condEntropy μZ coord0 (pastBlock k) via integral_map and the definition of MeasureFano.condEntropy.
Transport to the μ-side via condEntropy_μZ_eq_condEntropy_μ (joint-law equality + condEntropy_eq_pushforward).

Used by

theorem

InformationTheory.Shannon.TwoSided.integral_pmfLogCondInfty_eq_entropyRate

source

∫ (x : ℤ → α), pmfLogCondInfty μ p x ∂μZ μ p = entropyRate μ p

The SMB integral identity ∫ pmfLogCondInfty dμZ = entropyRate μ p.

Combines:

integral_pmfLogCondPast_eq_conditionalEntropyTail — the per-step identity;
DCT (forward Lévy a.s. limit + Real.exp (-1) uniform bound on negMulLog) applied per atom — ∫ negMulLog(condProbPast a k) → ∫ negMulLog(condProbInfty a);
entropyRate_eq_lim_condEntropy — conditionalEntropyTail μ p k → entropyRate.

Used by

InformationTheory.Probability.TwoSidedExtension.LogCondIntegral

Integrability of pmfLogCondPast and pmfLogCondInfty #

Integral identity proof #

Integrability of `pmfLogCondPast` and `pmfLogCondInfty` #