Lean module · Foundations
BanditRLProof.Algorithms.CausalAllocationRegret
The actual learner under uniform and attained optimal covered allocations.
Module map
Imports
BanditRLProof.Algorithms.CausalExpectedRegret
Imported by
BanditRLProof, BanditRLProof.Algorithms.CausalHeterogeneousSampling, BanditRLProof.Algorithms.CausalParallelRegret
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.Causal.GraphModel.expected_simpleRegret_uniform
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: Causal bandits
Canonical node identity
declaration:BanditRLProof.Causal.GraphModel.expected_simpleRegret_uniformReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem GraphModel.expected_simpleRegret_uniform (g : GraphModel V n) (rewardBit : V → Bool) (actions : A → Fin n → Option V) (i : Fin n) (hi : ∀ a, actions a i = none) (T : ℕ) (hT : 0 < T) : let eta := PMF.uniformOfFintype A let m := designCost (fun a => g.parentLaw (actions a) i) eta let L := sourceLog T (Fintype.card A) let B := sourceThreshold m T L (∫ w, g.simpleRegret rewardBit actions eta i B w ∂g.sampleLaw actions eta T) ≤ (2*Real.sqrt 2+7)*Real.sqrt ((Fintype.card A:ℝ)*L/T) + 1/(T:ℝ)
theorem
BanditRLProof.Causal.GraphModel.expected_simpleRegret_optimal
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: Causal bandits
Canonical node identity
declaration:BanditRLProof.Causal.GraphModel.expected_simpleRegret_optimalReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem GraphModel.expected_simpleRegret_optimal (g : GraphModel V n) (rewardBit : V → Bool) (actions : A → Fin n → Option V) (i : Fin n) (hi : ∀ a, actions a i = none) (T : ℕ) (hT : 0 < T) : let p := fun a => g.parentLaw (actions a) i let eta := optimalAllocation p let m := designCost p eta let L := sourceLog T (Fintype.card A) let B := sourceThreshold m T L (∫ w, g.simpleRegret rewardBit actions eta i B w ∂g.sampleLaw actions eta T) ≤ (2*Real.sqrt 2+7)*Real.sqrt (m*L/T) + 1/(T:ℝ)