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

The fixed source tuning used for the causal importance estimator.

Module map

Declarations
15
Placeholders
0

Imports

No project-local imports.

Imported by

BanditRLProof.Algorithms.CausalConfidence

Declarations

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

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

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

noncomputable def sourceThreshold (m T L : ℝ) : ℝ
Source line 9 Chapter context: Foundations
def BanditRLProof.Causal.sourceRadius 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.sourceRadius

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

noncomputable def sourceRadius (m T L : ℝ) : ℝ
Source line 11 Chapter context: Foundations
def BanditRLProof.Causal.sourceLog 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.sourceLog

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

noncomputable def sourceLog (T K : ℕ) : ℝ
Source line 14 Chapter context: Foundations
theorem BanditRLProof.Causal.sourceLog_pos 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.sourceLog_pos

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

theorem sourceLog_pos (T K : ℕ) (hT : 0 < T) (hK : 0 < K) : 0 < sourceLog T K
Source line 16 Chapter context: Foundations
theorem BanditRLProof.Causal.sourceLog_union_budget 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.sourceLog_union_budget

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

theorem sourceLog_union_budget (T K : ℕ) (hT : 0 < T) (hK : 0 < K) : (K:ℝ)*(2*Real.exp (-sourceLog T K)) = 1/(T:ℝ)
Source line 22 Chapter context: Foundations
theorem BanditRLProof.Causal.sourceThreshold_pos 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.sourceThreshold_pos

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

theorem sourceThreshold_pos (m T L : ℝ) (hm : 0 < m) (hT : 0 < T) (hL : 0 < L) : 0 < sourceThreshold m T L
Source line 29 Chapter context: Foundations
theorem BanditRLProof.Causal.sourceThreshold_sq 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.sourceThreshold_sq

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

theorem sourceThreshold_sq (m T L : ℝ) (hm : 0 ≤ m) (hT : 0 ≤ T) (hL : 0 ≤ L) : (sourceThreshold m T L)^2 = m*T/L
Source line 32 Chapter context: Foundations
theorem BanditRLProof.Causal.sourceTilt_admissible 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.sourceTilt_admissible

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

theorem sourceTilt_admissible (m T L : ℝ) (hm : 0 < m) (hT : 0 < T) (hL : 0 < L) : |1/(2*sourceThreshold m T L)| * (2*sourceThreshold m T L) ≤ 1
Source line 35 Chapter context: Foundations
theorem BanditRLProof.Causal.sourceTilt_budget 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.sourceTilt_budget

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

theorem sourceTilt_budget (m T L : ℝ) (hm : 0 < m) (hT : 0 < T) (hL : 0 < L) : T * ((1/(2*sourceThreshold m T L))^2*m) = L/4
Source line 41 Chapter context: Foundations
theorem BanditRLProof.Causal.sourceTilt_exponent_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 identitydeclaration:BanditRLProof.Causal.sourceTilt_exponent_le

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

theorem sourceTilt_exponent_le (m T L : ℝ) (hm : 0 < m) (hT : 0 < T) (hL : 0 < L) : -(1/(2*sourceThreshold m T L)) * (T*sourceRadius m T L) + T * ((1/(2*sourceThreshold m T L))^2*m) ≤ -L
Source line 50 Chapter context: Foundations
theorem BanditRLProof.Causal.sourceThreshold_scale 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.sourceThreshold_scale

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

theorem sourceThreshold_scale (m T L : ℝ) (hm : 0 < m) (hT : 0 < T) (hL : 0 < L) : sourceThreshold m T L * L / T = Real.sqrt (m*L/T)
Source line 67 Chapter context: Foundations
theorem BanditRLProof.Causal.sourceThreshold_bias_scale 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.sourceThreshold_bias_scale

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

theorem sourceThreshold_bias_scale (m T L : ℝ) (hm : 0 < m) (hT : 0 < T) (hL : 0 < L) : m/sourceThreshold m T L = Real.sqrt (m*L/T)
Source line 78 Chapter context: Foundations
theorem BanditRLProof.Causal.sourceRegret_scale 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.sourceRegret_scale

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

theorem sourceRegret_scale (m T L : ℝ) (hm : 0 < m) (hT : 0 < T) (hL : 0 < L) : 2*sourceRadius m T L + m/sourceThreshold m T L = (2*Real.sqrt 2+7)*Real.sqrt (m*L/T)
Source line 88 Chapter context: Foundations
theorem BanditRLProof.Causal.sourceLog_half_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 identitydeclaration:BanditRLProof.Causal.sourceLog_half_le

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

theorem sourceLog_half_le (T K : ℕ) (hT : 0 < T) (hK : 0 < K) : (1:ℝ)/2 ≤ sourceLog T K
Source line 102 Chapter context: Foundations
theorem BanditRLProof.Causal.sourceResidual_le_scale 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.sourceResidual_le_scale

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

theorem sourceResidual_le_scale (m : ℝ) (hm : 1 ≤ m) (T K : ℕ) (hT : 0 < T) (hK : 0 < K) : 1/(T:ℝ) ≤ Real.sqrt 2 * Real.sqrt (m*sourceLog T K/T)
Source line 112 Chapter context: Foundations