BanditRLProof.Algorithms.CausalHeterogeneous

No declaration docstring is present; use the chapter context and exact statement below.

abbrev NodeHistory {n : ℕ} (V : Fin n → Type*) (i : Fin n)

No declaration docstring is present; use the chapter context and exact statement below.

abbrev NodeTables {n : ℕ} (V : Fin n → Type*)

No declaration docstring is present; use the chapter context and exact statement below.

def NodeTables.prefix {n : ℕ} {V : Fin (n+1) → Type*} (p : NodeTables V) : NodeTables (fun i : Fin n => V i.castSucc)

No declaration docstring is present; use the chapter context and exact statement below.

noncomputable def nodeJoint : {n : ℕ} → {V : Fin n → Type*} → NodeTables V → PMF ((i : Fin n) → V i) | 0, _, _ => PMF.pure (fun i => Fin.elim0 i) | n+1, _, p => (nodeJoint p.prefix).bind fun h => (p (Fin.last n) h).bind fun x => PMF.pure (Fin.snoc h x) structure NodeCodec {n : ℕ} (V : Fin n → Type*) (W : Type*) where

No declaration docstring is present; use the chapter context and exact statement below.

structure NodeCodec {n : ℕ} (V : Fin n → Type*) (W : Type*) where

No declaration docstring is present; use the chapter context and exact statement below.

def NodeCodec.prefix {n : ℕ} {V : Fin (n+1) → Type*} {W : Type*} (c : NodeCodec V W) : NodeCodec (fun i : Fin n => V i.castSucc) W where

No declaration docstring is present; use the chapter context and exact statement below.

def NodeCodec.encodeAssignment {n : ℕ} {V : Fin n → Type*} {W : Type*} (c : NodeCodec V W) (x : (i : Fin n) → V i) : Fin n → W

No declaration docstring is present; use the chapter context and exact statement below.

def NodeCodec.decodeAssignment {n : ℕ} {V : Fin n → Type*} {W : Type*} (c : NodeCodec V W) (x : Fin n → W) : (i : Fin n) → V i

No declaration docstring is present; use the chapter context and exact statement below.

theorem NodeCodec.decode_encodeAssignment {n : ℕ} {V : Fin n → Type*} {W : Type*} (c : NodeCodec V W) (x : (i : Fin n) → V i) : c.decodeAssignment (c.encodeAssignment x) = x

No declaration docstring is present; use the chapter context and exact statement below.

noncomputable def NodeCodec.encodeTables {n : ℕ} {V : Fin n → Type*} {W : Type*} (c : NodeCodec V W) (p : NodeTables V) : Tables W n

No declaration docstring is present; use the chapter context and exact statement below.

theorem NodeCodec.encodeAssignment_snoc {n : ℕ} {V : Fin (n+1) → Type*} {W : Type*} (c : NodeCodec V W) (h : (i : Fin n) → V i.castSucc) (x : V (Fin.last n)) : c.encodeAssignment (Fin.snoc h x) = Fin.snoc (c.prefix.encodeAssignment h) (c.encode (Fin.last n) x)

No declaration docstring is present; use the chapter context and exact statement below.

theorem NodeCodec.joint_encodeTables {n : ℕ} {V : Fin n → Type*} {W : Type*} (c : NodeCodec V W) (p : NodeTables V) : joint (c.encodeTables p) = (nodeJoint p).map c.encodeAssignment

No declaration docstring is present; use the chapter context and exact statement below.

theorem NodeCodec.decode_joint_encodeTables {n : ℕ} {V : Fin n → Type*} {W : Type*} (c : NodeCodec V W) (p : NodeTables V) : (joint (c.encodeTables p)).map c.decodeAssignment = nodeJoint p

A finite common alphabet is constructed, not assumed: use the finite product. Each node stores its value at its own coordinate and defaults elsewhere.

noncomputable def productNodeCodec {n : ℕ} (V : Fin n → Type*) [∀ i, Inhabited (V i)] : NodeCodec V ((i : Fin n) → V i) where

No declaration docstring is present; use the chapter context and exact statement below.

noncomputable def nodeIntervene {n : ℕ} {V : Fin n → Type*} (p : NodeTables V) (a : (i : Fin n) → Option (V i)) : NodeTables V

No declaration docstring is present; use the chapter context and exact statement below.

def NodeCodec.encodeAction {n : ℕ} {V : Fin n → Type*} {W : Type*} (c : NodeCodec V W) (a : (i : Fin n) → Option (V i)) : Fin n → Option W

