Lean module · Tsallis-FTRL
BanditRLProof.TsallisFiniteArmIndependentRewardLaw
# Finite-arm independent nonidentical reward laws for scheduled half-Tsallis Each round may use a different probability law for every arm, while all roundwise arm laws retain the means of one fixed finite-bandit model. The roundwise product reward vectors are independent across time but need not be identically distributed.
Module map
Imports
BanditRLProof.TsallisFiniteArmIIDRewardLaw, BanditRLProof.TsallisScheduledIIDTimeVaryingMeanGap, BanditRLProof.TsallisScheduledIndependentMeanGap
Imported by
BanditRLProof, BanditRLProof.TsallisFiniteArmIndependentDriftingMeanRewardLaw
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
def
BanditRLProof.Tsallis.finiteArmIndependentRewardVectorLaw
Compiled
The independent finite-arm reward-vector law used at round `t`.
noncomputable def finiteArmIndependentRewardVectorLaw {K : Nat} (armLaw : Nat -> Fin K -> Measure Rat) (t : Nat) : Measure (Fin K -> Rat)
theorem
BanditRLProof.Tsallis.independentLossStateTimeVaryingMeanGap_finiteArmIndependentRewardVectorLoss_eq_gap
Compiled
Every roundwise loss gap has the fixed finite-bandit model gap when the possibly time-varying arm laws preserve the model means.
theorem independentLossStateTimeVaryingMeanGap_finiteArmIndependentRewardVectorLoss_eq_gap {K : Nat} (model : FiniteBanditModel K) (armLaw : Nat -> Fin K -> Measure Rat) (hprob : forall t arm, IsProbabilityMeasure (armLaw t arm)) (hbound : forall t arm, ∀ᵐ reward ∂armLaw t arm, ((reward : Rat) : Real) ∈ Set.Icc (0 : Real) 1) (hmean : forall t arm, integral (armLaw t arm) (fun reward : Rat => ((reward : Rat) : Real)) = ((model.mean arm : Rat) : Real)) (t : Nat) (arm : Fin K) : independentLossStateTimeVaryingMeanGap (finiteArmIndependentRewardVectorLaw armLaw) (fun _ => finiteArmIIDRewardVectorLoss) t model.bestArm arm = ((model.gap arm : Rat) : Real)
theorem
BanditRLProof.Tsallis.hasScheduledIndependentMeanGapLaw_of_finiteArmIndependentRewardVectorLaw
Compiled
Independent roundwise product reward vectors with fixed arm means supply the fixed model-gap law required by the scheduled self-bounding route.
theorem hasScheduledIndependentMeanGapLaw_of_finiteArmIndependentRewardVectorLaw {K : Nat} (model : FiniteBanditModel K) (armLaw : Nat -> Fin K -> Measure Rat) (hprob : forall t arm, IsProbabilityMeasure (armLaw t arm)) (hbound : forall t arm, ∀ᵐ reward ∂armLaw t arm, ((reward : Rat) : Real) ∈ Set.Icc (0 : Real) 1) (hmean : forall t arm, integral (armLaw t arm) (fun reward : Rat => ((reward : Rat) : Real)) = ((model.mean arm : Rat) : Real)) (horizon : Nat) (trajectoryKernel : Kernel (Nat -> Fin K -> Rat) ((k : Nat) -> Fin K × Real)) [IsMarkovKernel trajectoryKernel] (hfactor : HasScheduledIIDPrefixKernelFactorization trajectoryKernel horizon) : let law := finiteArmIndependentRewardVectorLaw armLaw let value := fun _ : Nat => finiteArmIIDRewardVectorLoss let prior := Measure.infinitePi law let mu := prior ⊗ₘ trajectoryKernel HasScheduledIndependentMeanGapLaw mu (Finset.univ : Finset (Fin K)) (iidTimeVaryingLossStatePredictableLossVector value (fun _ => measurable_finiteArmIIDRewardVectorLoss) (fun _ => finiteArmIIDRewardVectorLoss_nonneg) (fun _ => finiteArmIIDRewardVectorLoss_le_one)) model.bestArm (fun arm => ((model.gap arm : Rat) : Real)) horizon
theorem
BanditRLProof.Tsallis.integral_sampledScheduledHalfTsallisFiniteArmIndependentRewardLawRegret_le_log
Compiled
A time-varying collection of bounded rational arm-reward laws with fixed finite-bandit means supplies a concrete independent, nonidentically distributed stochastic model for the generated scheduled half-Tsallis logarithmic regret theorem.
theorem integral_sampledScheduledHalfTsallisFiniteArmIndependentRewardLawRegret_le_log {K : Nat} (model : FiniteBanditModel K) (armLaw : Nat -> Fin K -> Measure Rat) (hprob : forall t arm, IsProbabilityMeasure (armLaw t arm)) (hbound : forall t arm, ∀ᵐ reward ∂armLaw t arm, ((reward : Rat) : Real) ∈ Set.Icc (0 : Real) 1) (hmean : forall t arm, integral (armLaw t arm) (fun reward : Rat => ((reward : Rat) : Real)) = ((model.mean arm : Rat) : Real)) (hgapPos : forall arm, arm ≠ model.bestArm -> 0 < ((model.gap arm : Rat) : Real)) (horizon : Nat) (corruption : Real) (hcorruption : 0 <= corruption) : letI : Nonempty (Fin K)