BanditRLlib
Lean gate passed before this site build; local proof declarations are shown as compiled.Lean-verified build · exact declarations linked.

Lean module · Foundations

BanditRLProof.Algorithms.CausalParallelLaw

Actual independent-root intervention laws and their covered allocation cost.

Module map

Declarations
12
Placeholders
0

Imports

BanditRLProof.Algorithms.CausalParallelDesign

Imported by

BanditRLProof.Algorithms.CausalParallelRegret

Declarations

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

theorem BanditRLProof.Causal.mixture_mass_ge_component 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 identitydeclaration:BanditRLProof.Causal.mixture_mass_ge_component

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

theorem mixture_mass_ge_component {A Z : Type*} [Fintype A] (eta : PMF A) (p : A → PMF Z) (a : A) (z : Z) : mass eta a * mass (p a) z ≤ mass (mixture eta p) z
Source line 9 Chapter context: Foundations
def BanditRLProof.Causal.ParallelParameters.rootTable 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 identitydeclaration:BanditRLProof.Causal.ParallelParameters.rootTable

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

noncomputable def rootTable (i : Fin N) : PMF Bool
Source line 19 Chapter context: Foundations
theorem BanditRLProof.Causal.ParallelParameters.rootTable_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 identitydeclaration:BanditRLProof.Causal.ParallelParameters.rootTable_mass

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

theorem rootTable_mass (i : Fin N) (b : Bool) : mass (p.rootTable i) b = p.valueProbability (i,b)
Source line 22 Chapter context: Foundations
def BanditRLProof.Causal.ParallelParameters.rootAction 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 identitydeclaration:BanditRLProof.Causal.ParallelParameters.rootAction

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

def rootAction (a : Option (Fin N × Bool)) (i : Fin N) : Option Bool
Source line 28 Chapter context: Foundations
def BanditRLProof.Causal.ParallelParameters.rootLaw 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 identitydeclaration:BanditRLProof.Causal.ParallelParameters.rootLaw

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

noncomputable def rootLaw (a : Option (Fin N × Bool)) : PMF (Fin N → Bool)
Source line 31 Chapter context: Foundations
theorem BanditRLProof.Causal.ParallelParameters.rootLaw_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

Indexed settings: Causal bandits

Canonical node identitydeclaration:BanditRLProof.Causal.ParallelParameters.rootLaw_mass

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

theorem rootLaw_mass (a : Option (Fin N × Bool)) (x : Fin N → Bool) : mass (p.rootLaw a) x = ∏ i, match a with | none => p.valueProbability (i,x i) | some b => if i = b.1 then (if x i = b.2 then 1 else 0) else p.valueProbability (i,x i)
Source line 34 Chapter context: Foundations
theorem BanditRLProof.Causal.ParallelParameters.rootLaw_atom_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 identitydeclaration:BanditRLProof.Causal.ParallelParameters.rootLaw_atom_mass

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

theorem rootLaw_atom_mass (i : Fin N) (b : Bool) (x : Fin N → Bool) : mass (p.rootLaw (some (i,b))) x = (if x i = b then 1 else 0) * ∏ j ∈ Finset.univ.erase i, p.valueProbability (j,x j)
Source line 51 Chapter context: Foundations
theorem BanditRLProof.Causal.ParallelParameters.atomic_observational_domination 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 identitydeclaration:BanditRLProof.Causal.ParallelParameters.atomic_observational_domination

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

theorem atomic_observational_domination (a : Fin N × Bool) (x : Fin N → Bool) : p.valueProbability a * mass (p.rootLaw (some a)) x ≤ mass (p.rootLaw none) x
Source line 61 Chapter context: Foundations
theorem BanditRLProof.Causal.ParallelParameters.allocated_mass_domination 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 identitydeclaration:BanditRLProof.Causal.ParallelParameters.allocated_mass_domination

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

theorem allocated_mass_domination (a : Option (Fin N × Bool)) (x : Fin N → Bool) : mass (p.rootLaw a) x ≤ (2*p.rarity)*mass (mixture p.allocation p.rootLaw) x
Source line 72 Chapter context: Foundations
theorem BanditRLProof.Causal.ParallelParameters.allocation_covers 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 identitydeclaration:BanditRLProof.Causal.ParallelParameters.allocation_covers

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

theorem allocation_covers : Covers p.rootLaw (mixture p.allocation p.rootLaw)
Source line 101 Chapter context: Foundations
theorem BanditRLProof.Causal.ParallelParameters.allocation_cost_le 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 identitydeclaration:BanditRLProof.Causal.ParallelParameters.allocation_cost_le

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

theorem allocation_cost_le : designCost p.rootLaw p.allocation ≤ 2*p.rarity
Source line 104 Chapter context: Foundations
theorem BanditRLProof.Causal.ParallelParameters.optimal_cost_le 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 identitydeclaration:BanditRLProof.Causal.ParallelParameters.optimal_cost_le

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

theorem optimal_cost_le : designCost p.rootLaw (optimalAllocation p.rootLaw) ≤ 2*p.rarity
Source line 110 Chapter context: Foundations