Lean module · Foundations
BanditRLProof.Algorithms.CausalRecommendation
A fixed-order recommendation from observed estimates and its pathwise regret bound.
Module map
Imports
BanditRLProof.Algorithms.CausalConfidence, BanditRLProof.FiniteRealArgmax
Imported by
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
def
BanditRLProof.Causal.maximizingActions
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.maximizingActionsReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
noncomputable def maximizingActions (score : A → ℝ) : Finset A
theorem
BanditRLProof.Causal.maximizingActions_nonempty
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.maximizingActions_nonemptyReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem maximizingActions_nonempty (score : A → ℝ) : (maximizingActions score).Nonempty
def
BanditRLProof.Causal.orderedArgmax
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.orderedArgmaxReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
noncomputable def orderedArgmax (score : A → ℝ) : A
theorem
BanditRLProof.Causal.score_le_orderedArgmax
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.score_le_orderedArgmaxReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem score_le_orderedArgmax (score : A → ℝ) (a : A) : score a ≤ score (orderedArgmax score)
theorem
BanditRLProof.Causal.orderedArgmax_le_of_maximal
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.orderedArgmax_le_of_maximalReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem orderedArgmax_le_of_maximal (score : A → ℝ) (a : A) (ha : ∀ b, score b ≤ score a) : orderedArgmax score ≤ a
def
BanditRLProof.Causal.GraphModel.rewardMean
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.rewardMeanReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
noncomputable def GraphModel.rewardMean (g : GraphModel V n) (rewardBit : V → Bool) (actions : A → Fin n → Option V) (i : Fin n) (a : A) : ℝ
theorem
BanditRLProof.Causal.GraphModel.rewardMean_eq_integral
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.rewardMean_eq_integralReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem GraphModel.rewardMean_eq_integral (g : GraphModel V n) (rewardBit : V → Bool) (actions : A → Fin n → Option V) (i : Fin n) (a : A) (hi : actions a i = none) : g.rewardMean rewardBit actions i a = ∫ x, (if rewardBit (x i) then (1:ℝ) else 0) ∂(joint (g.doModel (actions a)).table).toMeasure
theorem
BanditRLProof.Causal.GraphModel.rewardMean_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
Canonical node identity
declaration:BanditRLProof.Causal.GraphModel.rewardMean_boundsReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem GraphModel.rewardMean_bounds (g : GraphModel V n) (rewardBit : V → Bool) (actions : A → Fin n → Option V) (i : Fin n) (a : A) : 0 ≤ g.rewardMean rewardBit actions i a ∧ g.rewardMean rewardBit actions i a ≤ 1
def
BanditRLProof.Causal.GraphModel.sampleRecommendation
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.sampleRecommendationReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
noncomputable def GraphModel.sampleRecommendation (g : GraphModel V n) (rewardBit : V → Bool) (actions : A → Fin n → Option V) (eta : PMF A) (i : Fin n) (B : ℝ) {T : ℕ} (w : Fin T → A × (Fin n → V)) : A
def
BanditRLProof.Causal.GraphModel.simpleRegret
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.simpleRegretReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
noncomputable def GraphModel.simpleRegret (g : GraphModel V n) (rewardBit : V → Bool) (actions : A → Fin n → Option V) (eta : PMF A) (i : Fin n) (B : ℝ) {T : ℕ} (w : Fin T → A × (Fin n → V)) : ℝ
theorem
BanditRLProof.Causal.GraphModel.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
Canonical node identity
declaration:BanditRLProof.Causal.GraphModel.simpleRegret_boundsReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem GraphModel.simpleRegret_bounds (g : GraphModel V n) (rewardBit : V → Bool) (actions : A → Fin n → Option V) (eta : PMF A) (i : Fin n) (B : ℝ) {T : ℕ} (w : Fin T → A × (Fin n → V)) : 0 ≤ g.simpleRegret rewardBit actions eta i B w ∧ g.simpleRegret rewardBit actions eta i B w ≤ 1
theorem
BanditRLProof.Causal.GraphModel.simpleRegret_le_on_confidence
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.simpleRegret_le_on_confidenceReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem GraphModel.simpleRegret_le_on_confidence (g : GraphModel V n) (rewardBit : V → Bool) (actions : A → Fin n → Option V) (eta : PMF A) (i : Fin n) (hc : Covers (fun a => g.parentLaw (actions a) i) (mixture eta (fun a => g.parentLaw (actions a) i))) (B : ℝ) (hB : 0 < B) (epsilon : ℝ) {T : ℕ} (w : Fin T → A × (Fin n → V)) (hw : ∀ a, |g.sampleEstimate rewardBit actions eta i a B w-g.estimateCenter rewardBit actions eta i a B| ≤ epsilon) : g.simpleRegret rewardBit actions eta i B w ≤ 2*epsilon + designCost (fun a => g.parentLaw (actions a) i) eta / B