Chapter 14: Foundations of Information Theory

structure BinaryPrefixCode (Symbol : Type*) where

theorem kraft_inequality [Fintype Symbol] [DecidableEq Symbol] (code : BinaryPrefixCode Symbol) : ∑ word ∈ code.codebook, (1 / 2 : Real) ^ word.length ≤ 1

theorem discreteEntropyBaseTwo_eq_div_log_two (support : Finset Symbol) (probability : Symbol → Real) : discreteEntropyBaseTwo support probability = discreteEntropy support probability / Real.log 2

noncomputable def expectedCodeLength [Fintype Symbol] (probability : Symbol → Real) (code : BinaryPrefixCode Symbol) : Real

theorem huffmanCode_optimal {α : Type*} [Fintype α] (p : α → ℝ) (hp : ∀ i, 0 ≤ p i) : IsOptimalPrefixCode p (huffmanCode p hp)

theorem exists_prefixCode_of_uniquelyDecodable {α : Type*} [Fintype α] (c : α → List Bool) (hinj : Function.Injective c) (hud : InformationTheory.UniquelyDecodable (Set.range c)) : ∃ code : BinaryPrefixCode α, ∀ i, (code.encode i).length = (c i).length

theorem IsOptimalPrefixCode.length_antitone {α : Type*} [Fintype α] [DecidableEq α] {p : α → ℝ} {code : BinaryPrefixCode α} (hopt : IsOptimalPrefixCode p code) (a b : α) (hp : p a < p b) : (code.encode b).length ≤ (code.encode a).length

theorem huffmanCode_entropy_sandwich {α : Type*} [Fintype α] (p : α → ℝ) (hp : ∀ i, 0 ≤ p i) (hs : ∑ i, p i = 1) : discreteEntropyBaseTwo Finset.univ p ≤ expectedCodeLength p (huffmanCode p hp) ∧ expectedCodeLength p (huffmanCode p hp) ≤ discreteEntropyBaseTwo Finset.univ p + 1

theorem arithmeticBlockCode_rate_tendsto_entropy {k : ℕ} (p : Fin k → ℝ) (hp : ∀ i, 0 ≤ p i) (hs : ∑ i, p i = 1) : Filter.Tendsto (fun n : ℕ => expectedCodeLength (sourceBlockMass p (n + 1)) (arithmeticBlockCode p hp hs (n + 1)) / (n + 1)) Filter.atTop (nhds (discreteEntropyBaseTwo Finset.univ p))

theorem arithmeticBlockCode_payload_interval {k : ℕ} (p : Fin k → ℝ) (hp : ∀ i, 0 ≤ p i) (hs : ∑ i, p i = 1) (n : ℕ) (x : SourceBlock.{0,0} (Fin k) n) (hx : 0 < sourceBlockMass p n x) : (arithmeticInterval p (sourceBlockList n x)).1 ≤ dyadicAddressLower ((arithmeticBlockCode p hp hs n).encode x).tail ∧ dyadicAddressUpper ((arithmeticBlockCode p hp hs n).encode x).tail < (arithmeticInterval p (sourceBlockList n x)).2

theorem sourceBlock_code_family_limit_ge_entropy {α : Type*} [Fintype α] [DecidableEq α] (p : α → ℝ) (hp : ∀ i, 0 ≤ p i) (hs : ∑ i, p i = 1) (code : (n : ℕ) → BinaryPrefixCode (SourceBlock α (n + 1))) (r : ℝ) (hr : Filter.Tendsto (fun n => expectedCodeLength (sourceBlockMass p (n + 1)) (code n) / (n + 1)) Filter.atTop (nhds r)) : discreteEntropyBaseTwo Finset.univ p ≤ r

theorem exists_ceilingLogPrefixCode {α : Type*} [Fintype α] (hcard : 1 < Fintype.card α) : ∃ code : BinaryPrefixCode α, ∀ a, (code.encode a).length = Nat.clog 2 (Fintype.card α)

theorem fixedLength_uniformPowerTwo_optimal {α : Type*} [Fintype α] (n : ℕ) (hcard : Fintype.card α = 2 ^ n) (code : BinaryPrefixCode α) (hlen : ∀ a, (code.encode a).length = n) : IsOptimalPrefixCode (fun _ : α => 1 / (2 : ℝ) ^ n) code

theorem uniform_three_fixedLength_not_optimal (code : BinaryPrefixCode (Fin 3)) (hlen : ∀ a, (code.encode a).length = 2) : ¬ IsOptimalPrefixCode (fun _ : Fin 3 => (1 / 3 : ℝ)) code

theorem relativeEntropy_finite_crossEntropy {α : Type*} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] (P Q : Measure α) [IsProbabilityMeasure P] [IsProbabilityMeasure Q] (h : P ≪ Q) : relativeEntropy P Q = ENNReal.ofReal (discreteCrossEntropy (fun i => (P {i}).toReal) (fun i => (Q {i}).toReal) - discreteEntropy Finset.univ (fun i => (P {i}).toReal))

