BanditRLlib
Lean gate passed before this site build; local proof declarations are shown as compiled.Lean-verified build · exact declarations linked.

Generated from every Lean source module

Declaration catalog

10,434 indexed public and private declarations. The catalog is exhaustive for the supported declaration kinds; teaching chapters add detailed explanations to the major mathematical interfaces.

Search and filter

Showing the first 20 of 10,434 declarations.

DeclarationKindChapterModuleStatusSource
BanditRLProof.ArmStreamPolicy.history definition Foundations BanditRLProof.Algorithms.ArmStreamPolicy Compiled BanditRLProof/Algorithms/ArmStreamPolicy.lean:10
BanditRLProof.ArmStreamPolicy.action definition Foundations BanditRLProof.Algorithms.ArmStreamPolicy Compiled BanditRLProof/Algorithms/ArmStreamPolicy.lean:20
BanditRLProof.ArmStreamPolicy.reward definition Foundations BanditRLProof.Algorithms.ArmStreamPolicy Compiled BanditRLProof/Algorithms/ArmStreamPolicy.lean:25
BanditRLProof.ArmStreamPolicy.action_zero theorem Foundations BanditRLProof.Algorithms.ArmStreamPolicy Compiled BanditRLProof/Algorithms/ArmStreamPolicy.lean:29
BanditRLProof.ArmStreamPolicy.action_succ theorem Foundations BanditRLProof.Algorithms.ArmStreamPolicy Compiled BanditRLProof/Algorithms/ArmStreamPolicy.lean:32
BanditRLProof.ArmStreamPolicy.history_eq_trace theorem Foundations BanditRLProof.Algorithms.ArmStreamPolicy Compiled BanditRLProof/Algorithms/ArmStreamPolicy.lean:36
BanditRLProof.ArmStreamPolicy.measurable_history theorem Foundations BanditRLProof.Algorithms.ArmStreamPolicy Compiled BanditRLProof/Algorithms/ArmStreamPolicy.lean:55
BanditRLProof.ArmStreamPolicy.measurable_action theorem Foundations BanditRLProof.Algorithms.ArmStreamPolicy Compiled BanditRLProof/Algorithms/ArmStreamPolicy.lean:74
BanditRLProof.ArmStreamPolicy.history_ucb theorem Foundations BanditRLProof.Algorithms.ArmStreamPolicy Compiled BanditRLProof/Algorithms/ArmStreamPolicy.lean:82
BanditRLProof.CUCB.SourceModel.integrable_actual_reward theorem Foundations BanditRLProof.Algorithms.CUCBActualReward Compiled BanditRLProof/Algorithms/CUCBActualReward.lean:11
BanditRLProof.CUCB.SourceModel.actual_reward_expectation theorem Foundations BanditRLProof.Algorithms.CUCBActualReward Compiled BanditRLProof/Algorithms/CUCBActualReward.lean:37
BanditRLProof.CUCB.SourceModel.cumulative_actual_reward_expectation theorem Foundations BanditRLProof.Algorithms.CUCBActualReward Compiled BanditRLProof/Algorithms/CUCBActualReward.lean:68
BanditRLProof.CUCB.SourceModel.approximationRegret definition Foundations BanditRLProof.Algorithms.CUCBActualReward Compiled BanditRLProof/Algorithms/CUCBActualReward.lean:77
BanditRLProof.CUCB.SourceModel.approximationRegret_zero theorem Foundations BanditRLProof.Algorithms.CUCBActualReward Compiled BanditRLProof/Algorithms/CUCBActualReward.lean:82
BanditRLProof.CUCB.SourceModel.approximationRegret_eq_mean theorem Foundations BanditRLProof.Algorithms.CUCBActualReward Compiled BanditRLProof/Algorithms/CUCBActualReward.lean:85
BanditRLProof.CUCB.SourceModel.integrable_actual_gap theorem Foundations BanditRLProof.Algorithms.CUCBActualReward Compiled BanditRLProof/Algorithms/CUCBActualReward.lean:91
BanditRLProof.CUCB.SourceModel.approximationRegret_eq_gap_sum theorem Foundations BanditRLProof.Algorithms.CUCBActualReward Compiled BanditRLProof/Algorithms/CUCBActualReward.lean:97
BanditRLProof.CUCB.ChargeData structure Foundations BanditRLProof.Algorithms.CUCBCharge Compiled BanditRLProof/Algorithms/CUCBCharge.lean:12
BanditRLProof.CUCB.ChargeData.choose definition Foundations BanditRLProof.Algorithms.CUCBCharge Compiled BanditRLProof/Algorithms/CUCBCharge.lean:26
BanditRLProof.CUCB.ChargeData.counters definition Foundations BanditRLProof.Algorithms.CUCBCharge Compiled BanditRLProof/Algorithms/CUCBCharge.lean:31
How a concept search connects to reusable Lean

Every search result links to its exact statement, source location, module context, chapter explanation, and recorded dependency neighborhood.

flowchart LR
    Search["Search a mathematical concept"] --> Decl["Exact Lean declaration"]
    Decl --> Statement["Statement + namespace + source line"]
    Decl --> Module["Owning module"]
    Module --> Imports["Imported prerequisites"]
    Decl --> Consumers["Downstream declarations"]
    Statement --> Chapter["Teaching explanation in Book Map"]
    Chapter --> Map["Implementation status and missing obligations"]
How a BanditRLlib concept search leads to source, dependencies, consumers, and teaching context · editable Mermaid source