BanditRLProof.Algorithms.UCB

Parameters for a finite-arm UCB run.

structure Spec (K : Nat) where

State visible to an index policy at one time step.

structure IndexState (K : Nat) where

Placeholder score surface for the first dependency-light layer. The Mathlib/LML migration will refine this to `mean + sqrt (2 * c * log n / pulls)`.

def score (_spec : Spec K) (state : IndexState K) (arm : Fin K) : Rat

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

@[simp] theorem score_eq_empiricalMean (spec : Spec K) (state : IndexState K) (arm : Fin K) : score spec state arm = state.empiricalMean arm

Real-valued UCB confidence score `empirical mean + radius`.

def confidenceScore {Arm : Type} (empiricalMean radius : Arm -> Real) (arm : Arm) : Real

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

@[simp] theorem confidenceScore_apply {Arm : Type} (empiricalMean radius : Arm -> Real) (arm : Arm) : confidenceScore empiricalMean radius arm = empiricalMean arm + radius arm

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

private theorem score_le_foldl_select {K : Nat} (scores : Fin K -> Real) (init : Fin K) : forall l : List (Fin K), (forall a : Fin K, List.Mem a l -> scores a <= scores (l.foldl (fun best arm : Fin K => if scores best < scores arm then arm else best) init)) /\ scores init <= scores (l.foldl (fun best arm : Fin K => if scores best < scores arm then arm else best) init) | [] => by exact And.intro (by intro _ ha cases ha) (by simp) | arm :: rest => by let select := fun best arm : Fin K => if scores best < scores arm then arm else best let next := select init arm have ih

Concrete finite-arm Real score argmax selector. The selector scans `List.finRange K`, keeps the previous arm on ties, and uses `hK` only to seed the nonempty finite arm set. This mirrors the ETC argmax oracle but targets the Real-valued UCB confidence-score surface.

noncomputable def scoreArgmax {K : Nat} (hK : 0 < K) (scores : Fin K -> Real) : Fin K

The concrete Real score argmax dominates every arm score.

theorem scoreArgmax_spec {K : Nat} (hK : 0 < K) (scores : Fin K -> Real) (a : Fin K) : scores a <= scores (scoreArgmax hK scores)

Concrete UCB action that maximizes the current confidence score.

noncomputable def confidenceScoreArgmaxAction {Omega : Type} {K : Nat} (hK : 0 < K) (empiricalMean : Omega -> Nat -> Fin K -> Real) (radius : Nat -> Fin K -> Real) : Omega -> Nat -> Fin K

The concrete confidence-score argmax action supplies score maximality against any comparison arm.

theorem confidenceScoreArgmaxAction_score_max {Omega : Type} {K : Nat} (hK : 0 < K) (empiricalMean : Omega -> Nat -> Fin K -> Real) (radius : Nat -> Fin K -> Real) (omega : Omega) (t : Nat) (arm : Fin K) : confidenceScore (empiricalMean omega t) (radius t) arm <= confidenceScore (empiricalMean omega t) (radius t) (confidenceScoreArgmaxAction hK empiricalMean radius omega t)

Selected-arm form of `confidenceScoreArgmaxAction_score_max`, matching the abstract selected-action bridge contract.

theorem confidenceScoreArgmaxAction_score_max_of_selected {Omega : Type} {K : Nat} (hK : 0 < K) (empiricalMean : Omega -> Nat -> Fin K -> Real) (radius : Nat -> Fin K -> Real) (omega : Omega) (t : Nat) (best chosen : Fin K) (hselected : confidenceScoreArgmaxAction hK empiricalMean radius omega t = chosen) : confidenceScore (empiricalMean omega t) (radius t) best <= confidenceScore (empiricalMean omega t) (radius t) chosen

Mean gap against a designated best arm for Real-valued UCB algebra.

def meanGap {Arm : Type} (trueMean : Arm -> Real) (best arm : Arm) : Real

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

@[simp] theorem meanGap_apply {Arm : Type} (trueMean : Arm -> Real) (best arm : Arm) : meanGap trueMean best arm = trueMean best - trueMean arm

UCB good-event algebra: if the best arm's true mean is below its upper confidence score, the chosen arm's true mean is above its lower confidence score, and the chosen arm maximizes the confidence score against the best arm, then the chosen arm's mean gap is at most twice its radius.

theorem meanGap_le_two_radius_of_confidenceScore_max {Arm : Type} (trueMean empiricalMean radius : Arm -> Real) (best chosen : Arm) (hbest_upper : trueMean best <= confidenceScore empiricalMean radius best) (hchosen_lower : empiricalMean chosen - radius chosen <= trueMean chosen) (hscore : confidenceScore empiricalMean radius best <= confidenceScore empiricalMean radius chosen) : meanGap trueMean best chosen <= 2 * radius chosen

Contrapositive consumer for the UCB good-event algebra: under the same good event and score-maximality hypotheses, a strict `2 * radius < gap` certificate rules out choosing that arm.

theorem not_two_radius_lt_meanGap_of_confidenceScore_max {Arm : Type} (trueMean empiricalMean radius : Arm -> Real) (best chosen : Arm) (hbest_upper : trueMean best <= confidenceScore empiricalMean radius best) (hchosen_lower : empiricalMean chosen - radius chosen <= trueMean chosen) (hscore : confidenceScore empiricalMean radius best <= confidenceScore empiricalMean radius chosen) (hgap_large : 2 * radius chosen < meanGap trueMean best chosen) : False

Upper-confidence failure for a random empirical-mean surface.

def upperConfidenceBad {Omega Arm : Type} (trueMean : Arm -> Real) (empiricalMean : Omega -> Arm -> Real) (radius : Arm -> Real) (arm : Arm) : Set Omega

Lower-confidence failure for a random empirical-mean surface.

def lowerConfidenceBad {Omega Arm : Type} (trueMean : Arm -> Real) (empiricalMean : Omega -> Arm -> Real) (radius : Arm -> Real) (arm : Arm) : Set Omega

Upper-confidence failure is measurable when the arm empirical mean is measurable.

theorem measurableSet_upperConfidenceBad {Omega Arm : Type} [MeasurableSpace Omega] (trueMean : Arm -> Real) (empiricalMean : Omega -> Arm -> Real) (radius : Arm -> Real) (arm : Arm) (hmeas : Measurable (fun omega : Omega => empiricalMean omega arm)) : MeasurableSet (upperConfidenceBad trueMean empiricalMean radius arm)

Lower-confidence failure is measurable when the arm empirical mean is measurable.

theorem measurableSet_lowerConfidenceBad {Omega Arm : Type} [MeasurableSpace Omega] (trueMean : Arm -> Real) (empiricalMean : Omega -> Arm -> Real) (radius : Arm -> Real) (arm : Arm) (hmeas : Measurable (fun omega : Omega => empiricalMean omega arm)) : MeasurableSet (lowerConfidenceBad trueMean empiricalMean radius arm)

The finite-arm UCB confidence bad event, as a union of upper/lower failures.

def confidenceBadEvent {Omega Arm : Type} [Fintype Arm] (trueMean : Arm -> Real) (empiricalMean : Omega -> Arm -> Real) (radius : Arm -> Real) : Set Omega

The finite-arm UCB confidence bad event is measurable from per-arm empirical-mean measurability.

theorem measurableSet_confidenceBadEvent {Omega Arm : Type} [MeasurableSpace Omega] [Fintype Arm] (trueMean : Arm -> Real) (empiricalMean : Omega -> Arm -> Real) (radius : Arm -> Real) (hmeas : forall arm : Arm, Measurable (fun omega : Omega => empiricalMean omega arm)) : MeasurableSet (confidenceBadEvent trueMean empiricalMean radius)

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

theorem not_upperConfidenceBad_of_not_confidenceBadEvent {Omega Arm : Type} [Fintype Arm] (trueMean : Arm -> Real) (empiricalMean : Omega -> Arm -> Real) (radius : Arm -> Real) (omega : Omega) (arm : Arm) (hgood : omega ∉ confidenceBadEvent trueMean empiricalMean radius) : omega ∉ upperConfidenceBad trueMean empiricalMean radius arm

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

theorem not_lowerConfidenceBad_of_not_confidenceBadEvent {Omega Arm : Type} [Fintype Arm] (trueMean : Arm -> Real) (empiricalMean : Omega -> Arm -> Real) (radius : Arm -> Real) (omega : Omega) (arm : Arm) (hgood : omega ∉ confidenceBadEvent trueMean empiricalMean radius) : omega ∉ lowerConfidenceBad trueMean empiricalMean radius arm

Event-level UCB good-event consumer: outside the finite-arm confidence bad event, score maximality against the best arm implies the standard `gap <= 2 * chosenRadius` conclusion.

theorem meanGap_le_two_radius_of_not_confidenceBadEvent {Omega Arm : Type} [Fintype Arm] (trueMean : Arm -> Real) (empiricalMean : Omega -> Arm -> Real) (radius : Arm -> Real) (omega : Omega) (best chosen : Arm) (hgood : omega ∉ confidenceBadEvent trueMean empiricalMean radius) (hscore : confidenceScore (empiricalMean omega) radius best <= confidenceScore (empiricalMean omega) radius chosen) : meanGap trueMean best chosen <= 2 * radius chosen

Finite-arm union bound for the UCB confidence bad event. This is still an outer-measure bound: it does not require measurability of the upper/lower confidence failure events.

theorem measure_confidenceBadEvent_le_sum_upper_lower {Omega Arm : Type} [MeasurableSpace Omega] [Fintype Arm] (mu : Measure Omega) (trueMean : Arm -> Real) (empiricalMean : Omega -> Arm -> Real) (radius : Arm -> Real) : mu (confidenceBadEvent trueMean empiricalMean radius) <= (Finset.univ : Finset Arm).sum (fun arm => mu (upperConfidenceBad trueMean empiricalMean radius arm) + mu (lowerConfidenceBad trueMean empiricalMean radius arm))

Time-indexed UCB confidence bad event.

def confidenceBadEventAt {Omega Arm : Type} [Fintype Arm] (trueMean : Arm -> Real) (empiricalMean : Omega -> Nat -> Arm -> Real) (radius : Nat -> Arm -> Real) (t : Nat) : Set Omega

The time-indexed UCB confidence bad event is measurable from per-arm empirical mean measurability at that time.

theorem measurableSet_confidenceBadEventAt {Omega Arm : Type} [MeasurableSpace Omega] [Fintype Arm] (trueMean : Arm -> Real) (empiricalMean : Omega -> Nat -> Arm -> Real) (radius : Nat -> Arm -> Real) (t : Nat) (hmeas : forall arm : Arm, Measurable (fun omega : Omega => empiricalMean omega t arm)) : MeasurableSet (confidenceBadEventAt trueMean empiricalMean radius t)

Finite-horizon union of time-indexed UCB confidence bad events.

def finiteHorizonConfidenceBadEvent {Omega Arm : Type} [Fintype Arm] (trueMean : Arm -> Real) (empiricalMean : Omega -> Nat -> Arm -> Real) (radius : Nat -> Arm -> Real) (T : Nat) : Set Omega

Outside the finite-horizon confidence bad event, every time-indexed bad event inside the horizon is absent.

theorem not_confidenceBadEventAt_of_not_finiteHorizonConfidenceBadEvent {Omega Arm : Type} [Fintype Arm] (trueMean : Arm -> Real) (empiricalMean : Omega -> Nat -> Arm -> Real) (radius : Nat -> Arm -> Real) (T : Nat) (omega : Omega) (t : Nat) (ht : t < T) (hgood : omega ∉ finiteHorizonConfidenceBadEvent trueMean empiricalMean radius T) : omega ∉ confidenceBadEventAt trueMean empiricalMean radius t

Finite-horizon good-event consumer: outside the finite-horizon confidence bad event, score maximality at any `t < T` gives the standard UCB gap-radius bound for the chosen arm.

theorem meanGap_le_two_radius_of_not_finiteHorizonConfidenceBadEvent {Omega Arm : Type} [Fintype Arm] (trueMean : Arm -> Real) (empiricalMean : Omega -> Nat -> Arm -> Real) (radius : Nat -> Arm -> Real) (T : Nat) (omega : Omega) (t : Nat) (best chosen : Arm) (ht : t < T) (hgood : omega ∉ finiteHorizonConfidenceBadEvent trueMean empiricalMean radius T) (hscore : confidenceScore (empiricalMean omega t) (radius t) best <= confidenceScore (empiricalMean omega t) (radius t) chosen) : meanGap trueMean best chosen <= 2 * radius t chosen

Contrapositive finite-horizon good-event consumer: if a chosen arm's gap is larger than twice its current radius and it beats the best arm's UCB score, the finite-horizon confidence bad event must occur.

theorem mem_finiteHorizonConfidenceBadEvent_of_two_radius_lt_meanGap_of_score_max {Omega Arm : Type} [Fintype Arm] (trueMean : Arm -> Real) (empiricalMean : Omega -> Nat -> Arm -> Real) (radius : Nat -> Arm -> Real) (T : Nat) (omega : Omega) (t : Nat) (best chosen : Arm) (ht : t < T) (hscore : confidenceScore (empiricalMean omega t) (radius t) best <= confidenceScore (empiricalMean omega t) (radius t) chosen) (hgap_large : 2 * radius t chosen < meanGap trueMean best chosen) : omega ∈ finiteHorizonConfidenceBadEvent trueMean empiricalMean radius T

Event-level form of the finite-horizon large-gap consumer. This is the set inclusion shape needed before applying measure monotonicity in pull-count arguments.

theorem scoreMaxEvent_subset_finiteHorizonConfidenceBadEvent_of_two_radius_lt_meanGap {Omega Arm : Type} [Fintype Arm] (trueMean : Arm -> Real) (empiricalMean : Omega -> Nat -> Arm -> Real) (radius : Nat -> Arm -> Real) (T : Nat) (t : Nat) (best chosen : Arm) (ht : t < T) (hgap_large : 2 * radius t chosen < meanGap trueMean best chosen) : {omega : Omega | confidenceScore (empiricalMean omega t) (radius t) best <= confidenceScore (empiricalMean omega t) (radius t) chosen} ⊆ finiteHorizonConfidenceBadEvent trueMean empiricalMean radius T

