Lean module · Foundations
BanditRLProof.Algorithms.CausalExpectedRegret
Expected simple regret of the actual intervention sampler and recommendation. The finite-budget residual is retained explicitly.
Module map
Imports
BanditRLProof.Algorithms.CausalRecommendation
Imported by
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_le_tuned
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.Causal.GraphModel.expected_simpleRegret_le_tunedReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem GraphModel.expected_simpleRegret_le_tuned (g : GraphModel V n) (rewardBit : V → Bool) (actions : A → Fin n → Option V) (eta : PMF A) (i : Fin n) (hi : ∀ a, actions a i = none) (hc : Covers (fun a => g.parentLaw (actions a) i) (mixture eta (fun a => g.parentLaw (actions a) i))) (T : ℕ) (hT : 0 < T) : 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*sourceRadius m T L + m/B + 1/(T:ℝ)
theorem
BanditRLProof.Causal.GraphModel.expected_simpleRegret_bounds
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_boundsReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem GraphModel.expected_simpleRegret_bounds (g : GraphModel V n) (rewardBit : V → Bool) (actions : A → Fin n → Option V) (eta : PMF A) (i : Fin n) (B : ℝ) (T : ℕ) : 0 ≤ (∫ w, g.simpleRegret rewardBit actions eta i B w ∂g.sampleLaw actions eta T) ∧ (∫ w, g.simpleRegret rewardBit actions eta i B w ∂g.sampleLaw actions eta T) ≤ 1
theorem
BanditRLProof.Causal.GraphModel.expected_simpleRegret_source_bound
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_source_boundReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem GraphModel.expected_simpleRegret_source_bound (g : GraphModel V n) (rewardBit : V → Bool) (actions : A → Fin n → Option V) (eta : PMF A) (i : Fin n) (hi : ∀ a, actions a i = none) (hc : Covers (fun a => g.parentLaw (actions a) i) (mixture eta (fun a => g.parentLaw (actions a) i))) (T : ℕ) (hT : 0 < T) : 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 (m*L/T) + 1/(T:ℝ)
theorem
BanditRLProof.Causal.GraphModel.expected_simpleRegret_explicit_rate
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_explicit_rateReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem GraphModel.expected_simpleRegret_explicit_rate (g : GraphModel V n) (rewardBit : V → Bool) (actions : A → Fin n → Option V) (eta : PMF A) (i : Fin n) (hi : ∀ a, actions a i = none) (hc : Covers (fun a => g.parentLaw (actions a) i) (mixture eta (fun a => g.parentLaw (actions a) i))) (T : ℕ) (hT : 0 < T) : 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) ≤ (3*Real.sqrt 2+7)*Real.sqrt (m*L/T)