Lean module · Foundations
BanditRLProof.Algorithms.HeavyTailRegretCap
Finite raw-moment regret cap and extended-real supremum obstruction. Source: Genalti et al., COLT2024, Theorem2 Eq5. This enlarged trace-law class supplies an upper obstruction, not a fixed-algorithm lower bound or an asymptotic impossibility theorem. See the paired reader page and source deltas.
Module map
Imports
BanditRLProof.Algorithms.HeavyTailRegret
Imported by
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.HeavyTail.GenaltiAudit.mean_abs_le_raw_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.HeavyTail.GenaltiAudit.mean_abs_le_raw_scaleReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem mean_abs_le_raw_scale (μ : Measure ℝ) [IsProbabilityMeasure μ] (ε u : ℝ) (hε : 0 ≤ ε) (hu : 0 < u) (hm : Integrable (fun x : ℝ => |x|^(1+ε)) μ) (hbound : (∫ x, |x|^(1+ε) ∂μ) ≤ u) : |∫ x, x ∂μ| ≤ u^(1/(1+ε))
theorem
BanditRLProof.HeavyTail.GenaltiAudit.trace_regret_bounds
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.HeavyTail.GenaltiAudit.trace_regret_boundsReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem trace_regret_bounds {K : ℕ} (hK : 0 < K) (m : Fin K → ℝ) (s : ℝ) (hs : 0 ≤ s) (hm : ∀ i, |m i| ≤ s) (action : ActionTrace (Fin K)) (T : ℕ) : 0 ≤ realMeanRegret m action T ∧ realMeanRegret m action T ≤ 2*T*s
theorem
BanditRLProof.HeavyTail.GenaltiAudit.expected_normalized_regret_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.HeavyTail.GenaltiAudit.expected_normalized_regret_leReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem expected_normalized_regret_le {K : ℕ} (hK : 0 < K) (ν : Kernel (Fin K) ℝ) [IsMarkovKernel ν] (ε u : ℝ) (hε : 0 ≤ ε) (hu : 0 < u) (hm : ∀ i, Integrable (fun x : ℝ => |x|^(1+ε)) (ν i)) (hb : ∀ i, (∫ x, |x|^(1+ε) ∂ν i) ≤ u) {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω) [IsProbabilityMeasure P] (action : Ω → ActionTrace (Fin K)) (T : ℕ) (ha : ∀ t, Measurable (fun ω => action ω t)) : (∫ ω, realMeanRegret (realKernelMean ν) (action ω) T ∂P) / u^(1/(1+ε)) ≤ 2*T
def
BanditRLProof.HeavyTail.GenaltiAudit.normalizedValues
Compiled
Actual values, with moment laws and trace laws as witnesses, not a bound premise.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.HeavyTail.GenaltiAudit.normalizedValuesReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
def normalizedValues (K : ℕ) (ε : ℝ) (T : ℕ) : Set EReal
theorem
BanditRLProof.HeavyTail.GenaltiAudit.normalizedValues_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.HeavyTail.GenaltiAudit.normalizedValues_leReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem normalizedValues_le {K : ℕ} (hK : 0 < K) (ε : ℝ) (hε : 0 ≤ ε) (T : ℕ) {r : EReal} (hr : r ∈ normalizedValues K ε T) : r ≤ ((2*(T:ℝ) : ℝ) : EReal)
theorem
BanditRLProof.HeavyTail.GenaltiAudit.normalized_sSup_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.HeavyTail.GenaltiAudit.normalized_sSup_leReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem normalized_sSup_le {K : ℕ} (hK : 0 < K) (ε : ℝ) (hε : 0 ≤ ε) (T : ℕ) : sSup (normalizedValues K ε T) ≤ ((2*(T:ℝ) : ℝ) : EReal)
theorem
BanditRLProof.HeavyTail.GenaltiAudit.normalized_sSup_ne_top
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: Heavy-tailed bandits
Canonical node identity
declaration:BanditRLProof.HeavyTail.GenaltiAudit.normalized_sSup_ne_topReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem normalized_sSup_ne_top {K : ℕ} (hK : 0 < K) (ε : ℝ) (hε : 0 ≤ ε) (T : ℕ) : sSup (normalizedValues K ε T) ≠ ⊤
theorem
BanditRLProof.HeavyTail.GenaltiAudit.process_value_mem
Compiled
Arbitrary measurable action processes enter the set via their actual image law.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Indexed settings: Heavy-tailed bandits
Canonical node identity
declaration:BanditRLProof.HeavyTail.GenaltiAudit.process_value_memReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem process_value_mem {K : ℕ} (ν : Kernel (Fin K) ℝ) [IsMarkovKernel ν] (ε u : ℝ) (hu : 0 < u) (hm : ∀ i, Integrable (fun x : ℝ => |x|^(1+ε)) (ν i)) (hb : ∀ i, (∫ x, |x|^(1+ε) ∂ν i) ≤ u) {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω) [IsProbabilityMeasure P] (action : Ω → ActionTrace (Fin K)) (ha : ∀ t, Measurable (fun ω => action ω t)) (T : ℕ) : (((∫ ω, realMeanRegret (realKernelMean ν) (action ω) T ∂P) / u^(1/(1+ε)) : ℝ) : EReal) ∈ normalizedValues K ε T
def
BanditRLProof.HeavyTail.GenaltiAudit.extremeKernel
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.HeavyTail.GenaltiAudit.extremeKernelReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
noncomputable def extremeKernel : Kernel (Fin 2) ℝ
theorem
BanditRLProof.HeavyTail.GenaltiAudit.extreme_apply
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.HeavyTail.GenaltiAudit.extreme_applyReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
@[simp] theorem extreme_apply (i : Fin 2) : extremeKernel i = Measure.dirac (if i=0 then (1:ℝ) else -1)
theorem
BanditRLProof.HeavyTail.GenaltiAudit.extreme_moment
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.HeavyTail.GenaltiAudit.extreme_momentReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem extreme_moment (i : Fin 2) : Integrable (fun x : ℝ => |x|^(1+(1:ℝ))) (extremeKernel i) ∧ (∫ x, |x|^(1+(1:ℝ)) ∂extremeKernel i) ≤ 1
theorem
BanditRLProof.HeavyTail.GenaltiAudit.extreme_mean
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.HeavyTail.GenaltiAudit.extreme_meanReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
@[simp] theorem extreme_mean (i : Fin 2) : realKernelMean extremeKernel i = if i=0 then 1 else -1
theorem
BanditRLProof.HeavyTail.GenaltiAudit.extreme_best
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.HeavyTail.GenaltiAudit.extreme_bestReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem extreme_best : (⨆ i : Fin 2, realKernelMean extremeKernel i) = 1
theorem
BanditRLProof.HeavyTail.GenaltiAudit.extreme_trace_regret
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.HeavyTail.GenaltiAudit.extreme_trace_regretReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem extreme_trace_regret (T : ℕ) : realMeanRegret (realKernelMean extremeKernel) (fun _ => 1) T = 2*T
theorem
BanditRLProof.HeavyTail.GenaltiAudit.cap_mem
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.HeavyTail.GenaltiAudit.cap_memReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem cap_mem (T : ℕ) : ((2*(T:ℝ) : ℝ) : EReal) ∈ normalizedValues 2 1 T
theorem
BanditRLProof.HeavyTail.GenaltiAudit.normalized_sSup_two_eq
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: Heavy-tailed bandits
Canonical node identity
declaration:BanditRLProof.HeavyTail.GenaltiAudit.normalized_sSup_two_eqReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem normalized_sSup_two_eq (T : ℕ) : sSup (normalizedValues 2 1 T) = ((2*(T:ℝ) : ℝ) : EReal)