BanditRLProof.TsallisFTRLEstimatedEnvironmentRegret

The pure half-Tsallis sampling probability at an actual trajectory time.

noncomputable def sampledHalfTsallisProbabilityAtTime {Env : Type u} {Action : Type v} [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Real) : Nat -> Env × ((k : Nat) -> Action × Real) -> Action -> Real | 0, _sample => initialHalfTsallisDistribution arms harms eta | n + 1, sample => sampledHalfTsallisHistoryDistribution arms harms eta n (Preorder.frestrictLe n sample.2) /-- The observed-scalar importance-weighted loss vector at an actual time. -/ noncomputable def sampledHalfTsallisObservedEstimatedLossAt {Env : Type u} {Action : Type v} [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Real) (t : Nat) (sample : Env × ((k : Nat) -> Action × Real)) : Action -> Real

The observed-scalar importance-weighted loss vector at an actual time.

noncomputable def sampledHalfTsallisObservedEstimatedLossAt {Env : Type u} {Action : Type v} [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Real) (t : Nat) (sample : Env × ((k : Nat) -> Action × Real)) : Action -> Real

The canonical cumulative selector generated by the observed estimator is the actual pure half-Tsallis probability at the same time.

theorem cumulativeLoss_sampledHalfTsallisObservedEstimatedLossAt_succ {Env : Type u} {Action : Type v} [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Real) (sample : Env × ((k : Nat) -> Action × Real)) (n : Nat) : FTRL.cumulativeLoss (fun t => sampledHalfTsallisObservedEstimatedLossAt arms harms eta t sample) (n + 1) = sampledHalfTsallisHistoryScore arms harms eta n (Preorder.frestrictLe n sample.2)

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

theorem halfTsallisCumulativeMinimizer_observedEstimatedLoss_eq_probabilityAtTime {Env : Type u} {Action : Type v} [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Real) (sample : Env × ((k : Nat) -> Action × Real)) (t : Nat) : halfTsallisCumulativeMinimizer arms harms eta (fun s => sampledHalfTsallisObservedEstimatedLossAt arms harms eta s sample) t = sampledHalfTsallisProbabilityAtTime arms harms eta t sample

The time-zero current-minus-updated stability term.

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

The pathwise successor stability term formed from the scalar reward stored in the generated trajectory.

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

Canonical time-zero update after sampling the initial action.

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

Canonical predictable stability score for the initial action.

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

The deterministic FTRL stability sum splits into the initial term and the generated successor terms.

theorem sum_observedEstimated_stability_eq_initial_add_successor {Env : Type u} {Action : Type v} [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Real) (sample : Env × ((k : Nat) -> Action × Real)) (horizon : Nat) : let estimatedLoss := fun t => sampledHalfTsallisObservedEstimatedLossAt arms harms eta t sample let p := halfTsallisCumulativeMinimizer arms harms eta estimatedLoss (Finset.range (horizon + 1)).sum (fun t => FTRL.linearLoss arms (p t) (estimatedLoss t) - FTRL.linearLoss arms (p (t + 1)) (estimatedLoss t)) = sampledHalfTsallisInitialStability arms harms eta sample + (Finset.range horizon).sum (fun n => sampledHalfTsallisObservedSuccessorStabilityAt arms harms eta n sample)

Pathwise estimated-loss regret decomposition for time zero followed by `horizon` generated successor rounds.

theorem sampledHalfTsallis_observedEstimatedRegret_le {Env : Type u} {Action : Type v} [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Real) (heta : 0 < eta) (q : Action -> Real) (hq : FTRL.finiteSimplex arms q) (sample : Env × ((k : Nat) -> Action × Real)) (horizon : Nat) : (Finset.range (horizon + 1)).sum (fun t => FTRL.linearLoss arms (sampledHalfTsallisProbabilityAtTime arms harms eta t sample) (sampledHalfTsallisObservedEstimatedLossAt arms harms eta t sample) - FTRL.linearLoss arms q (sampledHalfTsallisObservedEstimatedLossAt arms harms eta t sample)) <= sampledHalfTsallisInitialStability arms harms eta sample + (Finset.range horizon).sum (fun n => sampledHalfTsallisObservedSuccessorStabilityAt arms harms eta n sample) + ((powerSum arms (1 / 2 : Real) (initialHalfTsallisDistribution arms harms eta) - powerSum arms (1 / 2 : Real) q) / (1 - (1 / 2 : Real))) / eta

