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.CausalSampling

Actual intervention/assignment rounds and their fixed-budget product law.

Module map

Declarations
10
Placeholders
0

Imports

BanditRLProof.Algorithms.CausalOptimalAllocation

Imported by

BanditRLProof.Algorithms.CausalSampleMGF

Declarations

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

def BanditRLProof.Causal.GraphModel.roundLaw 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.GraphModel.roundLaw

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

noncomputable def GraphModel.roundLaw (g : GraphModel V n) (actions : A → Fin n → Option V) (eta : PMF A) : PMF (A × (Fin n → V))
Source line 16 Chapter context: Foundations
def BanditRLProof.Causal.GraphModel.observation 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.GraphModel.observation

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

def GraphModel.observation (g : GraphModel V n) (rewardBit : V → Bool) (i : Fin n) (ax : A × (Fin n → V)) : g.ParentConfig i × Bool
Source line 20 Chapter context: Foundations
theorem BanditRLProof.Causal.GraphModel.roundLaw_observation 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.GraphModel.roundLaw_observation

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

theorem GraphModel.roundLaw_observation (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) : (g.roundLaw actions eta).map (g.observation rewardBit i) = pairedLaw (mixture eta (fun a => g.parentLaw (actions a) i)) (fun z => (g.parentTable i z).map rewardBit)
Source line 25 Chapter context: Foundations
def BanditRLProof.Causal.GraphModel.sampleLaw 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.GraphModel.sampleLaw

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

noncomputable def GraphModel.sampleLaw (g : GraphModel V n) (actions : A → Fin n → Option V) (eta : PMF A) (T : ℕ) : Measure (Fin T → A × (Fin n → V))
Source line 36 Chapter context: Foundations
theorem BanditRLProof.Causal.GraphModel.sampleLaw_observation 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.GraphModel.sampleLaw_observation

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

theorem GraphModel.sampleLaw_observation (g : GraphModel V n) (rewardBit : V → Bool) (actions : A → Fin n → Option V) (eta : PMF A) (T : ℕ) (i : Fin n) (hi : ∀ a, actions a i = none) (t : Fin T) : (g.sampleLaw actions eta T).map (fun w => g.observation rewardBit i (w t)) = (pairedLaw (mixture eta (fun a => g.parentLaw (actions a) i)) (fun z => (g.parentTable i z).map rewardBit)).toMeasure
Source line 47 Chapter context: Foundations
theorem BanditRLProof.Causal.GraphModel.integral_sample_observation 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.GraphModel.integral_sample_observation

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

theorem GraphModel.integral_sample_observation (g : GraphModel V n) (rewardBit : V → Bool) (actions : A → Fin n → Option V) (eta : PMF A) (T : ℕ) (i : Fin n) (hi : ∀ a, actions a i = none) (t : Fin T) (f : g.ParentConfig i × Bool → ℝ) : (∫ w, f (g.observation rewardBit i (w t)) ∂g.sampleLaw actions eta T) = ∫ zy, f zy ∂(pairedLaw (mixture eta (fun a => g.parentLaw (actions a) i)) (fun z => (g.parentTable i z).map rewardBit)).toMeasure
Source line 62 Chapter context: Foundations
def BanditRLProof.Causal.GraphModel.sampleWeightedBit 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.GraphModel.sampleWeightedBit

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

noncomputable def GraphModel.sampleWeightedBit (g : GraphModel V n) (rewardBit : V → Bool) (actions : A → Fin n → Option V) (eta : PMF A) (i : Fin n) (a : A) (B : ℝ) {T : ℕ} (t : Fin T) (w : Fin T → A × (Fin n → V)) : ℝ
Source line 73 Chapter context: Foundations
theorem BanditRLProof.Causal.GraphModel.sampleWeightedBit_independent 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.GraphModel.sampleWeightedBit_independent

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

theorem GraphModel.sampleWeightedBit_independent (g : GraphModel V n) (rewardBit : V → Bool) (actions : A → Fin n → Option V) (eta : PMF A) (i : Fin n) (a : A) (B : ℝ) (T : ℕ) : iIndepFun (g.sampleWeightedBit rewardBit actions eta i a B (T := T)) (g.sampleLaw actions eta T)
Source line 79 Chapter context: Foundations
theorem BanditRLProof.Causal.GraphModel.sampleWeightedBit_mean 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.GraphModel.sampleWeightedBit_mean

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

theorem GraphModel.sampleWeightedBit_mean (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) (a : A) (B : ℝ) (T : ℕ) (t : Fin T) : (∫ w, g.sampleWeightedBit rewardBit actions eta i a B t w ∂g.sampleLaw actions eta T) = truncatedMean (g.parentLaw (actions a) i) (mixture eta (fun b => g.parentLaw (actions b) i)) (fun z => mass ((g.parentTable i z).map rewardBit) true) B
Source line 91 Chapter context: Foundations
theorem BanditRLProof.Causal.GraphModel.sampleWeightedBit_second_le 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.GraphModel.sampleWeightedBit_second_le

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

theorem GraphModel.sampleWeightedBit_second_le (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))) (a : A) (B : ℝ) (T : ℕ) (t : Fin T) : (∫ w, (g.sampleWeightedBit rewardBit actions eta i a B t w)^2 ∂g.sampleLaw actions eta T) ≤ secondMoment (g.parentLaw (actions a) i) (mixture eta (fun b => g.parentLaw (actions b) i))
Source line 105 Chapter context: Foundations