BanditRLProof.TsallisConjugatePotentialFiniteHorizon

A time-indexed paper-normalized half-Tsallis potential.

noncomputable def halfTsallisPotentialProcess {Action : Type u} (arms : Finset Action) (eta : Real) (score probability : Nat -> Action -> Real) (t : Nat) : Real

Exact fixed-learning-rate finite-horizon telescope for the candidate potential expression. When every probability is the corresponding certified minimizer, this is the constrained-potential telescope.

theorem sum_halfTsallisPotentialStability_eq_linearLoss_sum_add_terminal_sub_initial {Action : Type u} (arms : Finset Action) (eta : Real) (score probability estimate : Nat -> Action -> Real) (T : Nat) (hscoreSucc : forall t, t < T -> score (t + 1) = fun action => score t action + estimate t action) : (Finset.range T).sum (fun t => halfTsallisPotentialStability arms eta (score t) (probability t) (estimate t) (probability (t + 1))) = (Finset.range T).sum (fun t => FTRL.linearLoss arms (probability t) (estimate t)) + halfTsallisPotentialProcess arms eta score probability T - halfTsallisPotentialProcess arms eta score probability 0

The realized one-round conjugate-potential score on a history/action pair.

noncomputable def importanceWeightedPotentialStabilityScore {History : Type u} {Action : Type v} (arms : Finset Action) (eta : Real) (score prob loss : History -> Action -> Real) (next : History -> Action -> Action -> Real) (sample : History × Action) : Real

The paper-shaped one-round conditional expectation budget.

noncomputable def refinedPotentialStabilityBound {History : Type u} {Action : Type v} (arms : Finset Action) (eta : Real) (prob : History -> Action -> Real) (history : History) : Real

Coordinatewise measurability closes a finite linear-loss sum.

theorem measurable_linearLoss_of_coordinatewise {History : Type u} {Action : Type v} [MeasurableSpace History] (arms : Finset Action) (prob loss : History -> Action -> Real) (hprob : forall action, action ∈ arms -> Measurable (fun history => prob history action)) (hloss : forall action, action ∈ arms -> Measurable (fun history => loss history action)) : Measurable (fun history => FTRL.linearLoss arms (prob history) (loss history))

The paper-normalized potential is measurable from supported coordinate measurability of its score and simplex candidate.

theorem measurable_halfTsallisPotentialValue {History : Type u} {Action : Type v} [MeasurableSpace History] (arms : Finset Action) (eta : Real) (score probability : History -> Action -> Real) (hscore : forall action, action ∈ arms -> Measurable (fun history => score history action)) (hprobability : forall action, action ∈ arms -> Measurable (fun history => probability history action)) : Measurable (fun history => halfTsallisPotentialValue arms eta (score history) (probability history))

The conjugate-potential score is measurable from supported current score, probability, loss, and updated-selector coordinates.

theorem measurable_importanceWeightedPotentialStabilityScore {History : Type u} {Action : Type v} [MeasurableSpace History] [MeasurableSpace Action] [MeasurableSingletonClass Action] [DecidableEq Action] (arms : Finset Action) (eta : Real) (score prob loss : History -> Action -> Real) (next : History -> Action -> Action -> Real) (hscore : forall candidate, candidate ∈ arms -> Measurable (fun history => score history candidate)) (hprob : forall candidate, candidate ∈ arms -> Measurable (fun history => prob history candidate)) (hloss : forall candidate, candidate ∈ arms -> Measurable (fun history => loss history candidate)) (hnext : forall candidate, candidate ∈ arms -> Measurable (fun sample : History × Action => next sample.1 sample.2 candidate)) : Measurable (importanceWeightedPotentialStabilityScore arms eta score prob loss next)

The refined one-round budget is measurable from supported probability coordinates.

