BanditRLProof.TsallisFTRLMinimizerMeasurability

The canonical project minimizer, restricted to the explicit finite arm subtype and parameterized by a score vector on that subtype.

noncomputable def restrictedHalfTsallisMinimizer {Action : Type u} [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Real) (score : ↥arms -> Real) : ↥arms -> Real

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

theorem restrictedHalfTsallisMinimizer_mem_stdSimplex {Action : Type u} [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Real) (score : ↥arms -> Real) : restrictedHalfTsallisMinimizer arms harms eta score ∈ stdSimplex Real ↥arms

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

theorem restrictedHalfTsallisMinimizer_isMinOn {Action : Type u} [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Real) (score : ↥arms -> Real) : IsMinOn (fun weights : ↥arms -> Real => FTRL.regularizedObjective arms.attach eta (negEntropyRegularizer arms.attach (1 / 2 : Real)) score weights) (stdSimplex Real ↥arms) (restrictedHalfTsallisMinimizer arms harms eta score)

The restricted half-Tsallis objective is jointly continuous in the finite score vector and simplex vector.

theorem continuous_regularizedObjective_half_restricted_joint {Action : Type u} [DecidableEq Action] (arms : Finset Action) (eta : Real) : Continuous (fun pair : (↥arms -> Real) × (↥arms -> Real) => FTRL.regularizedObjective arms.attach eta (negEntropyRegularizer arms.attach (1 / 2 : Real)) pair.1 pair.2)

The finite-coordinate canonical half-Tsallis minimizer is continuous in the finite score vector.

theorem continuous_restrictedHalfTsallisMinimizer {Action : Type u} [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Real) : Continuous (restrictedHalfTsallisMinimizer arms harms eta)

Changing score coordinates outside the explicit arm set does not change the canonical half-Tsallis minimizer on supported coordinates.

theorem halfTsallisMinimizer_eq_on_arms_of_score_eq {Action : Type u} [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Real) (score₁ score₂ : Action -> Real) (hscore : forall action, action ∈ arms -> score₁ action = score₂ action) : forall action, action ∈ arms -> halfTsallisMinimizer arms harms eta score₁ action = halfTsallisMinimizer arms harms eta score₂ action

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

theorem restrictedHalfTsallisMinimizer_restrict_score_apply {Action : Type u} [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Real) (score : Action -> Real) (action : ↥arms) : restrictedHalfTsallisMinimizer arms harms eta (Finset.restrict arms score) action = halfTsallisMinimizer arms harms eta score action

Coordinatewise measurability of supported scores implies coordinatewise measurability of the existing canonical project minimizer.

theorem measurable_halfTsallisMinimizer_comp {Omega : Type*} {Action : Type u} [MeasurableSpace Omega] [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Real) (score : Omega -> Action -> Real) (hscore : forall action, action ∈ arms -> Measurable (fun omega => score omega action)) (action : Action) (haction : action ∈ arms) : Measurable (fun omega => halfTsallisMinimizer arms harms eta (score omega) action)