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.CausalConfidence

Source-tuned confidence for the actual fixed-budget intervention estimator.

Module map

Declarations
7
Placeholders
0

Imports

BanditRLProof.Algorithms.CausalSampleMGF, BanditRLProof.Algorithms.CausalTuning

Imported by

BanditRLProof.Algorithms.CausalRecommendation

Declarations

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

def BanditRLProof.Causal.GraphModel.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 identitydeclaration:BanditRLProof.Causal.GraphModel.sampleEstimate

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

noncomputable def GraphModel.sampleEstimate (g : GraphModel V n) (rewardBit : V → Bool) (actions : A → Fin n → Option V) (eta : PMF A) (i : Fin n) (a : A) (B : ℝ) {T : ℕ} (w : Fin T → A × (Fin n → V)) : ℝ
Source line 16 Chapter context: Foundations
def BanditRLProof.Causal.GraphModel.estimateCenter 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.GraphModel.estimateCenter

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

noncomputable def GraphModel.estimateCenter (g : GraphModel V n) (rewardBit : V → Bool) (actions : A → Fin n → Option V) (eta : PMF A) (i : Fin n) (a : A) (B : ℝ) : ℝ
Source line 21 Chapter context: Foundations
theorem BanditRLProof.Causal.GraphModel.sampleEstimate_centered_sum 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.GraphModel.sampleEstimate_centered_sum

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

theorem GraphModel.sampleEstimate_centered_sum (g : GraphModel V n) (rewardBit : V → Bool) (actions : A → Fin n → Option V) (eta : PMF A) (i : Fin n) (a : A) (B c sign : ℝ) (T : ℕ) (hT : 0 < T) (w : Fin T → A × (Fin n → V)) : (∑ t : Fin T, sign*(g.sampleWeightedBit rewardBit actions eta i a B t w-c)) = (T:ℝ) * (sign*(g.sampleEstimate rewardBit actions eta i a B w-c))
Source line 28 Chapter context: Foundations
theorem BanditRLProof.Causal.GraphModel.sampleEstimate_signed_tail 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.GraphModel.sampleEstimate_signed_tail

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

theorem GraphModel.sampleEstimate_signed_tail (g : GraphModel V n) (rewardBit : V → Bool) (actions : A → Fin n → Option V) (eta : PMF A) (i : Fin n) (hi : ∀ a, actions a i = none) (hc : Covers (fun a => g.parentLaw (actions a) i) (mixture eta (fun a => g.parentLaw (actions a) i))) (a : A) (T : ℕ) (hT : 0 < T) (L : ℝ) (hL : 0 < L) (sign : ℝ) (hs : |sign| = 1) : let m := designCost (fun b => g.parentLaw (actions b) i) eta let B := sourceThreshold m T L (g.sampleLaw actions eta T).real {w | sourceRadius m T L ≤ sign*(g.sampleEstimate rewardBit actions eta i a B w-g.estimateCenter rewardBit actions eta i a B)} ≤ Real.exp (-L)
Source line 39 Chapter context: Foundations
theorem BanditRLProof.Causal.GraphModel.sampleEstimate_abs_tail 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.GraphModel.sampleEstimate_abs_tail

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

theorem GraphModel.sampleEstimate_abs_tail (g : GraphModel V n) (rewardBit : V → Bool) (actions : A → Fin n → Option V) (eta : PMF A) (i : Fin n) (hi : ∀ a, actions a i = none) (hc : Covers (fun a => g.parentLaw (actions a) i) (mixture eta (fun a => g.parentLaw (actions a) i))) (a : A) (T : ℕ) (hT : 0 < T) (L : ℝ) (hL : 0 < L) : let m := designCost (fun b => g.parentLaw (actions b) i) eta let B := sourceThreshold m T L (g.sampleLaw actions eta T).real {w | sourceRadius m T L ≤ |g.sampleEstimate rewardBit actions eta i a B w-g.estimateCenter rewardBit actions eta i a B|} ≤ 2*Real.exp (-L)
Source line 74 Chapter context: Foundations
theorem BanditRLProof.Causal.GraphModel.sampleEstimate_simultaneous_tail 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.GraphModel.sampleEstimate_simultaneous_tail

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

theorem GraphModel.sampleEstimate_simultaneous_tail (g : GraphModel V n) (rewardBit : V → Bool) (actions : A → Fin n → Option V) (eta : PMF A) (i : Fin n) (hi : ∀ a, actions a i = none) (hc : Covers (fun a => g.parentLaw (actions a) i) (mixture eta (fun a => g.parentLaw (actions a) i))) (T : ℕ) (hT : 0 < T) (L : ℝ) (hL : 0 < L) : let m := designCost (fun b => g.parentLaw (actions b) i) eta let B := sourceThreshold m T L (g.sampleLaw actions eta T).real {w | ∃ a : A, sourceRadius m T L ≤ |g.sampleEstimate rewardBit actions eta i a B w-g.estimateCenter rewardBit actions eta i a B|} ≤ (Fintype.card A:ℝ) * (2*Real.exp (-L))
Source line 107 Chapter context: Foundations
theorem BanditRLProof.Causal.GraphModel.sampleEstimate_source_confidence 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.GraphModel.sampleEstimate_source_confidence

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

theorem GraphModel.sampleEstimate_source_confidence (g : GraphModel V n) (rewardBit : V → Bool) (actions : A → Fin n → Option V) (eta : PMF A) (i : Fin n) (hi : ∀ a, actions a i = none) (hc : Covers (fun a => g.parentLaw (actions a) i) (mixture eta (fun a => g.parentLaw (actions a) i))) (T : ℕ) (hT : 0 < T) : let m := designCost (fun b => g.parentLaw (actions b) i) eta let L := sourceLog T (Fintype.card A) let B := sourceThreshold m T L (g.sampleLaw actions eta T).real {w | ∃ a : A, sourceRadius m T L ≤ |g.sampleEstimate rewardBit actions eta i a B w-g.estimateCenter rewardBit actions eta i a B|} ≤ 1/(T:ℝ)
Source line 132 Chapter context: Foundations