BanditRLProof.TsallisFiniteArmIndependentSingleSwitchComparatorObstruction

Baseline two-arm model used by the single-switch obstruction.

def finiteArmIndependentSingleSwitchObstructionModel : FiniteBanditModel 2 where

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

theorem finiteArmIndependentSingleSwitchObstructionModel_bestArm : finiteArmIndependentSingleSwitchObstructionModel.bestArm = 0

Arm zero stays at mean `1/2`; arm one moves from `1/4` at round zero to `3/4` forever after round zero.

noncomputable def finiteArmIndependentSingleSwitchObstructionLaw (t : Nat) (arm : Fin 2) : Measure Rat

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

theorem finiteArmIndependentSingleSwitchObstructionLaw_isProbabilityMeasure (t : Nat) (arm : Fin 2) : IsProbabilityMeasure (finiteArmIndependentSingleSwitchObstructionLaw t arm)

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

theorem finiteArmIndependentSingleSwitchObstructionLaw_mem_Icc_ae (t : Nat) (arm : Fin 2) : ∀ᵐ reward ∂finiteArmIndependentSingleSwitchObstructionLaw t arm, ((reward : Rat) : Real) ∈ Set.Icc (0 : Real) 1

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

theorem finiteArmIndependentSingleSwitchObstructionMean_zero (t : Nat) : finiteArmIndependentRewardMean finiteArmIndependentSingleSwitchObstructionLaw t 0 = 1 / 2

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

theorem finiteArmIndependentSingleSwitchObstructionMean_one_zero : finiteArmIndependentRewardMean finiteArmIndependentSingleSwitchObstructionLaw 0 1 = 1 / 4

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

theorem finiteArmIndependentSingleSwitchObstructionMean_one_succ (t : Nat) : finiteArmIndependentRewardMean finiteArmIndependentSingleSwitchObstructionLaw (t + 1) 1 = 3 / 4

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

theorem finiteArmIndependentSingleSwitchObstructionInitialMean (arm : Fin 2) : finiteArmIndependentRewardMean finiteArmIndependentSingleSwitchObstructionLaw 0 arm = ((finiteArmIndependentSingleSwitchObstructionModel.mean arm : Rat) : Real)

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

theorem finiteArmIndependentSingleSwitchObstructionGap_pos (arm : Fin 2) (harm : arm ≠ finiteArmIndependentSingleSwitchObstructionModel.bestArm) : 0 < ((finiteArmIndependentSingleSwitchObstructionModel.gap arm : Rat) : Real)

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

theorem finiteArmIndependentSingleSwitchObstructionGap_le_one (arm : Fin 2) (harm : arm ≠ finiteArmIndependentSingleSwitchObstructionModel.bestArm) : ((finiteArmIndependentSingleSwitchObstructionModel.gap arm : Rat) : Real) <= 1

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

theorem finiteArmIndependentSingleSwitchObstructionBestArmAt_zero : finiteArmIndependentBestArmAt finiteArmIndependentSingleSwitchObstructionModel finiteArmIndependentSingleSwitchObstructionLaw 0 = 0

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

theorem finiteArmIndependentSingleSwitchObstructionBestArmAt_succ (t : Nat) : finiteArmIndependentBestArmAt finiteArmIndependentSingleSwitchObstructionModel finiteArmIndependentSingleSwitchObstructionLaw (t + 1) = 1

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

private theorem finiteArmIndependentSingleSwitchObstructionIndicator (s : Nat) : (if ∃ arm : Fin 2, finiteArmIndependentRewardMean finiteArmIndependentSingleSwitchObstructionLaw (s + 1) arm ≠ finiteArmIndependentRewardMean finiteArmIndependentSingleSwitchObstructionLaw s arm then (1 : Real) else 0) = if s = 0 then 1 else 0

Every positive prefix contains exactly the one change at `0 -> 1`.

theorem finiteArmIndependentSingleSwitchObstructionGlobalCount_succ (t : Nat) : finiteArmIndependentCumulativeGlobalMeanSwitchCount finiteArmIndependentSingleSwitchObstructionLaw (t + 1) = 1

Exact actual-mean advantage charged by the moving-comparator decomposition on the single-switch law.

noncomputable def finiteArmIndependentSingleSwitchComparatorAdvantage (horizon : Nat) : Real

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

theorem finiteArmIndependentSingleSwitchComparatorAdvantage_zero : finiteArmIndependentSingleSwitchComparatorAdvantage 0 = 0

One permanent switch makes the exact comparator advantage equal to `horizon / 4`, despite the global switch count being one.

theorem finiteArmIndependentSingleSwitchComparatorAdvantage_eq (horizon : Nat) : finiteArmIndependentSingleSwitchComparatorAdvantage horizon = (horizon : Real) / 4

The current repeated-prefix envelope penalty is exactly `2 * horizon` on the same one-switch law.

theorem finiteArmIndependentSingleSwitchDynamicComparatorPenalty_eq (horizon : Nat) : finiteArmIndependentDynamicComparatorPenalty finiteArmIndependentSingleSwitchObstructionModel finiteArmIndependentSingleSwitchObstructionLaw horizon (fun t _ => finiteArmIndependentCumulativeGlobalMeanSwitchCount finiteArmIndependentSingleSwitchObstructionLaw t) = 2 * (horizon : Real)

For every natural coefficient, a one-switch horizon exists where the exact separately charged comparator advantage exceeds that coefficient times `sqrt(horizon)`. This rules out obtaining a uniform square-root switch-rate by bounding this term independently.

theorem finiteArmIndependentSingleSwitchComparatorAdvantage_gt_nat_mul_sqrt (coefficient : Nat) : let horizon := (4 * coefficient + 1) ^ 2 finiteArmIndependentCumulativeGlobalMeanSwitchCount finiteArmIndependentSingleSwitchObstructionLaw horizon = 1 ∧ (coefficient : Real) * Real.sqrt (horizon : Real) < finiteArmIndependentSingleSwitchComparatorAdvantage horizon

Compiled blocker certificate for the current dynamic-comparator proof route. It does not assert a regret lower bound: a sharper proof could exploit cancellation between fixed-comparator regret and comparator advantage.

theorem finiteArmIndependentSingleSwitchDynamicComparatorRouteObstruction (horizon : Nat) (horizon_pos : 0 < horizon) : finiteArmIndependentCumulativeGlobalMeanSwitchCount finiteArmIndependentSingleSwitchObstructionLaw horizon = 1 ∧ finiteArmIndependentSingleSwitchComparatorAdvantage horizon = (horizon : Real) / 4 ∧ finiteArmIndependentDynamicComparatorPenalty finiteArmIndependentSingleSwitchObstructionModel finiteArmIndependentSingleSwitchObstructionLaw horizon (fun t _ => finiteArmIndependentCumulativeGlobalMeanSwitchCount finiteArmIndependentSingleSwitchObstructionLaw t) = 2 * (horizon : Real)