theorem entropyTerm_tendsto_zero_right : Filter.Tendsto (fun x : ℝ => x * Real.log x⁻¹) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

abbrev relativeEntropy {α : Type*} [MeasurableSpace α] (P Q : Measure α) : ENNReal

theorem relativeEntropy_of_absolutelyContinuous_of_integrable {α : Type*} [MeasurableSpace α] (P Q : Measure α) (hPQ : P ≪ Q) (hInt : Integrable (llr P Q) P) : relativeEntropy P Q = ENNReal.ofReal (∫ x, llr P Q x ∂P + Q.real univ - P.real univ)

theorem relativeEntropy_of_probability_absolutelyContinuous_of_integrable {α : Type*} [MeasurableSpace α] (P Q : Measure α) [IsProbabilityMeasure P] [IsProbabilityMeasure Q] (hPQ : P ≪ Q) (hInt : Integrable (llr P Q) P) : relativeEntropy P Q = ENNReal.ofReal (∫ x, llr P Q x ∂P)

theorem relativeEntropy_eq_top_of_not_absolutelyContinuous {α : Type*} [MeasurableSpace α] {P Q : Measure α} (hPQ : ¬ P ≪ Q) : relativeEntropy P Q = ∞

theorem relativeEntropy_ne_top_iff {α : Type*} [MeasurableSpace α] {P Q : Measure α} : relativeEntropy P Q ≠ ∞ ↔ P ≪ Q ∧ Integrable (llr P Q) P

theorem relativeEntropy_eq_zero_iff {α : Type*} [MeasurableSpace α] {P Q : Measure α} [IsFiniteMeasure P] [IsFiniteMeasure Q] : relativeEntropy P Q = 0 ↔ P = Q

theorem relativeEntropy_trim_le {α : Type*} {m m₀ : MeasurableSpace α} {P Q : @Measure α m₀} [IsFiniteMeasure P] [IsFiniteMeasure Q] (hm : m ≤ m₀) : @relativeEntropy α m (P.trim hm) (Q.trim hm) ≤ @relativeEntropy α m₀ P Q

abbrev bernoulliRelativeEntropy (p q : Real) : ENNReal

theorem relativeEntropy_finite_sum_log {α : Type*} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] (P Q : Measure α) [IsProbabilityMeasure P] [IsProbabilityMeasure Q] (h : P ≪ Q) : relativeEntropy P Q = ENNReal.ofReal (∑ x, (P {x}).toReal * Real.log ((P {x}).toReal / (Q {x}).toReal))

theorem relativeEntropy_finite_eq_if {α : Type*} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] (P Q : Measure α) [IsProbabilityMeasure P] [IsProbabilityMeasure Q] : relativeEntropy P Q = if ∀ x, Q {x} = 0 → P {x} = 0 then ENNReal.ofReal (∑ x, (P {x}).toReal * Real.log ((P {x}).toReal / (Q {x}).toReal)) else ∞

theorem relativeEntropy_finite_eq_top_iff {α : Type*} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] (P Q : Measure α) [IsProbabilityMeasure P] [IsProbabilityMeasure Q] : relativeEntropy P Q = ∞ ↔ ∃ x, P {x} ≠ 0 ∧ Q {x} = 0

def finitePartitionRelativeEntropy {α : Type*} [MeasurableSpace α] (P Q : Measure α) : ENNReal

theorem finitePartitionRelativeEntropy_eq_relativeEntropy {α : Type*} [m : MeasurableSpace α] (P Q : Measure α) [IsFiniteMeasure P] [IsFiniteMeasure Q] : finitePartitionRelativeEntropy P Q = relativeEntropy P Q

theorem relativeEntropy_commonDensity_eq_if {α : Type*} [MeasurableSpace α] (P Q μ : Measure α) [IsProbabilityMeasure P] [IsProbabilityMeasure Q] [SigmaFinite μ] (hP : P ≪ μ) (hQ : Q ≪ μ) : relativeEntropy P Q = if P ≪ Q ∧ Integrable (fun x => (P.rnDeriv μ x).toReal * Real.log ((P.rnDeriv μ x).toReal / (Q.rnDeriv μ x).toReal)) μ then ENNReal.ofReal (∫ x, (P.rnDeriv μ x).toReal * Real.log ((P.rnDeriv μ x).toReal / (Q.rnDeriv μ x).toReal) ∂μ) else (⊤ : ENNReal)

theorem exists_commonSigmaFiniteDominatingMeasure {α : Type*} [MeasurableSpace α] (P Q : Measure α) [IsFiniteMeasure P] [IsFiniteMeasure Q] : ∃ μ : Measure α, SigmaFinite μ ∧ P ≪ μ ∧ Q ≪ μ

