BanditRLProof.TsallisFTRLRecursiveTrajectory

Reusable regularity boundary for the noncomputable half-Tsallis selector. It asks only that measurable finite-history score coordinates produce measurable selected probability coordinates.

structure HalfTsallisFiniteHistorySelectorMeasurability {Action : Type u} [MeasurableSpace Action] [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Real) : Prop where

Initial pure half-Tsallis law, before any observed pair.

noncomputable def initialHalfTsallisDistribution {Action : Type u} [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Real) : Action -> Real

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

theorem finiteActionDistribution_initialHalfTsallisDistribution {Action : Type u} [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Real) : Exp3.FiniteActionDistribution arms (initialHalfTsallisDistribution arms harms eta)

Cumulative importance-weighted score through an inclusive observed pair history, using the pure half-Tsallis law generated by the previous score.

noncomputable def sampledHalfTsallisHistoryScore {Action : Type u} [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Real) : (n : Nat) -> History.FinitePairHistory Action Real n -> Action -> Real | 0, history, action => Exp3.importanceWeightedLoss (initialHalfTsallisDistribution arms harms eta) (fun _ => (history ⟨0, Finset.mem_Iic.mpr le_rfl⟩).2) (history ⟨0, Finset.mem_Iic.mpr le_rfl⟩).1 action | n + 1, history, action => let previous := Exp3.previousPairHistory history sampledHalfTsallisHistoryScore arms harms eta n previous action + Exp3.importanceWeightedLoss (halfTsallisMinimizer arms harms eta (sampledHalfTsallisHistoryScore arms harms eta n previous)) (fun _ => (history ⟨n + 1, Finset.mem_Iic.mpr le_rfl⟩).2) (history ⟨n + 1, Finset.mem_Iic.mpr le_rfl⟩).1 action @[simp] theorem sampledHalfTsallisHistoryScore_zero {Action : Type u} [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Real) (history : History.FinitePairHistory Action Real 0) (action : Action) : sampledHalfTsallisHistoryScore arms harms eta 0 history action = Exp3.importanceWeightedLoss (initialHalfTsallisDistribution arms harms eta) (fun _ => (history ⟨0, Finset.mem_Iic.mpr le_rfl⟩).2) (history ⟨0, Finset.mem_Iic.mpr le_rfl⟩).1 action

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

theorem sampledHalfTsallisHistoryScore_zero {Action : Type u} [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Real) (history : History.FinitePairHistory Action Real 0) (action : Action) : sampledHalfTsallisHistoryScore arms harms eta 0 history action = Exp3.importanceWeightedLoss (initialHalfTsallisDistribution arms harms eta) (fun _ => (history ⟨0, Finset.mem_Iic.mpr le_rfl⟩).2) (history ⟨0, Finset.mem_Iic.mpr le_rfl⟩).1 action

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

theorem sampledHalfTsallisHistoryScore_succ {Action : Type u} [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Real) (n : Nat) (history : History.FinitePairHistory Action Real (n + 1)) (action : Action) : sampledHalfTsallisHistoryScore arms harms eta (n + 1) history action = sampledHalfTsallisHistoryScore arms harms eta n (Exp3.previousPairHistory history) action + Exp3.importanceWeightedLoss (halfTsallisMinimizer arms harms eta (sampledHalfTsallisHistoryScore arms harms eta n (Exp3.previousPairHistory history))) (fun _ => (history ⟨n + 1, Finset.mem_Iic.mpr le_rfl⟩).2) (history ⟨n + 1, Finset.mem_Iic.mpr le_rfl⟩).1 action

The generic selector contract makes the recursively accumulated score measurable at every supported action coordinate.

theorem measurable_sampledHalfTsallisHistoryScore {Action : Type u} [MeasurableSpace Action] [MeasurableSingletonClass Action] [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Real) (selector : HalfTsallisFiniteHistorySelectorMeasurability arms harms eta) : forall n action, action ∈ arms -> Measurable (fun history : History.FinitePairHistory Action Real n => sampledHalfTsallisHistoryScore arms harms eta n history action)