The predictable importance-weighted loss vector at an actual trajectory time, using the same probability as the observed recursive update.

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

Estimated regret against a fixed comparator distribution, including time zero and `horizon` successor rounds.

noncomputable def sampledHalfTsallisObservedEstimatedRegret {Env : Type u} {Action : Type v} [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Real) (q : Action -> Real) (horizon : Nat) (sample : Env × ((k : Nat) -> Action × Real)) : Real

Predictable environment regret for the generated pure half-Tsallis probabilities against a fixed comparator distribution.

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

The same finite-horizon estimated regret after replacing stored rewards by their predictable loss-vector coordinates.

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

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

theorem measurable_sampledHalfTsallisProbabilityAtTime {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Real) (t : Nat) (candidate : Action) (hcandidate : candidate ∈ arms) : Measurable (fun sample : Env × ((k : Nat) -> Action × Real) => sampledHalfTsallisProbabilityAtTime arms harms eta t sample candidate)

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

theorem measurable_sampledHalfTsallisObservedEstimatedLossAt {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Real) (t : Nat) (candidate : Action) (hcandidate : candidate ∈ arms) : Measurable (fun sample : Env × ((k : Nat) -> Action × Real) => sampledHalfTsallisObservedEstimatedLossAt arms harms eta t sample candidate)

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

theorem measurable_sampledHalfTsallisPredictableEstimatedLossAt {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Real) (loss : Exp3.PredictableLossVector Env Action) (t : Nat) (candidate : Action) (hcandidate : candidate ∈ arms) : Measurable (fun sample : Env × ((k : Nat) -> Action × Real) => sampledHalfTsallisPredictableEstimatedLossAt arms harms eta loss t sample candidate)

Deterministic predictable feedback identifies the observed estimator with the corresponding predictable estimator almost surely at every actual time.

theorem sampledHalfTsallisObservedEstimatedLossAt_eq_predictable_ae {Env : Type u} {Action : Type v} [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) (loss : Exp3.PredictableLossVector Env Action) (t : Nat) : let selector := canonicalHalfTsallisFiniteHistorySelectorMeasurability arms harms eta let mu := prior ⊗ₘ sampledHalfTsallisTrajectoryKernel arms harms eta selector loss.environment (fun sample => sampledHalfTsallisObservedEstimatedLossAt arms harms eta t sample) =ᵐ[mu] (fun sample => sampledHalfTsallisPredictableEstimatedLossAt arms harms eta loss t sample)

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

theorem measurable_sampledHalfTsallisInitialUpdatedAt {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Real) (loss : Exp3.PredictableLossVector Env Action) (candidate : Action) (hcandidate : candidate ∈ arms) : Measurable (fun sample : Env × Action => sampledHalfTsallisInitialUpdatedAt arms harms eta loss sample.1 sample.2 candidate)

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

theorem measurable_sampledHalfTsallisInitialHistoryActionStability {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Real) (loss : Exp3.PredictableLossVector Env Action) : Measurable (sampledHalfTsallisInitialHistoryActionStability arms harms eta loss)

The stored-reward initial stability term agrees almost surely with the canonical predictable updated-minimizer score.

theorem sampledHalfTsallisInitialStability_eq_historyAction_ae {Env : Type u} {Action : Type v} [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) (loss : Exp3.PredictableLossVector Env Action) : let selector := canonicalHalfTsallisFiniteHistorySelectorMeasurability arms harms eta let mu := prior ⊗ₘ sampledHalfTsallisTrajectoryKernel arms harms eta selector loss.environment sampledHalfTsallisInitialStability arms harms eta =ᵐ[mu] (fun sample => sampledHalfTsallisInitialHistoryActionStability arms harms eta loss (sample.1, (sample.2 0).1))

Observed and predictable successor stability agree almost surely.

theorem sampledHalfTsallisObservedSuccessorStabilityAt_eq_predictable_ae {Env : Type u} {Action : Type v} [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) (loss : Exp3.PredictableLossVector Env Action) (n : Nat) : let selector := canonicalHalfTsallisFiniteHistorySelectorMeasurability arms harms eta let mu := prior ⊗ₘ sampledHalfTsallisTrajectoryKernel arms harms eta selector loss.environment sampledHalfTsallisObservedSuccessorStabilityAt arms harms eta n =ᵐ[mu] sampledHalfTsallisSuccessorStabilityAt arms harms eta loss n

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