Finite-horizon union bound for UCB confidence bad events. This assembles the single-time upper/lower confidence-event union bound across `t < T`. It does not produce concentration tails or simplify the resulting double finite sum.

theorem measure_finiteHorizonConfidenceBadEvent_le_sum_upper_lower {Omega Arm : Type} [MeasurableSpace Omega] [Fintype Arm] (mu : Measure Omega) (trueMean : Arm -> Real) (empiricalMean : Omega -> Nat -> Arm -> Real) (radius : Nat -> Arm -> Real) (T : Nat) : mu (finiteHorizonConfidenceBadEvent trueMean empiricalMean radius T) <= (Finset.range T).sum (fun t => (Finset.univ : Finset Arm).sum (fun arm => mu (upperConfidenceBad trueMean (fun omega arm => empiricalMean omega t arm) (radius t) arm) + mu (lowerConfidenceBad trueMean (fun omega arm => empiricalMean omega t arm) (radius t) arm)))

Finite-horizon tail-bound consumer for UCB confidence bad events. The hypotheses `hupper` and `hlower` are the per-time/per-arm concentration inputs for the upper and lower confidence failures. This wrapper only assembles those local tail budgets across `t < T` and finite arms.

theorem measure_finiteHorizonConfidenceBadEvent_le_tail_sum {Omega Arm : Type} [MeasurableSpace Omega] [Fintype Arm] (mu : Measure Omega) (trueMean : Arm -> Real) (empiricalMean : Omega -> Nat -> Arm -> Real) (radius : Nat -> Arm -> Real) (upperTail lowerTail : Nat -> Arm -> ENNReal) (T : Nat) (hupper : forall t arm, t < T -> mu (upperConfidenceBad trueMean (fun omega arm => empiricalMean omega t arm) (radius t) arm) <= upperTail t arm) (hlower : forall t arm, t < T -> mu (lowerConfidenceBad trueMean (fun omega arm => empiricalMean omega t arm) (radius t) arm) <= lowerTail t arm) : mu (finiteHorizonConfidenceBadEvent trueMean empiricalMean radius T) <= (Finset.range T).sum (fun t => (Finset.univ : Finset Arm).sum (fun arm => upperTail t arm + lowerTail t arm))

An upper-confidence failure implies an absolute empirical-mean deviation at least as large as the radius.

theorem upperConfidenceBad_subset_absDeviation {Omega Arm : Type} (trueMean : Arm -> Real) (empiricalMean : Omega -> Arm -> Real) (radius : Arm -> Real) (arm : Arm) : upperConfidenceBad trueMean empiricalMean radius arm ⊆ {omega | radius arm <= |empiricalMean omega arm - trueMean arm|}

A lower-confidence failure implies an absolute empirical-mean deviation at least as large as the radius.

theorem lowerConfidenceBad_subset_absDeviation {Omega Arm : Type} (trueMean : Arm -> Real) (empiricalMean : Omega -> Arm -> Real) (radius : Arm -> Real) (arm : Arm) : lowerConfidenceBad trueMean empiricalMean radius arm ⊆ {omega | radius arm <= |empiricalMean omega arm - trueMean arm|}

Measure monotonicity form of `upperConfidenceBad_subset_absDeviation`.

theorem measure_upperConfidenceBad_le_absDeviation {Omega Arm : Type} [MeasurableSpace Omega] (mu : Measure Omega) (trueMean : Arm -> Real) (empiricalMean : Omega -> Arm -> Real) (radius : Arm -> Real) (arm : Arm) : mu (upperConfidenceBad trueMean empiricalMean radius arm) <= mu {omega | radius arm <= |empiricalMean omega arm - trueMean arm|}

Measure monotonicity form of `lowerConfidenceBad_subset_absDeviation`.

theorem measure_lowerConfidenceBad_le_absDeviation {Omega Arm : Type} [MeasurableSpace Omega] (mu : Measure Omega) (trueMean : Arm -> Real) (empiricalMean : Omega -> Arm -> Real) (radius : Arm -> Real) (arm : Arm) : mu (lowerConfidenceBad trueMean empiricalMean radius arm) <= mu {omega | radius arm <= |empiricalMean omega arm - trueMean arm|}

Finite-horizon UCB confidence bad-event bound from absolute-deviation tails. This is the UCB-facing adapter for concentration inequalities that bound `mu {omega | radius <= |empiricalMean - trueMean|}`. The same absolute deviation tail controls both the upper and lower confidence failures.

theorem measure_finiteHorizonConfidenceBadEvent_le_absDeviation_tail_sum {Omega Arm : Type} [MeasurableSpace Omega] [Fintype Arm] (mu : Measure Omega) (trueMean : Arm -> Real) (empiricalMean : Omega -> Nat -> Arm -> Real) (radius : Nat -> Arm -> Real) (tail : Nat -> Arm -> ENNReal) (T : Nat) (htail : forall t arm, t < T -> mu {omega | radius t arm <= |empiricalMean omega t arm - trueMean arm|} <= tail t arm) : mu (finiteHorizonConfidenceBadEvent trueMean empiricalMean radius T) <= (Finset.range T).sum (fun t => (Finset.univ : Finset Arm).sum (fun arm => tail t arm + tail t arm))

Chebyshev tail budget for a UCB empirical mean at time `t` and arm `arm`. This is intentionally an abstract finite-variance budget: it does not prove the variance rate of an empirical mean or choose a log/sqrt UCB radius.

noncomputable def chebyshevAbsDeviationTail {Omega Arm : Type} [MeasurableSpace Omega] (mu : Measure Omega) (empiricalMean : Omega -> Nat -> Arm -> Real) (radius : Nat -> Arm -> Real) (t : Nat) (arm : Arm) : ENNReal

Single-time Chebyshev tail for the UCB absolute-deviation event, under an explicit mean-identification contract.

theorem measure_absDeviation_le_chebyshev_tail {Omega Arm : Type} [MeasurableSpace Omega] (mu : Measure Omega) [IsFiniteMeasure mu] (trueMean : Arm -> Real) (empiricalMean : Omega -> Nat -> Arm -> Real) (radius : Nat -> Arm -> Real) (t : Nat) (arm : Arm) (hmem : MemLp (fun omega : Omega => empiricalMean omega t arm) 2 mu) (hradius : 0 < radius t arm) (hmean : integral mu (fun omega : Omega => empiricalMean omega t arm) = trueMean arm) : mu {omega | radius t arm <= |empiricalMean omega t arm - trueMean arm|} <= chebyshevAbsDeviationTail mu empiricalMean radius t arm

Finite-horizon UCB confidence bad-event bound from Chebyshev absolute-deviation tails. This is a concrete concentration producer for the abstract absolute-deviation tail adapter. It still leaves empirical-mean construction, variance-rate simplification, log/sqrt radius choice, pull-count bounds, and final regret to later leaves.

theorem measure_finiteHorizonConfidenceBadEvent_le_chebyshev_tail_sum {Omega Arm : Type} [MeasurableSpace Omega] [Fintype Arm] (mu : Measure Omega) [IsFiniteMeasure mu] (trueMean : Arm -> Real) (empiricalMean : Omega -> Nat -> Arm -> Real) (radius : Nat -> Arm -> Real) (T : Nat) (hmem : forall t arm, t < T -> MemLp (fun omega : Omega => empiricalMean omega t arm) 2 mu) (hradius : forall t arm, t < T -> 0 < radius t arm) (hmean : forall t arm, t < T -> integral mu (fun omega : Omega => empiricalMean omega t arm) = trueMean arm) : mu (finiteHorizonConfidenceBadEvent trueMean empiricalMean radius T) <= (Finset.range T).sum (fun t => (Finset.univ : Finset Arm).sum (fun arm => chebyshevAbsDeviationTail mu empiricalMean radius t arm + chebyshevAbsDeviationTail mu empiricalMean radius t arm))

One-sided sub-Gaussian tail budget for a UCB empirical mean at time `t` and arm `arm`. The proxy is for the centered variable `empiricalMean t arm - trueMean arm`. This one-sided budget is the sharper producer for the existing upper/lower confidence tail consumer; the absolute-deviation wrapper remains available for two-sided concentration statements.

noncomputable def subGaussianOneSidedDeviationTail {Arm : Type} (radius : Nat -> Arm -> Real) (proxy : Nat -> Arm -> NNReal) (t : Nat) (arm : Arm) : ENNReal

Radius-budget simplification for the one-sided UCB sub-Gaussian tail. If `radius^2` dominates `2 * proxy * budget`, the canonical exponential producer is bounded by `exp (-budget)`. This is the algebraic handoff between abstract sub-Gaussian tails and later log/sqrt UCB radius choices.

theorem subGaussianOneSidedDeviationTail_le_exp_neg_budget {Arm : Type} (radius : Nat -> Arm -> Real) (proxy : Nat -> Arm -> NNReal) (budget : Nat -> Arm -> Real) (t : Nat) (arm : Arm) (hproxy : 0 < ((proxy t arm : NNReal) : Real)) (hradius_sq : 2 * ((proxy t arm : NNReal) : Real) * budget t arm <= (radius t arm) ^ 2) : subGaussianOneSidedDeviationTail radius proxy t arm <= ENNReal.ofReal (Real.exp (-(budget t arm)))

Concrete square-root radius associated with a one-sided sub-Gaussian budget. The budget is left abstract so later leaves can instantiate it with logarithmic schedules such as `log (T * |A| / delta)`.

noncomputable def subGaussianBudgetRadius {Arm : Type} (proxy : Nat -> Arm -> NNReal) (budget : Nat -> Arm -> Real) : Nat -> Arm -> Real

The concrete square-root budget radius is nonnegative.

theorem subGaussianBudgetRadius_nonneg {Arm : Type} (proxy : Nat -> Arm -> NNReal) (budget : Nat -> Arm -> Real) (t : Nat) (arm : Arm) : 0 <= subGaussianBudgetRadius proxy budget t arm

The concrete square-root budget radius satisfies the radius-square domination contract consumed by `subGaussianOneSidedDeviationTail_le_exp_neg_budget`. This uses `Real.sq_sqrt'`, so it does not need a separate nonnegativity assumption on `budget`.

theorem subGaussianBudgetRadius_sq_domination {Arm : Type} (proxy : Nat -> Arm -> NNReal) (budget : Nat -> Arm -> Real) (t : Nat) (arm : Arm) : 2 * ((proxy t arm : NNReal) : Real) * budget t arm <= (subGaussianBudgetRadius proxy budget t arm) ^ 2

One-sided sub-Gaussian tail bound specialized to the concrete square-root budget radius.

theorem subGaussianOneSidedDeviationTail_budgetRadius_le_exp_neg_budget {Arm : Type} (proxy : Nat -> Arm -> NNReal) (budget : Nat -> Arm -> Real) (t : Nat) (arm : Arm) (hproxy : 0 < ((proxy t arm : NNReal) : Real)) : subGaussianOneSidedDeviationTail (subGaussianBudgetRadius proxy budget) proxy t arm <= ENNReal.ofReal (Real.exp (-(budget t arm)))

Single-time one-sided sub-Gaussian tail for an upper-confidence failure.

theorem measure_upperConfidenceBad_le_subGaussian_tail {Omega Arm : Type} [MeasurableSpace Omega] (mu : Measure Omega) [IsFiniteMeasure mu] (trueMean : Arm -> Real) (empiricalMean : Omega -> Nat -> Arm -> Real) (radius : Nat -> Arm -> Real) (proxy : Nat -> Arm -> NNReal) (t : Nat) (arm : Arm) (hradius : 0 <= radius t arm) (hsubG : ProbabilityTheory.HasSubgaussianMGF (fun omega : Omega => empiricalMean omega t arm - trueMean arm) (proxy t arm) mu) : mu (upperConfidenceBad trueMean (fun omega arm => empiricalMean omega t arm) (radius t) arm) <= subGaussianOneSidedDeviationTail radius proxy t arm

Single-time upper-confidence failure bound with an explicit exponential budget.

theorem measure_upperConfidenceBad_le_subGaussian_exp_neg_budget {Omega Arm : Type} [MeasurableSpace Omega] (mu : Measure Omega) [IsFiniteMeasure mu] (trueMean : Arm -> Real) (empiricalMean : Omega -> Nat -> Arm -> Real) (radius : Nat -> Arm -> Real) (proxy : Nat -> Arm -> NNReal) (budget : Nat -> Arm -> Real) (t : Nat) (arm : Arm) (hradius : 0 <= radius t arm) (hproxy : 0 < ((proxy t arm : NNReal) : Real)) (hradius_sq : 2 * ((proxy t arm : NNReal) : Real) * budget t arm <= (radius t arm) ^ 2) (hsubG : ProbabilityTheory.HasSubgaussianMGF (fun omega : Omega => empiricalMean omega t arm - trueMean arm) (proxy t arm) mu) : mu (upperConfidenceBad trueMean (fun omega arm => empiricalMean omega t arm) (radius t) arm) <= ENNReal.ofReal (Real.exp (-(budget t arm)))

Single-time upper-confidence failure bound for the concrete square-root budget radius.

theorem measure_upperConfidenceBad_le_subGaussian_budgetRadius {Omega Arm : Type} [MeasurableSpace Omega] (mu : Measure Omega) [IsFiniteMeasure mu] (trueMean : Arm -> Real) (empiricalMean : Omega -> Nat -> Arm -> Real) (proxy : Nat -> Arm -> NNReal) (budget : Nat -> Arm -> Real) (t : Nat) (arm : Arm) (hproxy : 0 < ((proxy t arm : NNReal) : Real)) (hsubG : ProbabilityTheory.HasSubgaussianMGF (fun omega : Omega => empiricalMean omega t arm - trueMean arm) (proxy t arm) mu) : mu (upperConfidenceBad trueMean (fun omega arm => empiricalMean omega t arm) (subGaussianBudgetRadius proxy budget t) arm) <= ENNReal.ofReal (Real.exp (-(budget t arm)))

