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.
Used in these reading views: Bandit Book
10. Automation, resources, and open routes
Canonical node identity
declaration:BanditRLProof.UpstreamRefReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
structure UpstreamRef where
def
BanditRLProof.lmlRef
Compiled
Main upstream Lean library for bandit formalization.
Used in these reading views: Bandit Book
10. Automation, resources, and open routes
Canonical node identity
declaration:BanditRLProof.lmlRefReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
def lmlRef : UpstreamRef where
def
BanditRLProof.lmlBanditDeclarationCards
Compiled
Selected LML declarations that seed the retrieval memory.
Used in these reading views: Bandit Book
10. Automation, resources, and open routes
Canonical node identity
declaration:BanditRLProof.lmlBanditDeclarationCardsReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
def lmlBanditDeclarationCards : List RegretBoundCard