Lean module · Foundations
BanditRLProof.Algorithms.CausalHeterogeneousLaw
Native dependent joint factorization, independent of the common-alphabet target.
Module map
Imports
BanditRLProof.Algorithms.CausalHeterogeneous
Imported by
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.Causal.nodeJoint_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.nodeJoint_snocReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem nodeJoint_snoc {n : ℕ} {V : Fin (n+1) → Type*} (p : NodeTables V) (h : (i : Fin n) → V i.castSucc) (x : V (Fin.last n)) : nodeJoint p (Fin.snoc h x) = nodeJoint p.prefix h * p (Fin.last n) h x
theorem
BanditRLProof.Causal.nodeJoint_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.nodeJoint_factorizationReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem nodeJoint_factorization {n : ℕ} {V : Fin n → Type*} (p : NodeTables V) (x : (i : Fin n) → V i) : nodeJoint p x = ∏ i : Fin n, p i (nodeHistory x i) (x i)
theorem
BanditRLProof.Causal.nodeJoint_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.nodeJoint_normalizedReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem nodeJoint_normalized {n : ℕ} {V : Fin n → Type*} (p : NodeTables V) : ∑' x, nodeJoint p x = 1
theorem
BanditRLProof.Causal.nodeIntervention_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
Indexed settings: Causal bandits
Canonical node identity
declaration:BanditRLProof.Causal.nodeIntervention_factorizationReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem nodeIntervention_factorization {n : ℕ} {V : Fin n → Type*} (g : NodeGraphModel V) (a : (i : Fin n) → Option (V i)) (x : (i : Fin n) → V i) : nodeJoint (nodeIntervene g.table a) x = ∏ i : Fin n, (match a i with | none => g.table i (nodeHistory x i) (x i) | some v => if x i = v then 1 else 0)