Pure half-Tsallis probabilities generated by the sampled score.

noncomputable def sampledHalfTsallisHistoryDistribution {Action : Type u} [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Real) (n : Nat) : History.FinitePairHistory Action Real n -> Action -> Real

Measurable finite-action source for the recursively generated policy.

noncomputable def sampledHalfTsallisHistoryDistributionSource {Action : Type u} [MeasurableSpace Action] [MeasurableSingletonClass Action] [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Real) (selector : HalfTsallisFiniteHistorySelectorMeasurability arms harms eta) (n : Nat) : Exp3.MeasurableFiniteActionDistribution arms (sampledHalfTsallisHistoryDistribution arms harms eta n)

Stochastic finite-history algorithm generated by the recursive pure half-Tsallis score.

noncomputable def sampledHalfTsallisHistoryAlgorithm {Action : Type u} [MeasurableSpace Action] [MeasurableSingletonClass Action] [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Real) (selector : HalfTsallisFiniteHistorySelectorMeasurability arms harms eta) : Thompson.HistoryAlgorithm Action Real where

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

theorem sampledHalfTsallisHistoryAlgorithm_policy {Action : Type u} [MeasurableSpace Action] [MeasurableSingletonClass Action] [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Real) (selector : HalfTsallisFiniteHistorySelectorMeasurability arms harms eta) (n : Nat) : (sampledHalfTsallisHistoryAlgorithm arms harms eta selector).policy n = Exp3.finiteActionKernel arms (sampledHalfTsallisHistoryDistribution arms harms eta n) (sampledHalfTsallisHistoryDistributionSource arms harms eta selector n)

Complete environment-indexed recursive pure half-Tsallis trajectory.