theorem measurable_refinedPotentialStabilityBound {History : Type u} {Action : Type v} [MeasurableSpace History] (arms : Finset Action) (eta : Real) (prob : History -> Action -> Real) (hprob : forall action, action ∈ arms -> Measurable (fun history => prob history action)) : Measurable (refinedPotentialStabilityBound arms eta prob)

A true minimizer-to-minimizer potential step is nonnegative.

theorem halfTsallisPotentialStability_nonneg_of_minimizers {Action : Type u} (arms : Finset Action) (eta : Real) (score probability estimate next : Action -> Real) (heta : 0 < eta) (hprobabilityMin : FTRL.IsRegularizedMinimizer (FTRL.finiteSimplex arms) arms eta (negEntropyRegularizer arms (1 / 2 : Real)) score probability) (hnextMin : FTRL.IsRegularizedMinimizer (FTRL.finiteSimplex arms) arms eta (negEntropyRegularizer arms (1 / 2 : Real)) (fun action => score action + estimate action) next) : 0 <= halfTsallisPotentialStability arms eta score probability estimate next

The refined budget is uniformly integrable under a finite history measure.

theorem integrable_refinedPotentialStabilityBound_of_finiteSimplex {History : Type u} {Action : Type v} [MeasurableSpace History] (historyMu : Measure History) [IsFiniteMeasure historyMu] (arms : Finset Action) (eta : Real) (prob : History -> Action -> Real) (source : Exp3.MeasurableFiniteActionDistribution arms prob) (heta : 0 < eta) : Integrable (refinedPotentialStabilityBound arms eta prob) historyMu

Measurability plus exact minimizer certificates give integrability of the potential score under the finite sampling kernel, without a probability floor.

theorem integrable_importanceWeightedPotentialStabilityScore_finiteActionKernel {History : Type u} {Action : Type v} [MeasurableSpace History] [MeasurableSpace Action] [MeasurableSingletonClass Action] [DecidableEq Action] (historyMu : Measure History) [IsFiniteMeasure historyMu] (arms : Finset Action) (eta : Real) (score prob loss : History -> Action -> Real) (next : History -> Action -> Action -> Real) (source : Exp3.MeasurableFiniteActionDistribution arms prob) (heta : 0 < eta) (heta_le : eta <= 1 / 2) (hprobMin : forall history, FTRL.IsRegularizedMinimizer (FTRL.finiteSimplex arms) arms eta (negEntropyRegularizer arms (1 / 2 : Real)) (score history) (prob history)) (hnextMin : forall history chosen, chosen ∈ arms -> FTRL.IsRegularizedMinimizer (FTRL.finiteSimplex arms) arms eta (negEntropyRegularizer arms (1 / 2 : Real)) (fun candidate => score history candidate + Exp3.importanceWeightedLoss (prob history) (loss history) chosen candidate) (next history chosen)) (hloss : forall history action, action ∈ arms -> 0 <= loss history action ∧ loss history action <= 1) (hscore : Measurable (importanceWeightedPotentialStabilityScore arms eta score prob loss next)) : Integrable (importanceWeightedPotentialStabilityScore arms eta score prob loss next) (historyMu ⊗ₘ Exp3.finiteActionKernel arms prob source)

Product-law integrability pulls back to a realized history/action pair when the kernel is an identified conditional action law.

theorem integrable_score_comp_history_action_of_condDistrib_generic {Omega : Type u} {History : Type v} {Action : Type w} [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) (score : History × Action -> Real) (policy : Kernel History Action) [IsMarkovKernel policy] (hcond : condDistrib action history mu =ᵐ[mu.map history] policy) (hIntegrable : Integrable score (mu.map history ⊗ₘ policy)) : Integrable (fun omega => score (history omega, action omega)) mu

An identified finite conditional action law transports the deterministic ordinary-IW conjugate-potential theorem to a one-round integral inequality.

