BanditRLProof.TsallisOracleRestartGeneratedTrajectory

Start time of the current epoch, with either continuation or a fresh restart at every successor time.

structure OracleRestartSchedule where

One epoch containing the whole trajectory.

def oracleNeverRestartSchedule : OracleRestartSchedule where

A fresh one-round epoch at every actual time.

def oracleRestartEveryRoundSchedule : OracleRestartSchedule where

Away from a restart boundary, the current epoch starts no later than the last observed round.

theorem OracleRestartSchedule.start_succ_le_of_ne (schedule : OracleRestartSchedule) (n : Nat) (hboundary : schedule.start (n + 1) ≠ n + 1) : schedule.start (n + 1) <= n

Reindex the inclusive global history segment `start..n` as a local history through `n-start`.

def oracleRestartLocalPairHistory {Action Reward : Type*} (start n : Nat) (hstart : start <= n) (history : History.FinitePairHistory Action Reward n) : History.FinitePairHistory Action Reward (n - start)

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

theorem oracleRestartLocalPairHistory_zero {Action Reward : Type*} (n : Nat) (history : History.FinitePairHistory Action Reward n) : oracleRestartLocalPairHistory 0 n (Nat.zero_le n) history = history

Epoch-suffix reindexing is measurable coordinatewise.

