BanditRLProof.LowerBounds.BlockEntropy

No declaration docstring is present; use the chapter context and exact statement below.

theorem entropy_product_term (p q : ℝ) : (p * q) * Real.log (p * q)⁻¹ = q * (p * Real.log p⁻¹) + p * (q * Real.log q⁻¹)

Entropy of a product mass function before normalization.

theorem discreteEntropy_prod {α β : Type*} [Fintype α] [Fintype β] (p : α → ℝ) (q : β → ℝ) : discreteEntropy Finset.univ (fun x : α × β => p x.1 * q x.2) = (∑ j, q j) * discreteEntropy Finset.univ p + (∑ i, p i) * discreteEntropy Finset.univ q

No declaration docstring is present; use the chapter context and exact statement below.

theorem discreteEntropy_prod_probability {α β : Type*} [Fintype α] [Fintype β] (p : α → ℝ) (q : β → ℝ) (hp : ∑ i, p i = 1) (hq : ∑ j, q j = 1) : discreteEntropy Finset.univ (fun x : α × β => p x.1 * q x.2) = discreteEntropy Finset.univ p + discreteEntropy Finset.univ q

No declaration docstring is present; use the chapter context and exact statement below.

theorem discreteEntropyBaseTwo_prod_probability {α β : Type*} [Fintype α] [Fintype β] (p : α → ℝ) (q : β → ℝ) (hp : ∑ i, p i = 1) (hq : ∑ j, q j = 1) : discreteEntropyBaseTwo Finset.univ (fun x : α × β => p x.1 * q x.2) = discreteEntropyBaseTwo Finset.univ p + discreteEntropyBaseTwo Finset.univ q

An n-symbol source block, represented by a nested product.

def SourceBlock (α : Type*) : ℕ → Type _ | 0 => PUnit | n + 1 => α × SourceBlock α n instance sourceBlockFintype {α : Type*} [Fintype α] (n : ℕ) : Fintype (SourceBlock α n)

IID product mass, including the empty block of mass one.

def sourceBlockMass {α : Type*} (p : α → ℝ) : (n : ℕ) → SourceBlock α n → ℝ | 0, _ => 1 | n + 1, x => p x.1 * sourceBlockMass p n x.2 theorem sourceBlockMass_nonneg {α : Type*} (p : α → ℝ) (hp : ∀ i, 0 ≤ p i) (n : ℕ) (x : SourceBlock α n) : 0 ≤ sourceBlockMass p n x

No declaration docstring is present; use the chapter context and exact statement below.

theorem sourceBlockMass_nonneg {α : Type*} (p : α → ℝ) (hp : ∀ i, 0 ≤ p i) (n : ℕ) (x : SourceBlock α n) : 0 ≤ sourceBlockMass p n x

No declaration docstring is present; use the chapter context and exact statement below.

theorem sum_sourceBlockMass {α : Type*} [Fintype α] (p : α → ℝ) (hp : ∑ i, p i = 1) (n : ℕ) : ∑ x, sourceBlockMass p n x = 1

No declaration docstring is present; use the chapter context and exact statement below.

theorem discreteEntropyBaseTwo_sourceBlockMass {α : Type*} [Fintype α] (p : α → ℝ) (hp : ∑ i, p i = 1) (n : ℕ) : discreteEntropyBaseTwo Finset.univ (sourceBlockMass p n) = n * discreteEntropyBaseTwo Finset.univ p

Finite-block source coding with an explicit one-bit total overhead.

theorem exists_sourceBlock_code_rate_sandwich {α : Type*} [Fintype α] [DecidableEq α] (p : α → ℝ) (hp : ∀ i, 0 ≤ p i) (hs : ∑ i, p i = 1) (n : ℕ) (hn : 0 < n) : ∃ code : BinaryPrefixCode (SourceBlock α n), discreteEntropyBaseTwo Finset.univ p ≤ expectedCodeLength (sourceBlockMass p n) code / n ∧ expectedCodeLength (sourceBlockMass p n) code / n ≤ discreteEntropyBaseTwo Finset.univ p + 1 / n

Every finite block prefix code has rate at least the source entropy.

theorem sourceBlock_code_rate_lower_bound {α : Type*} [Fintype α] [DecidableEq α] (p : α → ℝ) (hp : ∀ i, 0 ≤ p i) (hs : ∑ i, p i = 1) (n : ℕ) (hn : 0 < n) (code : BinaryPrefixCode (SourceBlock α n)) : discreteEntropyBaseTwo Finset.univ p ≤ expectedCodeLength (sourceBlockMass p n) code / n

An actual family of block prefix codes has rate tending to entropy.

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

No convergent family of block prefix codes has limiting rate below entropy.

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