theorem integral_importanceWeightedPotentialStabilityScore_le_integral_refinedBound_of_condDistrib_of_minimizers {Omega : Type u} {History : Type v} {Action : Type w} [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) (eta : Real) (score prob loss : History -> Action -> Real) (next : History -> Action -> Action -> Real) (policy : Kernel History Action) [IsMarkovKernel policy] (hpolicy : policy =ᵐ[mu.map history] fun h => Exp3.finiteActionMeasure arms (prob h)) (hcond : condDistrib action history mu =ᵐ[mu.map history] policy) (heta : 0 < eta) (heta_le : eta <= 1 / 2) (hprobMin : forall h, FTRL.IsRegularizedMinimizer (FTRL.finiteSimplex arms) arms eta (negEntropyRegularizer arms (1 / 2 : Real)) (score h) (prob h)) (hnextMin : forall h chosen, chosen ∈ arms -> FTRL.IsRegularizedMinimizer (FTRL.finiteSimplex arms) arms eta (negEntropyRegularizer arms (1 / 2 : Real)) (fun candidate => score h candidate + Exp3.importanceWeightedLoss (prob h) (loss h) chosen candidate) (next h chosen)) (hloss : forall h candidate, candidate ∈ arms -> 0 <= loss h candidate ∧ loss h candidate <= 1) (hscore : Measurable (importanceWeightedPotentialStabilityScore arms eta score prob loss next)) (hIntegrable : Integrable (importanceWeightedPotentialStabilityScore arms eta score prob loss next) (mu.map history ⊗ₘ policy)) (hboundIntegrable : Integrable (refinedPotentialStabilityBound arms eta prob) (mu.map history)) : integral mu (fun omega => importanceWeightedPotentialStabilityScore arms eta score prob loss next (history omega, action omega)) <= integral (mu.map history) (refinedPotentialStabilityBound arms eta prob)

Finite-horizon expected conjugate-potential stability under identified conditional action laws and exact current/update minimizer certificates.

theorem integral_sum_importanceWeightedPotentialStabilityScore_le_integral_sum_refinedBound_of_condDistrib_of_minimizers {Omega : Type u} {History : Type v} {Action : Type w} [MeasurableSpace Omega] [MeasurableSpace History] [MeasurableSpace Action] [MeasurableSingletonClass Action] [StandardBorelSpace Action] [Nonempty Action] [DecidableEq Action] (mu : Measure Omega) [IsFiniteMeasure mu] (horizon : Nat) (arms : Finset Action) (eta : Real) (history : Nat -> Omega -> History) (action : Nat -> Omega -> Action) (score prob loss : Nat -> History -> Action -> Real) (next : Nat -> History -> Action -> Action -> Real) (policy : Nat -> Kernel History Action) (hmarkov : forall t, IsMarkovKernel (policy t)) (hhistory : forall t, Measurable (history t)) (haction : forall t, Measurable (action t)) (hpolicy : forall t, policy t =ᵐ[mu.map (history t)] fun h => Exp3.finiteActionMeasure arms (prob t h)) (hcond : forall t, condDistrib (action t) (history t) mu =ᵐ[mu.map (history t)] policy t) (heta : 0 < eta) (heta_le : eta <= 1 / 2) (hprobMin : forall t h, FTRL.IsRegularizedMinimizer (FTRL.finiteSimplex arms) arms eta (negEntropyRegularizer arms (1 / 2 : Real)) (score t h) (prob t h)) (hnextMin : forall t h chosen, chosen ∈ arms -> FTRL.IsRegularizedMinimizer (FTRL.finiteSimplex arms) arms eta (negEntropyRegularizer arms (1 / 2 : Real)) (fun candidate => score t h candidate + Exp3.importanceWeightedLoss (prob t h) (loss t h) chosen candidate) (next t h chosen)) (hloss : forall t h candidate, candidate ∈ arms -> 0 <= loss t h candidate ∧ loss t h candidate <= 1) (hscore : forall t, Measurable (importanceWeightedPotentialStabilityScore arms eta (score t) (prob t) (loss t) (next t))) (hIntegrable : forall t, Integrable (importanceWeightedPotentialStabilityScore arms eta (score t) (prob t) (loss t) (next t)) (mu.map (history t) ⊗ₘ policy t)) (hboundIntegrable : forall t, Integrable (refinedPotentialStabilityBound arms eta (prob t)) (mu.map (history t))) : integral mu (fun omega => (Finset.range horizon).sum (fun t => importanceWeightedPotentialStabilityScore arms eta (score t) (prob t) (loss t) (next t) (history t omega, action t omega))) <= integral mu (fun omega => (Finset.range horizon).sum (fun t => refinedPotentialStabilityBound arms eta (prob t) (history t omega)))

