Lean module · Foundations
BanditRLProof.Algorithms.CausalParallelRegret
Parallel DAG adapter and actual allocation-dependent expected simple regret.
Module map
Imports
BanditRLProof.Algorithms.CausalParallelLaw, BanditRLProof.Algorithms.CausalImportanceTransport, BanditRLProof.Algorithms.CausalAllocationRegret
Imported by
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
def
BanditRLProof.Causal.ParallelParameters.graph
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.ParallelParameters.graphReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
noncomputable def graph : GraphModel Bool (N+1) where
def
BanditRLProof.Causal.ParallelParameters.graphAction
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.ParallelParameters.graphActionReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
def graphAction (a : Option (Fin N × Bool)) : Fin (N+1) → Option Bool
theorem
BanditRLProof.Causal.ParallelParameters.graphAction_reward
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.ParallelParameters.graphAction_rewardReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem graphAction_reward (a : Option (Fin N × Bool)) : graphAction a (Fin.last N) = none
theorem
BanditRLProof.Causal.ParallelParameters.graph_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
Indexed settings: Causal bandits
Canonical node identity
declaration:BanditRLProof.Causal.ParallelParameters.graph_parentLawReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem graph_parentLaw (a : Option (Fin N × Bool)) : (p.graph reward).parentLaw (graphAction a) (Fin.last N) = (p.rootLaw a).map ((p.graph reward).parentConfig (Fin.last N))
theorem
BanditRLProof.Causal.ParallelParameters.graph_parentConfig_injective
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.ParallelParameters.graph_parentConfig_injectiveReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem graph_parentConfig_injective : Function.Injective ((p.graph reward).parentConfig (Fin.last N))
theorem
BanditRLProof.Causal.ParallelParameters.graph_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
Canonical node identity
declaration:BanditRLProof.Causal.ParallelParameters.graph_allocation_coversReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem graph_allocation_covers : Covers (fun a => (p.graph reward).parentLaw (graphAction a) (Fin.last N)) (mixture p.allocation (fun a => (p.graph reward).parentLaw (graphAction a) (Fin.last N)))
theorem
BanditRLProof.Causal.ParallelParameters.graph_designCost
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.ParallelParameters.graph_designCostReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem graph_designCost (eta : PMF (Option (Fin N × Bool))) : designCost (fun a => (p.graph reward).parentLaw (graphAction a) (Fin.last N)) eta = designCost p.rootLaw eta
theorem
BanditRLProof.Causal.ParallelParameters.graph_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
Canonical node identity
declaration:BanditRLProof.Causal.ParallelParameters.graph_allocation_cost_leReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem graph_allocation_cost_le : designCost (fun a => (p.graph reward).parentLaw (graphAction a) (Fin.last N)) p.allocation ≤ 2*p.rarity
theorem
BanditRLProof.Causal.ParallelParameters.graph_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
Canonical node identity
declaration:BanditRLProof.Causal.ParallelParameters.graph_optimal_cost_leReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem graph_optimal_cost_le : let laws := fun a => (p.graph reward).parentLaw (graphAction a) (Fin.last N) designCost laws (optimalAllocation laws) ≤ 2*p.rarity
theorem
BanditRLProof.Causal.ParallelParameters.expected_simpleRegret_parallel
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.ParallelParameters.expected_simpleRegret_parallelReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem expected_simpleRegret_parallel (T : ℕ) (hT : 0 < T) : let m := designCost p.rootLaw p.allocation let L := sourceLog T (Fintype.card (Option (Fin N × Bool))) let B := sourceThreshold m T L (∫ w, (p.graph reward).simpleRegret id graphAction p.allocation (Fin.last N) B w ∂(p.graph reward).sampleLaw graphAction p.allocation T) ≤ (2*Real.sqrt 2+7)*Real.sqrt ((2*p.rarity)*L/T)+1/(T:ℝ)
theorem
BanditRLProof.Causal.ParallelParameters.expected_simpleRegret_parallel_optimal
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.ParallelParameters.expected_simpleRegret_parallel_optimalReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem expected_simpleRegret_parallel_optimal (T : ℕ) (hT : 0 < T) : let laws := fun a => (p.graph reward).parentLaw (graphAction a) (Fin.last N) let eta := optimalAllocation laws let m := designCost laws eta let L := sourceLog T (Fintype.card (Option (Fin N × Bool))) let B := sourceThreshold m T L (∫ w, (p.graph reward).simpleRegret id graphAction eta (Fin.last N) B w ∂(p.graph reward).sampleLaw graphAction eta T) ≤ (2*Real.sqrt 2+7)*Real.sqrt ((2*p.rarity)*L/T)+1/(T:ℝ)