BanditRLProof.Algorithms.StochasticGradientBanditTheoremTwoNativePrefix

The native stationary environment: feedback is the law of the selected arm, independent of the observed history.

def stationaryRewardHistoryEnvironment {K : Nat} (nu : Kernel (Fin K) Real) [IsMarkovKernel nu] : HistoryEnvironment (Fin K) Real where

The native step kernel composes the policy with the selected-arm law.

theorem historyStepKernel_stationaryRewardHistoryEnvironment {K : Nat} (algorithm : HistoryAlgorithm (Fin K) Real) (nu : Kernel (Fin K) Real) [IsMarkovKernel nu] (n : Nat) : historyStepKernel algorithm (stationaryRewardHistoryEnvironment nu) n = algorithm.policy n ⊗ₖ UCB.armStreamSelectedRewardKernel n nu

One-step native extension of the visible prefix under the latent coupling. At every deterministic time `n`, the joint law of the visible prefix through `n` and the next observed action/reward pair is the prefix law composed with the native stationary step kernel. This is a single-step statement; it does not identify whole prefixes or the full native law.

theorem latentArmStreamVisiblePrefixNextPair_eq_compProd {Env : Type u} {K : Nat} [MeasurableSpace Env] [StandardBorelSpace Env] [NeZero K] (algorithm : HistoryAlgorithm (Fin K) Real) (env : Env) (nu : Kernel (Fin K) Real) [IsMarkovKernel nu] (n : Nat) : Measure.map (fun sample : UCB.ArmRewardStream K × ((t : Nat) -> Fin K × Real) => (Preorder.frestrictLe n sample.2, sample.2 (n + 1))) (latentArmStreamTrajectoryMeasure algorithm env nu) = Measure.map (fun sample : UCB.ArmRewardStream K × ((t : Nat) -> Fin K × Real) => Preorder.frestrictLe n sample.2) (latentArmStreamTrajectoryMeasure algorithm env nu) ⊗ₘ historyStepKernel algorithm (stationaryRewardHistoryEnvironment nu) n

Time-zero pair law of the latent coupling: the initial action follows the algorithm's initial law and the initial reward is a fresh draw from the selected arm law.

theorem latentArmStreamVisibleInitialPair_eq_compProd {Env : Type u} {K : Nat} [MeasurableSpace Env] [StandardBorelSpace Env] [NeZero K] (algorithm : HistoryAlgorithm (Fin K) Real) (env : Env) (nu : Kernel (Fin K) Real) [IsMarkovKernel nu] : Measure.map (fun sample : UCB.ArmRewardStream K × ((t : Nat) -> Fin K × Real) => sample.2 0) (latentArmStreamTrajectoryMeasure algorithm env nu) = algorithm.initialAction ⊗ₘ nu

The Ionescu-Tulcea trajectory law reproduces its initial law at time zero.

theorem trajMeasure_map_eval_zero {X : Nat -> Type u} [forall n, MeasurableSpace (X n)] (mu0 : Measure (X 0)) [IsProbabilityMeasure mu0] (kappa : (n : Nat) -> Kernel ((i : Finset.Iic n) -> X i) (X (n + 1))) [forall n, IsMarkovKernel (kappa n)] : (Kernel.trajMeasure mu0 kappa).map (fun x => x 0) = mu0

The visible prefix at `n + 1` is the prefix at `n` extended by the next pair.

theorem frestrictLe_succ_eq_extendPairHistorySucc {K : Nat} (n : Nat) (x : (t : Nat) -> Fin K × Real) : Preorder.frestrictLe (n + 1) x = History.extendPairHistorySucc (Preorder.frestrictLe n x) (x (n + 1))

The native fixed-i.i.d. trajectory law: the same algorithm run against the stationary environment whose feedback is the selected-arm law.

def nativeStationaryTrajectoryMeasure {K : Nat} (algorithm : HistoryAlgorithm (Fin K) Real) (nu : Kernel (Fin K) Real) [IsMarkovKernel nu] : Measure ((n : Nat) -> Fin K × Real)

*Native-prefix identification.** At every finite horizon `n`, the visible trajectory marginal of the latent arm-stream coupling and the native fixed-i.i.d. process induce the same law on prefixes through `n`. This is a finite-prefix identity. It does not by itself give the full native visible law, selected- or stopped-reward i.i.d. statements, the stopped-prefix future/no-return law, or Theorem 2.

theorem latentArmStreamVisibleTrajectoryMeasure_map_frestrictLe_eq_native {Env : Type u} {K : Nat} [MeasurableSpace Env] [StandardBorelSpace Env] [NeZero K] (algorithm : HistoryAlgorithm (Fin K) Real) (env : Env) (nu : Kernel (Fin K) Real) [IsMarkovKernel nu] (n : Nat) : ((latentArmStreamTrajectoryMeasure algorithm env nu).map Prod.snd).map (Preorder.frestrictLe n) = (nativeStationaryTrajectoryMeasure algorithm nu).map (Preorder.frestrictLe n)

*Full native visible-law identification.** Forgetting the latent reward stream from the arm-stream coupling gives exactly the native stationary fixed-i.i.d. SGB trajectory law. The proof promotes the compiled equality of every inclusive finite prefix to an equality of complete trajectory measures by projective-limit uniqueness. It does not assert that totalized stopped rewards are i.i.d., identify a random-time future cylinder, or prove the source Theorem 2 endpoint.

theorem latentArmStreamVisibleTrajectoryMeasure_eq_native {Env : Type u} {K : Nat} [MeasurableSpace Env] [StandardBorelSpace Env] [NeZero K] (algorithm : HistoryAlgorithm (Fin K) Real) (env : Env) (nu : Kernel (Fin K) Real) [IsMarkovKernel nu] : (latentArmStreamTrajectoryMeasure algorithm env nu).map Prod.snd = nativeStationaryTrajectoryMeasure algorithm nu