Single-time one-sided sub-Gaussian tail for a lower-confidence failure.

theorem measure_lowerConfidenceBad_le_subGaussian_tail {Omega Arm : Type} [MeasurableSpace Omega] (mu : Measure Omega) [IsFiniteMeasure mu] (trueMean : Arm -> Real) (empiricalMean : Omega -> Nat -> Arm -> Real) (radius : Nat -> Arm -> Real) (proxy : Nat -> Arm -> NNReal) (t : Nat) (arm : Arm) (hradius : 0 <= radius t arm) (hsubG : ProbabilityTheory.HasSubgaussianMGF (fun omega : Omega => empiricalMean omega t arm - trueMean arm) (proxy t arm) mu) : mu (lowerConfidenceBad trueMean (fun omega arm => empiricalMean omega t arm) (radius t) arm) <= subGaussianOneSidedDeviationTail radius proxy t arm

Single-time lower-confidence failure bound with an explicit exponential budget.

theorem measure_lowerConfidenceBad_le_subGaussian_exp_neg_budget {Omega Arm : Type} [MeasurableSpace Omega] (mu : Measure Omega) [IsFiniteMeasure mu] (trueMean : Arm -> Real) (empiricalMean : Omega -> Nat -> Arm -> Real) (radius : Nat -> Arm -> Real) (proxy : Nat -> Arm -> NNReal) (budget : Nat -> Arm -> Real) (t : Nat) (arm : Arm) (hradius : 0 <= radius t arm) (hproxy : 0 < ((proxy t arm : NNReal) : Real)) (hradius_sq : 2 * ((proxy t arm : NNReal) : Real) * budget t arm <= (radius t arm) ^ 2) (hsubG : ProbabilityTheory.HasSubgaussianMGF (fun omega : Omega => empiricalMean omega t arm - trueMean arm) (proxy t arm) mu) : mu (lowerConfidenceBad trueMean (fun omega arm => empiricalMean omega t arm) (radius t) arm) <= ENNReal.ofReal (Real.exp (-(budget t arm)))

Single-time lower-confidence failure bound for the concrete square-root budget radius.

theorem measure_lowerConfidenceBad_le_subGaussian_budgetRadius {Omega Arm : Type} [MeasurableSpace Omega] (mu : Measure Omega) [IsFiniteMeasure mu] (trueMean : Arm -> Real) (empiricalMean : Omega -> Nat -> Arm -> Real) (proxy : Nat -> Arm -> NNReal) (budget : Nat -> Arm -> Real) (t : Nat) (arm : Arm) (hproxy : 0 < ((proxy t arm : NNReal) : Real)) (hsubG : ProbabilityTheory.HasSubgaussianMGF (fun omega : Omega => empiricalMean omega t arm - trueMean arm) (proxy t arm) mu) : mu (lowerConfidenceBad trueMean (fun omega arm => empiricalMean omega t arm) (subGaussianBudgetRadius proxy budget t) arm) <= ENNReal.ofReal (Real.exp (-(budget t arm)))

Finite-horizon UCB confidence bad-event bound from one-sided sub-Gaussian upper/lower tails. This is the sharper UCB-facing sub-Gaussian producer for the existing upper/lower tail consumer. It still leaves empirical-mean construction, proxy/radius simplification to the textbook log/sqrt form, pull-count bounds, and final regret to later leaves.

theorem measure_finiteHorizonConfidenceBadEvent_le_subGaussian_oneSided_tail_sum {Omega Arm : Type} [MeasurableSpace Omega] [Fintype Arm] (mu : Measure Omega) [IsFiniteMeasure mu] (trueMean : Arm -> Real) (empiricalMean : Omega -> Nat -> Arm -> Real) (radius : Nat -> Arm -> Real) (proxy : Nat -> Arm -> NNReal) (T : Nat) (hradius : forall t arm, t < T -> 0 <= radius t arm) (hsubG : forall t arm, t < T -> ProbabilityTheory.HasSubgaussianMGF (fun omega : Omega => empiricalMean omega t arm - trueMean arm) (proxy t arm) mu) : mu (finiteHorizonConfidenceBadEvent trueMean empiricalMean radius T) <= (Finset.range T).sum (fun t => (Finset.univ : Finset Arm).sum (fun arm => subGaussianOneSidedDeviationTail radius proxy t arm + subGaussianOneSidedDeviationTail radius proxy t arm))

Finite-horizon confidence bad-event bound with explicit one-sided exponential budgets. This is the UCB radius-budget handoff: later leaves can instantiate `budget` with a log schedule and prove the displayed radius-square domination.

theorem measure_finiteHorizonConfidenceBadEvent_le_subGaussian_exp_neg_budget_sum {Omega Arm : Type} [MeasurableSpace Omega] [Fintype Arm] (mu : Measure Omega) [IsFiniteMeasure mu] (trueMean : Arm -> Real) (empiricalMean : Omega -> Nat -> Arm -> Real) (radius : Nat -> Arm -> Real) (proxy : Nat -> Arm -> NNReal) (budget : Nat -> Arm -> Real) (T : Nat) (hradius : forall t arm, t < T -> 0 <= radius t arm) (hproxy : forall t arm, t < T -> 0 < ((proxy t arm : NNReal) : Real)) (hradius_sq : forall t arm, t < T -> 2 * ((proxy t arm : NNReal) : Real) * budget t arm <= (radius t arm) ^ 2) (hsubG : forall t arm, t < T -> ProbabilityTheory.HasSubgaussianMGF (fun omega : Omega => empiricalMean omega t arm - trueMean arm) (proxy t arm) mu) : mu (finiteHorizonConfidenceBadEvent trueMean empiricalMean radius T) <= (Finset.range T).sum (fun t => (Finset.univ : Finset Arm).sum (fun arm => ENNReal.ofReal (Real.exp (-(budget t arm))) + ENNReal.ofReal (Real.exp (-(budget t arm)))))

Finite-horizon confidence bad-event bound for the concrete square-root budget radius. This is the direct UCB-facing consumer for later logarithmic budget schedules.

theorem measure_finiteHorizonConfidenceBadEvent_le_subGaussian_budgetRadius_sum {Omega Arm : Type} [MeasurableSpace Omega] [Fintype Arm] (mu : Measure Omega) [IsFiniteMeasure mu] (trueMean : Arm -> Real) (empiricalMean : Omega -> Nat -> Arm -> Real) (proxy : Nat -> Arm -> NNReal) (budget : Nat -> Arm -> Real) (T : Nat) (hproxy : forall t arm, t < T -> 0 < ((proxy t arm : NNReal) : Real)) (hsubG : forall t arm, t < T -> ProbabilityTheory.HasSubgaussianMGF (fun omega : Omega => empiricalMean omega t arm - trueMean arm) (proxy t arm) mu) : mu (finiteHorizonConfidenceBadEvent trueMean empiricalMean (subGaussianBudgetRadius proxy budget) T) <= (Finset.range T).sum (fun t => (Finset.univ : Finset Arm).sum (fun arm => ENNReal.ofReal (Real.exp (-(budget t arm))) + ENNReal.ofReal (Real.exp (-(budget t arm)))))

Elementary log-budget simplification used by UCB tail producers. The positivity hypothesis is the regularity contract for later concrete schedules such as `scale = T * |A| / delta`.

theorem exp_neg_log_eq_inv {x : Real} (hx : 0 < x) : Real.exp (-(Real.log x)) = x⁻¹

Concrete square-root radius with a logarithmic budget. This is still schedule-agnostic: `scale` is the positive quantity whose inverse will become the one-sided tail budget after simplifying `exp (-log scale)`.

noncomputable def subGaussianLogBudgetRadius {Arm : Type} (proxy : Nat -> Arm -> NNReal) (scale : Nat -> Arm -> Real) : Nat -> Arm -> Real

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

@[simp] theorem subGaussianLogBudgetRadius_apply {Arm : Type} (proxy : Nat -> Arm -> NNReal) (scale : Nat -> Arm -> Real) (t : Nat) (arm : Arm) : subGaussianLogBudgetRadius proxy scale t arm = Real.sqrt (2 * ((proxy t arm : NNReal) : Real) * Real.log (scale t arm))

The logarithmic square-root budget radius is nonnegative.

theorem subGaussianLogBudgetRadius_nonneg {Arm : Type} (proxy : Nat -> Arm -> NNReal) (scale : Nat -> Arm -> Real) (t : Nat) (arm : Arm) : 0 <= subGaussianLogBudgetRadius proxy scale t arm

The logarithmic square-root budget radius satisfies the square-domination contract with budget `log scale`.

theorem subGaussianLogBudgetRadius_sq_domination {Arm : Type} (proxy : Nat -> Arm -> NNReal) (scale : Nat -> Arm -> Real) (t : Nat) (arm : Arm) : 2 * ((proxy t arm : NNReal) : Real) * Real.log (scale t arm) <= (subGaussianLogBudgetRadius proxy scale t arm) ^ 2

One-sided sub-Gaussian tail bound specialized to a logarithmic square-root budget radius.

theorem subGaussianOneSidedDeviationTail_logBudgetRadius_le_inv_scale {Arm : Type} (proxy : Nat -> Arm -> NNReal) (scale : Nat -> Arm -> Real) (t : Nat) (arm : Arm) (hproxy : 0 < ((proxy t arm : NNReal) : Real)) (hscale : 0 < scale t arm) : subGaussianOneSidedDeviationTail (subGaussianLogBudgetRadius proxy scale) proxy t arm <= ENNReal.ofReal ((scale t arm)⁻¹)

Single-time upper-confidence failure bound for the logarithmic square-root budget radius.

theorem measure_upperConfidenceBad_le_subGaussian_logBudgetRadius {Omega Arm : Type} [MeasurableSpace Omega] (mu : Measure Omega) [IsFiniteMeasure mu] (trueMean : Arm -> Real) (empiricalMean : Omega -> Nat -> Arm -> Real) (proxy : Nat -> Arm -> NNReal) (scale : Nat -> Arm -> Real) (t : Nat) (arm : Arm) (hproxy : 0 < ((proxy t arm : NNReal) : Real)) (hscale : 0 < scale t arm) (hsubG : ProbabilityTheory.HasSubgaussianMGF (fun omega : Omega => empiricalMean omega t arm - trueMean arm) (proxy t arm) mu) : mu (upperConfidenceBad trueMean (fun omega arm => empiricalMean omega t arm) (subGaussianLogBudgetRadius proxy scale t) arm) <= ENNReal.ofReal ((scale t arm)⁻¹)

Single-time lower-confidence failure bound for the logarithmic square-root budget radius.

theorem measure_lowerConfidenceBad_le_subGaussian_logBudgetRadius {Omega Arm : Type} [MeasurableSpace Omega] (mu : Measure Omega) [IsFiniteMeasure mu] (trueMean : Arm -> Real) (empiricalMean : Omega -> Nat -> Arm -> Real) (proxy : Nat -> Arm -> NNReal) (scale : Nat -> Arm -> Real) (t : Nat) (arm : Arm) (hproxy : 0 < ((proxy t arm : NNReal) : Real)) (hscale : 0 < scale t arm) (hsubG : ProbabilityTheory.HasSubgaussianMGF (fun omega : Omega => empiricalMean omega t arm - trueMean arm) (proxy t arm) mu) : mu (lowerConfidenceBad trueMean (fun omega arm => empiricalMean omega t arm) (subGaussianLogBudgetRadius proxy scale t) arm) <= ENNReal.ofReal ((scale t arm)⁻¹)

Finite-horizon confidence bad-event bound for logarithmic square-root budget radii. This is the schedule-agnostic log-budget producer. Later UCB leaves can set `scale t arm` to a concrete positive expression and then simplify the double sum.

theorem measure_finiteHorizonConfidenceBadEvent_le_subGaussian_logBudgetRadius_inv_scale_sum {Omega Arm : Type} [MeasurableSpace Omega] [Fintype Arm] (mu : Measure Omega) [IsFiniteMeasure mu] (trueMean : Arm -> Real) (empiricalMean : Omega -> Nat -> Arm -> Real) (proxy : Nat -> Arm -> NNReal) (scale : Nat -> Arm -> Real) (T : Nat) (hproxy : forall t arm, t < T -> 0 < ((proxy t arm : NNReal) : Real)) (hscale : forall t arm, t < T -> 0 < scale t arm) (hsubG : forall t arm, t < T -> ProbabilityTheory.HasSubgaussianMGF (fun omega : Omega => empiricalMean omega t arm - trueMean arm) (proxy t arm) mu) : mu (finiteHorizonConfidenceBadEvent trueMean empiricalMean (subGaussianLogBudgetRadius proxy scale) T) <= (Finset.range T).sum (fun t => (Finset.univ : Finset Arm).sum (fun arm => ENNReal.ofReal ((scale t arm)⁻¹) + ENNReal.ofReal ((scale t arm)⁻¹)))

Logarithmic square-root radius with a constant positive scale. This is the direct finite-horizon shape for later choices such as `scale = T * |A| / delta`.

noncomputable def subGaussianConstantLogBudgetRadius {Arm : Type} (proxy : Nat -> Arm -> NNReal) (scale : Real) : Nat -> Arm -> Real

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

@[simp] theorem subGaussianConstantLogBudgetRadius_apply {Arm : Type} (proxy : Nat -> Arm -> NNReal) (scale : Real) (t : Nat) (arm : Arm) : subGaussianConstantLogBudgetRadius proxy scale t arm = Real.sqrt (2 * ((proxy t arm : NNReal) : Real) * Real.log scale)

Constant logarithmic square-root budget radii are nonnegative.

theorem subGaussianConstantLogBudgetRadius_nonneg {Arm : Type} (proxy : Nat -> Arm -> NNReal) (scale : Real) (t : Nat) (arm : Arm) : 0 <= subGaussianConstantLogBudgetRadius proxy scale t arm