noncomputable def sampledHalfTsallisTrajectoryKernel {Env : Type v} {Action : Type u} [MeasurableSpace Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [DecidableEq Action] [Nonempty Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Real) (selector : HalfTsallisFiniteHistorySelectorMeasurability arms harms eta) (environment : Thompson.MeasurableHistoryEnvironment Env Action Real) : Kernel Env ((n : Nat) -> Action × Real)

Every successor action has the recursive pure half-Tsallis finite-action law conditional on its visible pair-history prefix.

theorem sampledHalfTsallisTrajectoryMeasure_condDistrib_action {Env : Type v} {Action : Type u} [MeasurableSpace Env] [StandardBorelSpace Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [StandardBorelSpace Action] [Nonempty Action] [DecidableEq Action] (prior : Measure Env) [IsFiniteMeasure prior] (arms : Finset Action) (harms : arms.Nonempty) (eta : Real) (selector : HalfTsallisFiniteHistorySelectorMeasurability arms harms eta) (environment : Thompson.MeasurableHistoryEnvironment Env Action Real) (n : Nat) : condDistrib (fun sample : Env × ((k : Nat) -> Action × Real) => (sample.2 (n + 1)).1) (fun sample => Preorder.frestrictLe n sample.2) (prior ⊗ₘ sampledHalfTsallisTrajectoryKernel arms harms eta selector environment) =ᵐ[ (prior ⊗ₘ sampledHalfTsallisTrajectoryKernel arms harms eta selector environment).map (fun sample => Preorder.frestrictLe n sample.2)] Exp3.finiteActionKernel arms (sampledHalfTsallisHistoryDistribution arms harms eta n) (sampledHalfTsallisHistoryDistributionSource arms harms eta selector n)

The same conditional law after retaining the environment in the visible history. The policy kernel is comapped along the pair-history projection.

theorem sampledHalfTsallisTrajectoryMeasure_condDistrib_action_given_environment {Env : Type v} {Action : Type u} [MeasurableSpace Env] [StandardBorelSpace Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [StandardBorelSpace Action] [Nonempty Action] [DecidableEq Action] (prior : Measure Env) [IsFiniteMeasure prior] (arms : Finset Action) (harms : arms.Nonempty) (eta : Real) (selector : HalfTsallisFiniteHistorySelectorMeasurability arms harms eta) (environment : Thompson.MeasurableHistoryEnvironment Env Action Real) (n : Nat) : condDistrib (fun sample : Env × ((k : Nat) -> Action × Real) => (sample.2 (n + 1)).1) (fun sample : Env × ((k : Nat) -> Action × Real) => (sample.1, Preorder.frestrictLe n sample.2)) (prior ⊗ₘ sampledHalfTsallisTrajectoryKernel arms harms eta selector environment) =ᵐ[ (prior ⊗ₘ sampledHalfTsallisTrajectoryKernel arms harms eta selector environment).map (fun sample : Env × ((k : Nat) -> Action × Real) => (sample.1, Preorder.frestrictLe n sample.2))] (Exp3.finiteActionKernel arms (sampledHalfTsallisHistoryDistribution arms harms eta n) (sampledHalfTsallisHistoryDistributionSource arms harms eta selector n)).comap (fun input : Env × History.FinitePairHistory Action Real n => input.2) (measurable_snd : Measurable (fun input : Env × History.FinitePairHistory Action Real n => input.2))

Visible environment/pair-history state before successor action `n + 1`.

def sampledHalfTsallisHistoryAt {Env : Type v} {Action : Type u} (n : Nat) (sample : Env × ((k : Nat) -> Action × Real)) : Env × History.FinitePairHistory Action Real n

Successor action sampled after the visible prefix through `n`.

def sampledHalfTsallisActionAt {Env : Type v} {Action : Type u} (n : Nat) (sample : Env × ((k : Nat) -> Action × Real)) : Action

Recursive half-Tsallis score on an environment/prefix state.

noncomputable def sampledHalfTsallisScoreAt {Env : Type v} {Action : Type u} [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Real) (n : Nat) : Env × History.FinitePairHistory Action Real n -> Action -> Real

Predictable successor loss vector on an environment/prefix state.

def sampledHalfTsallisPredictableLossAt {Env : Type v} {Action : Type u} [MeasurableSpace Env] [MeasurableSpace Action] (loss : Exp3.PredictableLossVector Env Action) (n : Nat) : Env × History.FinitePairHistory Action Real n -> Action -> Real

Pure half-Tsallis probability on an environment/prefix state.

noncomputable def sampledHalfTsallisProbabilityAt {Env : Type v} {Action : Type u} [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Real) (n : Nat) : Env × History.FinitePairHistory Action Real n -> Action -> Real

Canonical sampled-action update on an environment/prefix state.

noncomputable def sampledHalfTsallisUpdatedAt {Env : Type v} {Action : Type u} [MeasurableSpace Env] [MeasurableSpace Action] [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Real) (loss : Exp3.PredictableLossVector Env Action) (n : Nat) : Env × History.FinitePairHistory Action Real n -> Action -> Action -> Real

The one-round stability score on visible history/action pairs.

noncomputable def sampledHalfTsallisHistoryActionStabilityAt {Env : Type v} {Action : Type u} [MeasurableSpace Env] [MeasurableSpace Action] [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Real) (loss : Exp3.PredictableLossVector Env Action) (n : Nat) : (Env × History.FinitePairHistory Action Real n) × Action -> Real

The roundwise half-power budget on a visible history.

noncomputable def sampledHalfTsallisHalfPowerBoundAt {Env : Type v} {Action : Type u} [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Real) (n : Nat) : Env × History.FinitePairHistory Action Real n -> Real

The actual displayed stability term with the next generated prefix's current selector, rather than the sampled-action update notation.

noncomputable def sampledHalfTsallisSuccessorStabilityAt {Env : Type v} {Action : Type u} [MeasurableSpace Env] [MeasurableSpace Action] [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Real) (loss : Exp3.PredictableLossVector Env Action) (n : Nat) (sample : Env × ((k : Nat) -> Action × Real)) : Real

Environment-lifted measurable probability source at one prefix level.

noncomputable def sampledHalfTsallisEnvironmentHistoryDistributionSource {Env : Type v} {Action : Type u} [MeasurableSpace Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Real) (selector : HalfTsallisFiniteHistorySelectorMeasurability arms harms eta) (n : Nat) : Exp3.MeasurableFiniteActionDistribution arms (sampledHalfTsallisProbabilityAt (Env := Env) arms harms eta n)

Algorithm policy comapped to the environment/prefix state.

noncomputable def sampledHalfTsallisPolicyAt {Env : Type v} {Action : Type u} [MeasurableSpace Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Real) (selector : HalfTsallisFiniteHistorySelectorMeasurability arms harms eta) (n : Nat) : Kernel (Env × History.FinitePairHistory Action Real n) Action

The recursive score on generated prefixes follows the predictable importance-weighted update almost surely.

theorem sampledHalfTsallisScoreAt_succ_ae {Env : Type v} {Action : Type u} [MeasurableSpace Env] [StandardBorelSpace Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [StandardBorelSpace Action] [Nonempty Action] [DecidableEq Action] (prior : Measure Env) [IsFiniteMeasure prior] (arms : Finset Action) (harms : arms.Nonempty) (eta : Real) (selector : HalfTsallisFiniteHistorySelectorMeasurability arms harms eta) (loss : Exp3.PredictableLossVector Env Action) (n : Nat) : let mu := prior ⊗ₘ sampledHalfTsallisTrajectoryKernel arms harms eta selector loss.environment (fun sample => sampledHalfTsallisHistoryScore arms harms eta (n + 1) (Preorder.frestrictLe (n + 1) sample.2)) =ᵐ[mu] (fun sample candidate => sampledHalfTsallisHistoryScore arms harms eta n (Preorder.frestrictLe n sample.2) candidate + Exp3.importanceWeightedLoss (sampledHalfTsallisHistoryDistribution arms harms eta n (Preorder.frestrictLe n sample.2)) (loss.successor n sample.1 (Preorder.frestrictLe n sample.2)) (sample.2 (n + 1)).1 candidate)

Generated predictable-trajectory finite-horizon half-Tsallis stability. The trajectory construction discharges the policy-kernel, conditional-law, and successor-score-recursion obligations. The remaining explicit inputs are the canonical selector measurability contract and regularity of the updated stability score under each generated history/action product law.

theorem integral_sum_sampledHalfTsallisSuccessorStability_le_integral_sum_halfPowerStabilityBound {Env : Type v} {Action : Type u} [MeasurableSpace Env] [StandardBorelSpace Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [StandardBorelSpace Action] [Nonempty Action] [DecidableEq Action] (prior : Measure Env) [IsFiniteMeasure prior] (horizon : Nat) (arms : Finset Action) (harms : arms.Nonempty) (eta : Real) (heta : 0 < eta) (selector : HalfTsallisFiniteHistorySelectorMeasurability arms harms eta) (loss : Exp3.PredictableLossVector Env Action) (hscore : forall n, Measurable (sampledHalfTsallisHistoryActionStabilityAt arms harms eta loss n)) (hIntegrable : forall n, Integrable (sampledHalfTsallisHistoryActionStabilityAt arms harms eta loss n) ((prior ⊗ₘ sampledHalfTsallisTrajectoryKernel arms harms eta selector loss.environment).map (sampledHalfTsallisHistoryAt n) ⊗ₘ sampledHalfTsallisPolicyAt (Env := Env) arms harms eta selector n)) (hboundIntegrable : forall n, Integrable (sampledHalfTsallisHalfPowerBoundAt (Env := Env) arms harms eta n) ((prior ⊗ₘ sampledHalfTsallisTrajectoryKernel arms harms eta selector loss.environment).map (sampledHalfTsallisHistoryAt n))) : let mu := prior ⊗ₘ sampledHalfTsallisTrajectoryKernel arms harms eta selector loss.environment integral mu (fun sample => (Finset.range horizon).sum (fun n => sampledHalfTsallisSuccessorStabilityAt arms harms eta loss n sample)) <= integral mu (fun sample => (Finset.range horizon).sum (fun n => sampledHalfTsallisHalfPowerBoundAt (Env := Env) arms harms eta n (sampledHalfTsallisHistoryAt n sample)))