theorem relativeEntropy_finite_lt_top_iff_ac {α : Type*} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] (P Q : Measure α) [IsProbabilityMeasure P] [IsProbabilityMeasure Q] : relativeEntropy P Q < ⊤ ↔ P ≪ Q

theorem bernoulliRelativeEntropy_asymmetry : bernoulliRelativeEntropy 0 (1 / 2) ≠ bernoulliRelativeEntropy (1 / 2) 0

theorem relativeEntropy_triangle_counterexample : relativeEntropy (gaussianReal 0 1) (gaussianReal 1 1) + relativeEntropy (gaussianReal 1 1) (gaussianReal 2 1) < relativeEntropy (gaussianReal 0 1) (gaussianReal 2 1)

theorem bretagnolleHuberScale_le_half_commonDensityAffinity_sq {α : Type*} [MeasurableSpace α] (P Q μ : Measure α) [IsProbabilityMeasure P] [IsProbabilityMeasure Q] [SigmaFinite μ] (hQ : Q ≪ μ) : bretagnolleHuberScale (relativeEntropy P Q) ≤ (1 / 2 : ℝ) * commonDensityAffinity P Q μ ^ 2

theorem half_commonDensityAffinity_sq_le_overlap {α : Type*} [MeasurableSpace α] (P Q μ : Measure α) [IsProbabilityMeasure P] [IsProbabilityMeasure Q] [SigmaFinite μ] (hP : P ≪ μ) (hQ : Q ≪ μ) : (1 / 2 : ℝ) * commonDensityAffinity P Q μ ^ 2 ≤ commonDensityOverlap P Q μ

theorem commonDensityOverlap_le_testingError {α : Type*} [MeasurableSpace α] (P Q μ : Measure α) [IsFiniteMeasure P] [IsFiniteMeasure Q] [SigmaFinite μ] (hP : P ≪ μ) (hQ : Q ≪ μ) {A : Set α} (hA : MeasurableSet A) : commonDensityOverlap P Q μ ≤ P.real A + Q.real Aᶜ

theorem klDiv_gaussianReal_same_variance (m n : ℝ) (v : ℝ≥0) (hv : v ≠ 0) : InformationTheory.klDiv (gaussianReal m v) (gaussianReal n v) = ENNReal.ofReal ((m - n) ^ 2 / (2 * v))

theorem gaussian_testing_max_error_three_twentieths (Δ : ℝ) (v : ℝ≥0) (hv : v ≠ 0) (hsnr : Δ ^ 2 / (v : ℝ) ≤ 1) {A : Set ℝ} (hA : MeasurableSet A) : (3 / 20 : ℝ) ≤ max ((gaussianReal 0 v).real A) ((gaussianReal Δ v).real Aᶜ)

theorem rnDeriv_restrict_restrict {α : Type*} [MeasurableSpace α] {P Q : Measure α} [SigmaFinite P] [SigmaFinite Q] (hPQ : P ≪ Q) {A : Set α} (hA : MeasurableSet A) : (P.restrict A).rnDeriv (Q.restrict A) =ᵐ[Q.restrict A] P.rnDeriv Q

theorem relativeEntropy_restrict_add_compl {α : Type*} [MeasurableSpace α] {P Q : Measure α} [IsFiniteMeasure P] [IsFiniteMeasure Q] (hPQ : P ≪ Q) {A : Set α} (hA : MeasurableSet A) : relativeEntropy P Q = relativeEntropy (P.restrict A) (Q.restrict A) + relativeEntropy (P.restrict Aᶜ) (Q.restrict Aᶜ)

theorem bernoulliRelativeEntropy_event_le {α : Type*} [MeasurableSpace α] {P Q : Measure α} [IsProbabilityMeasure P] [IsProbabilityMeasure Q] {A : Set α} (hA : MeasurableSet A) : bernoulliRelativeEntropy (P.real A) (Q.real A) ≤ relativeEntropy P Q

theorem binaryBretagnolleHuber {p q : Real} (hp : KLUCB.IsBernoulliParameter p) (hq : KLUCB.IsBernoulliParameter q) : bretagnolleHuberScale (bernoulliRelativeEntropy p q) ≤ p + (1 - q)

noncomputable def bretagnolleHuberScale (d : ENNReal) : Real

theorem bretagnolleHuberScale_antitone {d D : ENNReal} (h : d ≤ D) : bretagnolleHuberScale D ≤ bretagnolleHuberScale d

theorem bretagnolleHuber {α : Type*} [MeasurableSpace α] {P Q : Measure α} [IsProbabilityMeasure P] [IsProbabilityMeasure Q] {A : Set α} (hA : MeasurableSet A) : bretagnolleHuberScale (relativeEntropy P Q) ≤ P.real A + Q.real Aᶜ