Lean module · Tsallis-FTRL
BanditRLProof.TsallisScheduledRecursiveTrajectory
# Scheduled recursive half-Tsallis trajectories This module lifts the recursive pure half-Tsallis trajectory from a fixed learning rate to a deterministic schedule. The initial action uses `eta 0`; after the visible prefix through round `n`, the successor policy uses `eta (n + 1)`. This indexing matches the scheduled FTRL penalty route. The module constructs only the selector, score, policy, trajectory, and conditional action law. It does not prove a refined stability or regret bound.
Module map
Imports
BanditRLProof.TsallisFTRLGeneratedMeasurability
Imported by
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
structure
BanditRLProof.Tsallis.HalfTsallisScheduleFiniteHistorySelectorMeasurability
Compiled
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
def
BanditRLProof.Tsallis.canonicalHalfTsallisScheduleFiniteHistorySelectorMeasurability
Compiled
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
def
BanditRLProof.Tsallis.sampledScheduledHalfTsallisHistoryScore
Compiled
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
theorem
BanditRLProof.Tsallis.sampledScheduledHalfTsallisHistoryScore_zero
Compiled
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
theorem
BanditRLProof.Tsallis.sampledScheduledHalfTsallisHistoryScore_succ
Compiled
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
theorem
BanditRLProof.Tsallis.measurable_sampledScheduledHalfTsallisHistoryScore
Compiled
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)
def
BanditRLProof.Tsallis.sampledScheduledHalfTsallisHistoryDistribution
Compiled
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
def
BanditRLProof.Tsallis.sampledScheduledHalfTsallisHistoryDistributionSource
Compiled
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)
def
BanditRLProof.Tsallis.sampledScheduledHalfTsallisHistoryAlgorithm
Compiled
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
theorem
BanditRLProof.Tsallis.sampledScheduledHalfTsallisHistoryAlgorithm_policy
Compiled
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)
def
BanditRLProof.Tsallis.sampledScheduledHalfTsallisTrajectoryKernel
Compiled
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)
theorem
BanditRLProof.Tsallis.sampledScheduledHalfTsallisTrajectoryMeasure_condDistrib_action
Compiled
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)
theorem
BanditRLProof.Tsallis.sampledScheduledHalfTsallisTrajectoryMeasure_condDistrib_action_given_environment
Compiled
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))