theorem measurable_mixedImportanceWeightedLoss_of_coordinates {History : Type u} {Action : Type v} [MeasurableSpace History] [MeasurableSpace Action] [MeasurableSingletonClass Action] [DecidableEq Action] (arms : Finset Action) (prob loss : History -> Action -> Real) (hprob : forall candidate, candidate ∈ arms -> Measurable (fun history => prob history candidate)) (hloss : forall candidate, candidate ∈ arms -> Measurable (fun history => loss history candidate)) : Measurable (fun sample : History × Action => Exp3.mixedImportanceWeightedLoss arms (prob sample.1) (loss sample.1) sample.2)

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

theorem measurable_weightedImportanceWeightedLoss_of_coordinates {History : Type u} {Action : Type v} [MeasurableSpace History] [MeasurableSpace Action] [MeasurableSingletonClass Action] [DecidableEq Action] (arms : Finset Action) (prob weight loss : History -> Action -> Real) (hprob : forall candidate, candidate ∈ arms -> Measurable (fun history => prob history candidate)) (hweight : forall candidate, candidate ∈ arms -> Measurable (fun history => weight history candidate)) (hloss : forall candidate, candidate ∈ arms -> Measurable (fun history => loss history candidate)) : Measurable (fun sample : History × Action => Exp3.weightedImportanceWeightedLoss arms (prob sample.1) (weight sample.1) (loss sample.1) sample.2)

Mixed importance-weighted loss is integrable under its finite sampling kernel without a uniform probability floor.

theorem integrable_mixedImportanceWeightedLoss_finiteActionKernel {History : Type u} {Action : Type v} [MeasurableSpace History] [MeasurableSpace Action] [MeasurableSingletonClass Action] [DecidableEq Action] (historyMu : Measure History) [IsFiniteMeasure historyMu] (arms : Finset Action) (prob loss : History -> Action -> Real) (source : Exp3.MeasurableFiniteActionDistribution arms prob) (hprobPos : forall history candidate, candidate ∈ arms -> 0 < prob history candidate) (hloss : forall history candidate, candidate ∈ arms -> 0 <= loss history candidate ∧ loss history candidate <= 1) (hscore : Measurable (fun sample : History × Action => Exp3.mixedImportanceWeightedLoss arms (prob sample.1) (loss sample.1) sample.2)) : Integrable (fun sample : History × Action => Exp3.mixedImportanceWeightedLoss arms (prob sample.1) (loss sample.1) sample.2) (historyMu ⊗ₘ Exp3.finiteActionKernel arms prob source)

A fixed simplex comparator weighting of the importance-weighted loss is integrable under the sampling kernel, again without a uniform floor.

theorem integrable_weightedImportanceWeightedLoss_finiteActionKernel {History : Type u} {Action : Type v} [MeasurableSpace History] [MeasurableSpace Action] [MeasurableSingletonClass Action] [DecidableEq Action] (historyMu : Measure History) [IsFiniteMeasure historyMu] (arms : Finset Action) (prob loss : History -> Action -> Real) (q : Action -> Real) (hq : FTRL.finiteSimplex arms q) (source : Exp3.MeasurableFiniteActionDistribution arms prob) (hprobPos : forall history candidate, candidate ∈ arms -> 0 < prob history candidate) (hloss : forall history candidate, candidate ∈ arms -> 0 <= loss history candidate ∧ loss history candidate <= 1) (hscore : Measurable (fun sample : History × Action => Exp3.weightedImportanceWeightedLoss arms (prob sample.1) q (loss sample.1) sample.2)) : Integrable (fun sample : History × Action => Exp3.weightedImportanceWeightedLoss arms (prob sample.1) q (loss sample.1) sample.2) (historyMu ⊗ₘ Exp3.finiteActionKernel arms prob source)

Constant environment-indexed source for the initial half-Tsallis law.

noncomputable def initialHalfTsallisEnvironmentDistributionSource {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Real) : Exp3.MeasurableFiniteActionDistribution arms (fun _env : Env => initialHalfTsallisDistribution arms harms eta) where

