Lean module · Frontier
BanditRLProof.BudgetStoppingTime
# Budget stopping-time wrappers This module exposes a narrow Mathlib-backed stopping-time surface for resource/budget processes. It deliberately stays at the filtration foundation layer: no knapsack model, policy construction, optional stopping theorem, or regret theorem is introduced here.
Module map
Imports
No project-local imports.
Imported by
BanditRLProof, BanditRLProof.OFULScheduledBudgetExhaustionExpectedRegret
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
def
BanditRLProof.Budget.budgetExhaustionTime
Compiled
First time an accumulated `Nat` resource process reaches a budget. This is a project-local name for Mathlib's `hittingAfter` specialized to the upper set `{spent >= budget}` and start time `0`.
noncomputable def budgetExhaustionTime {Omega : Type u} (spent : Nat -> Omega -> Nat) (budget : Nat) : Omega -> WithTop Nat
theorem
BanditRLProof.Budget.isStoppingTime_budgetExhaustionTime_of_adapted
Compiled
An adapted accumulated-resource process has a budget-exhaustion stopping time. This is the `STOPPING-TIME-BUDGET` wrapper over `MeasureTheory.Adapted.isStoppingTime_hittingAfter`.
theorem isStoppingTime_budgetExhaustionTime_of_adapted {Omega : Type u} [mOmega : MeasurableSpace Omega] {F : Filtration Nat mOmega} {spent : Nat -> Omega -> Nat} (budget : Nat) (hspent : Adapted F spent) : IsStoppingTime F (budgetExhaustionTime spent budget)
theorem
BanditRLProof.Budget.measurableSet_budgetExhaustionTime_le_of_adapted
Compiled
At each horizon `n`, the event that the budget has already been exhausted is measurable at filtration level `n`.
theorem measurableSet_budgetExhaustionTime_le_of_adapted {Omega : Type u} [mOmega : MeasurableSpace Omega] {F : Filtration Nat mOmega} {spent : Nat -> Omega -> Nat} (budget n : Nat) (hspent : Adapted F spent) : MeasurableSet[F n] {omega | budgetExhaustionTime spent budget omega <= n}