No declaration docstring is present; use the chapter context and exact statement below.

theorem NodeCodec.encodeTables_intervene {n : ℕ} {V : Fin n → Type*} {W : Type*} (c : NodeCodec V W) (p : NodeTables V) (a : (i : Fin n) → Option (V i)) : c.encodeTables (nodeIntervene p a) = intervene (c.encodeTables p) (c.encodeAction a)

No declaration docstring is present; use the chapter context and exact statement below.

theorem NodeCodec.joint_intervene {n : ℕ} {V : Fin n → Type*} {W : Type*} (c : NodeCodec V W) (p : NodeTables V) (a : (i : Fin n) → Option (V i)) : joint (intervene (c.encodeTables p) (c.encodeAction a)) = (nodeJoint (nodeIntervene p a)).map c.encodeAssignment

No declaration docstring is present; use the chapter context and exact statement below.

structure NodeGraphModel {n : ℕ} (V : Fin n → Type*) where

No declaration docstring is present; use the chapter context and exact statement below.

noncomputable def NodeGraphModel.encodeGraph {n : ℕ} {V : Fin n → Type*} {W : Type*} (g : NodeGraphModel V) (c : NodeCodec V W) : GraphModel W n where

No declaration docstring is present; use the chapter context and exact statement below.

theorem NodeGraphModel.intervention_joint_encoded {n : ℕ} {V : Fin n → Type*} {W : Type*} (g : NodeGraphModel V) (c : NodeCodec V W) (a : (i : Fin n) → Option (V i)) : joint ((g.encodeGraph c).doModel (c.encodeAction a)).table = (nodeJoint (nodeIntervene g.table a)).map c.encodeAssignment

No declaration docstring is present; use the chapter context and exact statement below.

theorem NodeCodec.encoded_joint_valid {n : ℕ} {V : Fin n → Type*} {W : Type*} (c : NodeCodec V W) (p : NodeTables V) (w : Fin n → W) (hw : w ∈ (joint (c.encodeTables p)).support) : c.encodeAssignment (c.decodeAssignment w) = w

No declaration docstring is present; use the chapter context and exact statement below.

def nodeHistory {n : ℕ} {V : Fin n → Type*} (x : (i : Fin n) → V i) (i : Fin n) : NodeHistory V i

No declaration docstring is present; use the chapter context and exact statement below.

abbrev NodeGraphModel.ParentConfig {n : ℕ} {V : Fin n → Type*} (g : NodeGraphModel V) (i : Fin n)

No declaration docstring is present; use the chapter context and exact statement below.

def NodeGraphModel.parentConfig {n : ℕ} {V : Fin n → Type*} (g : NodeGraphModel V) (i : Fin n) (h : NodeHistory V i) : g.ParentConfig i

No declaration docstring is present; use the chapter context and exact statement below.

def NodeGraphModel.encodeParent {n : ℕ} {V : Fin n → Type*} {W : Type*} (g : NodeGraphModel V) (c : NodeCodec V W) (i : Fin n) (z : g.ParentConfig i) : (g.encodeGraph c).ParentConfig i

No declaration docstring is present; use the chapter context and exact statement below.

def NodeGraphModel.decodeParent {n : ℕ} {V : Fin n → Type*} {W : Type*} (g : NodeGraphModel V) (c : NodeCodec V W) (i : Fin n) (z : (g.encodeGraph c).ParentConfig i) : g.ParentConfig i

No declaration docstring is present; use the chapter context and exact statement below.

theorem NodeGraphModel.decode_encodeParent {n : ℕ} {V : Fin n → Type*} {W : Type*} (g : NodeGraphModel V) (c : NodeCodec V W) (i : Fin n) (z : g.ParentConfig i) : g.decodeParent c i (g.encodeParent c i z) = z

No declaration docstring is present; use the chapter context and exact statement below.

noncomputable def NodeGraphModel.parentLaw {n : ℕ} {V : Fin n → Type*} (g : NodeGraphModel V) (a : (i : Fin n) → Option (V i)) (i : Fin n) : PMF (g.ParentConfig i)

No declaration docstring is present; use the chapter context and exact statement below.

theorem NodeGraphModel.parentLaw_encoded {n : ℕ} {V : Fin n → Type*} {W : Type*} (g : NodeGraphModel V) (c : NodeCodec V W) (a : (i : Fin n) → Option (V i)) (i : Fin n) : (g.encodeGraph c).parentLaw (c.encodeAction a) i = (g.parentLaw a i).map (g.encodeParent c i)