BanditRLProof.TsallisFiniteArmIIDRewardLaw

Pointwise projection of a rational reward into the real unit interval.

noncomputable def clippedUnitReward (reward : Rat) : Real

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

theorem clippedUnitReward_nonneg (reward : Rat) : 0 <= clippedUnitReward reward

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

theorem clippedUnitReward_le_one (reward : Rat) : clippedUnitReward reward <= 1

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

theorem clippedUnitReward_eq_of_mem_Icc (reward : Rat) (hreward : ((reward : Rat) : Real) ∈ Set.Icc (0 : Real) 1) : clippedUnitReward reward = ((reward : Rat) : Real)

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

theorem measurable_clippedUnitReward : Measurable clippedUnitReward

The independent one-round reward vector induced by one law per arm.

noncomputable def finiteArmIIDRewardVectorLaw {K : Nat} (armLaw : Fin K -> Measure Rat) : Measure (Fin K -> Rat)

Convert a sampled reward vector into the selected arm's clipped loss.

noncomputable def finiteArmIIDRewardVectorLoss {K : Nat} (state : Fin K -> Rat) (arm : Fin K) : Real

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

theorem measurable_finiteArmIIDRewardVectorLoss {K : Nat} : Measurable (fun input : (Fin K -> Rat) × Fin K => finiteArmIIDRewardVectorLoss input.1 input.2)

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

theorem finiteArmIIDRewardVectorLoss_nonneg {K : Nat} (state : Fin K -> Rat) (arm : Fin K) : 0 <= finiteArmIIDRewardVectorLoss state arm

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

theorem finiteArmIIDRewardVectorLoss_le_one {K : Nat} (state : Fin K -> Rat) (arm : Fin K) : finiteArmIIDRewardVectorLoss state arm <= 1

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

theorem integrable_clippedUnitReward (mu : Measure Rat) [IsFiniteMeasure mu] : Integrable clippedUnitReward mu

Under an almost-sure unit-interval contract, the product-coordinate clipped reward has exactly the supplied finite-bandit mean.

theorem integral_finiteArmIIDRewardVectorLaw_clippedUnitReward_eq_mean {K : Nat} (model : FiniteBanditModel K) (armLaw : Fin K -> Measure Rat) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) (hbound : forall arm, ∀ᵐ reward ∂armLaw arm, ((reward : Rat) : Real) ∈ Set.Icc (0 : Real) 1) (hmean : forall arm, integral (armLaw arm) (fun reward : Rat => ((reward : Rat) : Real)) = ((model.mean arm : Rat) : Real)) (arm : Fin K) : integral (finiteArmIIDRewardVectorLaw armLaw) (fun state => clippedUnitReward (state arm)) = ((model.mean arm : Rat) : Real)

The one-round IID loss-state mean gap is exactly the rational finite-bandit model gap after coercion to the reals.

theorem iidLossStateMeanGap_finiteArmIIDRewardVectorLoss_eq_gap {K : Nat} (model : FiniteBanditModel K) (armLaw : Fin K -> Measure Rat) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) (hbound : forall arm, ∀ᵐ reward ∂armLaw arm, ((reward : Rat) : Real) ∈ Set.Icc (0 : Real) 1) (hmean : forall arm, integral (armLaw arm) (fun reward : Rat => ((reward : Rat) : Real)) = ((model.mean arm : Rat) : Real)) (arm : Fin K) : iidLossStateMeanGap (finiteArmIIDRewardVectorLaw armLaw) finiteArmIIDRewardVectorLoss model.bestArm arm = ((model.gap arm : Rat) : Real)

A finite collection of bounded rational reward laws supplies the concrete IID stochastic model for the generated scheduled half-Tsallis logarithmic regret theorem. The latent one-round law is the independent product of arm laws, while the observed feedback is the selected clipped loss.

theorem integral_sampledScheduledHalfTsallisFiniteArmIIDRewardLawRegret_le_log {K : Nat} (model : FiniteBanditModel K) (armLaw : Fin K -> Measure Rat) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) (hbound : forall arm, ∀ᵐ reward ∂armLaw arm, ((reward : Rat) : Real) ∈ Set.Icc (0 : Real) 1) (hmean : forall arm, integral (armLaw 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)