Lean module · Foundations

BanditRLProof.Algorithms.CUCBUnderCount

Actual distinct charged counters and the refined under-sampling gap-tail cardinality. No count bound is supplied as a source-model hypothesis.

Module map

Source: BanditRLProof/Algorithms/CUCBUnderCount.lean
Teaching chapter: 1. Finite bandits, traces, and regret
Declarations: 14
Placeholders: 0

Imports

BanditRLProof.Algorithms.CUCBGapInverse, BanditRLProof.Algorithms.CUCBRegretDecomposition

Imported by

BanditRLProof, BanditRLProof.Algorithms.CUCBUnderCountIntegral

Declarations

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

theorem BanditRLProof.CUCB.ChargeData.counters_monotone 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.CUCB.ChargeData.counters_monotone

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

theorem counters_monotone (actions : ℕ → A) (i : Fin m) : Monotone (fun n => C.counters actions n i)

Source line 13 Chapter context: Foundations

theorem BanditRLProof.CUCB.ChargeData.counters_strict_of_charge 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.CUCB.ChargeData.counters_strict_of_charge

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

theorem counters_strict_of_charge (actions : ℕ → A) (i : Fin m) {t s : ℕ} (hts : t<s) (ht : C.choose (C.counters actions t) (actions t)=some i) : C.counters actions t i<C.counters actions s i

Source line 17 Chapter context: Foundations

theorem BanditRLProof.CUCB.ChargeData.counters_injOn_charges 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.CUCB.ChargeData.counters_injOn_charges

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

theorem counters_injOn_charges (actions : ℕ → A) (i : Fin m) : Set.InjOn (fun t => C.counters actions t i) {t | C.choose (C.counters actions t) (actions t)=some i}

Source line 25 Chapter context: Foundations

theorem BanditRLProof.CUCB.ChargeData.card_charges_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.CUCB.ChargeData.card_charges_le

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

theorem card_charges_le (actions : ℕ → A) (i : Fin m) (times : Finset ℕ) (B : ℝ) (hB : 0≤B) (hc : ∀t∈times, C.choose (C.counters actions t) (actions t)=some i) (hb : ∀t∈times, (C.counters actions t i : ℝ)≤B) : (times.card:ℝ)≤B+1

Source line 37 Chapter context: Foundations

def BanditRLProof.CUCB.SourceModel.underChargeTimes 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.CUCB.SourceModel.underChargeTimes

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

noncomputable def underChargeTimes (H : ℕ) (actions : ℕ → A) (i : Fin m) : Finset ℕ

Source line 56 Chapter context: Foundations

theorem BanditRLProof.CUCB.SourceModel.underChargeTimes_spec 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.CUCB.SourceModel.underChargeTimes_spec

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

theorem underChargeTimes_spec (H : ℕ) (actions : ℕ → A) (i : Fin m) {t : ℕ} (ht : t∈S.underChargeTimes H actions i) : t<H ∧ S.chargeData.choose (S.chargeData.counters actions t) (actions t)=some i ∧ 0<S.gap (actions t) ∧ i∈M.possible (actions t) ∧ (S.chargeData.counters actions t i:ℝ)≤S.gapThreshold H (M.minTrigger i) (S.gap (actions t))

Source line 63 Chapter context: Foundations

def BanditRLProof.CUCB.SourceModel.underChargeGapTail 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.CUCB.SourceModel.underChargeGapTail

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

noncomputable def underChargeGapTail (H : ℕ) (actions : ℕ → A) (i : Fin m) (x : ℝ) : Finset ℕ

Source line 76 Chapter context: Foundations

theorem BanditRLProof.CUCB.SourceModel.card_underChargeGapTail_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.CUCB.SourceModel.card_underChargeGapTail_le

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

theorem card_underChargeGapTail_le (H : ℕ) (hH : 1≤H) (actions : ℕ → A) (i : Fin m) (x : ℝ) (hx : x∈S.gapDomain) : ((S.underChargeGapTail H actions i x).card:ℝ)≤S.gapThreshold H (M.minTrigger i) x+1

Source line 80 Chapter context: Foundations

def BanditRLProof.CUCB.SourceModel.badActions 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.CUCB.SourceModel.badActions

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

noncomputable def badActions (i : Fin m) : Finset A

Source line 94 Chapter context: Foundations

theorem BanditRLProof.CUCB.SourceModel.underChargeTimes_mem_badActions 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.CUCB.SourceModel.underChargeTimes_mem_badActions

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

theorem underChargeTimes_mem_badActions (H : ℕ) (actions : ℕ → A) (i : Fin m) {t : ℕ} (ht : t∈S.underChargeTimes H actions i) : actions t∈S.badActions i

Source line 98 Chapter context: Foundations

theorem BanditRLProof.CUCB.SourceModel.underChargeTimes_empty_of_no_bad 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.CUCB.SourceModel.underChargeTimes_empty_of_no_bad

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

theorem underChargeTimes_empty_of_no_bad (H : ℕ) (actions : ℕ → A) (i : Fin m) (hi : S.badActions i=∅) : S.underChargeTimes H actions i=∅

Source line 104 Chapter context: Foundations

def BanditRLProof.CUCB.SourceModel.minBadGap 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.CUCB.SourceModel.minBadGap

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

noncomputable def minBadGap (i : Fin m) (hi : (S.badActions i).Nonempty) : ℝ

Source line 112 Chapter context: Foundations

def BanditRLProof.CUCB.SourceModel.maxBadGap 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.CUCB.SourceModel.maxBadGap

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

noncomputable def maxBadGap (i : Fin m) (hi : (S.badActions i).Nonempty) : ℝ

Source line 115 Chapter context: Foundations

theorem BanditRLProof.CUCB.SourceModel.badGap_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.CUCB.SourceModel.badGap_bounds

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

theorem badGap_bounds (i : Fin m) (hi : (S.badActions i).Nonempty) : S.minBadGap i hi∈S.gapDomain ∧ S.maxBadGap i hi∈S.gapDomain ∧ S.minBadGap i hi≤S.maxBadGap i hi

Source line 118 Chapter context: Foundations