BanditRLlib
Lean gate passed before this site build; local proof declarations are shown as compiled.Lean-verified build · exact declarations linked.

Lean module · Foundations

BanditRLProof.Algorithms.CausalHeterogeneousRegret

Actual expected simple regret on native heterogeneous finite DAGs.

Module map

Declarations
13
Placeholders
0

Imports

BanditRLProof.Algorithms.CausalHeterogeneousSampling

Imported by

BanditRLProof

Declarations

Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.

def BanditRLProof.Causal.NodeGraphModel.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 identitydeclaration:BanditRLProof.Causal.NodeGraphModel.rewardMean

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

noncomputable def NodeGraphModel.rewardMean (g : NodeGraphModel V) (actions : A → (j : Fin n) → Option (V j)) (i : Fin n) (rewardBit : V i → Bool) (a : A) : ℝ
Source line 17 Chapter context: Foundations
theorem BanditRLProof.Causal.NodeGraphModel.rewardMean_encoded 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 identitydeclaration:BanditRLProof.Causal.NodeGraphModel.rewardMean_encoded

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem NodeGraphModel.rewardMean_encoded (g : NodeGraphModel V) (c : NodeCodec V W) (actions : A → (j : Fin n) → Option (V j)) (i : Fin n) (rewardBit : V i → Bool) (a : A) (hi : actions a i = none) : (g.encodeGraph c).rewardMean (fun v => rewardBit (c.decode i v)) (fun a => c.encodeAction (actions a)) i a = g.rewardMean actions i rewardBit a
Source line 21 Chapter context: Foundations
def BanditRLProof.Causal.NodeGraphModel.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 identitydeclaration:BanditRLProof.Causal.NodeGraphModel.sampleRecommendation

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

noncomputable def NodeGraphModel.sampleRecommendation (g : NodeGraphModel V) (actions : A → (j : Fin n) → Option (V j)) (eta : PMF A) (i : Fin n) (rewardBit : V i → Bool) (B : ℝ) {T : ℕ} (w : Fin T → A × ((j : Fin n) → V j)) : A
Source line 33 Chapter context: Foundations
def BanditRLProof.Causal.NodeGraphModel.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 identitydeclaration:BanditRLProof.Causal.NodeGraphModel.simpleRegret

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

noncomputable def NodeGraphModel.simpleRegret (g : NodeGraphModel V) (actions : A → (j : Fin n) → Option (V j)) (eta : PMF A) (i : Fin n) (rewardBit : V i → Bool) (B : ℝ) {T : ℕ} (w : Fin T → A × ((j : Fin n) → V j)) : ℝ
Source line 39 Chapter context: Foundations
theorem BanditRLProof.Causal.NodeGraphModel.sampleRecommendation_encoded 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 identitydeclaration:BanditRLProof.Causal.NodeGraphModel.sampleRecommendation_encoded

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem NodeGraphModel.sampleRecommendation_encoded (g : NodeGraphModel V) (c : NodeCodec V W) (actions : A → (j : Fin n) → Option (V j)) (eta : PMF A) (i : Fin n) (rewardBit : V i → Bool) (B : ℝ) {T : ℕ} (w : Fin T → A × ((j : Fin n) → V j)) : (g.encodeGraph c).sampleRecommendation (fun v => rewardBit (c.decode i v)) (fun a => c.encodeAction (actions a)) eta i B (c.encodeSamples w) = g.sampleRecommendation actions eta i rewardBit B w
Source line 46 Chapter context: Foundations
theorem BanditRLProof.Causal.NodeGraphModel.simpleRegret_encoded 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 identitydeclaration:BanditRLProof.Causal.NodeGraphModel.simpleRegret_encoded

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem NodeGraphModel.simpleRegret_encoded (g : NodeGraphModel V) (c : NodeCodec V W) (actions : A → (j : Fin n) → Option (V j)) (eta : PMF A) (i : Fin n) (rewardBit : V i → Bool) (hi : ∀ a, actions a i = none) (B : ℝ) {T : ℕ} (w : Fin T → A × ((j : Fin n) → V j)) : (g.encodeGraph c).simpleRegret (fun v => rewardBit (c.decode i v)) (fun a => c.encodeAction (actions a)) eta i B (c.encodeSamples w) = g.simpleRegret actions eta i rewardBit B w
Source line 55 Chapter context: Foundations
theorem BanditRLProof.Causal.NodeGraphModel.expected_simpleRegret_encoded 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 identitydeclaration:BanditRLProof.Causal.NodeGraphModel.expected_simpleRegret_encoded

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem NodeGraphModel.expected_simpleRegret_encoded (g : NodeGraphModel V) (c : NodeCodec V W) (actions : A → (j : Fin n) → Option (V j)) (eta : PMF A) (i : Fin n) (rewardBit : V i → Bool) (hi : ∀ a, actions a i = none) (B : ℝ) (T : ℕ) : (∫ w, g.simpleRegret actions eta i rewardBit B w ∂g.sampleLaw actions eta T) = ∫ w, (g.encodeGraph c).simpleRegret (fun v => rewardBit (c.decode i v)) (fun a => c.encodeAction (actions a)) eta i B w ∂(g.encodeGraph c).sampleLaw (fun a => c.encodeAction (actions a)) eta T
Source line 67 Chapter context: Foundations
theorem BanditRLProof.Causal.NodeGraphModel.covers_encoded 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 identitydeclaration:BanditRLProof.Causal.NodeGraphModel.covers_encoded

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem NodeGraphModel.covers_encoded (g : NodeGraphModel V) (c : NodeCodec V W) (actions : A → (j : Fin n) → Option (V j)) (eta : PMF A) (i : Fin n) (hc : Covers (fun a => g.parentLaw (actions a) i) (mixture eta (fun a => g.parentLaw (actions a) i))) : Covers (fun a => (g.encodeGraph c).parentLaw (c.encodeAction (actions a)) i) (mixture eta (fun a => (g.encodeGraph c).parentLaw (c.encodeAction (actions a)) i))
Source line 78 Chapter context: Foundations
theorem BanditRLProof.Causal.NodeGraphModel.expected_simpleRegret_source_bound Compiled

