BanditRLProof.Algorithms.CUCBThresholdTail

No declaration docstring is present; use the chapter context and exact statement below.

theorem probabilistic_threshold_crossing (H n : ℕ) (hH : n+1≤H) (u p k : ℝ) (hu : 0<u) (hp : 0<p) (hp1 : p≠1) (hk : samplingThreshold H u p<k) : 0<k ∧ 6*Real.log ((n:ℝ)+1)/u^2<k*p/2 ∧ -k*p/8≤-(3*Real.log ((n:ℝ)+1))

No declaration docstring is present; use the chapter context and exact statement below.

theorem arms_nonempty : (Finset.univ : Finset (Fin m)).Nonempty

No declaration docstring is present; use the chapter context and exact statement below.

noncomputable def globalMinTrigger : ℝ

No declaration docstring is present; use the chapter context and exact statement below.

theorem globalMinTrigger_pos : 0<M.globalMinTrigger

No declaration docstring is present; use the chapter context and exact statement below.

theorem globalMinTrigger_le (i : Fin m) : M.globalMinTrigger≤M.minTrigger i

No declaration docstring is present; use the chapter context and exact statement below.

theorem globalMinTrigger_le_one : M.globalMinTrigger≤1

No declaration docstring is present; use the chapter context and exact statement below.

theorem globalMinTrigger_eq_one_iff : M.globalMinTrigger=1 ↔ ∀i, M.minTrigger i=1

No declaration docstring is present; use the chapter context and exact statement below.

theorem trigger_shortfall_fixed_count (H n : ℕ) (hH : n+1≤H) (i : Fin m) (u k : ℝ) (hu : 0<u) (hp1 : M.minTrigger i≠1) (hk : samplingThreshold H u (M.minTrigger i)<k) : (cucbTrajectory S.oracle M.environment) {Y | k≤(S.chargeData.counters (fun t => (Y t).1) n i : ℝ) ∧ (observationCount (fun t => (Y t).2) n i : ℝ)≤6*Real.log ((n:ℝ)+1)/u^2} ≤ ENNReal.ofReal (((n:ℝ)+1)^3)⁻¹

A single fixed-count tail covers every eligible action: minimize its positive inverse gap before taking probabilities, instead of unioning over actions.

theorem trigger_shortfall_slice (H n : ℕ) (hH : n+1≤H) (i : Fin m) (hp1 : M.minTrigger i≠1) (k : ℕ) : (cucbTrajectory S.oracle M.environment) {Y | S.chargeData.counters (fun t => (Y t).1) n i=k ∧ ∃a, 0<S.gap a ∧ i∈M.possible a ∧ samplingThreshold H (S.inverseGap a) (M.minTrigger i)<k ∧ (observationCount (fun t => (Y t).2) n i : ℝ)≤ 6*Real.log ((n:ℝ)+1)/(S.inverseGap a)^2} ≤ ENNReal.ofReal (((n:ℝ)+1)^3)⁻¹

The actual observation shortfall after crossing the source horizon threshold.

def TriggerShortfall (H n : ℕ) (i : Fin m) : Set (ℕ → Round A m)

No declaration docstring is present; use the chapter context and exact statement below.

theorem trigger_shortfall_probability (H n : ℕ) (hH : n+1≤H) (i : Fin m) (hp1 : M.minTrigger i≠1) : (cucbTrajectory S.oracle M.environment) (S.TriggerShortfall H n i) ≤ ENNReal.ofReal ((((n:ℝ)+1)^2)⁻¹)

No declaration docstring is present; use the chapter context and exact statement below.

theorem trigger_shortfall_probability_of_one (H n : ℕ) (hH : n+1≤H) (i : Fin m) (hp : M.minTrigger i=1) : (cucbTrajectory S.oracle M.environment) (S.TriggerShortfall H n i)=0

Sum only over base arms; the action family has already been absorbed in each fixed-count tail. Deterministically observed arms contribute zero.

theorem trigger_shortfall_union_probability (H n : ℕ) (hH : n+1≤H) : (cucbTrajectory S.oracle M.environment) (⋃i, S.TriggerShortfall H n i) ≤ ENNReal.ofReal ((m:ℝ)/((n:ℝ)+1)^2)

No declaration docstring is present; use the chapter context and exact statement below.

theorem trigger_shortfall_union_probability_of_all_one (H n : ℕ) (hH : n+1≤H) (hp : ∀i, M.minTrigger i=1) : (cucbTrajectory S.oracle M.environment) (⋃i, S.TriggerShortfall H n i)=0