Constant logarithmic square-root budget radii satisfy the square-domination contract with budget `log scale`.

theorem subGaussianConstantLogBudgetRadius_sq_domination {Arm : Type} (proxy : Nat -> Arm -> NNReal) (scale : Real) (t : Nat) (arm : Arm) : 2 * ((proxy t arm : NNReal) : Real) * Real.log scale <= (subGaussianConstantLogBudgetRadius proxy scale t arm) ^ 2

Double finite sum of a constant inverse-scale one-sided tail budget.

theorem constant_invScale_double_sum {Arm : Type} [Fintype Arm] (T : Nat) (scale : Real) : (Finset.range T).sum (fun _ => (Finset.univ : Finset Arm).sum (fun _ => ENNReal.ofReal scale⁻¹ + ENNReal.ofReal scale⁻¹)) = HSMul.hSMul T (HSMul.hSMul (Fintype.card Arm) (ENNReal.ofReal scale⁻¹ + ENNReal.ofReal scale⁻¹))

Finite-horizon confidence bad-event bound for a constant logarithmic scale, with the time/arm double sum folded into `T` and `Fintype.card Arm`.

theorem measure_finiteHorizonConfidenceBadEvent_le_subGaussian_constantLogBudgetRadius_card {Omega Arm : Type} [MeasurableSpace Omega] [Fintype Arm] (mu : Measure Omega) [IsFiniteMeasure mu] (trueMean : Arm -> Real) (empiricalMean : Omega -> Nat -> Arm -> Real) (proxy : Nat -> Arm -> NNReal) (scale : Real) (T : Nat) (hproxy : forall t arm, t < T -> 0 < ((proxy t arm : NNReal) : Real)) (hscale : 0 < scale) (hsubG : forall t arm, t < T -> ProbabilityTheory.HasSubgaussianMGF (fun omega : Omega => empiricalMean omega t arm - trueMean arm) (proxy t arm) mu) : mu (finiteHorizonConfidenceBadEvent trueMean empiricalMean (subGaussianConstantLogBudgetRadius proxy scale) T) <= HSMul.hSMul T (HSMul.hSMul (Fintype.card Arm) (ENNReal.ofReal scale⁻¹ + ENNReal.ofReal scale⁻¹))

Convert a constant inverse-scale finite-horizon ENNReal tail budget back to an ordinary real budget.

theorem constant_invScale_double_sum_le_of_real {Arm : Type} [Fintype Arm] (T : Nat) (scale delta : Real) (hscale : 0 < scale) (hreal : (T : Real) * ((Fintype.card Arm : Real) * (scale⁻¹ + scale⁻¹)) <= delta) : HSMul.hSMul T (HSMul.hSMul (Fintype.card Arm) (ENNReal.ofReal scale⁻¹ + ENNReal.ofReal scale⁻¹)) <= ENNReal.ofReal delta

Textbook UCB finite-horizon scale for allocating two one-sided tails across `T` times and all arms. The factor `2` accounts for upper and lower confidence failures.

noncomputable def textbookDeltaScale {Arm : Type} [Fintype Arm] (T : Nat) (delta : Real) : Real

The textbook delta scale is positive under the usual horizon/arm/delta contracts.

