Lean module · Foundations
BanditRLProof.Algorithms.CausalMarginalLaw
Marginal laws derived from topologically ordered sampling.
Module map
Imports
BanditRLProof.Algorithms.CausalOrderedLaw
Imported by
BanditRLProof, BanditRLProof.Algorithms.CausalHeterogeneous, BanditRLProof.Algorithms.CausalImportance
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.Causal.joint_map_init
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_map_initReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem joint_map_init {V : Type*} {n : ℕ} (p : Tables V (n+1)) : (joint p).map Fin.init = joint p.prefix
def
BanditRLProof.Causal.take
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.takeReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
def take {V : Type*} {m n : ℕ} (hm : m ≤ n) (x : Fin n → V) : Fin m → V
def
BanditRLProof.Causal.Tables.restrict
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.restrictReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
def Tables.restrict {V : Type*} {m n : ℕ} (p : Tables V n) (hm : m ≤ n) : Tables V m
theorem
BanditRLProof.Causal.joint_map_take
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_map_takeReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem joint_map_take {V : Type*} {m n : ℕ} (p : Tables V n) (hm : m ≤ n) : (joint p).map (take hm) = joint (p.restrict hm)
abbrev
BanditRLProof.Causal.GraphModel.ParentConfig
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.ParentConfigReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
abbrev GraphModel.ParentConfig {V : Type*} {n : ℕ} (g : GraphModel V n) (i : Fin n)
def
BanditRLProof.Causal.GraphModel.parentConfig
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.parentConfigReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
def GraphModel.parentConfig {V : Type*} {n : ℕ} (g : GraphModel V n) (i : Fin n) (h : Fin i.val → V) : g.ParentConfig i
def
BanditRLProof.Causal.GraphModel.parentTable
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.parentTableReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
noncomputable def GraphModel.parentTable {V : Type*} [Inhabited V] {n : ℕ} (g : GraphModel V n) (i : Fin n) (z : g.ParentConfig i) : PMF V
theorem
BanditRLProof.Causal.GraphModel.table_eq_parentTable
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.table_eq_parentTableReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem GraphModel.table_eq_parentTable {V : Type*} [Inhabited V] {n : ℕ} (g : GraphModel V n) (i : Fin n) (h : Fin i.val → V) : g.table i h = g.parentTable i (g.parentConfig i h)
theorem
BanditRLProof.Causal.joint_map_last_pair
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_map_last_pairReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem joint_map_last_pair {V Z : Type*} {n : ℕ} (p : Tables V (n+1)) (f : (Fin n → V) → Z) : (joint p).map (fun x => (f (Fin.init x), x (Fin.last n))) = (joint p.prefix).bind (fun h => (p (Fin.last n) h).map (fun y => (f h, y)))
theorem
BanditRLProof.Causal.GraphModel.last_parent_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.GraphModel.last_parent_jointReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem GraphModel.last_parent_joint {V : Type*} [Inhabited V] {n : ℕ} (g : GraphModel V (n+1)) : (joint g.table).map (fun x => (g.parentConfig (Fin.last n) (Fin.init x), x (Fin.last n))) = ((joint g.table.prefix).map (g.parentConfig (Fin.last n))).bind (fun z => (g.parentTable (Fin.last n) z).map (fun y => (z,y)))
theorem
BanditRLProof.Causal.joint_map_node_pair
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_map_node_pairReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem joint_map_node_pair {V Z : Type*} {n : ℕ} (p : Tables V n) (i : Fin n) (f : (Fin i.val → V) → Z) : (joint p).map (fun x => (f (history x i), x i)) = (joint (p.restrict (Nat.le_of_lt i.isLt))).bind (fun h => (p i h).map (fun y => (f h,y)))
theorem
BanditRLProof.Causal.joint_map_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.joint_map_historyReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem joint_map_history {V : Type*} {n : ℕ} (p : Tables V n) (i : Fin n) : (joint p).map (fun x => history x i) = joint (p.restrict (Nat.le_of_lt i.isLt))
def
BanditRLProof.Causal.GraphModel.parentLaw
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.parentLawReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
noncomputable def GraphModel.parentLaw {V : Type*} {n : ℕ} (g : GraphModel V n) (a : Fin n → Option V) (i : Fin n) : PMF (g.ParentConfig i)
theorem
BanditRLProof.Causal.GraphModel.parentLaw_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.GraphModel.parentLaw_prefixReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem GraphModel.parentLaw_prefix {V : Type*} {n : ℕ} (g : GraphModel V n) (a : Fin n → Option V) (i : Fin n) : g.parentLaw a i = (joint ((g.doModel a).table.restrict (Nat.le_of_lt i.isLt))).map (g.parentConfig i)
theorem
BanditRLProof.Causal.GraphModel.intervention_parent_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.GraphModel.intervention_parent_jointReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem GraphModel.intervention_parent_joint {V : Type*} [Inhabited V] {n : ℕ} (g : GraphModel V n) (a : Fin n → Option V) (i : Fin n) (hi : a i = none) : (joint (g.doModel a).table).map (fun x => (g.parentConfig i (history x i),x i)) = (g.parentLaw a i).bind (fun z => (g.parentTable i z).map (fun y => (z,y)))
theorem
BanditRLProof.Causal.paired_mass
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.paired_massReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem paired_mass {Z V : Type*} (p : PMF Z) (k : Z → PMF V) (z : Z) (y : V) : (p.bind (fun w => (k w).map (fun v => (w,v)))) (z,y) = p z * k z y
theorem
BanditRLProof.Causal.GraphModel.intervention_parent_mass
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.intervention_parent_massReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem GraphModel.intervention_parent_mass {V : Type*} [Inhabited V] {n : ℕ} (g : GraphModel V n) (a : Fin n → Option V) (i : Fin n) (hi : a i = none) (z : g.ParentConfig i) (y : V) : ((joint (g.doModel a).table).map (fun x => (g.parentConfig i (history x i),x i))) (z,y) = g.parentLaw a i z * g.parentTable i z y