Product-law integrability of an arbitrary score transports to the actual history/action composition under an identified conditional action law.

theorem integrable_score_comp_history_action_of_condDistrib {Omega : Type u} {History : Type v} {Action : Type*} [MeasurableSpace Omega] [MeasurableSpace History] [MeasurableSpace Action] [StandardBorelSpace Action] [Nonempty Action] (mu : Measure Omega) [IsFiniteMeasure mu] (history : Omega -> History) (hhistory : Measurable history) (action : Omega -> Action) (haction : Measurable action) (policy : Kernel History Action) [IsMarkovKernel policy] (hcond : condDistrib action history mu =ᵐ[mu.map history] policy) (score : History × Action -> Real) (hIntegrable : Integrable score (mu.map history ⊗ₘ policy)) : Integrable (fun omega => score (history omega, action omega)) mu

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

theorem integrable_mixed_weightedImportanceWeightedLoss_of_condDistrib {Omega : Type u} {History : Type v} {Action : Type*} [MeasurableSpace Omega] [MeasurableSpace History] [MeasurableSpace Action] [MeasurableSingletonClass Action] [StandardBorelSpace Action] [Nonempty Action] [DecidableEq Action] (mu : Measure Omega) [IsFiniteMeasure mu] (history : Omega -> History) (hhistory : Measurable history) (action : Omega -> Action) (haction : Measurable action) (arms : Finset Action) (prob loss : History -> Action -> Real) (q : Action -> Real) (hq : FTRL.finiteSimplex arms q) (source : Exp3.MeasurableFiniteActionDistribution arms prob) (hcond : condDistrib action history mu =ᵐ[mu.map history] Exp3.finiteActionKernel arms prob source) (hprobPos : forall h candidate, candidate ∈ arms -> 0 < prob h candidate) (hlossMeas : forall candidate, candidate ∈ arms -> Measurable (fun h => loss h candidate)) (hloss : forall h candidate, candidate ∈ arms -> 0 <= loss h candidate ∧ loss h candidate <= 1) : Integrable (fun omega => Exp3.mixedImportanceWeightedLoss arms (prob (history omega)) (loss (history omega)) (action omega)) mu ∧ Integrable (fun omega => Exp3.weightedImportanceWeightedLoss arms (prob (history omega)) q (loss (history omega)) (action omega)) mu

Conditional first moments for a positive finite sampling law, with no uniform probability floor.

theorem integral_mixed_weightedImportanceWeightedLoss_eq_predictable {Omega : Type u} {History : Type v} {Action : Type*} [MeasurableSpace Omega] [MeasurableSpace History] [MeasurableSpace Action] [MeasurableSingletonClass Action] [StandardBorelSpace Action] [Nonempty Action] [DecidableEq Action] (mu : Measure Omega) [IsFiniteMeasure mu] (history : Omega -> History) (hhistory : Measurable history) (action : Omega -> Action) (haction : Measurable action) (arms : Finset Action) (prob loss : History -> Action -> Real) (q : Action -> Real) (hq : FTRL.finiteSimplex arms q) (source : Exp3.MeasurableFiniteActionDistribution arms prob) (hcond : condDistrib action history mu =ᵐ[mu.map history] Exp3.finiteActionKernel arms prob source) (hprobPos : forall h candidate, candidate ∈ arms -> 0 < prob h candidate) (hlossMeas : forall candidate, candidate ∈ arms -> Measurable (fun h => loss h candidate)) (hloss : forall h candidate, candidate ∈ arms -> 0 <= loss h candidate ∧ loss h candidate <= 1) : (integral mu (fun omega => Exp3.mixedImportanceWeightedLoss arms (prob (history omega)) (loss (history omega)) (action omega)) = integral mu (fun omega => FTRL.linearLoss arms (prob (history omega)) (loss (history omega)))) ∧ (integral mu (fun omega => Exp3.weightedImportanceWeightedLoss arms (prob (history omega)) q (loss (history omega)) (action omega)) = integral mu (fun omega => FTRL.linearLoss arms q (loss (history omega))))

At every actual time, both the sampling-distribution mixed estimator and the fixed-comparator weighted estimator have the corresponding predictable first moment under the generated half-Tsallis trajectory.