theorem textbookDeltaScale_pos {Arm : Type} [Fintype Arm] [Nonempty Arm] (T : Nat) (delta : Real) (hT : 0 < T) (hdelta : 0 < delta) : 0 < textbookDeltaScale (Arm

The textbook delta scale makes the folded constant inverse-scale tail budget equal to `delta` at the real-number level.

theorem textbookDeltaScale_total_inv_budget_eq_delta {Arm : Type} [Fintype Arm] [Nonempty Arm] (T : Nat) (delta : Real) (hT : 0 < T) (hdelta : 0 < delta) : (T : Real) * ((Fintype.card Arm : Real) * ((textbookDeltaScale (Arm

The folded constant-scale UCB tail budget with textbook delta scale is bounded by `delta`.

theorem constant_invScale_double_sum_textbookDeltaScale_le_delta {Arm : Type} [Fintype Arm] [Nonempty Arm] (T : Nat) (delta : Real) (hT : 0 < T) (hdelta : 0 < delta) : HSMul.hSMul T (HSMul.hSMul (Fintype.card Arm) (ENNReal.ofReal (textbookDeltaScale (Arm

Textbook delta-scale logarithmic UCB radius.

noncomputable def subGaussianTextbookDeltaRadius {Arm : Type} [Fintype Arm] (proxy : Nat -> Arm -> NNReal) (T : Nat) (delta : Real) : Nat -> Arm -> Real

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

@[simp] theorem subGaussianTextbookDeltaRadius_apply {Arm : Type} [Fintype Arm] (proxy : Nat -> Arm -> NNReal) (T : Nat) (delta : Real) (t : Nat) (arm : Arm) : subGaussianTextbookDeltaRadius proxy T delta t arm = Real.sqrt (2 * ((proxy t arm : NNReal) : Real) * Real.log (textbookDeltaScale (Arm

Finite-horizon confidence bad-event bound for the textbook delta-scale logarithmic UCB radius.

theorem measure_finiteHorizonConfidenceBadEvent_le_subGaussian_textbookDeltaRadius_delta {Omega Arm : Type} [MeasurableSpace Omega] [Fintype Arm] [Nonempty Arm] (mu : Measure Omega) [IsFiniteMeasure mu] (trueMean : Arm -> Real) (empiricalMean : Omega -> Nat -> Arm -> Real) (proxy : Nat -> Arm -> NNReal) (T : Nat) (delta : Real) (hT : 0 < T) (hdelta : 0 < delta) (hproxy : forall t arm, t < T -> 0 < ((proxy t arm : NNReal) : Real)) (hsubG : forall t arm, t < T -> ProbabilityTheory.HasSubgaussianMGF (fun omega : Omega => empiricalMean omega t arm - trueMean arm) (proxy t arm) mu) : mu (finiteHorizonConfidenceBadEvent trueMean empiricalMean (subGaussianTextbookDeltaRadius proxy T delta) T) <= ENNReal.ofReal delta

Large-gap score-max events under the textbook delta radius are controlled by the finite-horizon confidence budget. This is a probability-facing handoff for later pull-count arguments: once a chosen arm has gap larger than twice its current radius, selecting it by UCB score can only happen on the confidence bad event.

theorem measure_scoreMaxEvent_le_subGaussian_textbookDeltaRadius_delta_of_gap {Omega Arm : Type} [MeasurableSpace Omega] [Fintype Arm] [Nonempty Arm] (mu : Measure Omega) [IsFiniteMeasure mu] (trueMean : Arm -> Real) (empiricalMean : Omega -> Nat -> Arm -> Real) (proxy : Nat -> Arm -> NNReal) (T : Nat) (delta : Real) (t : Nat) (best chosen : Arm) (hT : 0 < T) (hdelta : 0 < delta) (ht : t < T) (hgap_large : 2 * subGaussianTextbookDeltaRadius proxy T delta t chosen < meanGap trueMean best chosen) (hproxy : forall t arm, t < T -> 0 < ((proxy t arm : NNReal) : Real)) (hsubG : forall t arm, t < T -> ProbabilityTheory.HasSubgaussianMGF (fun omega : Omega => empiricalMean omega t arm - trueMean arm) (proxy t arm) mu) : mu {omega : Omega | confidenceScore (empiricalMean omega t) (subGaussianTextbookDeltaRadius proxy T delta t) best <= confidenceScore (empiricalMean omega t) (subGaussianTextbookDeltaRadius proxy T delta t) chosen} <= ENNReal.ofReal delta

Selecting `chosen` is contained in the corresponding UCB score-max event when the action trace exposes score maximality against `best`. This is intentionally abstract: the concrete argmax/tie-breaking policy can later discharge `hscore_of_selected`.

theorem selectedEvent_subset_scoreMaxEvent_of_action_score_max {Omega Arm : Type} (empiricalMean : Omega -> Nat -> Arm -> Real) (radius : Nat -> Arm -> Real) (action : Omega -> Nat -> Arm) (t : Nat) (best chosen : Arm) (hscore_of_selected : forall omega, action omega t = chosen -> confidenceScore (empiricalMean omega t) (radius t) best <= confidenceScore (empiricalMean omega t) (radius t) chosen) : Set.Subset {omega : Omega | action omega t = chosen} {omega : Omega | confidenceScore (empiricalMean omega t) (radius t) best <= confidenceScore (empiricalMean omega t) (radius t) chosen}

Selected large-gap arms inherit the textbook delta probability budget once the selected-action trace certifies UCB score maximality. This is the action-trace-facing bridge before a concrete pull-count summation: selection plus a large-gap radius condition implies that the selected event is covered by the finite-horizon confidence bad event.

theorem measure_selectedLargeGapEvent_le_subGaussian_textbookDeltaRadius_delta {Omega Arm : Type} [MeasurableSpace Omega] [Fintype Arm] [Nonempty Arm] (mu : Measure Omega) [IsFiniteMeasure mu] (trueMean : Arm -> Real) (empiricalMean : Omega -> Nat -> Arm -> Real) (action : Omega -> Nat -> Arm) (proxy : Nat -> Arm -> NNReal) (T : Nat) (delta : Real) (t : Nat) (best chosen : Arm) (hT : 0 < T) (hdelta : 0 < delta) (ht : t < T) (hgap_large : 2 * subGaussianTextbookDeltaRadius proxy T delta t chosen < meanGap trueMean best chosen) (hscore_of_selected : forall omega, action omega t = chosen -> confidenceScore (empiricalMean omega t) (subGaussianTextbookDeltaRadius proxy T delta t) best <= confidenceScore (empiricalMean omega t) (subGaussianTextbookDeltaRadius proxy T delta t) chosen) (hproxy : forall t arm, t < T -> 0 < ((proxy t arm : NNReal) : Real)) (hsubG : forall t arm, t < T -> ProbabilityTheory.HasSubgaussianMGF (fun omega : Omega => empiricalMean omega t arm - trueMean arm) (proxy t arm) mu) : mu {omega : Omega | action omega t = chosen} <= ENNReal.ofReal delta

Finite-time selected-action events are covered by the finite-horizon confidence bad event when every selected time in the index set has a large enough gap and certifies UCB score maximality. This is the event-level bridge needed before turning selected-time collections into pull-count or suffix-time bounds.

theorem selectedEventOn_subset_finiteHorizonConfidenceBadEvent_of_action_score_max {Omega Arm : Type} [Fintype Arm] (trueMean : Arm -> Real) (empiricalMean : Omega -> Nat -> Arm -> Real) (radius : Nat -> Arm -> Real) (action : Omega -> Nat -> Arm) (T : Nat) (times : Finset Nat) (best chosen : Arm) (htimes : forall t, t ∈ times -> t < T) (hscore_of_selected : forall omega t, t ∈ times -> action omega t = chosen -> confidenceScore (empiricalMean omega t) (radius t) best <= confidenceScore (empiricalMean omega t) (radius t) chosen) (hgap_large : forall t, t ∈ times -> 2 * radius t chosen < meanGap trueMean best chosen) : Set.Subset {omega : Omega | exists t, t ∈ times /\ action omega t = chosen} (finiteHorizonConfidenceBadEvent trueMean empiricalMean radius T)

The textbook delta budget also controls the event that a fixed arm is selected at any time from a finite index set, provided each such time satisfies the large-gap radius condition and selected-action score maximality.

theorem measure_selectedLargeGapEventOn_le_subGaussian_textbookDeltaRadius_delta {Omega Arm : Type} [MeasurableSpace Omega] [Fintype Arm] [Nonempty Arm] (mu : Measure Omega) [IsFiniteMeasure mu] (trueMean : Arm -> Real) (empiricalMean : Omega -> Nat -> Arm -> Real) (action : Omega -> Nat -> Arm) (proxy : Nat -> Arm -> NNReal) (T : Nat) (delta : Real) (times : Finset Nat) (best chosen : Arm) (hT : 0 < T) (hdelta : 0 < delta) (htimes : forall t, t ∈ times -> t < T) (hgap_large : forall t, t ∈ times -> 2 * subGaussianTextbookDeltaRadius proxy T delta t chosen < meanGap trueMean best chosen) (hscore_of_selected : forall omega t, t ∈ times -> action omega t = chosen -> confidenceScore (empiricalMean omega t) (subGaussianTextbookDeltaRadius proxy T delta t) best <= confidenceScore (empiricalMean omega t) (subGaussianTextbookDeltaRadius proxy T delta t) chosen) (hproxy : forall t arm, t < T -> 0 < ((proxy t arm : NNReal) : Real)) (hsubG : forall t arm, t < T -> ProbabilityTheory.HasSubgaussianMGF (fun omega : Omega => empiricalMean omega t arm - trueMean arm) (proxy t arm) mu) : mu {omega : Omega | exists t, t ∈ times /\ action omega t = chosen} <= ENNReal.ofReal delta

Concrete confidence-score argmax version of the selected large-gap delta bound. The score-maximality contract is discharged by `confidenceScoreArgmaxAction`, so the remaining assumptions are the textbook radius/concentration contracts and the large-gap condition for the selected arm.

theorem measure_confidenceScoreArgmax_selectedLargeGapEvent_le_subGaussian_textbookDeltaRadius_delta {Omega : Type} [MeasurableSpace Omega] {K : Nat} (hK : 0 < K) (mu : Measure Omega) [IsFiniteMeasure mu] (trueMean : Fin K -> Real) (empiricalMean : Omega -> Nat -> Fin K -> Real) (proxy : Nat -> Fin K -> NNReal) (T : Nat) (delta : Real) (t : Nat) (best chosen : Fin K) (hT : 0 < T) (hdelta : 0 < delta) (ht : t < T) (hgap_large : 2 * subGaussianTextbookDeltaRadius proxy T delta t chosen < meanGap trueMean best chosen) (hproxy : forall t arm, t < T -> 0 < ((proxy t arm : NNReal) : Real)) (hsubG : forall t arm, t < T -> ProbabilityTheory.HasSubgaussianMGF (fun omega : Omega => empiricalMean omega t arm - trueMean arm) (proxy t arm) mu) : mu {omega : Omega | confidenceScoreArgmaxAction hK empiricalMean (subGaussianTextbookDeltaRadius proxy T delta) omega t = chosen} <= ENNReal.ofReal delta

Finite-time-set concrete confidence-score argmax version of the selected large-gap delta bound.

theorem measure_confidenceScoreArgmax_selectedLargeGapEventOn_le_subGaussian_textbookDeltaRadius_delta {Omega : Type} [MeasurableSpace Omega] {K : Nat} (hK : 0 < K) (mu : Measure Omega) [IsFiniteMeasure mu] (trueMean : Fin K -> Real) (empiricalMean : Omega -> Nat -> Fin K -> Real) (proxy : Nat -> Fin K -> NNReal) (T : Nat) (delta : Real) (times : Finset Nat) (best chosen : Fin K) (hT : 0 < T) (hdelta : 0 < delta) (htimes : forall t, t ∈ times -> t < T) (hgap_large : forall t, t ∈ times -> 2 * subGaussianTextbookDeltaRadius proxy T delta t chosen < meanGap trueMean best chosen) (hproxy : forall t arm, t < T -> 0 < ((proxy t arm : NNReal) : Real)) (hsubG : forall t arm, t < T -> ProbabilityTheory.HasSubgaussianMGF (fun omega : Omega => empiricalMean omega t arm - trueMean arm) (proxy t arm) mu) : mu {omega : Omega | exists t, t ∈ times /\ confidenceScoreArgmaxAction hK empiricalMean (subGaussianTextbookDeltaRadius proxy T delta) omega t = chosen} <= ENNReal.ofReal delta

Summing the single-time concrete score-argmax selected large-gap bounds over a finite time set gives a finite-count probability budget. This is the first counting-facing UCB bridge: it keeps the statement as a sum of selected-action event probabilities before converting it to a lower integral of selected-time indicators.

theorem sum_measure_confidenceScoreArgmax_selectedLargeGapEventOn_le_card_mul_delta {Omega : Type} [MeasurableSpace Omega] {K : Nat} (hK : 0 < K) (mu : Measure Omega) [IsFiniteMeasure mu] (trueMean : Fin K -> Real) (empiricalMean : Omega -> Nat -> Fin K -> Real) (proxy : Nat -> Fin K -> NNReal) (T : Nat) (delta : Real) (times : Finset Nat) (best chosen : Fin K) (hT : 0 < T) (hdelta : 0 < delta) (htimes : forall t, t ∈ times -> t < T) (hgap_large : forall t, t ∈ times -> 2 * subGaussianTextbookDeltaRadius proxy T delta t chosen < meanGap trueMean best chosen) (hproxy : forall t arm, t < T -> 0 < ((proxy t arm : NNReal) : Real)) (hsubG : forall t arm, t < T -> ProbabilityTheory.HasSubgaussianMGF (fun omega : Omega => empiricalMean omega t arm - trueMean arm) (proxy t arm) mu) : times.sum (fun t : Nat => mu {omega : Omega | confidenceScoreArgmaxAction hK empiricalMean (subGaussianTextbookDeltaRadius proxy T delta) omega t = chosen}) <= (times.card : ENNReal) * ENNReal.ofReal delta

Lower-integral selected-count budget for concrete score-argmax UCB over an explicit finite time set. The integrand is the finite sum of selected-action indicators over `times`. This is not yet the recursive `pullCount`, but it is the expectation-facing finite-count surface needed to bridge the selected-event probability bounds into pull-count and regret arguments.

theorem lintegral_confidenceScoreArgmax_selectedLargeGapCountOn_le_card_mul_delta {Omega : Type} [MeasurableSpace Omega] {K : Nat} (hK : 0 < K) [MeasurableSpace (Fin K)] [MeasurableSingletonClass (Fin K)] (mu : Measure Omega) [IsFiniteMeasure mu] (trueMean : Fin K -> Real) (empiricalMean : Omega -> Nat -> Fin K -> Real) (proxy : Nat -> Fin K -> NNReal) (T : Nat) (delta : Real) (times : Finset Nat) (best chosen : Fin K) (hT : 0 < T) (hdelta : 0 < delta) (htimes : forall t, t ∈ times -> t < T) (hgap_large : forall t, t ∈ times -> 2 * subGaussianTextbookDeltaRadius proxy T delta t chosen < meanGap trueMean best chosen) (haction : forall t : Nat, Measurable (fun omega : Omega => confidenceScoreArgmaxAction hK empiricalMean (subGaussianTextbookDeltaRadius proxy T delta) omega t)) (hproxy : forall t arm, t < T -> 0 < ((proxy t arm : NNReal) : Real)) (hsubG : forall t arm, t < T -> ProbabilityTheory.HasSubgaussianMGF (fun omega : Omega => empiricalMean omega t arm - trueMean arm) (proxy t arm) mu) : MeasureTheory.lintegral mu (fun omega : Omega => times.sum (fun t : Nat => (({omega' : Omega | confidenceScoreArgmaxAction hK empiricalMean (subGaussianTextbookDeltaRadius proxy T delta) omega' t = chosen} : Set Omega).indicator (1 : Omega -> ENNReal)) omega)) <= (times.card : ENNReal) * ENNReal.ofReal delta

Recursive pull-count lower-integral budget for a concrete score-argmax UCB arm whose large-gap condition holds throughout the horizon. This specializes the finite-time selected-count bridge to `Finset.range T` and then uses the existing project-local `pullCount` lower-integral identity. It does not yet split the horizon into small-radius and large-radius phases.

theorem lintegral_confidenceScoreArgmax_pullCount_le_horizon_mul_delta {Omega : Type} [MeasurableSpace Omega] {K : Nat} (hK : 0 < K) [MeasurableSpace (Fin K)] [MeasurableSingletonClass (Fin K)] (mu : Measure Omega) [IsFiniteMeasure mu] (trueMean : Fin K -> Real) (empiricalMean : Omega -> Nat -> Fin K -> Real) (proxy : Nat -> Fin K -> NNReal) (T : Nat) (delta : Real) (best chosen : Fin K) (hT : 0 < T) (hdelta : 0 < delta) (hgap_large : forall t, t < T -> 2 * subGaussianTextbookDeltaRadius proxy T delta t chosen < meanGap trueMean best chosen) (haction : forall t : Nat, Measurable (fun omega : Omega => confidenceScoreArgmaxAction hK empiricalMean (subGaussianTextbookDeltaRadius proxy T delta) omega t)) (hproxy : forall t arm, t < T -> 0 < ((proxy t arm : NNReal) : Real)) (hsubG : forall t arm, t < T -> ProbabilityTheory.HasSubgaussianMGF (fun omega : Omega => empiricalMean omega t arm - trueMean arm) (proxy t arm) mu) : MeasureTheory.lintegral mu (fun omega : Omega => ((pullCount ((confidenceScoreArgmaxAction hK empiricalMean (subGaussianTextbookDeltaRadius proxy T delta)) omega) chosen T : Nat) : ENNReal)) <= (T : ENNReal) * ENNReal.ofReal delta

Threshold/suffix-shaped pull-count budget for concrete score-argmax UCB. Times in `freeTimes` are charged by the trivial probability bound `1`; every other horizon time must be listed in `chargedTimes` and satisfy the large-gap condition, so those selected events are charged by `delta`.

theorem lintegral_confidenceScoreArgmax_pullCount_le_free_or_delta_sum {Omega : Type} [MeasurableSpace Omega] {K : Nat} (hK : 0 < K) [MeasurableSpace (Fin K)] [MeasurableSingletonClass (Fin K)] (mu : Measure Omega) [MeasureTheory.IsProbabilityMeasure mu] (trueMean : Fin K -> Real) (empiricalMean : Omega -> Nat -> Fin K -> Real) (proxy : Nat -> Fin K -> NNReal) (T : Nat) (delta : Real) (freeTimes chargedTimes : Finset Nat) (best chosen : Fin K) (hT : 0 < T) (hdelta : 0 < delta) (hcharged_of_not_free : forall t, t < T -> t ∉ freeTimes -> t ∈ chargedTimes) (hgap_large : forall t, t ∈ chargedTimes -> 2 * subGaussianTextbookDeltaRadius proxy T delta t chosen < meanGap trueMean best chosen) (haction : forall t : Nat, Measurable (fun omega : Omega => confidenceScoreArgmaxAction hK empiricalMean (subGaussianTextbookDeltaRadius proxy T delta) omega t)) (hproxy : forall t arm, t < T -> 0 < ((proxy t arm : NNReal) : Real)) (hsubG : forall t arm, t < T -> ProbabilityTheory.HasSubgaussianMGF (fun omega : Omega => empiricalMean omega t arm - trueMean arm) (proxy t arm) mu) : MeasureTheory.lintegral mu (fun omega : Omega => ((pullCount ((confidenceScoreArgmaxAction hK empiricalMean (subGaussianTextbookDeltaRadius proxy T delta)) omega) chosen T : Nat) : ENNReal)) <= (Finset.range T).sum (fun t : Nat => if t ∈ freeTimes then (1 : ENNReal) else ENNReal.ofReal delta)

Budgeted form of the threshold/suffix pull-count split. The only new input is a bound on the free-time indicator sum. Future radius-threshold leaves can discharge `hfree_budget` by proving a cardinality bound for the low-radius/small-sample times.

theorem lintegral_confidenceScoreArgmax_pullCount_le_freeBudget_add_horizon_delta {Omega : Type} [MeasurableSpace Omega] {K : Nat} (hK : 0 < K) [MeasurableSpace (Fin K)] [MeasurableSingletonClass (Fin K)] (mu : Measure Omega) [MeasureTheory.IsProbabilityMeasure mu] (trueMean : Fin K -> Real) (empiricalMean : Omega -> Nat -> Fin K -> Real) (proxy : Nat -> Fin K -> NNReal) (T : Nat) (delta : Real) (freeTimes chargedTimes : Finset Nat) (freeBudget : ENNReal) (best chosen : Fin K) (hT : 0 < T) (hdelta : 0 < delta) (hfree_budget : (Finset.range T).sum (fun t : Nat => if t ∈ freeTimes then (1 : ENNReal) else 0) <= freeBudget) (hcharged_of_not_free : forall t, t < T -> t ∉ freeTimes -> t ∈ chargedTimes) (hgap_large : forall t, t ∈ chargedTimes -> 2 * subGaussianTextbookDeltaRadius proxy T delta t chosen < meanGap trueMean best chosen) (haction : forall t : Nat, Measurable (fun omega : Omega => confidenceScoreArgmaxAction hK empiricalMean (subGaussianTextbookDeltaRadius proxy T delta) omega t)) (hproxy : forall t arm, t < T -> 0 < ((proxy t arm : NNReal) : Real)) (hsubG : forall t arm, t < T -> ProbabilityTheory.HasSubgaussianMGF (fun omega : Omega => empiricalMean omega t arm - trueMean arm) (proxy t arm) mu) : MeasureTheory.lintegral mu (fun omega : Omega => ((pullCount ((confidenceScoreArgmaxAction hK empiricalMean (subGaussianTextbookDeltaRadius proxy T delta)) omega) chosen T : Nat) : ENNReal)) <= freeBudget + (T : ENNReal) * ENNReal.ofReal delta

The ENNReal indicator count of a finite set of free horizon times is bounded by the total number of declared free times.

theorem freeTimes_indicator_sum_le_card (T : Nat) (freeTimes : Finset Nat) : (Finset.range T).sum (fun t : Nat => if t ∈ freeTimes then (1 : ENNReal) else 0) <= (freeTimes.card : ENNReal)

Along one concrete action trace, the number of selected times whose previous pull count is still below threshold `B` is the minimum of the terminal pull count and `B`. This is the pathwise source of the usual UCB small-count budget: selected occurrences with `pullCount < B` can happen at most `B` times, regardless of the ambient horizon length.

theorem selectedSmallPullCount_sum_eq_min_pullCount {Action : Type} [DecidableEq Action] (action : ActionTrace Action) (chosen : Action) (T B : Nat) : (Finset.range T).sum (fun t : Nat => if action t = chosen ∧ pullCount action chosen t < B then (1 : Nat) else 0) = Nat.min (pullCount action chosen T) B

Pathwise UCB small-count budget in Nat form.

theorem selectedSmallPullCount_sum_le_threshold {Action : Type} [DecidableEq Action] (action : ActionTrace Action) (chosen : Action) (T B : Nat) : (Finset.range T).sum (fun t : Nat => if action t = chosen ∧ pullCount action chosen t < B then (1 : Nat) else 0) <= B

ENNReal-facing pathwise UCB small-count budget.

theorem selectedSmallPullCount_indicator_sum_le_threshold {Action : Type} [DecidableEq Action] (action : ActionTrace Action) (chosen : Action) (T B : Nat) : (Finset.range T).sum (fun t : Nat => if action t = chosen ∧ pullCount action chosen t < B then (1 : ENNReal) else 0) <= (B : ENNReal)

Probability-facing version of the pathwise selected-small budget. No measurability assumption is needed for this upper bound: the lower integral is dominated pointwise by the constant `B`, and the measure is a probability measure.

theorem lintegral_selectedSmallPullCount_indicator_sum_le_threshold {Omega Action : Type} [MeasurableSpace Omega] [DecidableEq Action] (mu : Measure Omega) [MeasureTheory.IsProbabilityMeasure mu] (action : Omega -> ActionTrace Action) (chosen : Action) (T B : Nat) : MeasureTheory.lintegral mu (fun omega : Omega => (Finset.range T).sum (fun t : Nat => if action omega t = chosen ∧ pullCount (action omega) chosen t < B then (1 : ENNReal) else 0)) <= (B : ENNReal)

The selected-time Nat indicator sum is exactly the recursive pull count.

theorem selectedPullCount_sum_eq_pullCount {Action : Type} [DecidableEq Action] (action : ActionTrace Action) (chosen : Action) (T : Nat) : (Finset.range T).sum (fun t : Nat => if action t = chosen then (1 : Nat) else 0) = pullCount action chosen T

ENNReal-facing selected-time indicator identity for the recursive pull count.

theorem selectedPullCount_indicator_sum_eq_natCast_pullCount {Action : Type} [DecidableEq Action] (action : ActionTrace Action) (chosen : Action) (T : Nat) : (Finset.range T).sum (fun t : Nat => if action t = chosen then (1 : ENNReal) else 0) = ((pullCount action chosen T : Nat) : ENNReal)

Every selected time is either a selected-small time or a selected-large-count time, split by the threshold `B`.

theorem selectedPullCount_indicator_sum_eq_selectedSmall_add_selectedLargePullCount {Action : Type} [DecidableEq Action] (action : ActionTrace Action) (chosen : Action) (T B : Nat) : (Finset.range T).sum (fun t : Nat => if action t = chosen then (1 : ENNReal) else 0) = (Finset.range T).sum (fun t : Nat => if action t = chosen ∧ pullCount action chosen t < B then (1 : ENNReal) else 0) + (Finset.range T).sum (fun t : Nat => if action t = chosen ∧ B <= pullCount action chosen t then (1 : ENNReal) else 0)

Pointwise ENNReal UCB count budget after isolating selected-large-count times. The selected-small part is charged by `B`; only selected times whose prior pull count is at least `B` remain for a future large-gap tail bound.

theorem natCast_pullCount_le_threshold_add_selectedLargePullCount_indicator_sum {Action : Type} [DecidableEq Action] (action : ActionTrace Action) (chosen : Action) (T B : Nat) : ((pullCount action chosen T : Nat) : ENNReal) <= (B : ENNReal) + (Finset.range T).sum (fun t : Nat => if action t = chosen ∧ B <= pullCount action chosen t then (1 : ENNReal) else 0)

Measurability of a selected-large-count event for a fixed time.

theorem measurableSet_selectedLargePullCount {Omega Action : Type} [MeasurableSpace Omega] [MeasurableSpace Action] [MeasurableSingletonClass Action] [MeasurableSpace Nat] [MeasurableAdd₂ Nat] [OpensMeasurableSpace Nat] [DecidableEq Action] (action : Omega -> ActionTrace Action) (haction : forall t : Nat, Measurable (fun omega : Omega => action omega t)) (chosen : Action) (t B : Nat) : MeasurableSet {omega : Omega | action omega t = chosen ∧ B <= pullCount (action omega) chosen t}

The lower integral of selected-large-count indicators is the corresponding finite sum of event measures.

theorem lintegral_selectedLargePullCount_indicator_sum_eq_sum_measure {Omega Action : Type} [MeasurableSpace Omega] [MeasurableSpace Action] [MeasurableSingletonClass Action] [MeasurableSpace Nat] [MeasurableAdd₂ Nat] [OpensMeasurableSpace Nat] [DecidableEq Action] (mu : Measure Omega) (action : Omega -> ActionTrace Action) (haction : forall t : Nat, Measurable (fun omega : Omega => action omega t)) (chosen : Action) (T B : Nat) : MeasureTheory.lintegral mu (fun omega : Omega => (Finset.range T).sum (fun t : Nat => if action omega t = chosen ∧ B <= pullCount (action omega) chosen t then (1 : ENNReal) else 0)) = (Finset.range T).sum (fun t : Nat => mu {omega : Omega | action omega t = chosen ∧ B <= pullCount (action omega) chosen t})

Single-time selected-large-count event budget for concrete score-argmax UCB. If the event is nonempty but the deterministic large-gap inequality fails, the pointwise large-count-to-large-gap contract gives a contradiction. Otherwise it reduces to the existing selected-event `delta` bound.

theorem measure_confidenceScoreArgmax_selectedLargePullCountEvent_le_subGaussian_textbookDeltaRadius_delta {Omega : Type} [MeasurableSpace Omega] {K : Nat} (hK : 0 < K) (mu : Measure Omega) [IsFiniteMeasure mu] (trueMean : Fin K -> Real) (empiricalMean : Omega -> Nat -> Fin K -> Real) (proxy : Nat -> Fin K -> NNReal) (T : Nat) (delta : Real) (t B : Nat) (best chosen : Fin K) (hT : 0 < T) (hdelta : 0 < delta) (ht : t < T) (hlarge_count_gap : forall omega : Omega, confidenceScoreArgmaxAction hK empiricalMean (subGaussianTextbookDeltaRadius proxy T delta) omega t = chosen -> B <= pullCount ((confidenceScoreArgmaxAction hK empiricalMean (subGaussianTextbookDeltaRadius proxy T delta)) omega) chosen t -> 2 * subGaussianTextbookDeltaRadius proxy T delta t chosen < meanGap trueMean best chosen) (hproxy : forall t arm, t < T -> 0 < ((proxy t arm : NNReal) : Real)) (hsubG : forall t arm, t < T -> ProbabilityTheory.HasSubgaussianMGF (fun omega : Omega => empiricalMean omega t arm - trueMean arm) (proxy t arm) mu) : mu {omega : Omega | confidenceScoreArgmaxAction hK empiricalMean (subGaussianTextbookDeltaRadius proxy T delta) omega t = chosen ∧ B <= pullCount ((confidenceScoreArgmaxAction hK empiricalMean (subGaussianTextbookDeltaRadius proxy T delta)) omega) chosen t} <= ENNReal.ofReal delta

Finite-horizon sum budget for selected-large-count concrete score-argmax events.

theorem sum_measure_confidenceScoreArgmax_selectedLargePullCountEvent_le_horizon_mul_delta {Omega : Type} [MeasurableSpace Omega] {K : Nat} (hK : 0 < K) (mu : Measure Omega) [IsFiniteMeasure mu] (trueMean : Fin K -> Real) (empiricalMean : Omega -> Nat -> Fin K -> Real) (proxy : Nat -> Fin K -> NNReal) (T : Nat) (delta : Real) (B : Nat) (best chosen : Fin K) (hT : 0 < T) (hdelta : 0 < delta) (hlarge_count_gap : forall omega t, t < T -> confidenceScoreArgmaxAction hK empiricalMean (subGaussianTextbookDeltaRadius proxy T delta) omega t = chosen -> B <= pullCount ((confidenceScoreArgmaxAction hK empiricalMean (subGaussianTextbookDeltaRadius proxy T delta)) omega) chosen t -> 2 * subGaussianTextbookDeltaRadius proxy T delta t chosen < meanGap trueMean best chosen) (hproxy : forall t arm, t < T -> 0 < ((proxy t arm : NNReal) : Real)) (hsubG : forall t arm, t < T -> ProbabilityTheory.HasSubgaussianMGF (fun omega : Omega => empiricalMean omega t arm - trueMean arm) (proxy t arm) mu) : (Finset.range T).sum (fun t : Nat => mu {omega : Omega | confidenceScoreArgmaxAction hK empiricalMean (subGaussianTextbookDeltaRadius proxy T delta) omega t = chosen ∧ B <= pullCount ((confidenceScoreArgmaxAction hK empiricalMean (subGaussianTextbookDeltaRadius proxy T delta)) omega) chosen t}) <= (T : ENNReal) * ENNReal.ofReal delta

Lower-integral finite-sum budget for selected-large-count concrete score-argmax events.

theorem lintegral_confidenceScoreArgmax_selectedLargePullCount_indicator_sum_le_horizon_mul_delta {Omega : Type} [MeasurableSpace Omega] {K : Nat} (hK : 0 < K) [MeasurableSpace (Fin K)] [MeasurableSingletonClass (Fin K)] [MeasurableSpace Nat] [MeasurableAdd₂ Nat] [OpensMeasurableSpace Nat] (mu : Measure Omega) [IsFiniteMeasure mu] (trueMean : Fin K -> Real) (empiricalMean : Omega -> Nat -> Fin K -> Real) (proxy : Nat -> Fin K -> NNReal) (T : Nat) (delta : Real) (B : Nat) (best chosen : Fin K) (hT : 0 < T) (hdelta : 0 < delta) (haction : forall t : Nat, Measurable (fun omega : Omega => confidenceScoreArgmaxAction hK empiricalMean (subGaussianTextbookDeltaRadius proxy T delta) omega t)) (hlarge_count_gap : forall omega t, t < T -> confidenceScoreArgmaxAction hK empiricalMean (subGaussianTextbookDeltaRadius proxy T delta) omega t = chosen -> B <= pullCount ((confidenceScoreArgmaxAction hK empiricalMean (subGaussianTextbookDeltaRadius proxy T delta)) omega) chosen t -> 2 * subGaussianTextbookDeltaRadius proxy T delta t chosen < meanGap trueMean best chosen) (hproxy : forall t arm, t < T -> 0 < ((proxy t arm : NNReal) : Real)) (hsubG : forall t arm, t < T -> ProbabilityTheory.HasSubgaussianMGF (fun omega : Omega => empiricalMean omega t arm - trueMean arm) (proxy t arm) mu) : MeasureTheory.lintegral mu (fun omega : Omega => (Finset.range T).sum (fun t : Nat => if confidenceScoreArgmaxAction hK empiricalMean (subGaussianTextbookDeltaRadius proxy T delta) omega t = chosen ∧ B <= pullCount ((confidenceScoreArgmaxAction hK empiricalMean (subGaussianTextbookDeltaRadius proxy T delta)) omega) chosen t then (1 : ENNReal) else 0)) <= (T : ENNReal) * ENNReal.ofReal delta

Integrated UCB pull-count budget from a selected-large-count large-gap source.

theorem lintegral_confidenceScoreArgmax_pullCount_le_threshold_add_horizon_delta_of_selectedLargePullCount {Omega : Type} [MeasurableSpace Omega] {K : Nat} (hK : 0 < K) [MeasurableSpace (Fin K)] [MeasurableSingletonClass (Fin K)] [MeasurableSpace Nat] [MeasurableAdd₂ Nat] [OpensMeasurableSpace Nat] (mu : Measure Omega) [MeasureTheory.IsProbabilityMeasure mu] (trueMean : Fin K -> Real) (empiricalMean : Omega -> Nat -> Fin K -> Real) (proxy : Nat -> Fin K -> NNReal) (T : Nat) (delta : Real) (B : Nat) (best chosen : Fin K) (hT : 0 < T) (hdelta : 0 < delta) (haction : forall t : Nat, Measurable (fun omega : Omega => confidenceScoreArgmaxAction hK empiricalMean (subGaussianTextbookDeltaRadius proxy T delta) omega t)) (hlarge_count_gap : forall omega t, t < T -> confidenceScoreArgmaxAction hK empiricalMean (subGaussianTextbookDeltaRadius proxy T delta) omega t = chosen -> B <= pullCount ((confidenceScoreArgmaxAction hK empiricalMean (subGaussianTextbookDeltaRadius proxy T delta)) omega) chosen t -> 2 * subGaussianTextbookDeltaRadius proxy T delta t chosen < meanGap trueMean best chosen) (hproxy : forall t arm, t < T -> 0 < ((proxy t arm : NNReal) : Real)) (hsubG : forall t arm, t < T -> ProbabilityTheory.HasSubgaussianMGF (fun omega : Omega => empiricalMean omega t arm - trueMean arm) (proxy t arm) mu) : MeasureTheory.lintegral mu (fun omega : Omega => ((pullCount ((confidenceScoreArgmaxAction hK empiricalMean (subGaussianTextbookDeltaRadius proxy T delta)) omega) chosen T : Nat) : ENNReal)) <= (B : ENNReal) + (T : ENNReal) * ENNReal.ofReal delta

Concrete cardinality-budget version of the threshold/suffix pull-count split. This discharges the abstract `freeBudget` input with `freeTimes.card`. A later radius-threshold leaf can instantiate `freeTimes` and prove its cardinality is the usual logarithmic/gap-dependent budget.

theorem lintegral_confidenceScoreArgmax_pullCount_le_freeCard_add_horizon_delta {Omega : Type} [MeasurableSpace Omega] {K : Nat} (hK : 0 < K) [MeasurableSpace (Fin K)] [MeasurableSingletonClass (Fin K)] (mu : Measure Omega) [MeasureTheory.IsProbabilityMeasure mu] (trueMean : Fin K -> Real) (empiricalMean : Omega -> Nat -> Fin K -> Real) (proxy : Nat -> Fin K -> NNReal) (T : Nat) (delta : Real) (freeTimes chargedTimes : Finset Nat) (best chosen : Fin K) (hT : 0 < T) (hdelta : 0 < delta) (hcharged_of_not_free : forall t, t < T -> t ∉ freeTimes -> t ∈ chargedTimes) (hgap_large : forall t, t ∈ chargedTimes -> 2 * subGaussianTextbookDeltaRadius proxy T delta t chosen < meanGap trueMean best chosen) (haction : forall t : Nat, Measurable (fun omega : Omega => confidenceScoreArgmaxAction hK empiricalMean (subGaussianTextbookDeltaRadius proxy T delta) omega t)) (hproxy : forall t arm, t < T -> 0 < ((proxy t arm : NNReal) : Real)) (hsubG : forall t arm, t < T -> ProbabilityTheory.HasSubgaussianMGF (fun omega : Omega => empiricalMean omega t arm - trueMean arm) (proxy t arm) mu) : MeasureTheory.lintegral mu (fun omega : Omega => ((pullCount ((confidenceScoreArgmaxAction hK empiricalMean (subGaussianTextbookDeltaRadius proxy T delta)) omega) chosen T : Nat) : ENNReal)) <= (freeTimes.card : ENNReal) + (T : ENNReal) * ENNReal.ofReal delta

Horizon times where the textbook delta radius is already small enough for the selected arm to satisfy the large-gap condition.

noncomputable def subGaussianTextbookDeltaRadiusChargedTimes {K : Nat} (trueMean : Fin K -> Real) (proxy : Nat -> Fin K -> NNReal) (T : Nat) (delta : Real) (best chosen : Fin K) : Finset Nat

Horizon times not yet discharged by the textbook large-gap radius condition. The next cardinality leaf can bound this concrete set by a closed-form gap/log/sample threshold.

noncomputable def subGaussianTextbookDeltaRadiusFreeTimes {K : Nat} (trueMean : Fin K -> Real) (proxy : Nat -> Fin K -> NNReal) (T : Nat) (delta : Real) (best chosen : Fin K) : Finset Nat

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

@[simp] theorem mem_subGaussianTextbookDeltaRadiusChargedTimes_iff {K : Nat} (trueMean : Fin K -> Real) (proxy : Nat -> Fin K -> NNReal) (T : Nat) (delta : Real) (best chosen : Fin K) (t : Nat) : t ∈ subGaussianTextbookDeltaRadiusChargedTimes trueMean proxy T delta best chosen ↔ t < T ∧ 2 * subGaussianTextbookDeltaRadius proxy T delta t chosen < meanGap trueMean best chosen

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

@[simp] theorem mem_subGaussianTextbookDeltaRadiusFreeTimes_iff {K : Nat} (trueMean : Fin K -> Real) (proxy : Nat -> Fin K -> NNReal) (T : Nat) (delta : Real) (best chosen : Fin K) (t : Nat) : t ∈ subGaussianTextbookDeltaRadiusFreeTimes trueMean proxy T delta best chosen ↔ t < T ∧ ¬ 2 * subGaussianTextbookDeltaRadius proxy T delta t chosen < meanGap trueMean best chosen

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

theorem subGaussianTextbookDeltaRadiusChargedTimes_of_not_free {K : Nat} (trueMean : Fin K -> Real) (proxy : Nat -> Fin K -> NNReal) (T : Nat) (delta : Real) (best chosen : Fin K) (t : Nat) : t < T -> t ∉ subGaussianTextbookDeltaRadiusFreeTimes trueMean proxy T delta best chosen -> t ∈ subGaussianTextbookDeltaRadiusChargedTimes trueMean proxy T delta best chosen

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

theorem subGaussianTextbookDeltaRadiusChargedTimes_gap_large {K : Nat} (trueMean : Fin K -> Real) (proxy : Nat -> Fin K -> NNReal) (T : Nat) (delta : Real) (best chosen : Fin K) (t : Nat) : t ∈ subGaussianTextbookDeltaRadiusChargedTimes trueMean proxy T delta best chosen -> 2 * subGaussianTextbookDeltaRadius proxy T delta t chosen < meanGap trueMean best chosen

Concrete radius-threshold split for the textbook delta UCB pull-count budget. This instantiates the abstract `freeTimes`/`chargedTimes` split with the large-gap predicate induced by `subGaussianTextbookDeltaRadius`. It leaves the closed-form cardinality bound for the concrete free-time set to the next leaf.

theorem lintegral_confidenceScoreArgmax_pullCount_le_textbookDeltaRadiusFreeCard_add_horizon_delta {Omega : Type} [MeasurableSpace Omega] {K : Nat} (hK : 0 < K) [MeasurableSpace (Fin K)] [MeasurableSingletonClass (Fin K)] (mu : Measure Omega) [MeasureTheory.IsProbabilityMeasure mu] (trueMean : Fin K -> Real) (empiricalMean : Omega -> Nat -> Fin K -> Real) (proxy : Nat -> Fin K -> NNReal) (T : Nat) (delta : Real) (best chosen : Fin K) (hT : 0 < T) (hdelta : 0 < delta) (haction : forall t : Nat, Measurable (fun omega : Omega => confidenceScoreArgmaxAction hK empiricalMean (subGaussianTextbookDeltaRadius proxy T delta) omega t)) (hproxy : forall t arm, t < T -> 0 < ((proxy t arm : NNReal) : Real)) (hsubG : forall t arm, t < T -> ProbabilityTheory.HasSubgaussianMGF (fun omega : Omega => empiricalMean omega t arm - trueMean arm) (proxy t arm) mu) : MeasureTheory.lintegral mu (fun omega : Omega => ((pullCount ((confidenceScoreArgmaxAction hK empiricalMean (subGaussianTextbookDeltaRadius proxy T delta)) omega) chosen T : Nat) : ENNReal)) <= ((subGaussianTextbookDeltaRadiusFreeTimes trueMean proxy T delta best chosen).card : ENNReal) + (T : ENNReal) * ENNReal.ofReal delta

If every horizon time at or beyond threshold `B` satisfies the textbook large-gap radius condition, then the concrete free-time set has cardinality at most `B`.

theorem subGaussianTextbookDeltaRadiusFreeTimes_card_le_threshold {K : Nat} (trueMean : Fin K -> Real) (proxy : Nat -> Fin K -> NNReal) (T : Nat) (delta : Real) (best chosen : Fin K) (B : Nat) (hlarge_after : forall t, t < T -> B <= t -> 2 * subGaussianTextbookDeltaRadius proxy T delta t chosen < meanGap trueMean best chosen) : (subGaussianTextbookDeltaRadiusFreeTimes trueMean proxy T delta best chosen).card <= B

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

theorem subGaussianTextbookDeltaRadiusFreeTimes_card_le_threshold_ennreal {K : Nat} (trueMean : Fin K -> Real) (proxy : Nat -> Fin K -> NNReal) (T : Nat) (delta : Real) (best chosen : Fin K) (B : Nat) (hlarge_after : forall t, t < T -> B <= t -> 2 * subGaussianTextbookDeltaRadius proxy T delta t chosen < meanGap trueMean best chosen) : ((subGaussianTextbookDeltaRadiusFreeTimes trueMean proxy T delta best chosen).card : ENNReal) <= (B : ENNReal)

Threshold-budget version of the concrete textbook-radius UCB pull-count split. The only new deterministic input is that all times `t >= B` in the horizon satisfy the large-gap radius condition. A later leaf can instantiate `B` with a closed-form logarithmic/gap-dependent expression.

theorem lintegral_confidenceScoreArgmax_pullCount_le_textbookDeltaRadiusThreshold_add_horizon_delta {Omega : Type} [MeasurableSpace Omega] {K : Nat} (hK : 0 < K) [MeasurableSpace (Fin K)] [MeasurableSingletonClass (Fin K)] (mu : Measure Omega) [MeasureTheory.IsProbabilityMeasure mu] (trueMean : Fin K -> Real) (empiricalMean : Omega -> Nat -> Fin K -> Real) (proxy : Nat -> Fin K -> NNReal) (T : Nat) (delta : Real) (best chosen : Fin K) (B : Nat) (hT : 0 < T) (hdelta : 0 < delta) (hlarge_after : forall t, t < T -> B <= t -> 2 * subGaussianTextbookDeltaRadius proxy T delta t chosen < meanGap trueMean best chosen) (haction : forall t : Nat, Measurable (fun omega : Omega => confidenceScoreArgmaxAction hK empiricalMean (subGaussianTextbookDeltaRadius proxy T delta) omega t)) (hproxy : forall t arm, t < T -> 0 < ((proxy t arm : NNReal) : Real)) (hsubG : forall t arm, t < T -> ProbabilityTheory.HasSubgaussianMGF (fun omega : Omega => empiricalMean omega t arm - trueMean arm) (proxy t arm) mu) : MeasureTheory.lintegral mu (fun omega : Omega => ((pullCount ((confidenceScoreArgmaxAction hK empiricalMean (subGaussianTextbookDeltaRadius proxy T delta)) omega) chosen T : Nat) : ENNReal)) <= (B : ENNReal) + (T : ENNReal) * ENNReal.ofReal delta

Half-gap radius condition in the textbook form implies the large-gap condition consumed by the UCB selected-event and pull-count budget wrappers.

theorem subGaussianTextbookDeltaRadius_large_gap_of_lt_half_meanGap {K : Nat} (trueMean : Fin K -> Real) (proxy : Nat -> Fin K -> NNReal) (T : Nat) (delta : Real) (best chosen : Fin K) (t : Nat) (hhalf : subGaussianTextbookDeltaRadius proxy T delta t chosen < meanGap trueMean best chosen / 2) : 2 * subGaussianTextbookDeltaRadius proxy T delta t chosen < meanGap trueMean best chosen

Half-gap threshold version of the concrete textbook-radius UCB pull-count budget. This is the surface normally targeted by the remaining logarithmic/gap algebra: prove that after threshold `B`, the textbook radius is below half the chosen arm's gap.

theorem lintegral_confidenceScoreArgmax_pullCount_le_textbookDeltaRadiusHalfGapThreshold_add_horizon_delta {Omega : Type} [MeasurableSpace Omega] {K : Nat} (hK : 0 < K) [MeasurableSpace (Fin K)] [MeasurableSingletonClass (Fin K)] (mu : Measure Omega) [MeasureTheory.IsProbabilityMeasure mu] (trueMean : Fin K -> Real) (empiricalMean : Omega -> Nat -> Fin K -> Real) (proxy : Nat -> Fin K -> NNReal) (T : Nat) (delta : Real) (best chosen : Fin K) (B : Nat) (hT : 0 < T) (hdelta : 0 < delta) (hhalf_after : forall t, t < T -> B <= t -> subGaussianTextbookDeltaRadius proxy T delta t chosen < meanGap trueMean best chosen / 2) (haction : forall t : Nat, Measurable (fun omega : Omega => confidenceScoreArgmaxAction hK empiricalMean (subGaussianTextbookDeltaRadius proxy T delta) omega t)) (hproxy : forall t arm, t < T -> 0 < ((proxy t arm : NNReal) : Real)) (hsubG : forall t arm, t < T -> ProbabilityTheory.HasSubgaussianMGF (fun omega : Omega => empiricalMean omega t arm - trueMean arm) (proxy t arm) mu) : MeasureTheory.lintegral mu (fun omega : Omega => ((pullCount ((confidenceScoreArgmaxAction hK empiricalMean (subGaussianTextbookDeltaRadius proxy T delta)) omega) chosen T : Nat) : ENNReal)) <= (B : ENNReal) + (T : ENNReal) * ENNReal.ofReal delta

Square-form deterministic algebra for the textbook delta radius: if the quantity under the square root is below `(gap / 2)^2`, the radius is below half the gap.

theorem subGaussianTextbookDeltaRadius_lt_half_meanGap_of_sq_lt {K : Nat} (trueMean : Fin K -> Real) (proxy : Nat -> Fin K -> NNReal) (T : Nat) (delta : Real) (best chosen : Fin K) (t : Nat) (hgap_pos : 0 < meanGap trueMean best chosen) (hsq : 2 * ((proxy t chosen : NNReal) : Real) * Real.log (textbookDeltaScale (Arm

Common UCB algebra form for the textbook delta radius: the sufficient condition `8 * proxy * log(scale) < gap^2` implies `radius < gap / 2`.

theorem subGaussianTextbookDeltaRadius_lt_half_meanGap_of_eight_mul_lt_sq {K : Nat} (trueMean : Fin K -> Real) (proxy : Nat -> Fin K -> NNReal) (T : Nat) (delta : Real) (best chosen : Fin K) (t : Nat) (hgap_pos : 0 < meanGap trueMean best chosen) (height : 8 * ((proxy t chosen : NNReal) : Real) * Real.log (textbookDeltaScale (Arm

Eight-proxy-log threshold version of the concrete textbook-radius UCB pull-count budget. The remaining closed-form work is to prove the displayed square inequality from a concrete choice of `B` and whatever sample-count/proxy monotonicity the eventual empirical-mean construction provides.

theorem lintegral_confidenceScoreArgmax_pullCount_le_textbookDeltaRadiusEightProxyLogThreshold_add_horizon_delta {Omega : Type} [MeasurableSpace Omega] {K : Nat} (hK : 0 < K) [MeasurableSpace (Fin K)] [MeasurableSingletonClass (Fin K)] (mu : Measure Omega) [MeasureTheory.IsProbabilityMeasure mu] (trueMean : Fin K -> Real) (empiricalMean : Omega -> Nat -> Fin K -> Real) (proxy : Nat -> Fin K -> NNReal) (T : Nat) (delta : Real) (best chosen : Fin K) (B : Nat) (hT : 0 < T) (hdelta : 0 < delta) (hgap_pos : 0 < meanGap trueMean best chosen) (height_after : forall t, t < T -> B <= t -> 8 * ((proxy t chosen : NNReal) : Real) * Real.log (textbookDeltaScale (Arm

Proxy-small form of the textbook radius half-gap algebra. Under a positive logarithmic scale, bounding the selected arm's proxy by `gap^2 / (8 * log scale)` implies the usual eight-proxy-log condition and hence `radius < gap / 2`.

theorem subGaussianTextbookDeltaRadius_lt_half_meanGap_of_proxy_lt_gap_sq_div {K : Nat} (trueMean : Fin K -> Real) (proxy : Nat -> Fin K -> NNReal) (T : Nat) (delta : Real) (best chosen : Fin K) (t : Nat) (hgap_pos : 0 < meanGap trueMean best chosen) (hlog_pos : 0 < Real.log (textbookDeltaScale (Arm

Proxy-small threshold version of the concrete textbook-radius UCB pull-count budget. This is the handoff expected from a later empirical-mean/sample-count leaf: after threshold `B`, prove the selected arm's sub-Gaussian proxy is below the displayed gap/log scale.

theorem lintegral_confidenceScoreArgmax_pullCount_le_textbookDeltaRadiusProxyThreshold_add_horizon_delta {Omega : Type} [MeasurableSpace Omega] {K : Nat} (hK : 0 < K) [MeasurableSpace (Fin K)] [MeasurableSingletonClass (Fin K)] (mu : Measure Omega) [MeasureTheory.IsProbabilityMeasure mu] (trueMean : Fin K -> Real) (empiricalMean : Omega -> Nat -> Fin K -> Real) (proxy : Nat -> Fin K -> NNReal) (T : Nat) (delta : Real) (best chosen : Fin K) (B : Nat) (hT : 0 < T) (hdelta : 0 < delta) (hgap_pos : 0 < meanGap trueMean best chosen) (hlog_pos : 0 < Real.log (textbookDeltaScale (Arm

Sample-count proxy form of the textbook radius half-gap algebra. If the selected arm's proxy is bounded by `varianceProxy / count`, then a count threshold of the form `8 * varianceProxy * log(scale) < gap^2 * count` implies the proxy-small condition and hence `radius < gap / 2`.

theorem subGaussianTextbookDeltaRadius_lt_half_meanGap_of_proxy_le_variance_div_count {K : Nat} (trueMean : Fin K -> Real) (proxy : Nat -> Fin K -> NNReal) (T : Nat) (delta : Real) (best chosen : Fin K) (t : Nat) (varianceProxy : NNReal) (count : Nat) (hgap_pos : 0 < meanGap trueMean best chosen) (hlog_pos : 0 < Real.log (textbookDeltaScale (Arm

Sample-count threshold version of the concrete textbook-radius UCB pull-count budget. This keeps the probabilistic/concentration assumptions abstract, but turns the remaining radius-threshold algebra into explicit count and proxy contracts.

theorem lintegral_confidenceScoreArgmax_pullCount_le_textbookDeltaRadiusSampleCountThreshold_add_horizon_delta {Omega : Type} [MeasurableSpace Omega] {K : Nat} (hK : 0 < K) [MeasurableSpace (Fin K)] [MeasurableSingletonClass (Fin K)] (mu : Measure Omega) [MeasureTheory.IsProbabilityMeasure mu] (trueMean : Fin K -> Real) (empiricalMean : Omega -> Nat -> Fin K -> Real) (proxy : Nat -> Fin K -> NNReal) (T : Nat) (delta : Real) (best chosen : Fin K) (B : Nat) (varianceProxy : NNReal) (count : Nat -> Fin K -> Nat) (hT : 0 < T) (hdelta : 0 < delta) (hgap_pos : 0 < meanGap trueMean best chosen) (hlog_pos : 0 < Real.log (textbookDeltaScale (Arm

Closed threshold-to-count algebra: if the real threshold `8 * varianceProxy * log(scale) / gap^2` is below `B`, and `B <= count`, then the count is large enough for the sample-count UCB radius condition.

theorem subGaussianTextbookDeltaRadius_count_large_of_threshold_lt_bound {K : Nat} (trueMean : Fin K -> Real) (T : Nat) (delta : Real) (best chosen : Fin K) (varianceProxy : NNReal) (B count : Nat) (hgap_pos : 0 < meanGap trueMean best chosen) (hthreshold_lt_B : 8 * ((varianceProxy : NNReal) : Real) * Real.log (textbookDeltaScale (Arm

Lower-bound-on-count version of the concrete textbook-radius UCB pull-count budget. A later adaptive trace leaf can aim to prove `B <= count t chosen` after the same threshold `B`; this wrapper then supplies the usual `B + T * delta` pull-count budget.

theorem lintegral_confidenceScoreArgmax_pullCount_le_textbookDeltaRadiusSampleCountLowerBound_add_horizon_delta {Omega : Type} [MeasurableSpace Omega] {K : Nat} (hK : 0 < K) [MeasurableSpace (Fin K)] [MeasurableSingletonClass (Fin K)] (mu : Measure Omega) [MeasureTheory.IsProbabilityMeasure mu] (trueMean : Fin K -> Real) (empiricalMean : Omega -> Nat -> Fin K -> Real) (proxy : Nat -> Fin K -> NNReal) (T : Nat) (delta : Real) (best chosen : Fin K) (B : Nat) (varianceProxy : NNReal) (count : Nat -> Fin K -> Nat) (hT : 0 < T) (hdelta : 0 < delta) (hgap_pos : 0 < meanGap trueMean best chosen) (hlog_pos : 0 < Real.log (textbookDeltaScale (Arm

Recursive sample-count adapter for the selected-large-count UCB budget. For selected times whose previous recursive pull count is at least `B`, a variance-over-count proxy bound plus the closed real threshold certificate implies the textbook radius is below half the gap. The selected-large-count wrapper then yields the usual `B + T * delta` pull-count budget.

theorem lintegral_confidenceScoreArgmax_pullCount_le_textbookDeltaRadiusRecursiveSampleCount_add_horizon_delta {Omega : Type} [MeasurableSpace Omega] {K : Nat} (hK : 0 < K) [MeasurableSpace (Fin K)] [MeasurableSingletonClass (Fin K)] [MeasurableSpace Nat] [MeasurableAdd₂ Nat] [OpensMeasurableSpace Nat] (mu : Measure Omega) [MeasureTheory.IsProbabilityMeasure mu] (trueMean : Fin K -> Real) (empiricalMean : Omega -> Nat -> Fin K -> Real) (proxy : Nat -> Fin K -> NNReal) (T : Nat) (delta : Real) (B : Nat) (best chosen : Fin K) (varianceProxy : NNReal) (hT : 0 < T) (hdelta : 0 < delta) (hgap_pos : 0 < meanGap trueMean best chosen) (hlog_pos : 0 < Real.log (textbookDeltaScale (Arm

Source-count version of the recursive sample-count UCB budget. This wrapper is meant for later empirical-mean leaves: they can expose their own history-derived `sampleCount`, prove it agrees with recursive `pullCount` on selected-large events, and provide the usual variance-over-count proxy bound for that source count. The existing recursive sample-count adapter then gives the same `B + T * delta` pull-count budget.

theorem lintegral_confidenceScoreArgmax_pullCount_le_textbookDeltaRadiusSampleCountSource_add_horizon_delta {Omega : Type} [MeasurableSpace Omega] {K : Nat} (hK : 0 < K) [MeasurableSpace (Fin K)] [MeasurableSingletonClass (Fin K)] [MeasurableSpace Nat] [MeasurableAdd₂ Nat] [OpensMeasurableSpace Nat] (mu : Measure Omega) [MeasureTheory.IsProbabilityMeasure mu] (trueMean : Fin K -> Real) (empiricalMean : Omega -> Nat -> Fin K -> Real) (proxy : Nat -> Fin K -> NNReal) (T : Nat) (delta : Real) (B : Nat) (best chosen : Fin K) (varianceProxy : NNReal) (sampleCount : Omega -> Nat -> Fin K -> Nat) (hT : 0 < T) (hdelta : 0 < delta) (hgap_pos : 0 < meanGap trueMean best chosen) (hlog_pos : 0 < Real.log (textbookDeltaScale (Arm

History-action source-count version of the textbook-radius UCB pull-count budget. If an externally generated history trace agrees with the concrete score-argmax UCB trace throughout the horizon, and its own recursive pull count supplies the variance-over-count proxy contract on selected-large events, then that history trace inherits the same `B + T * delta` selected-arm count budget.

theorem lintegral_historyAction_pullCount_le_textbookDeltaRadiusSampleCountSource_add_horizon_delta {Omega : Type} [MeasurableSpace Omega] {K : Nat} (hK : 0 < K) [MeasurableSpace (Fin K)] [MeasurableSingletonClass (Fin K)] [MeasurableSpace Nat] [MeasurableAdd₂ Nat] [OpensMeasurableSpace Nat] (mu : Measure Omega) [MeasureTheory.IsProbabilityMeasure mu] (trueMean : Fin K -> Real) (empiricalMean : Omega -> Nat -> Fin K -> Real) (proxy : Nat -> Fin K -> NNReal) (T : Nat) (delta : Real) (B : Nat) (best chosen : Fin K) (varianceProxy : NNReal) (historyAction : Omega -> ActionTrace (Fin K)) (hT : 0 < T) (hdelta : 0 < delta) (hgap_pos : 0 < meanGap trueMean best chosen) (hlog_pos : 0 < Real.log (textbookDeltaScale (Arm

Generated-policy source-count version of the textbook-radius UCB pull-count budget. This packages the previous history-action wrapper for a concrete `Policy.generatedActionTrace`. Pointwise equality with score argmax over all time coordinates transfers measurability from the generated policy trace to the score-argmax trace, and the existing history-action adapter supplies the `B + T * delta` selected-arm count budget.

theorem lintegral_generatedActionTrace_pullCount_le_textbookDeltaRadiusSampleCountSource_add_horizon_delta {Omega State : Type} [MeasurableSpace Omega] [MeasurableSpace State] {K : Nat} (hK : 0 < K) [MeasurableSpace (Fin K)] [MeasurableSingletonClass (Fin K)] [MeasurableSpace Nat] [MeasurableAdd₂ Nat] [OpensMeasurableSpace Nat] (mu : Measure Omega) [MeasureTheory.IsProbabilityMeasure mu] (trueMean : Fin K -> Real) (empiricalMean : Omega -> Nat -> Fin K -> Real) (proxy : Nat -> Fin K -> NNReal) (T : Nat) (delta : Real) (B : Nat) (best chosen : Fin K) (varianceProxy : NNReal) (policy : Policy.MeasurablePolicy State (Fin K)) (state : Nat -> Omega -> State) (hT : 0 < T) (hdelta : 0 < delta) (hgap_pos : 0 < meanGap trueMean best chosen) (hlog_pos : 0 < Real.log (textbookDeltaScale (Arm

Identity measurable policy on an action space.

def identityActionPolicy (Action : Type) [MeasurableSpace Action] : Policy.MeasurablePolicy Action Action where

State process whose value is the current concrete UCB score-argmax action. This is a thin policy/state adapter: a generated trace using `identityActionPolicy` over this state is definitionally the concrete score-argmax action trace.

noncomputable def confidenceScoreArgmaxGeneratedState {Omega : Type} {K : Nat} (hK : 0 < K) (empiricalMean : Omega -> Nat -> Fin K -> Real) (proxy : Nat -> Fin K -> NNReal) (T : Nat) (delta : Real) : Nat -> Omega -> Fin K

Concrete UCB score-argmax action trace expressed as a generated policy trace.

noncomputable def confidenceScoreArgmaxGeneratedTrace {Omega : Type} {K : Nat} (hK : 0 < K) [MeasurableSpace (Fin K)] (empiricalMean : Omega -> Nat -> Fin K -> Real) (proxy : Nat -> Fin K -> NNReal) (T : Nat) (delta : Real) : Omega -> ActionTrace (Fin K)

Generated-trace instantiation of the textbook-radius UCB pull-count budget. The generated trace is built from the identity action policy and the concrete score-argmax state, so the generated-policy equality contract from the previous wrapper is discharged definitionally.

theorem lintegral_confidenceScoreArgmaxGeneratedTrace_pullCount_le_textbookDeltaRadiusSampleCountSource_add_horizon_delta {Omega : Type} [MeasurableSpace Omega] {K : Nat} (hK : 0 < K) [MeasurableSpace (Fin K)] [MeasurableSingletonClass (Fin K)] [MeasurableSpace Nat] [MeasurableAdd₂ Nat] [OpensMeasurableSpace Nat] (mu : Measure Omega) [MeasureTheory.IsProbabilityMeasure mu] (trueMean : Fin K -> Real) (empiricalMean : Omega -> Nat -> Fin K -> Real) (proxy : Nat -> Fin K -> NNReal) (T : Nat) (delta : Real) (B : Nat) (best chosen : Fin K) (varianceProxy : NNReal) (hT : 0 < T) (hdelta : 0 < delta) (hgap_pos : 0 < meanGap trueMean best chosen) (hlog_pos : 0 < Real.log (textbookDeltaScale (Arm

Two-sided sub-Gaussian tail budget for a UCB empirical mean at time `t` and arm `arm`. The proxy is for the centered variable `empiricalMean t arm - trueMean arm`. This is still abstract: a later empirical-mean construction must prove the sub-Gaussian proxy and choose the usual log/sqrt radius.

noncomputable def subGaussianAbsDeviationTail {Arm : Type} (radius : Nat -> Arm -> Real) (proxy : Nat -> Arm -> NNReal) (t : Nat) (arm : Arm) : ENNReal

Single-time two-sided sub-Gaussian tail for the UCB absolute-deviation event.

theorem measure_absDeviation_le_subGaussian_tail {Omega Arm : Type} [MeasurableSpace Omega] (mu : Measure Omega) [IsFiniteMeasure mu] (trueMean : Arm -> Real) (empiricalMean : Omega -> Nat -> Arm -> Real) (radius : Nat -> Arm -> Real) (proxy : Nat -> Arm -> NNReal) (t : Nat) (arm : Arm) (hradius : 0 <= radius t arm) (hsubG : ProbabilityTheory.HasSubgaussianMGF (fun omega : Omega => empiricalMean omega t arm - trueMean arm) (proxy t arm) mu) : mu {omega | radius t arm <= |empiricalMean omega t arm - trueMean arm|} <= subGaussianAbsDeviationTail radius proxy t arm

Finite-horizon UCB confidence bad-event bound from abstract sub-Gaussian absolute-deviation tails. This is the UCB-facing sub-Gaussian producer layer. It still leaves empirical mean construction, proxy simplification, log/sqrt radius choice, pull-count bounds, and final regret to later leaves.

theorem measure_finiteHorizonConfidenceBadEvent_le_subGaussian_tail_sum {Omega Arm : Type} [MeasurableSpace Omega] [Fintype Arm] (mu : Measure Omega) [IsFiniteMeasure mu] (trueMean : Arm -> Real) (empiricalMean : Omega -> Nat -> Arm -> Real) (radius : Nat -> Arm -> Real) (proxy : Nat -> Arm -> NNReal) (T : Nat) (hradius : forall t arm, t < T -> 0 <= radius t arm) (hsubG : forall t arm, t < T -> ProbabilityTheory.HasSubgaussianMGF (fun omega : Omega => empiricalMean omega t arm - trueMean arm) (proxy t arm) mu) : mu (finiteHorizonConfidenceBadEvent trueMean empiricalMean radius T) <= (Finset.range T).sum (fun t => (Finset.univ : Finset Arm).sum (fun arm => subGaussianAbsDeviationTail radius proxy t arm + subGaussianAbsDeviationTail radius proxy t arm))

The proof-DAG leaves usually needed for UCB regret formalization.

def obligationNames : List String