BanditRLProof.TsallisScheduledRecursiveTrajectory

Roundwise selector regularity for a deterministic learning-rate schedule.

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

The canonical selected minimizer satisfies the scheduled regularity contract at every round.

noncomputable def canonicalHalfTsallisScheduleFiniteHistorySelectorMeasurability {Action : Type u} [MeasurableSpace Action] [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) : HalfTsallisScheduleFiniteHistorySelectorMeasurability arms harms eta where

Cumulative importance-weighted score through an inclusive history under the scheduled policies.

noncomputable def sampledScheduledHalfTsallisHistoryScore {Action : Type u} [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) : (n : Nat) -> History.FinitePairHistory Action Real n -> Action -> Real | 0, history, action => Exp3.importanceWeightedLoss (initialHalfTsallisDistribution arms harms (eta 0)) (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 sampledScheduledHalfTsallisHistoryScore arms harms eta n previous action + Exp3.importanceWeightedLoss (halfTsallisMinimizer arms harms (eta (n + 1)) (sampledScheduledHalfTsallisHistoryScore 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 sampledScheduledHalfTsallisHistoryScore_zero {Action : Type u} [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (history : History.FinitePairHistory Action Real 0) (action : Action) : sampledScheduledHalfTsallisHistoryScore arms harms eta 0 history action = Exp3.importanceWeightedLoss (initialHalfTsallisDistribution arms harms (eta 0)) (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 sampledScheduledHalfTsallisHistoryScore_zero {Action : Type u} [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (history : History.FinitePairHistory Action Real 0) (action : Action) : sampledScheduledHalfTsallisHistoryScore arms harms eta 0 history action = Exp3.importanceWeightedLoss (initialHalfTsallisDistribution arms harms (eta 0)) (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 sampledScheduledHalfTsallisHistoryScore_succ {Action : Type u} [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (n : Nat) (history : History.FinitePairHistory Action Real (n + 1)) (action : Action) : sampledScheduledHalfTsallisHistoryScore arms harms eta (n + 1) history action = sampledScheduledHalfTsallisHistoryScore arms harms eta n (Exp3.previousPairHistory history) action + Exp3.importanceWeightedLoss (halfTsallisMinimizer arms harms (eta (n + 1)) (sampledScheduledHalfTsallisHistoryScore 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

Scheduled selector regularity makes every supported score coordinate measurable.

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

Scheduled successor probabilities after the visible prefix through `n`.

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

Measurable finite-action source for one scheduled successor policy.

noncomputable def sampledScheduledHalfTsallisHistoryDistributionSource {Action : Type u} [MeasurableSpace Action] [MeasurableSingletonClass Action] [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (selector : HalfTsallisScheduleFiniteHistorySelectorMeasurability arms harms eta) (n : Nat) : Exp3.MeasurableFiniteActionDistribution arms (sampledScheduledHalfTsallisHistoryDistribution arms harms eta n)

Stochastic finite-history algorithm generated by the scheduled recursive score.

noncomputable def sampledScheduledHalfTsallisHistoryAlgorithm {Action : Type u} [MeasurableSpace Action] [MeasurableSingletonClass Action] [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (selector : HalfTsallisScheduleFiniteHistorySelectorMeasurability arms harms eta) : Thompson.HistoryAlgorithm Action Real where

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

theorem sampledScheduledHalfTsallisHistoryAlgorithm_policy {Action : Type u} [MeasurableSpace Action] [MeasurableSingletonClass Action] [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (selector : HalfTsallisScheduleFiniteHistorySelectorMeasurability arms harms eta) (n : Nat) : (sampledScheduledHalfTsallisHistoryAlgorithm arms harms eta selector).policy n = Exp3.finiteActionKernel arms (sampledScheduledHalfTsallisHistoryDistribution arms harms eta n) (sampledScheduledHalfTsallisHistoryDistributionSource arms harms eta selector n)

Complete environment-indexed scheduled half-Tsallis trajectory.

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

The successor action has its scheduled finite-action law conditional on the visible pair-history prefix.

theorem sampledScheduledHalfTsallisTrajectoryMeasure_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 : Nat -> Real) (selector : HalfTsallisScheduleFiniteHistorySelectorMeasurability 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 ⊗ₘ sampledScheduledHalfTsallisTrajectoryKernel arms harms eta selector environment) =ᵐ[ (prior ⊗ₘ sampledScheduledHalfTsallisTrajectoryKernel arms harms eta selector environment).map (fun sample => Preorder.frestrictLe n sample.2)] Exp3.finiteActionKernel arms (sampledScheduledHalfTsallisHistoryDistribution arms harms eta n) (sampledScheduledHalfTsallisHistoryDistributionSource arms harms eta selector n)

The scheduled conditional law after retaining the environment in the visible history.

theorem sampledScheduledHalfTsallisTrajectoryMeasure_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 : Nat -> Real) (selector : HalfTsallisScheduleFiniteHistorySelectorMeasurability 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 ⊗ₘ sampledScheduledHalfTsallisTrajectoryKernel arms harms eta selector environment) =ᵐ[ (prior ⊗ₘ sampledScheduledHalfTsallisTrajectoryKernel arms harms eta selector environment).map (fun sample : Env × ((k : Nat) -> Action × Real) => (sample.1, Preorder.frestrictLe n sample.2))] (Exp3.finiteActionKernel arms (sampledScheduledHalfTsallisHistoryDistribution arms harms eta n) (sampledScheduledHalfTsallisHistoryDistributionSource 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))