theorem sampledHalfTsallisPredictableEstimatedLossAt_first_moments {Env : Type u} {Action : Type v} [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) (loss : Exp3.PredictableLossVector Env Action) (q : Action -> Real) (hq : FTRL.finiteSimplex arms q) (t : Nat) : let selector := canonicalHalfTsallisFiniteHistorySelectorMeasurability arms harms eta let mu := prior ⊗ₘ sampledHalfTsallisTrajectoryKernel arms harms eta selector loss.environment (Integrable (fun sample => FTRL.linearLoss arms (sampledHalfTsallisProbabilityAtTime arms harms eta t sample) (sampledHalfTsallisPredictableEstimatedLossAt arms harms eta loss t sample)) mu ∧ Integrable (fun sample => FTRL.linearLoss arms q (sampledHalfTsallisPredictableEstimatedLossAt arms harms eta loss t sample)) mu) ∧ ((integral mu (fun sample => FTRL.linearLoss arms (sampledHalfTsallisProbabilityAtTime arms harms eta t sample) (sampledHalfTsallisPredictableEstimatedLossAt arms harms eta loss t sample)) = integral mu (fun sample => FTRL.linearLoss arms (sampledHalfTsallisProbabilityAtTime arms harms eta t sample) (Exp3.predictableLossAt loss t sample))) ∧ (integral mu (fun sample => FTRL.linearLoss arms q (sampledHalfTsallisPredictableEstimatedLossAt arms harms eta loss t sample)) = integral mu (fun sample => FTRL.linearLoss arms q (Exp3.predictableLossAt loss t sample))))

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

theorem finiteSimplex_sampledHalfTsallisProbabilityAtTime {Env : Type u} {Action : Type v} [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Real) (t : Nat) (sample : Env × ((k : Nat) -> Action × Real)) : FTRL.finiteSimplex arms (sampledHalfTsallisProbabilityAtTime arms harms eta t sample)

Current mixed predictable loss and fixed-comparator predictable loss are integrable at every actual time.

