BanditRLProof.TsallisFiniteArmIndependentMeanSwitchCountDynamicRegret

A bounded probability reward law has its population mean in the unit interval.

theorem finiteArmIndependentRewardMean_mem_Icc {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) : finiteArmIndependentRewardMean armLaw t arm ∈ Set.Icc (0 : Real) 1

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

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

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

theorem finiteArmIndependentCumulativeMeanSwitchCount_zero {K : Nat} (armLaw : Nat -> Fin K -> Measure Rat) (arm : Fin K) : finiteArmIndependentCumulativeMeanSwitchCount armLaw 0 arm = 0

The real-valued switch count is exactly the coercion of the filtered cardinality of nonzero consecutive population-mean changes.

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

Unit-supported reward laws make every nonzero population-mean jump at most one, so cumulative mean path variation is bounded by switch count.

theorem finiteArmIndependentCumulativeMeanPathVariation_le_switchCount {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 <= finiteArmIndependentCumulativeMeanSwitchCount armLaw t arm

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

theorem abs_finiteArmIndependentRewardMean_sub_model_le_switchCount {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)| <= finiteArmIndependentCumulativeMeanSwitchCount armLaw t arm

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

noncomputable def finiteArmIndependentMeanSwitchCountDynamicAllRegimeBound {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 finiteArmIndependentMeanSwitchCountDynamicAllRegimeBound_fin_one (model : FiniteBanditModel 1) (armLaw : Nat -> Fin 1 -> Measure Rat) (horizon : Nat) : finiteArmIndependentMeanSwitchCountDynamicAllRegimeBound model armLaw horizon = 1 + Real.log (((horizon + 1 : Nat) : Real))

Generated expected predictable-environment dynamic regret with the all-time deviation envelope derived from armwise population-mean switch counts. No caller supplies a comparator, variation family, or switch budget. This is an exact prefix-envelope specialization, not a minimax change-point or horizon-compressed standard nonstationary rate.

theorem integral_sampledScheduledHalfTsallisFiniteArmIndependentMeanSwitchCountDynamicRegret_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)