BanditRLProof.Algorithms.ETCGeneratedHistoryPolicy

The state reconstructed from a finite reward history for the ETC commit rule. The prefix through `t` is retained exactly and the unobserved suffix is zero. The defaulted suffix is only an implementation device: score reconstruction requires the exploration horizon to be contained in the retained prefix.

def explorationArgmaxHistoryState (t : Nat) (history : History.FiniteRewardHistory Rat t) : RewardTrace Rat

The finite-history ETC state reconstruction is measurable as a trace.

theorem measurable_explorationArgmaxHistoryState (t : Nat) : Measurable (explorationArgmaxHistoryState t)

At policy time `t`, explore at action time `t + 1` while that action lies in the exploration prefix; otherwise choose the empirical-mean argmax computed from the completed finite-history state.

noncomputable def explorationArgmaxHistoryPolicy {K : Nat} (spec : ETC.Spec K) (model : FiniteBanditModel K) (t : Nat) : Policy.MeasurablePolicy (RewardTrace Rat) (Fin K) where

The canonical ETC action generator obtained by running the finite-history policy against the identity reward trace.

noncomputable def explorationArgmaxGeneratedAction {K : Nat} (spec : ETC.Spec K) (model : FiniteBanditModel K) : RewardTrace Rat -> ActionTrace (Fin K)

The canonical empirical-mean ETC trace is generated by the measurable policy over finite reward histories. Positive exploration pulls are essential at time zero: the shifted generated trace starts with `ETC.exploreArm spec 0`, which matches the ETC trace only when time zero belongs to the exploration prefix. At later commit times, the finite-history score reconstruction theorem supplies the argmax equality.

theorem explorationArgmaxGeneratedAction_eq_explorationArgmaxAction {K : Nat} (spec : ETC.Spec K) (model : FiniteBanditModel K) (hexplorationPulls_pos : 0 < spec.explorationPulls) : ETC.explorationArgmaxGeneratedAction spec model = ETC.explorationArgmaxAction spec model

During the exploration prefix, the generated finite-history ETC policy agrees with every fixed-commit ETC trace because both choose the same round-robin arm. The post-exploration commit arm is deliberately arbitrary in this statement; only the strict exploration-horizon hypothesis is used.

theorem explorationArgmaxGeneratedAction_eq_actionWithCommit_of_lt {K : Nat} (spec : ETC.Spec K) (model : FiniteBanditModel K) (commitArm : Fin K) (reward : RewardTrace Rat) {t : Nat} (hexplorationPulls_pos : 0 < spec.explorationPulls) (ht : t < spec.explorationPulls * K) : ETC.explorationArgmaxGeneratedAction spec model reward t = ETC.actionWithCommit spec commitArm t

Canonical kernel-trajectory law source for the finite-history ETC policy. The reward process is the identity coordinate process under the `RewardKernel.historyStepKernelFamily` trajectory measure. The existing canonical `trajMeasure` construction proves the full finite-pair `partialTraj` law for the generated policy action without assuming an ambient selected-reward law. Combined with `explorationArgmaxGeneratedAction_eq_explorationArgmaxAction`, this law is the action-dependent probability foundation for the canonical ETC action trace. It remains a kernel-generated trajectory law. Transport to an arbitrary adaptive environment and identification with the fixed product-coordinate source remain separate obligations.

noncomputable def explorationArgmaxGeneratedActionPartialTrajectoryPairLawSource_trajMeasure {K : Nat} {Context : Type} [MeasurableSpace Context] (spec : ETC.Spec K) (model : FiniteBanditModel K) (mu0 : MeasureTheory.Measure Rat) [MeasureTheory.IsProbabilityMeasure mu0] (rewardKernel : RewardKernel.MarkovRewardKernel (Prod Context (Fin K)) Rat) (context : (n : Nat) -> ((j : Finset.Iic n) -> Rat) -> Context) (hcontext : forall n : Nat, Measurable (context n)) : ConditionalExpectationReward.GeneratedActionPartialTrajectoryPairLawSource (ProbabilityTheory.Kernel.trajMeasure (X := fun _ : Nat => Rat) mu0 (RewardKernel.historyStepKernelFamily rewardKernel (fun t => ETC.explorationArgmaxHistoryPolicy spec model t) context (fun t history => ETC.explorationArgmaxHistoryState t history) hcontext (fun t => ETC.measurable_explorationArgmaxHistoryState t))) rewardKernel (fun t => ETC.explorationArgmaxHistoryPolicy spec model t) context (fun t history => ETC.explorationArgmaxHistoryState t history) (ETC.exploreArm spec 0) (fun trajectory : RewardTrace Rat => trajectory) (fun t => measurable_pi_apply t)

Canonical trajectory conditional sub-Gaussian MGF for the successor reward centered at the finite-bandit model mean selected by the ETC policy. The mean surface is context-independent, `fun _ action => model.mean action`. The kernel centered-reward law supplies conditional mean-zero and the one-step MGF; the remaining regularity contract is the selected finite-history variance ceiling at the requested successor time. This theorem is therefore a concentration foundation for the canonical kernel trajectory, not a transport to the fixed product-coordinate reward source or an arbitrary adaptive bandit environment.

theorem explorationArgmaxHistory_centeredReward_succ_hasCondSubgaussianMGF_trajMeasure {K : Nat} {Context : Type} [MeasurableSpace Context] (spec : ETC.Spec K) (model : FiniteBanditModel K) (mu0 : MeasureTheory.Measure Rat) [MeasureTheory.IsProbabilityMeasure mu0] (rewardKernel : RewardKernel.MarkovRewardKernel (Prod Context (Fin K)) Rat) (context : (n : Nat) -> ((j : Finset.Iic n) -> Rat) -> Context) (hcontext : forall n : Nat, Measurable (context n)) (varianceProxy : Context -> Fin K -> NNReal) (law : RewardKernel.CenteredRewardKernelLaw rewardKernel (fun _ action => model.mean action) varianceProxy) (i : Nat) (c : NNReal) (hvariance : forall history : ((j : Finset.Iic i) -> Rat), varianceProxy (context i history) ((ETC.explorationArgmaxHistoryPolicy spec model i).action (ETC.explorationArgmaxHistoryState i history)) <= c) : let policy := fun t => ETC.explorationArgmaxHistoryPolicy spec model t let state := fun t history => ETC.explorationArgmaxHistoryState t history let stepKernel := RewardKernel.historyStepKernelFamily rewardKernel policy context state hcontext (fun t => ETC.measurable_explorationArgmaxHistoryState t) let trajMeasure := ProbabilityTheory.Kernel.trajMeasure (X := fun _ : Nat => Rat) mu0 stepKernel let reward : RewardTrace Rat -> RewardTrace Rat := fun trajectory => trajectory let hreward : forall t : Nat, Measurable (fun trajectory : RewardTrace Rat => reward trajectory t)