Native finite-node theorem: no codec or common-alphabet premise is required.

Used in these reading views: Bandit Book

1. Finite bandits, traces, and regret

Indexed settings: Causal bandits

Canonical node identitydeclaration:BanditRLProof.Causal.NodeGraphModel.expected_simpleRegret_source_bound

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem NodeGraphModel.expected_simpleRegret_source_bound (g : NodeGraphModel V) (actions : A → (j : Fin n) → Option (V j)) (eta : PMF A) (i : Fin n) (rewardBit : V i → Bool) (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 actions eta i rewardBit B w ∂g.sampleLaw actions eta T) ≤ (2*Real.sqrt 2+7)*Real.sqrt (m*L/T)+1/(T:ℝ)
Source line 88 Chapter context: Foundations
theorem BanditRLProof.Causal.NodeGraphModel.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

Canonical node identitydeclaration:BanditRLProof.Causal.NodeGraphModel.expected_simpleRegret_bounds

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem NodeGraphModel.expected_simpleRegret_bounds (g : NodeGraphModel V) (actions : A → (j : Fin n) → Option (V j)) (eta : PMF A) (i : Fin n) (rewardBit : V i → Bool) (hi : ∀ a, actions a i = none) (B : ℝ) (T : ℕ) : 0 ≤ (∫ w, g.simpleRegret actions eta i rewardBit B w ∂g.sampleLaw actions eta T) ∧ (∫ w, g.simpleRegret actions eta i rewardBit B w ∂g.sampleLaw actions eta T) ≤ 1
Source line 110 Chapter context: Foundations
theorem BanditRLProof.Causal.NodeGraphModel.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 identitydeclaration:BanditRLProof.Causal.NodeGraphModel.expected_simpleRegret_explicit_rate

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem NodeGraphModel.expected_simpleRegret_explicit_rate (g : NodeGraphModel V) (actions : A → (j : Fin n) → Option (V j)) (eta : PMF A) (i : Fin n) (rewardBit : V i → Bool) (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 actions eta i rewardBit B w ∂g.sampleLaw actions eta T) ≤ (3*Real.sqrt 2+7)*Real.sqrt (m*L/T)
Source line 119 Chapter context: Foundations
theorem BanditRLProof.Causal.NodeGraphModel.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 identitydeclaration:BanditRLProof.Causal.NodeGraphModel.expected_simpleRegret_uniform

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem NodeGraphModel.expected_simpleRegret_uniform (g : NodeGraphModel V) (actions : A → (j : Fin n) → Option (V j)) (i : Fin n) (rewardBit : V i → Bool) (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 actions eta i rewardBit B w ∂g.sampleLaw actions eta T) ≤ (2*Real.sqrt 2+7)*Real.sqrt ((Fintype.card A:ℝ)*L/T)+1/(T:ℝ)
Source line 135 Chapter context: Foundations
theorem BanditRLProof.Causal.NodeGraphModel.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 identitydeclaration:BanditRLProof.Causal.NodeGraphModel.expected_simpleRegret_optimal

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem NodeGraphModel.expected_simpleRegret_optimal (g : NodeGraphModel V) (actions : A → (j : Fin n) → Option (V j)) (i : Fin n) (rewardBit : V i → Bool) (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 actions eta i rewardBit B w ∂g.sampleLaw actions eta T) ≤ (2*Real.sqrt 2+7)*Real.sqrt (m*L/T)+1/(T:ℝ)
Source line 154 Chapter context: Foundations