Lean module · Tsallis-FTRL
BanditRLProof.TsallisFTRLMinimizerMeasurability
# Measurability of the canonical half-Tsallis minimizer The project minimizer is chosen noncomputably on the ambient action space, but the objective only sees the explicit finite arm set. We restrict the selected minimizer to that finite subtype and prove continuity in the restricted score vector. Compactness supplies cluster points and strict convexity identifies every cluster point with the unique minimizer.
Module map
Imports
BanditRLProof.TsallisFTRLMinimizerUniqueness
Imported by
BanditRLProof, BanditRLProof.TsallisFTRLGeneratedMeasurability
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
def
BanditRLProof.Tsallis.restrictedHalfTsallisMinimizer
Compiled
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
theorem
BanditRLProof.Tsallis.restrictedHalfTsallisMinimizer_mem_stdSimplex
Compiled
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
theorem
BanditRLProof.Tsallis.restrictedHalfTsallisMinimizer_isMinOn
Compiled
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)
theorem
BanditRLProof.Tsallis.continuous_regularizedObjective_half_restricted_joint
Compiled
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)
theorem
BanditRLProof.Tsallis.continuous_restrictedHalfTsallisMinimizer
Compiled
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)
theorem
BanditRLProof.Tsallis.halfTsallisMinimizer_eq_on_arms_of_score_eq
Compiled
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
theorem
BanditRLProof.Tsallis.restrictedHalfTsallisMinimizer_restrict_score_apply
Compiled
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
theorem
BanditRLProof.Tsallis.measurable_halfTsallisMinimizer_comp
Compiled
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)