Lean module · Foundations
BanditRLProof.LowerBounds.FixedLengthCoding
Generated source map for this Lean module.
Module map
Imports
BanditRLProof.LowerBounds.DyadicAddresses
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.exists_fixedLengthPrefixCode
Compiled
A finite alphabet fitting in n bits has an actual fixed-length prefix code.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.LowerBounds.exists_fixedLengthPrefixCodeReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem exists_fixedLengthPrefixCode {α : Type*} [Fintype α] (n : ℕ) (hn : 0 < n) (hcapacity : Fintype.card α ≤ 2 ^ n) : ∃ code : BinaryPrefixCode α, ∀ a, (code.encode a).length = n
theorem
BanditRLProof.LowerBounds.exists_ceilingLogPrefixCode
Compiled
The source's ceiling-log binary code, for at least two symbols.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret · Chapter 14: Foundations of Information Theory
Canonical node identity
declaration:BanditRLProof.LowerBounds.exists_ceilingLogPrefixCodeReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem exists_ceilingLogPrefixCode {α : Type*} [Fintype α] (hcard : 1 < Fintype.card α) : ∃ code : BinaryPrefixCode α, ∀ a, (code.encode a).length = Nat.clog 2 (Fintype.card α)
theorem
BanditRLProof.LowerBounds.expectedCodeLength_fixedLength
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.expectedCodeLength_fixedLengthReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem expectedCodeLength_fixedLength {α : Type*} [Fintype α] (p : α → ℝ) (hs : ∑ a, p a = 1) (code : BinaryPrefixCode α) (n : ℕ) (hlen : ∀ a, (code.encode a).length = n) : expectedCodeLength p code = n