Mathematics ↔ prose ↔ Lean
Implementation map
A theorem-route milestone can be locally compiled, partial, stated without a finished proof, planned, or blocked. The declaration catalog below is generated from source; the milestone ledger records the mathematical boundary.
Mathematical milestone map
Start with the mathematical claim and status. Open a row's evidence only when you need exact declarations, dependencies, and the remaining boundary.
- Compiled
- 86 routes
- Partial
- 8 routes
- Blocked
- 2 routes
- Planned
- 1 routes
11 routes are not terminal. 8 partial · 2 blocked · 1 planned. These remain visible evidence, not completed results.
Showing the first 12 of 97 milestones.
| Result | Chapter | Status | Meaning and evidence |
|---|---|---|---|
Repaired parallel causal allocation and actual expected simple regretCAUSAL-PARALLEL-ACTUAL-REGRET |
UCB | Compiled | For N>=2 known independent binary roots, the constructed strict rarity r and normalized allocation have actual design cost<=2r, including q=0/1. Actual graph-law transport gives expected regret <=(2sqrt(2)+7)sqrt(2r log(2TK)/T)+1/T for the repaired design and… Lean evidence and boundary
|
Causal actual-sampling expected simple regret on a common finite alphabetCAUSAL-COMMON-ALPHABET-EXPECTED-REGRET |
UCB | Compiled | Actual intervention samples and fixed-order empirical recommendation satisfy R_T <= (2sqrt(2)+7)sqrt(m log(2TK)/T)+1/T and R_T<=1; explicit rate constant 3sqrt(2)+7. Internally derived confidence, binary reward readout and covered allocation. Independently… Lean evidence and boundary
|
HOO full expected regret for arbitrary reward familiesHOO-REWARD-FAMILY-RATE |
UCB | Compiled | The same causal HOO trajectory with arbitrary arm-indexed probability reward laws satisfies the all-horizon source-repaired dimension rate, without global reward-kernel measurability. Actual and pseudo-regret expectations coincide. Fixed choices… Lean evidence and boundary
|
Finite raw-moment regret supremum and actual-law adapterHEAVY-TAIL-GENALTI-FINITE-SUPREMUM |
UCB | Compiled | At each finite horizon, actual raw-moment arm laws and arbitrary probability trace laws yield normalized expected pseudo-regret at most2T; the EReal supremum is not positive infinity. The actual-process pushforward preserves the integral. A two-arm+1/-1… Lean evidence and boundary
|
Finite counterexample to the printed source-policy regret coefficientHEAVY-TAIL-PRINTED-REGRET-COUNTEREXAMPLE |
UCB | Compiled | For the unchanged source-radius4/r^-2 policy with its permissible deterministic ties, valid Dirac0/-1 arm laws and epsilon=u=1, expected pseudo-regret at T=2^50 exceeds32logT+5. The actual finite count contradiction, raw-second-moment witness, product-law… Lean evidence and boundary
|
Clipped-prefix confidence under consumed-sample corruptionHEAVY-TAIL-CLIPPED-CORRUPTION-TRANSFER |
UCB | Compiled | Independent clean coordinates with raw p moments produce clipped-mean confidence at any outcome-dependent positive count N<=t, enlarged by C/N for a pathwise consumed-prefix corruption budget. Nonmeasurable count/adversary events use finite outer measure.… Lean evidence and boundary
|
Corrected expected regret for source-parameter robust UCBHEAVY-TAIL-CORRECTED-SOURCE-REGRET |
UCB | Compiled | For the unchanged radius4/r^-2 causal policy, raw p moments imply expected pseudo-regret at most sum over positive gaps of Delta*(A+5), A=2log(max(T,1))/(Delta/(8u^(1/p)))^(p/epsilon). This explicit corrected coefficient is128u/Delta at epsilon1; the… Lean evidence and boundary
|
Source-schedule causal robust-UCB confidence budgetsHEAVY-TAIL-SOURCE-SCHEDULE-CONFIDENCE |
UCB | Compiled | The actual history-based robust UCB with source radius4 and paper-round confidence parameter r^(-2) has each per-arm signed deviation probability at most t exp(-5L_t/4), L_t=2log(t+1), after initialization. Each signed finite-time event-probability sum is at… Lean evidence and boundary
|
Sample-index truncated confidence with source radius fourHEAVY-TAIL-SOURCE-CONFIDENCE-FOUR |
Probability layer | Compiled | For independent common-mean samples with bounded raw (1+epsilon)-moments, each closed signed deviation of the unchanged sample-index truncated mean at radius 4 u^(1/(1+epsilon)) (L/n)^(epsilon/(1+epsilon)) has probability at most exp(-5L/4), for L>0. This… Lean evidence and boundary
|
Finite-arm pseudo-regret decompositionFOUNDATION-REGRET-DECOMPOSITION |
Foundations | Compiled | Finite-horizon pseudo-regret equals the sum over arms of each gap multiplied by its pull count. Lean evidence and boundary
|
Generated-history conditional sub-Gaussian reward lawPROBABILITY-GENERATED-COND-MGF |
Probability layer | Compiled | A selected successor reward on the canonical generated trajectory inherits the centered conditional MGF bound supplied by its step kernel. Lean evidence and boundary
|
Finite-index geometric all-time confidence unionPROBABILITY-FINTYPE-GEOMETRIC-ALL-TIME-UNION |
Probability layer | Compiled | If every index in a nonempty finite family receives an equal geometric confidence share at every time, the outer measure of any time-index failure is at most the total confidence budget. Lean evidence and boundary
|
How to read compiled, partial, stated, planned, and blocked
Compiled
The named declaration exists and the publishing gate compiled the Lean project.
Partial
Useful declarations compile, but the stated route still has named missing steps.
Stated, proof incomplete
A target or Lean declaration is stated but its proof is incomplete. None is promoted to compiled.
Planned
The result is part of the roadmap but has no claimed local endpoint.
Blocked
Progress requires a specific missing law transport, algorithm construction, or mathematical interface.
flowchart LR Math["Natural-language model and theorem"] --> Ledger["Assumption ledger"] Ledger --> Statement["Exact Lean statement"] Statement --> DAG["Proof-DAG leaves"] DAG --> Decl["Compiled declaration"] Decl --> Explain["Plain-English explanation"] Explain --> Map["Implementation map"] Map --> IDE["Research IDE mapping + dependency tree"] IDE -. "local compile request" .-> Decl Map -. "source link" .-> Decl Map -. "mathematical back-link" .-> Math Cards["Theorem and retrieval cards"] -. "route evidence only" .-> Ledger Cards -. "never a local proof certificate" .-> Map
Major theorem dependencies
The overview names the shared core; five focused, editable diagrams preserve readable labels for each algorithm family. They stay collapsed until requested so the milestone search remains the primary reading path. Module pages list exact import dependencies.
Open six editable theorem-dependency maps
flowchart LR Core["Shared proof core<br/>models · generated trajectories<br/>conditional reward laws"] Core --> Stochastic["Finite stochastic<br/>ETC · UCB"] Core --> OFUL["Linear optimism<br/>OFUL · stopping"] Core --> Thompson["Bayesian route<br/>Thompson sampling"] Core --> Adversarial["Adversarial route<br/>EXP3 · Tsallis-FTRL"] Core --> RL["Finite-horizon RL<br/>UCBVI-CH"] Stochastic --> Regret["Regret terminals"] OFUL --> Regret Thompson --> Regret Adversarial --> Regret RL --> Regret
flowchart TB Model["FiniteBanditModel"] --> Decomp["pseudoRegret = Σ gap × pullCount"] Trace["ActionTrace / RewardTrace"] --> Decomp Policy["MeasurablePolicy"] --> Traj["generated history kernels<br/>and trajectory measure"] Kernel["conditional reward-kernel contracts"] --> Traj Traj --> CondMGF["selected centered-reward<br/>conditional MGF"] CondMGF --> Concentration["sub-Gaussian and<br/>martingale tails"] Decomp --> ETC["ETC expected regret"] Concentration --> ETC Decomp --> UCB["UCB gap-sum and<br/>average consistency"] Concentration --> UCB
flowchart TB GramDet["Gram matrix and<br/>rank-one determinant"] --> Ellipse["log-det and<br/>elliptical potential"] Ellipse --> SelfNorm["self-normalized confidence"] CondMGF["conditional reward MGF"] --> SelfNorm SelfNorm --> Ridge["ridge confidence ellipsoid"] Ridge --> Optimistic["measurable optimistic policy"] Optimistic --> AllTime["one-policy all-time confidence"] AllTime --> OFULRate["same-policy all-horizon<br/>pseudo-regret"] OFULRate --> StopBounded["bounded stopping consumer"] OFULRate --> StopL2["square-integrable<br/>stopping consumer"] Ridge --> Expected["separate horizon-indexed<br/>expectation and consistency"]
flowchart TB Prior["prior"] --> Posterior["posterior kernel"] Likelihood["likelihood kernel"] --> Posterior Posterior --> Match["one-step probability matching"] Match --> Recursive["recursive generated<br/>Thompson trajectory"] Traj["generated trajectory law"] --> Recursive Recursive --> Bayes["comparator / Bayesian<br/>regret decomposition"] Selector["pointwise mean-optimal selector"] --> Bayes Bayes --> Clipped["clipped confidence bridge"] Clipped --> Latent["stationary latent-arm stream"] Latent --> Terminal["generated stationary<br/>Bayesian-regret terminal"]
flowchart TB Hedge["EXP3 potential and Hedge"] --> IW["importance-weighted support<br/>and conditional moments"] Traj["generated trajectory law"] --> IW IW --> Expected["horizon-tuned expected regret"] IW --> Window["best-arm realized tail"] Concentration["martingale concentration"] --> Window IW --> Predictable["predictable all-prefix event"] Concentration --> Deviation["realized-deviation<br/>all-prefix event"] Predictable --> EXP3All["same-process all-prefix regret"] Deviation --> EXP3All IW --> Sparse["sparse / variance-sensitive route"] FTRL["half-Tsallis simplex minimizer"] --> Stability["one-step stability and penalty"] Stability --> Generated["scheduled generated action law"] Traj --> Generated Generated --> Alignment["observed IW score alignment"] Alignment --> AllRate["all-rate expected regret"] AllRate --> SelfBound["fixed-gap self-bounding"] SelfBound --> IID["bounded-IID logarithmic regret"] SelfBound --> Dynamic["corruption and dynamic routes"] Dynamic --> Restart["population-mean oracle restart"]
flowchart TB MDP["finite-horizon MDP"] --> Bellman["optimal Bellman recursion"] Bellman --> Occupancy["occupancy-gap identity"] Episodes["generated adaptive episodes"] --> Counts["strict-prefix aggregate counts"] Counts --> Empirical["aggregate empirical transition"] Empirical --> Planner["previous-Q clipped<br/>UCBVI-CH planner"] Planner --> Policy["measurable argmax policy"] CondMGF["same-law conditional MGF"] --> Confidence["transition and value confidence"] Counts --> Confidence Confidence --> Optimism["all-episode Bellman optimism"] Planner --> Optimism Occupancy --> EpisodeRegret["generated-episode pseudo-regret"] Policy --> EpisodeRegret Optimism --> Decomp["charge and innovation decomposition"] EpisodeRegret --> Decomp Counts --> CountSum["actual-count charge summation"] CondMGF --> Martingale["generated-filtration<br/>innovation tail"] Decomp --> Terminal["20/250 high-probability<br/>UCBVI-CH terminal"] CountSum --> Terminal Martingale --> Terminal Terminal --> Expected["expected regret + K H δ"] Confidence --> Behavior["natural-causal consistency"] StopL2["L2 stopping foundation"] --> Hitting["uncapped inverse-sqrt hitting"] Behavior --> Hitting Hitting --> ExpectedHit["stopped-value expectation bound"] Terminal -. "separate milestone" .-> Bernstein["Bernstein / minimax UCB-VI"]
Complete module inventory
Every project module is assigned to a teaching chapter. The first page is included in the HTML; search and “show more” progressively load the complete generated inventory, keeping the mathematical milestones fast and primary.
Open the complete generated module inventory (796 modules)
Showing the first 30 of 796 modules.