Lean module · Foundations
BanditRLProof.Algorithms.CausalOrderedLaw
Topologically ordered conditional tables and their actual joint PMF. Interventions replace node tables before sampling the joint law.
Module map
Imports
No project-local imports.
Imported by
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
abbrev
BanditRLProof.Causal.Tables
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.TablesReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
abbrev Tables (V : Type*) (n : ℕ)
def
BanditRLProof.Causal.Tables.prefix
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.Tables.prefixReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
def Tables.prefix {V : Type*} {n : ℕ} (p : Tables V (n+1)) : Tables V n
def
BanditRLProof.Causal.joint
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.jointReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
noncomputable def joint {V : Type*} : {n : ℕ} → Tables V n → PMF (Fin n → V) | 0, _ => PMF.pure Fin.elim0 | n+1, p => (joint p.prefix).bind fun h => (p (Fin.last n) h).bind fun x => PMF.pure (Fin.snoc h x) noncomputable def intervene {V : Type*} {n : ℕ} (p : Tables V n) (a : Fin n → Option V) : Tables V n
def
BanditRLProof.Causal.intervene
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.interveneReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
noncomputable def intervene {V : Type*} {n : ℕ} (p : Tables V n) (a : Fin n → Option V) : Tables V n
theorem
BanditRLProof.Causal.intervene_none
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.intervene_noneReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem intervene_none {V : Type*} {n : ℕ} (p : Tables V n) : intervene p (fun _ => none) = p
theorem
BanditRLProof.Causal.intervene_at
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.intervene_atReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem intervene_at {V : Type*} {n : ℕ} (p : Tables V n) (a : Fin n → Option V) (i : Fin n) (x : V) (ha : a i = some x) (h : Fin i.val → V) : intervene p a i h = PMF.pure x
theorem
BanditRLProof.Causal.joint_snoc
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.joint_snocReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem joint_snoc {V : Type*} {n : ℕ} (p : Tables V (n+1)) (h : Fin n → V) (x : V) : joint p (Fin.snoc h x) = joint p.prefix h * p (Fin.last n) h x
def
BanditRLProof.Causal.history
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.historyReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
def history {V : Type*} {n : ℕ} (x : Fin n → V) (i : Fin n) : Fin i.val → V
theorem
BanditRLProof.Causal.joint_factorization
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.joint_factorizationReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem joint_factorization {V : Type*} {n : ℕ} (p : Tables V n) (x : Fin n → V) : joint p x = ∏ i : Fin n, p i (history x i) (x i)
theorem
BanditRLProof.Causal.joint_normalized
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.joint_normalizedReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem joint_normalized {V : Type*} {n : ℕ} (p : Tables V n) : ∑' x, joint p x = 1
structure
BanditRLProof.Causal.GraphModel
Compiled
Parent indices are strictly earlier in the topological order.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.Causal.GraphModelReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
structure GraphModel (V : Type*) (n : ℕ) where
def
BanditRLProof.Causal.GraphModel.doModel
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.doModelReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
noncomputable def GraphModel.doModel {V : Type*} {n : ℕ} (g : GraphModel V n) (a : Fin n → Option V) : GraphModel V n where
theorem
BanditRLProof.Causal.doModel_factorization
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.doModel_factorizationReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem doModel_factorization {V : Type*} {n : ℕ} (g : GraphModel V n) (a : Fin n → Option V) (x : Fin n → V) : joint (g.doModel a).table x = ∏ i : Fin n, (match a i with | none => g.table i (history x i) (x i) | some v => if x i = v then 1 else 0)
theorem
BanditRLProof.Causal.intervention_incompatible_zero
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.intervention_incompatible_zeroReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem intervention_incompatible_zero {V : Type*} {n : ℕ} (g : GraphModel V n) (a : Fin n → Option V) (x : Fin n → V) (i : Fin n) (v : V) (ha : a i = some v) (hx : x i ≠ v) : joint (g.doModel a).table x = 0