The canonical generated one-round potential score on a visible environment/prefix and sampled successor action.

noncomputable def sampledHalfTsallisHistoryActionPotentialStabilityAt {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) (n : Nat) : (Env × History.FinitePairHistory Action Real n) × Action -> Real

The generated visible-prefix refined potential budget.

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

The generated canonical potential score is measurable.

theorem measurable_sampledHalfTsallisHistoryActionPotentialStabilityAt {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) (n : Nat) : Measurable (sampledHalfTsallisHistoryActionPotentialStabilityAt arms harms eta loss n)

The generated refined potential budget is automatically integrable.

theorem integrable_sampledHalfTsallisRefinedPotentialStabilityBoundAt {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [DecidableEq Action] (n : Nat) (historyMu : Measure (Env × History.FinitePairHistory Action Real n)) [IsFiniteMeasure historyMu] (arms : Finset Action) (harms : arms.Nonempty) (eta : Real) (heta : 0 < eta) (selector : HalfTsallisFiniteHistorySelectorMeasurability arms harms eta) : Integrable (sampledHalfTsallisRefinedPotentialStabilityBoundAt (Env

The generated canonical potential score is automatically integrable under the visible-history/action product law.

theorem integrable_sampledHalfTsallisHistoryActionPotentialStabilityAt {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) (heta : 0 < eta) (heta_le : eta <= 1 / 2) (loss : Exp3.PredictableLossVector Env Action) (n : Nat) : let selector := canonicalHalfTsallisGeneratedSelectorMeasurability arms harms eta loss let mu := prior ⊗ₘ sampledHalfTsallisTrajectoryKernel arms harms eta selector.finiteHistory loss.environment Integrable (sampledHalfTsallisHistoryActionPotentialStabilityAt arms harms eta loss n) (mu.map (sampledHalfTsallisHistoryAt n) ⊗ₘ sampledHalfTsallisPolicyAt (Env

The actual generated successor potential step, written with the next prefix's current selector.

noncomputable def sampledHalfTsallisSuccessorPotentialStabilityAt {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) (n : Nat) (sample : Env × ((k : Nat) -> Action × Real)) : Real

Generated canonical finite-horizon successor conjugate-potential stability. The trajectory action law, score recursion, selector measurability, score integrability, and refined-budget integrability are all discharged internally.

theorem integral_sum_sampledHalfTsallisSuccessorPotentialStability_le_integral_sum_refinedPotentialStabilityBound_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] (horizon : Nat) (arms : Finset Action) (harms : arms.Nonempty) (eta : Real) (heta : 0 < eta) (heta_le : eta <= 1 / 2) (loss : Exp3.PredictableLossVector Env Action) : let selector := canonicalHalfTsallisGeneratedSelectorMeasurability arms harms eta loss let mu := prior ⊗ₘ sampledHalfTsallisTrajectoryKernel arms harms eta selector.finiteHistory loss.environment integral mu (fun sample => (Finset.range horizon).sum (fun n => sampledHalfTsallisSuccessorPotentialStabilityAt arms harms eta loss n sample)) <= integral mu (fun sample => (Finset.range horizon).sum (fun n => sampledHalfTsallisRefinedPotentialStabilityBoundAt (Env