theorem integrable_sampledHalfTsallisPredictableLinearLossAt {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [DecidableEq Action] (mu : Measure (Env × ((k : Nat) -> Action × Real))) [IsFiniteMeasure mu] (arms : Finset Action) (harms : arms.Nonempty) (eta : Real) (loss : Exp3.PredictableLossVector Env Action) (q : Action -> Real) (hq : FTRL.finiteSimplex arms q) (t : Nat) : Integrable (fun sample => FTRL.linearLoss arms (sampledHalfTsallisProbabilityAtTime arms harms eta t sample) (Exp3.predictableLossAt loss t sample)) mu ∧ Integrable (fun sample => FTRL.linearLoss arms q (Exp3.predictableLossAt loss t sample)) mu

Finite-horizon predictable estimated regret is integrable and has exactly the same integral as predictable environment regret.

theorem integral_sampledHalfTsallisPredictableEstimatedRegret_eq_environmentRegret {Env : Type u} {Action : Type v} [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) (loss : Exp3.PredictableLossVector Env Action) (q : Action -> Real) (hq : FTRL.finiteSimplex arms q) (horizon : Nat) : let selector := canonicalHalfTsallisFiniteHistorySelectorMeasurability arms harms eta let mu := prior ⊗ₘ sampledHalfTsallisTrajectoryKernel arms harms eta selector loss.environment Integrable (sampledHalfTsallisPredictableEstimatedRegret arms harms eta loss q horizon) mu ∧ Integrable (sampledHalfTsallisPredictableEnvironmentRegret arms harms eta loss q horizon) mu ∧ integral mu (sampledHalfTsallisPredictableEstimatedRegret arms harms eta loss q horizon) = integral mu (sampledHalfTsallisPredictableEnvironmentRegret arms harms eta loss q horizon)

The observed estimated-regret functional agrees almost surely with its predictable-estimator version over every finite horizon.

theorem sampledHalfTsallisObservedEstimatedRegret_eq_predictable_ae {Env : Type u} {Action : Type v} [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) (loss : Exp3.PredictableLossVector Env Action) (q : Action -> Real) (horizon : Nat) : let selector := canonicalHalfTsallisFiniteHistorySelectorMeasurability arms harms eta let mu := prior ⊗ₘ sampledHalfTsallisTrajectoryKernel arms harms eta selector loss.environment sampledHalfTsallisObservedEstimatedRegret arms harms eta q horizon =ᵐ[mu] sampledHalfTsallisPredictableEstimatedRegret arms harms eta loss q horizon

Observed importance-weighted regret is integrable and has exactly the predictable environment-regret integral.

theorem integral_sampledHalfTsallisObservedEstimatedRegret_eq_environmentRegret {Env : Type u} {Action : Type v} [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) (loss : Exp3.PredictableLossVector Env Action) (q : Action -> Real) (hq : FTRL.finiteSimplex arms q) (horizon : Nat) : let selector := canonicalHalfTsallisFiniteHistorySelectorMeasurability arms harms eta let mu := prior ⊗ₘ sampledHalfTsallisTrajectoryKernel arms harms eta selector loss.environment Integrable (sampledHalfTsallisObservedEstimatedRegret arms harms eta q horizon) mu ∧ Integrable (sampledHalfTsallisPredictableEnvironmentRegret arms harms eta loss q horizon) mu ∧ integral mu (sampledHalfTsallisObservedEstimatedRegret arms harms eta q horizon) = integral mu (sampledHalfTsallisPredictableEnvironmentRegret arms harms eta loss q horizon)

The time-zero observed stability has the same half-power bound as every successor round. A probability prior keeps the constant bound unscaled.

theorem integral_sampledHalfTsallisInitialStability_le_halfPower {Env : Type u} {Action : Type v} [MeasurableSpace Env] [StandardBorelSpace Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [StandardBorelSpace Action] [Nonempty Action] [DecidableEq Action] (prior : Measure Env) [IsProbabilityMeasure prior] (arms : Finset Action) (harms : arms.Nonempty) (eta : Real) (heta : 0 < eta) (loss : Exp3.PredictableLossVector Env Action) : let selector := canonicalHalfTsallisFiniteHistorySelectorMeasurability arms harms eta let mu := prior ⊗ₘ sampledHalfTsallisTrajectoryKernel arms harms eta selector loss.environment Integrable (sampledHalfTsallisInitialStability arms harms eta) mu ∧ integral mu (sampledHalfTsallisInitialStability arms harms eta) <= 2 * eta * powerSum arms (1 / 2 : Real) (initialHalfTsallisDistribution arms harms eta)

Predictable and observed successor stability are both integrable under the canonical generated half-Tsallis trajectory.

theorem integrable_sampledHalfTsallisSuccessorStabilitiesAt_canonical {Env : Type u} {Action : Type v} [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) (loss : Exp3.PredictableLossVector Env Action) (n : Nat) : let selector := canonicalHalfTsallisFiniteHistorySelectorMeasurability arms harms eta let mu := prior ⊗ₘ sampledHalfTsallisTrajectoryKernel arms harms eta selector loss.environment Integrable (sampledHalfTsallisSuccessorStabilityAt arms harms eta loss n) mu ∧ Integrable (sampledHalfTsallisObservedSuccessorStabilityAt arms harms eta n) mu

Complete estimated-to-environment regret theorem for the generated pure half-Tsallis policy. The horizon contains time zero plus `horizon` successor rounds; self-bounding and learning-rate tuning remain downstream.

theorem integral_sampledHalfTsallisPredictableEnvironmentRegret_le {Env : Type u} {Action : Type v} [MeasurableSpace Env] [StandardBorelSpace Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [StandardBorelSpace Action] [Nonempty Action] [DecidableEq Action] (prior : Measure Env) [IsProbabilityMeasure prior] (arms : Finset Action) (harms : arms.Nonempty) (eta : Real) (heta : 0 < eta) (loss : Exp3.PredictableLossVector Env Action) (q : Action -> Real) (hq : FTRL.finiteSimplex arms q) (horizon : Nat) : let selector := canonicalHalfTsallisFiniteHistorySelectorMeasurability arms harms eta let mu := prior ⊗ₘ sampledHalfTsallisTrajectoryKernel arms harms eta selector loss.environment integral mu (sampledHalfTsallisPredictableEnvironmentRegret arms harms eta loss q horizon) <= 2 * eta * powerSum arms (1 / 2 : Real) (initialHalfTsallisDistribution arms harms eta) + integral mu (fun sample => (Finset.range horizon).sum (fun n => sampledHalfTsallisHalfPowerBoundAt (Env