Lean module · Foundations
BanditRLProof.Algorithms.CUCBTrajectory
The actual CUCB trajectory first samples a feasible oracle action, then its fresh triggered feedback. Neither concentration nor oracle success is assumed by this construction; those properties must be derived separately.
Module map
Imports
BanditRLProof.Algorithms.CUCBHistory
Imported by
BanditRLProof, BanditRLProof.Algorithms.CUCBCharge, BanditRLProof.Algorithms.CUCBObservationMGF
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
abbrev
BanditRLProof.CUCB.Round
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.CUCB.RoundReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
abbrev Round (A : Type*) (m : ℕ)
abbrev
BanditRLProof.CUCB.Input
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.CUCB.InputReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
abbrev Input (m : ℕ)
def
BanditRLProof.CUCB.emptyFeedback
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.CUCB.emptyFeedbackReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
def emptyFeedback (m : ℕ) : Feedback m
def
BanditRLProof.CUCB.initialInput
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.CUCB.initialInputReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
def initialInput (m : ℕ) : Input m
theorem
BanditRLProof.CUCB.oracleInput_zero
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.CUCB.oracleInput_zeroReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem oracleInput_zero {m : ℕ} (Y : ℕ → Feedback m) : oracleInput Y 0 = initialInput m
def
BanditRLProof.CUCB.roundKernel
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.CUCB.roundKernelReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
noncomputable def roundKernel (oracle : Kernel (Input m) A) (environment : Kernel A (Feedback m)) : Kernel (Input m) (Round A m)
theorem
BanditRLProof.CUCB.roundKernel_rectangle
Compiled
The oracle draw precedes environment feedback; the latter depends on the realized action, not on an independently redrawn action.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.CUCB.roundKernel_rectangleReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem roundKernel_rectangle (oracle : Kernel (Input m) A) (environment : Kernel A (Feedback m)) [IsMarkovKernel oracle] [IsMarkovKernel environment] (v : Input m) (s : Set A) (t : Set (Feedback m)) (hs : MeasurableSet s) (ht : MeasurableSet t) : roundKernel oracle environment v (s ×ˢ t) = ∫⁻ a in s, environment a t ∂oracle v
theorem
BanditRLProof.CUCB.roundKernel_action_law
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.CUCB.roundKernel_action_lawReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem roundKernel_action_law (oracle : Kernel (Input m) A) (environment : Kernel A (Feedback m)) [IsMarkovKernel oracle] [IsMarkovKernel environment] (v : Input m) : (roundKernel oracle environment v).map Prod.fst = oracle v
def
BanditRLProof.CUCB.feedbackExtension
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.CUCB.feedbackExtensionReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
def feedbackExtension (n : ℕ) (h : (i : Finset.Iic n) → Round A m) : ℕ → Feedback m
theorem
BanditRLProof.CUCB.measurable_feedbackExtension
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.CUCB.measurable_feedbackExtensionReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem measurable_feedbackExtension (n : ℕ) : Measurable (feedbackExtension (A:=A) (m:=m) n)
theorem
BanditRLProof.CUCB.oracleInput_feedbackExtension
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.CUCB.oracleInput_feedbackExtensionReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem oracleInput_feedbackExtension (Y : ℕ → Round A m) (n : ℕ) : oracleInput (feedbackExtension n (Preorder.frestrictLe n Y)) (n+1) = oracleInput (fun t => (Y t).2) (n+1)
def
BanditRLProof.CUCB.cucbStepKernel
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.CUCB.cucbStepKernelReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
noncomputable def cucbStepKernel (oracle : Kernel (Input m) A) (environment : Kernel A (Feedback m)) (n : ℕ) : Kernel ((i : Finset.Iic n) → Round A m) (Round A m)
def
BanditRLProof.CUCB.cucbTrajectory
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Indexed settings: Combinatorial bandits
Canonical node identity
declaration:BanditRLProof.CUCB.cucbTrajectoryReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
noncomputable def cucbTrajectory (oracle : Kernel (Input m) A) (environment : Kernel A (Feedback m)) [IsMarkovKernel oracle] [IsMarkovKernel environment] : Measure (ℕ → Round A m)
theorem
BanditRLProof.CUCB.cucbStepKernel_apply_prefix
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.CUCB.cucbStepKernel_apply_prefixReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem cucbStepKernel_apply_prefix (oracle : Kernel (Input m) A) (environment : Kernel A (Feedback m)) (Y : ℕ → Round A m) (n : ℕ) : cucbStepKernel oracle environment n (Preorder.frestrictLe n Y) = roundKernel oracle environment (oracleInput (fun t => (Y t).2) (n+1))
theorem
BanditRLProof.CUCB.cucbTrajectory_prefix_compProd
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.CUCB.cucbTrajectory_prefix_compProdReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem cucbTrajectory_prefix_compProd (oracle : Kernel (Input m) A) (environment : Kernel A (Feedback m)) [IsMarkovKernel oracle] [IsMarkovKernel environment] (n : ℕ) : (cucbTrajectory oracle environment).map (Preorder.frestrictLe n) ⊗ₘ cucbStepKernel oracle environment n = (cucbTrajectory oracle environment).map (fun Y => (Preorder.frestrictLe n Y, Y (n+1)))
theorem
BanditRLProof.CUCB.cucbTrajectory_condDistrib
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.CUCB.cucbTrajectory_condDistribReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem cucbTrajectory_condDistrib [StandardBorelSpace A] [Nonempty A] (oracle : Kernel (Input m) A) (environment : Kernel A (Feedback m)) [IsMarkovKernel oracle] [IsMarkovKernel environment] (n : ℕ) : condDistrib (fun Y : ℕ → Round A m => Y (n+1)) (Preorder.frestrictLe n) (cucbTrajectory oracle environment) =ᵐ[ (cucbTrajectory oracle environment).map (Preorder.frestrictLe n)] cucbStepKernel oracle environment n
theorem
BanditRLProof.CUCB.cucbTrajectory_initial_law
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.CUCB.cucbTrajectory_initial_lawReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem cucbTrajectory_initial_law (oracle : Kernel (Input m) A) (environment : Kernel A (Feedback m)) [IsMarkovKernel oracle] [IsMarkovKernel environment] : (cucbTrajectory oracle environment).map (fun Y => Y 0) = roundKernel oracle environment (initialInput m)