BanditRLProof.LowerBounds.ShannonLengths

Strict Shannon length, leaving Kraft slack on every positive-mass symbol. This definition is not a prefix-code constructor.

def shannonLength (p : ℝ) : ℕ

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

theorem shannonLength_pos (p : ℝ) : 0 < shannonLength p

Each positive-mass symbol leaves strict Kraft slack.

theorem shannonLength_kraft_weight_lt {p : ℝ} (hp : 0 < p) : (1 / 2 : ℝ) ^ shannonLength p < p

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

theorem shannonLength_le_information_add_one {p : ℝ} (hp : 0 < p) (hp1 : p ≤ 1) : (shannonLength p : ℝ) ≤ Real.log p⁻¹ / Real.log 2 + 1

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

theorem weighted_shannonLength_le {p : ℝ} (hp : 0 ≤ p) (hp1 : p ≤ 1) : p * shannonLength p ≤ p * (Real.log p⁻¹ / Real.log 2) + p

A numerical expected-length bound; realizability by a prefix code is separate.

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

The positive support occupies strictly less than the available Kraft mass.

theorem sum_positive_shannon_weights_lt_one {α : Type*} [Fintype α] (p : α → ℝ) (hp : ∀ i, 0 ≤ p i) (hs : ∑ i, p i = 1) : (∑ i, if 0 < p i then (1 / 2 : ℝ) ^ shannonLength (p i) else 0) < 1

Complete length assignment, including zero-mass symbols; codewords are not yet constructed.

theorem exists_lengths_kraft_lt_one_entropy_bound {α : Type*} [Fintype α] (p : α → ℝ) (hp : ∀ i, 0 ≤ p i) (hs : ∑ i, p i = 1) : ∃ l : α → ℕ, (∀ i, 0 < l i) ∧ (∑ i, (1 / 2 : ℝ) ^ l i) < 1 ∧ (∑ i, p i * l i) ≤ discreteEntropyBaseTwo Finset.univ p + 1