theorem measurable_oracleRestartLocalPairHistory {Action Reward : Type*} [MeasurableSpace Action] [MeasurableSpace Reward] (start n : Nat) (hstart : start <= n) : Measurable (oracleRestartLocalPairHistory (Action

Restarted successor action distribution. Boundary times use a fresh initial law; continuation times use only the current epoch's local suffix.

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

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

theorem sampledOracleRestartHalfTsallisHistoryDistribution_of_boundary {Action : Type u} [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (schedule : OracleRestartSchedule) (n : Nat) (hboundary : schedule.start (n + 1) = n + 1) (history : History.FinitePairHistory Action Real n) : sampledOracleRestartHalfTsallisHistoryDistribution arms harms eta schedule n history = initialHalfTsallisDistribution arms harms (eta 0)

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

theorem sampledOracleRestartHalfTsallisHistoryDistribution_of_continuation {Action : Type u} [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (schedule : OracleRestartSchedule) (n : Nat) (hboundary : schedule.start (n + 1) ≠ n + 1) (history : History.FinitePairHistory Action Real n) : sampledOracleRestartHalfTsallisHistoryDistribution arms harms eta schedule n history = sampledScheduledHalfTsallisHistoryDistribution arms harms eta (n - schedule.start (n + 1)) (oracleRestartLocalPairHistory (schedule.start (n + 1)) n (schedule.start_succ_le_of_ne n hboundary) history)

Every arm in the finite action set keeps strictly positive probability under either the boundary reset or the continued local scheduled policy.

theorem sampledOracleRestartHalfTsallisHistoryDistribution_pos {Action : Type u} [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (schedule : OracleRestartSchedule) (n : Nat) (history : History.FinitePairHistory Action Real n) (candidate : Action) (hcandidate : candidate ∈ arms) : 0 < sampledOracleRestartHalfTsallisHistoryDistribution arms harms eta schedule n history candidate

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

theorem sampledOracleRestartHalfTsallisHistoryDistribution_neverRestart {Action : Type u} [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (n : Nat) (history : History.FinitePairHistory Action Real n) : sampledOracleRestartHalfTsallisHistoryDistribution arms harms eta oracleNeverRestartSchedule n history = sampledScheduledHalfTsallisHistoryDistribution arms harms eta n history

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

theorem sampledOracleRestartHalfTsallisHistoryDistribution_restartEveryRound {Action : Type u} [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (n : Nat) (history : History.FinitePairHistory Action Real n) : sampledOracleRestartHalfTsallisHistoryDistribution arms harms eta oracleRestartEveryRoundSchedule n history = initialHalfTsallisDistribution arms harms (eta 0)

Measurable finite-action source for every restarted successor policy.

noncomputable def sampledOracleRestartHalfTsallisHistoryDistributionSource {Action : Type u} [MeasurableSpace Action] [MeasurableSingletonClass Action] [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (schedule : OracleRestartSchedule) (n : Nat) : Exp3.MeasurableFiniteActionDistribution arms (sampledOracleRestartHalfTsallisHistoryDistribution arms harms eta schedule n)

Stochastic finite-history algorithm whose score resets at every scheduled epoch boundary.

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

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

theorem sampledOracleRestartHalfTsallisHistoryAlgorithm_policy {Action : Type u} [MeasurableSpace Action] [MeasurableSingletonClass Action] [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (schedule : OracleRestartSchedule) (n : Nat) : (sampledOracleRestartHalfTsallisHistoryAlgorithm arms harms eta schedule).policy n = Exp3.finiteActionKernel arms (sampledOracleRestartHalfTsallisHistoryDistribution arms harms eta schedule n) (sampledOracleRestartHalfTsallisHistoryDistributionSource arms harms eta schedule n)

Restarted sampling probabilities at actual trajectory times.

noncomputable def sampledOracleRestartHalfTsallisProbabilityAtTime {Env : Type v} {Action : Type u} [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (schedule : OracleRestartSchedule) : Nat -> Env × ((k : Nat) -> Action × Real) -> Action -> Real | 0, _sample => initialHalfTsallisDistribution arms harms (eta 0) | n + 1, sample => sampledOracleRestartHalfTsallisHistoryDistribution arms harms eta schedule n (Preorder.frestrictLe n sample.2) @[simp] theorem sampledOracleRestartHalfTsallisProbabilityAtTime_neverRestart {Env : Type v} {Action : Type u} [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (t : Nat) (sample : Env × ((k : Nat) -> Action × Real)) : sampledOracleRestartHalfTsallisProbabilityAtTime arms harms eta oracleNeverRestartSchedule t sample = sampledScheduledHalfTsallisProbabilityAtTime arms harms eta t sample

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

theorem sampledOracleRestartHalfTsallisProbabilityAtTime_neverRestart {Env : Type v} {Action : Type u} [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (t : Nat) (sample : Env × ((k : Nat) -> Action × Real)) : sampledOracleRestartHalfTsallisProbabilityAtTime arms harms eta oracleNeverRestartSchedule t sample = sampledScheduledHalfTsallisProbabilityAtTime arms harms eta t sample

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

theorem sampledOracleRestartHalfTsallisProbabilityAtTime_restartEveryRound {Env : Type v} {Action : Type u} [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (t : Nat) (sample : Env × ((k : Nat) -> Action × Real)) : sampledOracleRestartHalfTsallisProbabilityAtTime arms harms eta oracleRestartEveryRoundSchedule t sample = initialHalfTsallisDistribution arms harms (eta 0)

Full environment-indexed trajectory generated by the restarted policy.

noncomputable def sampledOracleRestartHalfTsallisTrajectoryKernel {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) (schedule : OracleRestartSchedule) (environment : Thompson.MeasurableHistoryEnvironment Env Action Real) : Kernel Env ((n : Nat) -> Action × Real)

The generated successor action has the restarted finite-action law conditional on the complete visible global history.

theorem sampledOracleRestartHalfTsallisTrajectoryMeasure_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) (schedule : OracleRestartSchedule) (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 ⊗ₘ sampledOracleRestartHalfTsallisTrajectoryKernel arms harms eta schedule environment) =ᵐ[ (prior ⊗ₘ sampledOracleRestartHalfTsallisTrajectoryKernel arms harms eta schedule environment).map (fun sample => Preorder.frestrictLe n sample.2)] Exp3.finiteActionKernel arms (sampledOracleRestartHalfTsallisHistoryDistribution arms harms eta schedule n) (sampledOracleRestartHalfTsallisHistoryDistributionSource arms harms eta schedule n)

The restarted successor action law after retaining both the environment and the visible global prefix. This is the conditioning surface needed by predictable-loss first-moment transport.

theorem sampledOracleRestartHalfTsallisTrajectoryMeasure_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) (schedule : OracleRestartSchedule) (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 ⊗ₘ sampledOracleRestartHalfTsallisTrajectoryKernel arms harms eta schedule environment) =ᵐ[ (prior ⊗ₘ sampledOracleRestartHalfTsallisTrajectoryKernel arms harms eta schedule environment).map (fun sample : Env × ((k : Nat) -> Action × Real) => (sample.1, Preorder.frestrictLe n sample.2))] (Exp3.finiteActionKernel arms (sampledOracleRestartHalfTsallisHistoryDistribution arms harms eta schedule n) (sampledOracleRestartHalfTsallisHistoryDistributionSource arms harms eta schedule 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))