Lean module · Foundations
BanditRLProof.LowerBounds.CodingEntropyBound
Generated source map for this Lean module.
Module map
Imports
BanditRLProof.LowerBounds.InformationTheory
Imported by
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.LowerBounds.entropy_term_le_codeLength_remainder
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.LowerBounds.entropy_term_le_codeLength_remainderReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem entropy_term_le_codeLength_remainder {p : ℝ} (hp : 0 ≤ p) (l : ℕ) : p * Real.log p⁻¹ ≤ p * l * Real.log 2 + (1 / 2 : ℝ) ^ l - p
theorem
BanditRLProof.LowerBounds.discreteEntropyBaseTwo_le_expectedCodeLength
Compiled
The lower half of Eq. (14.2), for every finite binary prefix code.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.LowerBounds.discreteEntropyBaseTwo_le_expectedCodeLengthReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem discreteEntropyBaseTwo_le_expectedCodeLength {Symbol : Type*} [Fintype Symbol] [DecidableEq Symbol] (p : Symbol → ℝ) (hp : ∀ i, 0 ≤ p i) (hsum : ∑ i, p i = 1) (code : BinaryPrefixCode Symbol) : discreteEntropyBaseTwo Finset.univ p ≤ expectedCodeLength p code