Lean module · Foundations
BanditRLProof.LowerBounds.DyadicAddresses
Generated source map for this Lean module.
Module map
Imports
BanditRLProof.LowerBounds.ArithmeticIntervals
Imported by
BanditRLProof, BanditRLProof.LowerBounds.ArithmeticPrefixCode, BanditRLProof.LowerBounds.FixedLengthCoding
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
def
BanditRLProof.LowerBounds.binaryAddressValue
Compiled
Big-endian binary address, with leading zeroes retained by the word length.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.LowerBounds.binaryAddressValueReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
def binaryAddressValue : List Bool → ℕ | [] => 0 | b :: w => (if b then 2 ^ w.length else 0) + binaryAddressValue w theorem binaryAddressValue_lt (w : List Bool) : binaryAddressValue w < 2 ^ w.length
theorem
BanditRLProof.LowerBounds.binaryAddressValue_lt
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.binaryAddressValue_ltReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem binaryAddressValue_lt (w : List Bool) : binaryAddressValue w < 2 ^ w.length
theorem
BanditRLProof.LowerBounds.exists_binaryAddress
Compiled
Every dyadic cell index has a binary address of the specified length.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.LowerBounds.exists_binaryAddressReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem exists_binaryAddress (n m : ℕ) (hm : m < 2 ^ n) : ∃ w : List Bool, w.length = n ∧ binaryAddressValue w = m
theorem
BanditRLProof.LowerBounds.binaryAddressValue_append
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.binaryAddressValue_appendReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem binaryAddressValue_append (u v : List Bool) : binaryAddressValue (u ++ v) = binaryAddressValue u * 2 ^ v.length + binaryAddressValue v
def
BanditRLProof.LowerBounds.dyadicAddressLower
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.dyadicAddressLowerReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
noncomputable def dyadicAddressLower (w : List Bool) : ℝ
def
BanditRLProof.LowerBounds.dyadicAddressUpper
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.dyadicAddressUpperReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
noncomputable def dyadicAddressUpper (w : List Bool) : ℝ
theorem
BanditRLProof.LowerBounds.dyadicAddress_width
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.dyadicAddress_widthReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem dyadicAddress_width (w : List Bool) : dyadicAddressUpper w - dyadicAddressLower w = 1 / (2 : ℝ) ^ w.length
theorem
BanditRLProof.LowerBounds.dyadicAddress_nonempty
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.dyadicAddress_nonemptyReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem dyadicAddress_nonempty (w : List Bool) : dyadicAddressLower w < dyadicAddressUpper w
theorem
BanditRLProof.LowerBounds.dyadicAddress_append_contained
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.dyadicAddress_append_containedReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem dyadicAddress_append_contained (u v : List Bool) : dyadicAddressLower u ≤ dyadicAddressLower (u ++ v) ∧ dyadicAddressUpper (u ++ v) ≤ dyadicAddressUpper u
theorem
BanditRLProof.LowerBounds.dyadicAddress_prefix_contained
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.dyadicAddress_prefix_containedReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem dyadicAddress_prefix_contained (u v : List Bool) (h : u <+: v) : dyadicAddressLower u ≤ dyadicAddressLower v ∧ dyadicAddressUpper v ≤ dyadicAddressUpper u
theorem
BanditRLProof.LowerBounds.exists_dyadicAddress_inside
Compiled
Select an actual binary word whose dyadic cell fits inside the given interval.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.LowerBounds.exists_dyadicAddress_insideReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem exists_dyadicAddress_inside (L U : ℝ) (n : ℕ) (hL : 0 ≤ L) (hU : U ≤ 1) (hwidth : 2 * (1 / (2 : ℝ) ^ n) ≤ U - L) : ∃ w : List Bool, w.length = n ∧ L ≤ dyadicAddressLower w ∧ dyadicAddressUpper w < U