BanditRLProof.TsallisFiniteArmIndependentGlobalMeanSwitchCountDynamicRegret

Real-valued prefix count of rounds before `t` at which at least one arm's population mean changes.

noncomputable def finiteArmIndependentCumulativeGlobalMeanSwitchCount {K : Nat} (armLaw : Nat -> Fin K -> Measure Rat) (t : Nat) : Real

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

theorem finiteArmIndependentCumulativeGlobalMeanSwitchCount_zero {K : Nat} (armLaw : Nat -> Fin K -> Measure Rat) : finiteArmIndependentCumulativeGlobalMeanSwitchCount armLaw 0 = 0

The global real-valued count is the coercion of the filtered cardinality of rounds with at least one population-mean change.

theorem finiteArmIndependentCumulativeGlobalMeanSwitchCount_eq_card {K : Nat} (armLaw : Nat -> Fin K -> Measure Rat) (t : Nat) : finiteArmIndependentCumulativeGlobalMeanSwitchCount armLaw t = ((((Finset.range t).filter (fun s => ∃ arm : Fin K, finiteArmIndependentRewardMean armLaw (s + 1) arm ≠ finiteArmIndependentRewardMean armLaw s arm)).card : Nat) : Real)

Every armwise prefix switch count is bounded by the global count.

theorem finiteArmIndependentCumulativeMeanSwitchCount_le_globalMeanSwitchCount {K : Nat} (armLaw : Nat -> Fin K -> Measure Rat) (t : Nat) (arm : Fin K) : finiteArmIndependentCumulativeMeanSwitchCount armLaw t arm <= finiteArmIndependentCumulativeGlobalMeanSwitchCount armLaw t

Unit-supported cumulative path variation of any arm is bounded by the single global population-mean switch count.

theorem finiteArmIndependentCumulativeMeanPathVariation_le_globalMeanSwitchCount {K : Nat} (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) (t : Nat) (arm : Fin K) : finiteArmIndependentCumulativeMeanPathVariation armLaw t arm <= finiteArmIndependentCumulativeGlobalMeanSwitchCount armLaw t

Initial model matching turns the global prefix switch count into the all-time deviation envelope required by the dynamic-regret theorem.

theorem abs_finiteArmIndependentRewardMean_sub_model_le_globalMeanSwitchCount {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) (hinitialMean : forall arm, finiteArmIndependentRewardMean armLaw 0 arm = ((model.mean arm : Rat) : Real)) (t : Nat) (arm : Fin K) : |finiteArmIndependentRewardMean armLaw t arm - ((model.mean arm : Rat) : Real)| <= finiteArmIndependentCumulativeGlobalMeanSwitchCount armLaw t

Dynamic all-regimes bound specialized to the exact global prefix population-mean switch count.

noncomputable def finiteArmIndependentGlobalMeanSwitchCountDynamicAllRegimeBound {K : Nat} (model : FiniteBanditModel K) (armLaw : Nat -> Fin K -> Measure Rat) (horizon : Nat) : Real

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

theorem finiteArmIndependentGlobalMeanSwitchCountDynamicAllRegimeBound_fin_one (model : FiniteBanditModel 1) (armLaw : Nat -> Fin 1 -> Measure Rat) (horizon : Nat) : finiteArmIndependentGlobalMeanSwitchCountDynamicAllRegimeBound model armLaw horizon = 1 + Real.log (((horizon + 1 : Nat) : Real))

Generated expected predictable-environment dynamic regret with the all-time deviation envelope derived from one global prefix count of population-mean change-points. No caller supplies a comparator, variation family, armwise switch budget, or global switch budget. This is not a minimax or horizon-compressed switch-rate theorem.

theorem integral_sampledScheduledHalfTsallisFiniteArmIndependentGlobalMeanSwitchCountDynamicRegret_le_allRegimes {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) (hinitialMean : forall arm, finiteArmIndependentRewardMean armLaw 0 arm = ((model.mean arm : Rat) : Real)) (hgapPos : forall arm, arm ≠ model.bestArm -> 0 < ((model.gap arm : Rat) : Real)) (hgapLeOne : forall arm, arm ≠ model.bestArm -> ((model.gap arm : Rat) : Real) <= 1) (horizon : Nat) : letI : Nonempty (Fin K)