Lean module · Foundations

BanditRLProof.Algorithms.CausalHeterogeneousSampling

Native heterogeneous observations, estimates, and their actual sampling law.

Module map

Source: BanditRLProof/Algorithms/CausalHeterogeneousSampling.lean
Teaching chapter: 1. Finite bandits, traces, and regret
Declarations: 12
Placeholders: 0

Imports

BanditRLProof.Algorithms.CausalHeterogeneous, BanditRLProof.Algorithms.CausalImportanceTransport, BanditRLProof.Algorithms.CausalAllocationRegret

Imported by

BanditRLProof.Algorithms.CausalHeterogeneousRegret

Declarations

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

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

Canonical node identity

declaration:BanditRLProof.Causal.NodeGraphModel.roundLaw

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

noncomputable def NodeGraphModel.roundLaw (g : NodeGraphModel V) (actions : A → (i : Fin n) → Option (V i)) (eta : PMF A) : PMF (A × ((i : Fin n) → V i))

Source line 19 Chapter context: Foundations

def BanditRLProof.Causal.NodeGraphModel.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 identity

declaration:BanditRLProof.Causal.NodeGraphModel.sampleLaw

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

noncomputable def NodeGraphModel.sampleLaw (g : NodeGraphModel V) (actions : A → (i : Fin n) → Option (V i)) (eta : PMF A) (T : ℕ) : Measure (Fin T → A × ((i : Fin n) → V i))

Source line 24 Chapter context: Foundations

def BanditRLProof.Causal.NodeCodec.encodeRound 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.NodeCodec.encodeRound

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

def NodeCodec.encodeRound (c : NodeCodec V W) (ax : A × ((i : Fin n) → V i)) : A × (Fin n → W)

Source line 33 Chapter context: Foundations

def BanditRLProof.Causal.NodeCodec.encodeSamples 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.NodeCodec.encodeSamples

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

def NodeCodec.encodeSamples (c : NodeCodec V W) {T : ℕ} (w : Fin T → A × ((i : Fin n) → V i)) : Fin T → A × (Fin n → W)

Source line 36 Chapter context: Foundations

theorem BanditRLProof.Causal.NodeGraphModel.roundLaw_encoded 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.NodeGraphModel.roundLaw_encoded

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

theorem NodeGraphModel.roundLaw_encoded (g : NodeGraphModel V) (c : NodeCodec V W) (actions : A → (i : Fin n) → Option (V i)) (eta : PMF A) : (g.roundLaw actions eta).map c.encodeRound = (g.encodeGraph c).roundLaw (fun a => c.encodeAction (actions a)) eta

Source line 40 Chapter context: Foundations

theorem BanditRLProof.Causal.NodeGraphModel.sampleLaw_encoded 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.NodeGraphModel.sampleLaw_encoded

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

theorem NodeGraphModel.sampleLaw_encoded (g : NodeGraphModel V) (c : NodeCodec V W) (actions : A → (i : Fin n) → Option (V i)) (eta : PMF A) (T : ℕ) : (g.sampleLaw actions eta T).map c.encodeSamples = (g.encodeGraph c).sampleLaw (fun a => c.encodeAction (actions a)) eta T

Source line 48 Chapter context: Foundations

def BanditRLProof.Causal.NodeGraphModel.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 identity

declaration:BanditRLProof.Causal.NodeGraphModel.observation

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

def NodeGraphModel.observation (g : NodeGraphModel V) (i : Fin n) (rewardBit : V i → Bool) (ax : A × ((i : Fin n) → V i)) : g.ParentConfig i × Bool

Source line 58 Chapter context: Foundations

def BanditRLProof.Causal.NodeGraphModel.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 identity

declaration:BanditRLProof.Causal.NodeGraphModel.sampleWeightedBit

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

noncomputable def NodeGraphModel.sampleWeightedBit (g : NodeGraphModel V) (actions : A → (i : Fin n) → Option (V i)) (eta : PMF A) (i : Fin n) (rewardBit : V i → Bool) (a : A) (B : ℝ) {T : ℕ} (t : Fin T) (w : Fin T → A × ((i : Fin n) → V i)) : ℝ

Source line 62 Chapter context: Foundations

def BanditRLProof.Causal.NodeGraphModel.sampleEstimate 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.NodeGraphModel.sampleEstimate

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

noncomputable def NodeGraphModel.sampleEstimate (g : NodeGraphModel V) (actions : A → (i : Fin n) → Option (V i)) (eta : PMF A) (i : Fin n) (rewardBit : V i → Bool) (a : A) (B : ℝ) {T : ℕ} (w : Fin T → A × ((i : Fin n) → V i)) : ℝ

Source line 69 Chapter context: Foundations

theorem BanditRLProof.Causal.NodeGraphModel.sampleWeightedBit_encoded 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.NodeGraphModel.sampleWeightedBit_encoded

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

theorem NodeGraphModel.sampleWeightedBit_encoded (g : NodeGraphModel V) (c : NodeCodec V W) (actions : A → (i : Fin n) → Option (V i)) (eta : PMF A) (i : Fin n) (rewardBit : V i → Bool) (a : A) (B : ℝ) {T : ℕ} (t : Fin T) (w : Fin T → A × ((i : Fin n) → V i)) : (g.encodeGraph c).sampleWeightedBit (fun v => rewardBit (c.decode i v)) (fun a => c.encodeAction (actions a)) eta i a B t (c.encodeSamples w) = g.sampleWeightedBit actions eta i rewardBit a B t w

Source line 75 Chapter context: Foundations

theorem BanditRLProof.Causal.NodeGraphModel.sampleEstimate_encoded 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.NodeGraphModel.sampleEstimate_encoded

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

theorem NodeGraphModel.sampleEstimate_encoded (g : NodeGraphModel V) (c : NodeCodec V W) (actions : A → (i : Fin n) → Option (V i)) (eta : PMF A) (i : Fin n) (rewardBit : V i → Bool) (a : A) (B : ℝ) {T : ℕ} (w : Fin T → A × ((i : Fin n) → V i)) : (g.encodeGraph c).sampleEstimate (fun v => rewardBit (c.decode i v)) (fun a => c.encodeAction (actions a)) eta i a B (c.encodeSamples w) = g.sampleEstimate actions eta i rewardBit a B w

Source line 95 Chapter context: Foundations

theorem BanditRLProof.Causal.NodeGraphModel.designCost_encoded 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.NodeGraphModel.designCost_encoded

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

theorem NodeGraphModel.designCost_encoded (g : NodeGraphModel V) (c : NodeCodec V W) (actions : A → (i : Fin n) → Option (V i)) (eta : PMF A) (i : Fin n) : designCost (fun a => (g.encodeGraph c).parentLaw (c.encodeAction (actions a)) i) eta = designCost (fun a => g.parentLaw (actions a) i) eta

Source line 104 Chapter context: Foundations