Lean module · Foundations
BanditRLProof.LowerBounds.UniformCoding
Generated source map for this Lean module.
Module map
Imports
BanditRLProof.LowerBounds.FixedLengthCoding, BanditRLProof.LowerBounds.PrefixCodeExchange
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.uniformPowerTwo_entropy
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.uniformPowerTwo_entropyReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem uniformPowerTwo_entropy {α : Type*} [Fintype α] (n : ℕ) (hcard : Fintype.card α = 2 ^ n) : discreteEntropyBaseTwo Finset.univ (fun _ : α => (1 / (2 : ℝ) ^ n)) = n
theorem
BanditRLProof.LowerBounds.fixedLength_uniformPowerTwo_optimal
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 · Chapter 14: Foundations of Information Theory
Canonical node identity
declaration:BanditRLProof.LowerBounds.fixedLength_uniformPowerTwo_optimalReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
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
def
BanditRLProof.LowerBounds.ternaryPrefixWord
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.ternaryPrefixWordReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
def ternaryPrefixWord (a : Fin 3) : List Bool
def
BanditRLProof.LowerBounds.ternaryPrefixCode
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.ternaryPrefixCodeReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
def ternaryPrefixCode : BinaryPrefixCode (Fin 3) where
theorem
BanditRLProof.LowerBounds.ternaryPrefixCode_uniform_length
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.ternaryPrefixCode_uniform_lengthReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem ternaryPrefixCode_uniform_length : expectedCodeLength (fun _ : Fin 3 => (1 / 3 : ℝ)) ternaryPrefixCode = 5 / 3
theorem
BanditRLProof.LowerBounds.uniform_three_fixedLength_not_optimal
Compiled
Uniform masses do not make a constant-length code optimal for every alphabet size.
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.uniform_three_fixedLength_not_optimalReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem uniform_three_fixedLength_not_optimal (code : BinaryPrefixCode (Fin 3)) (hlen : ∀ a, (code.encode a).length = 2) : ¬ IsOptimalPrefixCode (fun _ : Fin 3 => (1 / 3 : ℝ)) code