BanditRLProof.TsallisScheduledInitialExpectedStability

Canonical time-zero conjugate-potential score on the environment and sampled initial action.

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

Refined time-zero budget under the canonical initial half-Tsallis law.

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

The canonical time-zero history/action potential score is measurable.

theorem measurable_sampledScheduledHalfTsallisInitialHistoryActionPotentialStability {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (loss : Exp3.PredictableLossVector Env Action) : Measurable (sampledScheduledHalfTsallisInitialHistoryActionPotentialStability arms harms eta loss)

The time-zero refined budget is integrable under any finite environment law when the initial rate is positive.

theorem integrable_sampledScheduledHalfTsallisInitialRefinedPotentialStabilityBound {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [DecidableEq Action] (prior : Measure Env) [IsFiniteMeasure prior] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (heta : 0 < eta 0) : Integrable (sampledScheduledHalfTsallisInitialRefinedPotentialStabilityBound (Env

The actual scheduled time-zero potential term agrees almost surely with the canonical environment/action score.

theorem sampledScheduledHalfTsallisPotentialStabilityAtTime_zero_eq_initial_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 : Nat -> Real) (loss : Exp3.PredictableLossVector Env Action) : let selector := canonicalHalfTsallisScheduleGeneratedSelectorMeasurability arms harms eta loss let mu := prior ⊗ₘ sampledScheduledHalfTsallisTrajectoryKernel arms harms eta selector.finiteHistory loss.environment (fun sample => sampledScheduledHalfTsallisPotentialStabilityAtTime arms harms eta sample 0) =ᵐ[mu] (fun sample => sampledScheduledHalfTsallisInitialHistoryActionPotentialStability arms harms eta loss (sample.1, (sample.2 0).1))

The actual scheduled time-zero potential term agrees almost surely with the canonical environment/action score. -/ theorem sampledScheduledHalfTsallisPotentialStabilityAtTime_zero_eq_initial_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 : Nat -> Real) (loss : Exp3.PredictableLossVector Env Action) : let selector := canonicalHalfTsallisScheduleGeneratedSelectorMeasurability arms harms eta loss let mu := prior ⊗ₘ sampledScheduledHalfTsallisTrajectoryKernel arms harms eta selector.finiteHistory loss.environment (fun sample => sampledScheduledHalfTsallisPotentialStabilityAtTime arms harms eta sample 0) =ᵐ[mu] (fun sample => sampledScheduledHalfTsallisInitialHistoryActionPotentialStability arms harms eta loss (sample.1, (sample.2 0).1)) := by dsimp only let selector := canonicalHalfTsallisScheduleGeneratedSelectorMeasurability arms harms eta loss let algorithm := sampledScheduledHalfTsallisHistoryAlgorithm arms harms eta selector.finiteHistory let mu := prior ⊗ₘ sampledScheduledHalfTsallisTrajectoryKernel arms harms eta selector.finiteHistory loss.environment have hreward := Exp3.canonicalPredictableTrajectoryMeasure_reward_zero_eq_initialLoss_ae prior algorithm loss have hreward' : (fun sample : Env × ((k : Nat) -> Action × Real) => (sample.2 0).2) =ᵐ[mu] (fun sample => loss.initial sample.1 (sample.2 0).1) := by simpa [mu, algorithm, sampledScheduledHalfTsallisTrajectoryKernel] using hreward filter_upwards [hreward'] with sample hrewardSample have hestimate : sampledScheduledHalfTsallisObservedEstimatedLossAt arms harms eta 0 sample = Exp3.importanceWeightedLoss (initialHalfTsallisDistribution arms harms (eta 0)) (loss.initial sample.1) (sample.2 0).1 := by funext candidate unfold sampledScheduledHalfTsallisObservedEstimatedLossAt sampledScheduledHalfTsallisProbabilityAtTime by_cases hchosen : (sample.2 0).1 = candidate · simp [Exp3.importanceWeightedLoss, hchosen, hrewardSample] · simp [Exp3.importanceWeightedLoss, hchosen] have hnext : sampledScheduledHalfTsallisSameRateNextAt arms harms eta sample 0 = sampledHalfTsallisInitialUpdatedAt arms harms (eta 0) loss sample.1 (sample.2 0).1 := by unfold sampledScheduledHalfTsallisSameRateNextAt halfTsallisScheduledSameRateNext sampledHalfTsallisInitialUpdatedAt halfTsallisHistoryUpdatedMinimizer halfTsallisUpdatedMinimizer rw [FTRL.cumulativeLoss_succ] simp only [FTRL.cumulativeLoss_zero, zero_add] rw [hestimate] simp [initialHalfTsallisDistribution] unfold sampledScheduledHalfTsallisPotentialStabilityAtTime sampledScheduledHalfTsallisInitialHistoryActionPotentialStability importanceWeightedPotentialStabilityScore dsimp only rw [hestimate, hnext] simp [FTRL.cumulativeLoss_zero, sampledScheduledHalfTsallisProbabilityAtTime] congr 1 /-! The scheduled time-zero expected stability bound. It uses only the canonical initial action law and deterministic predictable initial reward. No schedule monotonicity, probability floor, or successor-round premise is required.

theorem integral_sampledScheduledHalfTsallisInitialPotentialStabilityAtTime_le_refined {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 : Nat -> Real) (heta : 0 < eta 0) (heta_le : eta 0 <= 1 / 2) (loss : Exp3.PredictableLossVector Env Action) : let selector := canonicalHalfTsallisScheduleGeneratedSelectorMeasurability arms harms eta loss let mu := prior ⊗ₘ sampledScheduledHalfTsallisTrajectoryKernel arms harms eta selector.finiteHistory loss.environment Integrable (fun sample => sampledScheduledHalfTsallisPotentialStabilityAtTime arms harms eta sample 0) mu ∧ integral mu (fun sample => sampledScheduledHalfTsallisPotentialStabilityAtTime arms harms eta sample 0) <= integral mu (fun sample => sampledScheduledHalfTsallisInitialRefinedPotentialStabilityBound (Env