Lean module · Foundations

BanditRLProof.Algorithms.CausalTuning

The fixed source tuning used for the causal importance estimator.

Module map

Source: BanditRLProof/Algorithms/CausalTuning.lean
Teaching chapter: 1. Finite bandits, traces, and regret
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 identity

declaration: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 identity

declaration: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 identity

declaration: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 identity

declaration: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 identity

declaration: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 identity

declaration: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 identity

declaration: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 identity

declaration: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 identity

declaration: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 identity

declaration: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 identity

declaration: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 identity

declaration: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 identity

declaration: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 identity

declaration: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 identity

declaration: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