Lean module · Frontier
BanditRLProof.Literature
# Literature and upstream theorem registry
Module map
Imports
BanditRLProof.Algorithms.ETC, BanditRLProof.Algorithms.UCB, BanditRLProof.Algorithms.Thompson
Imported by
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
structure
BanditRLProof.UpstreamRef
Compiled
Public upstream source used by the memory layer.
structure UpstreamRef where
def
BanditRLProof.lmlRef
Compiled
Main upstream Lean library for bandit formalization.
def lmlRef : UpstreamRef where
def
BanditRLProof.lmlBanditDeclarationCards
Compiled
Selected LML declarations that seed the retrieval memory.
def lmlBanditDeclarationCards : List RegretBoundCard