BanditRLProof.Algorithms.StochasticGradientBanditTheoremTwoNativeTrajectory

Restricting the latent arm stream through time `n` gives the exact finite product of the per-round arm-vector laws.

theorem armStreamMeasure_map_frestrictLe_eq_pi {K : Nat} (nu : Kernel (Fin K) Real) [IsMarkovKernel nu] (n : Nat) : Measure.map (Preorder.frestrictLe n) (armStreamMeasure nu) = Measure.pi (fun _ : Finset.Iic n => Measure.infinitePi fun arm : Fin K => nu arm)

Extend a finite arm-stream box by zero rows after its endpoint.

def extendArmStreamFinitePrefix {K : Nat} (n : Nat) (streamBox : (i : Finset.Iic n) -> Fin K -> Real) : ArmRewardStream K

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

theorem measurable_extendArmStreamFinitePrefix {K : Nat} (n : Nat) : Measurable (extendArmStreamFinitePrefix (K := K) n)

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

theorem extendArmStreamFinitePrefix_apply_of_le {K : Nat} (n t : Nat) (ht : t <= n) (streamBox : (i : Finset.Iic n) -> Fin K -> Real) : extendArmStreamFinitePrefix n streamBox t = streamBox ⟨t, Finset.mem_Iic.mpr ht⟩

A finite kernel driven only by the complement of one arm-stream coordinate leaves that coordinate's prescribed marginal independent of the kernel output. The output kernel may be sub-Markov, as needed after branch restriction.

theorem armStreamMeasure_map_output_coordinate_compProd_comap_without_eq_prod {K : Nat} {Output : Type*} [MeasurableSpace Output] (nu : Kernel (Fin K) Real) [IsMarkovKernel nu] (target : Nat × Fin K) (kernel : Kernel ({index : Nat × Fin K // index ≠ target} -> Real) Output) [IsFiniteKernel kernel] : Measure.map (fun sample : ArmRewardStream K × Output => (sample.2, armStreamCoordinate target sample.1)) (armStreamMeasure nu ⊗ₘ kernel.comap (armStreamWithoutCoordinate target) (measurable_armStreamWithoutCoordinate target)) = (Measure.map Prod.snd (armStreamMeasure nu ⊗ₘ kernel.comap (armStreamWithoutCoordinate target) (measurable_armStreamWithoutCoordinate target))).prod (nu target.2)

Fixed-stream finite-prefix/next-pair recursion for the latent arm-stream trajectory. This is the trajectory-level recurrence used by the count-capped locality induction below.

theorem latentArmStreamTrajectoryKernel_map_prefix_next_eq_compProd {Env : Type u} {K : Nat} [MeasurableSpace Env] [StandardBorelSpace Env] [NeZero K] (algorithm : HistoryAlgorithm (Fin K) Real) (env : Env) (stream : UCB.ArmRewardStream K) (n : Nat) : (latentArmStreamTrajectoryKernel algorithm env stream).map (fun trajectory => (Preorder.frestrictLe n trajectory, trajectory (n + 1))) = (latentArmStreamTrajectoryKernel algorithm env stream).map (Preorder.frestrictLe n) ⊗ₘ historyStepKernel algorithm ((latentArmStreamMeasurableHistoryEnvironment (Env := Env) (K := K)).at (env, stream)) n

If two latent reward streams agree away from one coordinate, then their feedback laws agree at every history/action pair whose next-unused coordinate is not the omitted one.

theorem latentArmStreamFeedback_eq_of_withoutCoordinate_eq_of_selectedCoordinate_ne {Env : Type u} {K : Nat} [MeasurableSpace Env] (env : Env) (target : Nat × Fin K) (stream₁ stream₂ : UCB.ArmRewardStream K) (n : Nat) (history : History.FinitePairHistory (Fin K) Real n) (arm : Fin K) (hwithout : UCB.armStreamWithoutCoordinate target stream₁ = UCB.armStreamWithoutCoordinate target stream₂) (hne : (ETC.realHistoryPullCount n history arm, arm) ≠ target) : ((latentArmStreamMeasurableHistoryEnvironment (Env := Env) (K := K)).at (env, stream₁)).feedback n (history, arm) = ((latentArmStreamMeasurableHistoryEnvironment (Env := Env) (K := K)).at (env, stream₂)).feedback n (history, arm)

Before the target coordinate can be the next coordinate of its arm, the entire next-pair law agrees for streams with the same omitted-coordinate projection.

theorem historyStepKernel_apply_eq_of_withoutCoordinate_eq_of_target_count_lt {Env : Type u} {K : Nat} [MeasurableSpace Env] (algorithm : HistoryAlgorithm (Fin K) Real) (env : Env) (target : Nat × Fin K) (stream₁ stream₂ : UCB.ArmRewardStream K) (n : Nat) (history : History.FinitePairHistory (Fin K) Real n) (hwithout : UCB.armStreamWithoutCoordinate target stream₁ = UCB.armStreamWithoutCoordinate target stream₂) (hcount : ETC.realHistoryPullCount n history target.2 < target.1) : historyStepKernel algorithm ((latentArmStreamMeasurableHistoryEnvironment (Env := Env) (K := K)).at (env, stream₁)) n history = historyStepKernel algorithm ((latentArmStreamMeasurableHistoryEnvironment (Env := Env) (K := K)).at (env, stream₂)) n history

Next pairs whose action avoids a designated arm.

def latentArmStreamNextActionNeSet {K : Nat} (arm : Fin K) : Set (Fin K × Real)

Initial actions whose time-zero reward coordinate is not the omitted target.

def latentArmStreamInitialSafeArmSet {K : Nat} (target : Nat × Fin K) : Set (Fin K)

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

theorem measurableSet_latentArmStreamNextActionNeSet {K : Nat} (arm : Fin K) : MeasurableSet (latentArmStreamNextActionNeSet arm)

Even when the target pull index may already be next, the part of the next-pair law selecting another arm remains independent of the target coordinate.

theorem historyStepKernel_apply_restrict_nextActionNe_eq_of_withoutCoordinate_eq {Env : Type u} {K : Nat} [MeasurableSpace Env] (algorithm : HistoryAlgorithm (Fin K) Real) (env : Env) (target : Nat × Fin K) (stream₁ stream₂ : UCB.ArmRewardStream K) (n : Nat) (history : History.FinitePairHistory (Fin K) Real n) (hwithout : UCB.armStreamWithoutCoordinate target stream₁ = UCB.armStreamWithoutCoordinate target stream₂) : (historyStepKernel algorithm ((latentArmStreamMeasurableHistoryEnvironment (Env := Env) (K := K)).at (env, stream₁)) n history).restrict (latentArmStreamNextActionNeSet target.2) = (historyStepKernel algorithm ((latentArmStreamMeasurableHistoryEnvironment (Env := Env) (K := K)).at (env, stream₂)) n history).restrict (latentArmStreamNextActionNeSet target.2)

The time-zero visible prefix is the initial action/feedback pair pushed through the singleton-history constructor.

theorem latentArmStreamTrajectoryKernel_map_frestrictLe_zero {Env : Type u} {K : Nat} [MeasurableSpace Env] [StandardBorelSpace Env] [NeZero K] (algorithm : HistoryAlgorithm (Fin K) Real) (env : Env) (stream : UCB.ArmRewardStream K) : (latentArmStreamTrajectoryKernel algorithm env stream).map (Preorder.frestrictLe 0) = (algorithm.initialAction ⊗ₘ ((latentArmStreamMeasurableHistoryEnvironment (Env := Env) (K := K)).at (env, stream)).initialFeedback).map singletonPairHistory

Two latent streams agreeing through `n` generate the same visible trajectory law through `n`. Action randomization remains inside the canonical trajectory kernel; the argument changes only deterministic reward fibers.

theorem latentArmStreamTrajectoryKernel_map_frestrictLe_eq_of_streamPrefix_eq {Env : Type u} {K : Nat} [MeasurableSpace Env] [StandardBorelSpace Env] [NeZero K] (algorithm : HistoryAlgorithm (Fin K) Real) (env : Env) (stream₁ stream₂ : UCB.ArmRewardStream K) (n : Nat) (hstream : Preorder.frestrictLe n stream₁ = Preorder.frestrictLe n stream₂) : (latentArmStreamTrajectoryKernel algorithm env stream₁).map (Preorder.frestrictLe n) = (latentArmStreamTrajectoryKernel algorithm env stream₂).map (Preorder.frestrictLe n)

Finite visible-prefix kernel after replacing the infinite reward stream by its zero-extended finite box.

noncomputable def latentArmStreamVisiblePrefixKernel {Env : Type u} {K : Nat} [MeasurableSpace Env] [NeZero K] (algorithm : HistoryAlgorithm (Fin K) Real) (env : Env) (n : Nat) : Kernel ((i : Finset.Iic n) -> Fin K -> Real) (History.FinitePairHistory (Fin K) Real n)

The latent visible-prefix kernel factors exactly through the finite stream box through the same endpoint.

theorem latentArmStreamTrajectoryKernel_map_frestrictLe_eq_prefixKernel_comap {Env : Type u} {K : Nat} [MeasurableSpace Env] [StandardBorelSpace Env] [NeZero K] (algorithm : HistoryAlgorithm (Fin K) Real) (env : Env) (n : Nat) : (latentArmStreamTrajectoryKernel algorithm env).map (Preorder.frestrictLe n) = (latentArmStreamVisiblePrefixKernel algorithm env n).comap (Preorder.frestrictLe n) (Preorder.measurable_frestrictLe n)

Visible history through `n` paired with the action selected at `n + 1`.

def latentArmStreamVisiblePrefixNextAction {K : Nat} (n : Nat) : ((t : Nat) -> Fin K × Real) -> History.FinitePairHistory (Fin K) Real n × Fin K

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

theorem measurable_latentArmStreamVisiblePrefixNextAction {K : Nat} (n : Nat) : Measurable (latentArmStreamVisiblePrefixNextAction (K := K) n)

Reward observed at the shifted successor time `n + 1`.

def latentArmStreamVisibleNextReward {K : Nat} (n : Nat) : ((t : Nat) -> Fin K × Real) -> Real

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

theorem measurable_latentArmStreamVisibleNextReward {K : Nat} (n : Nat) : Measurable (latentArmStreamVisibleNextReward (K := K) n)

Canonical candidate for the condition kernel on one next-coordinate branch, reconstructed after fixing the omitted coordinate to zero.

noncomputable def latentArmStreamVisiblePrefixNextActionBranchKernel {Env : Type u} {K : Nat} [MeasurableSpace Env] [StandardBorelSpace Env] [NeZero K] (algorithm : HistoryAlgorithm (Fin K) Real) (env : Env) (n : Nat) (target : Nat × Fin K) : Kernel ({index : Nat × Fin K // index ≠ target} -> Real) (History.FinitePairHistory (Fin K) Real n × Fin K)

Histories through `n` that have not consumed the designated latent coordinate. The inclusive history count can equal the coordinate index: that coordinate is used only by the next reward from the same arm.

def latentArmStreamPrefixCountCap {K : Nat} (n : Nat) (target : Nat × Fin K) : Set (History.FinitePairHistory (Fin K) Real n)

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

theorem measurableSet_latentArmStreamPrefixCountCap {K : Nat} (n : Nat) (target : Nat × Fin K) : MeasurableSet (latentArmStreamPrefixCountCap n target)

Pulling the time-zero count cap back through the singleton-history constructor leaves exactly the actions whose initial reward coordinate is not the omitted target.

theorem singletonPairHistory_preimage_latentArmStreamPrefixCountCap_zero {K : Nat} (target : Nat × Fin K) : (@singletonPairHistory (Fin K) Real) ⁻¹' latentArmStreamPrefixCountCap 0 target = latentArmStreamInitialSafeArmSet target ×ˢ Set.univ

Count-cap locality at the initial pair.

theorem latentArmStreamPrefixCountCapLocality_zero {Env : Type u} {K : Nat} [MeasurableSpace Env] [StandardBorelSpace Env] [NeZero K] (algorithm : HistoryAlgorithm (Fin K) Real) (env : Env) (target : Nat × Fin K) (stream₁ stream₂ : UCB.ArmRewardStream K) (hwithout : UCB.armStreamWithoutCoordinate target stream₁ = UCB.armStreamWithoutCoordinate target stream₂) : ((latentArmStreamTrajectoryKernel algorithm env stream₁).map (Preorder.frestrictLe 0)).restrict (latentArmStreamPrefixCountCap 0 target) = ((latentArmStreamTrajectoryKernel algorithm env stream₂).map (Preorder.frestrictLe 0)).restrict (latentArmStreamPrefixCountCap 0 target)

Strict count region used by the first rectangle in the successor cap decomposition.

def latentArmStreamPrefixCountLt {K : Nat} (n : Nat) (target : Nat × Fin K) : Set (History.FinitePairHistory (Fin K) Real n)

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

theorem measurableSet_latentArmStreamPrefixCountLt {K : Nat} (n : Nat) (target : Nat × Fin K) : MeasurableSet (latentArmStreamPrefixCountLt n target)

Exact count region used by the second rectangle in the successor cap decomposition.

def latentArmStreamPrefixCountEq {K : Nat} (n : Nat) (target : Nat × Fin K) : Set (History.FinitePairHistory (Fin K) Real n)

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

theorem measurableSet_latentArmStreamPrefixCountEq {K : Nat} (n : Nat) (target : Nat × Fin K) : MeasurableSet (latentArmStreamPrefixCountEq n target)

Extending an inclusive finite pair history increments exactly the count of the arm selected by the appended pair.

theorem realHistoryPullCount_extendPairHistorySucc {K : Nat} (n : Nat) (history : History.FinitePairHistory (Fin K) Real n) (next : Fin K × Real) (arm : Fin K) : ETC.realHistoryPullCount (n + 1) (History.extendPairHistorySucc history next) arm = ETC.realHistoryPullCount n history arm + if next.1 = arm then 1 else 0

The successor prefix remains below the target count cap exactly when the old prefix is capped and either has strict slack or avoids the target arm.

theorem mem_latentArmStreamPrefixCountCap_extendPairHistorySucc_iff {K : Nat} (n : Nat) (history : History.FinitePairHistory (Fin K) Real n) (next : Fin K × Real) (target : Nat × Fin K) : History.extendPairHistorySucc history next ∈ latentArmStreamPrefixCountCap (n + 1) target ↔ history ∈ latentArmStreamPrefixCountCap n target ∧ (ETC.realHistoryPullCount n history target.2 < target.1 ∨ next.1 ≠ target.2)

A capped successor prefix was already capped before appending its last action/reward pair.

theorem latentArmStreamPrefixCountCap_of_extendPairHistorySucc_mem {K : Nat} (n : Nat) (history : History.FinitePairHistory (Fin K) Real n) (next : Fin K × Real) (target : Nat × Fin K) (hcap : History.extendPairHistorySucc history next ∈ latentArmStreamPrefixCountCap (n + 1) target) : history ∈ latentArmStreamPrefixCountCap n target

Every appended pair that remains in the successor cap reads a stream coordinate different from the omitted target.

theorem selectedCoordinate_ne_of_extendPairHistorySucc_mem_prefixCountCap {K : Nat} (n : Nat) (history : History.FinitePairHistory (Fin K) Real n) (next : Fin K × Real) (target : Nat × Fin K) (hcap : History.extendPairHistorySucc history next ∈ latentArmStreamPrefixCountCap (n + 1) target) : (ETC.realHistoryPullCount n history next.1, next.1) ≠ target

Pulling the successor count cap back through history extension gives two measurable rectangles: below the target count every action is safe, while at the target count only actions avoiding the target arm are safe.

theorem latentArmStreamSuccessorCountCap_preimage {K : Nat} (n : Nat) (target : Nat × Fin K) : (fun sample : History.FinitePairHistory (Fin K) Real n × (Fin K × Real) => History.extendPairHistorySucc sample.1 sample.2) ⁻¹' latentArmStreamPrefixCountCap (n + 1) target = (latentArmStreamPrefixCountLt n target ×ˢ Set.univ) ∪ (latentArmStreamPrefixCountEq n target ×ˢ latentArmStreamNextActionNeSet target.2)

Next action/reward pairs that keep a fixed old prefix below the successor count cap.

def latentArmStreamSuccessorCountCapSection {K : Nat} (n : Nat) (target : Nat × Fin K) (history : History.FinitePairHistory (Fin K) Real n) : Set (Fin K × Real)

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

theorem measurableSet_latentArmStreamSuccessorCountCapSection {K : Nat} (n : Nat) (target : Nat × Fin K) (history : History.FinitePairHistory (Fin K) Real n) : MeasurableSet (latentArmStreamSuccessorCountCapSection n target history)

Over a previously capped prefix, the one-step law restricted to capped successors depends only on the complement of the omitted stream coordinate.

theorem historyStepKernel_apply_restrict_successorCountCap_eq_of_withoutCoordinate_eq {Env : Type u} {K : Nat} [MeasurableSpace Env] (algorithm : HistoryAlgorithm (Fin K) Real) (env : Env) (target : Nat × Fin K) (stream₁ stream₂ : UCB.ArmRewardStream K) (n : Nat) (history : History.FinitePairHistory (Fin K) Real n) (hwithout : UCB.armStreamWithoutCoordinate target stream₁ = UCB.armStreamWithoutCoordinate target stream₂) (hcap : history ∈ latentArmStreamPrefixCountCap n target) : (historyStepKernel algorithm ((latentArmStreamMeasurableHistoryEnvironment (Env := Env) (K := K)).at (env, stream₁)) n history).restrict (latentArmStreamSuccessorCountCapSection n target history) = (historyStepKernel algorithm ((latentArmStreamMeasurableHistoryEnvironment (Env := Env) (K := K)).at (env, stream₂)) n history).restrict (latentArmStreamSuccessorCountCapSection n target history)

Successor step for count-capped locality of the fixed-stream visible trajectory prefix law.

theorem latentArmStreamTrajectoryKernel_map_frestrictLe_restrict_countCap_succ {Env : Type u} {K : Nat} [MeasurableSpace Env] [StandardBorelSpace Env] [NeZero K] (algorithm : HistoryAlgorithm (Fin K) Real) (env : Env) (target : Nat × Fin K) (stream₁ stream₂ : UCB.ArmRewardStream K) (hwithout : UCB.armStreamWithoutCoordinate target stream₁ = UCB.armStreamWithoutCoordinate target stream₂) (n : Nat) (hprefix : ((latentArmStreamTrajectoryKernel algorithm env stream₁).map (Preorder.frestrictLe n)).restrict (latentArmStreamPrefixCountCap n target) = ((latentArmStreamTrajectoryKernel algorithm env stream₂).map (Preorder.frestrictLe n)).restrict (latentArmStreamPrefixCountCap n target)) : ((latentArmStreamTrajectoryKernel algorithm env stream₁).map (Preorder.frestrictLe (n + 1))).restrict (latentArmStreamPrefixCountCap (n + 1) target) = ((latentArmStreamTrajectoryKernel algorithm env stream₂).map (Preorder.frestrictLe (n + 1))).restrict (latentArmStreamPrefixCountCap (n + 1) target)

Count-capped fixed-stream prefix locality under equality of all latent coordinates except the omitted target.

theorem latentArmStreamTrajectoryKernel_map_frestrictLe_restrict_countCap_eq_of_withoutCoordinate_eq {Env : Type u} {K : Nat} [MeasurableSpace Env] [StandardBorelSpace Env] [NeZero K] (algorithm : HistoryAlgorithm (Fin K) Real) (env : Env) (target : Nat × Fin K) (stream₁ stream₂ : UCB.ArmRewardStream K) (hwithout : UCB.armStreamWithoutCoordinate target stream₁ = UCB.armStreamWithoutCoordinate target stream₂) (n : Nat) : ((latentArmStreamTrajectoryKernel algorithm env stream₁).map (Preorder.frestrictLe n)).restrict (latentArmStreamPrefixCountCap n target) = ((latentArmStreamTrajectoryKernel algorithm env stream₂).map (Preorder.frestrictLe n)).restrict (latentArmStreamPrefixCountCap n target)

Exact contract for branchwise prefix/action locality. The count-capped trajectory induction above proves this contract below.

def LatentArmStreamVisiblePrefixNextActionBranchLocality {Env : Type u} {K : Nat} [MeasurableSpace Env] [StandardBorelSpace Env] [NeZero K] (algorithm : HistoryAlgorithm (Fin K) Real) (env : Env) (n : Nat) : Prop

Count-cap locality of visible prefixes implies the exact history/action branch-locality contract.

theorem latentArmStreamVisiblePrefixNextActionBranchLocality_of_prefixCountCapLocality {Env : Type u} {K : Nat} [MeasurableSpace Env] [StandardBorelSpace Env] [NeZero K] (algorithm : HistoryAlgorithm (Fin K) Real) (env : Env) (n : Nat) (hcap : ∀ (target : Nat × Fin K) (stream₁ stream₂ : UCB.ArmRewardStream K), UCB.armStreamWithoutCoordinate target stream₁ = UCB.armStreamWithoutCoordinate target stream₂ → (((latentArmStreamTrajectoryKernel algorithm env stream₁).map (Preorder.frestrictLe n)).restrict (latentArmStreamPrefixCountCap n target)) = (((latentArmStreamTrajectoryKernel algorithm env stream₂).map (Preorder.frestrictLe n)).restrict (latentArmStreamPrefixCountCap n target))) : LatentArmStreamVisiblePrefixNextActionBranchLocality algorithm env n

Every latent arm-stream trajectory kernel satisfies branch locality: on the exact next-coordinate branch, the visible prefix and next action depend only on the complementary latent coordinates. This does not yet identify the latent visible law with the native fixed-IID process.

theorem latentArmStreamVisiblePrefixNextActionBranchLocality {Env : Type u} {K : Nat} [MeasurableSpace Env] [StandardBorelSpace Env] [NeZero K] (algorithm : HistoryAlgorithm (Fin K) Real) (env : Env) (n : Nat) : LatentArmStreamVisiblePrefixNextActionBranchLocality algorithm env n

Once the branch-locality producer is available, coordinate independence immediately yields the exact branchwise condition/selected-coordinate product law. This consumer is valid for the sub-Markov branch kernel and therefore does not misstate branch restriction as ordinary probability independence.

theorem latentArmStreamVisiblePrefixNextAction_coordinate_branch_eq_prod_of_locality {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) (hlocal : LatentArmStreamVisiblePrefixNextActionBranchLocality algorithm env n) (target : Nat × Fin K) : let branchKernel := ((latentArmStreamTrajectoryKernel algorithm env).map (latentArmStreamVisiblePrefixNextAction n)).restrict (UCB.measurableSet_armStreamHistoryActionCoordinateBranch n target) Measure.map (fun sample : UCB.ArmRewardStream K × (History.FinitePairHistory (Fin K) Real n × Fin K) => (sample.2, UCB.armStreamCoordinate target sample.1)) (UCB.armStreamMeasure nu ⊗ₘ branchKernel) = (Measure.map Prod.snd (UCB.armStreamMeasure nu ⊗ₘ branchKernel)).prod (nu target.2)

Unconditional compiled branchwise product law obtained from the proved count-capped locality producer.

theorem latentArmStreamVisiblePrefixNextAction_coordinate_branch_eq_prod {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) (target : Nat × Fin K) : let branchKernel := ((latentArmStreamTrajectoryKernel algorithm env).map (latentArmStreamVisiblePrefixNextAction n)).restrict (UCB.measurableSet_armStreamHistoryActionCoordinateBranch n target) Measure.map (fun sample : UCB.ArmRewardStream K × (History.FinitePairHistory (Fin K) Real n × Fin K) => (sample.2, UCB.armStreamCoordinate target sample.1)) (UCB.armStreamMeasure nu ⊗ₘ branchKernel) = (Measure.map Prod.snd (UCB.armStreamMeasure nu ⊗ₘ branchKernel)).prod (nu target.2)

After the latent reward stream is mixed out, the next action still follows the algorithm's history policy. This isolates action randomization from the remaining selected-reward freshness obligation.

theorem latentArmStreamTrajectoryMeasure_map_visiblePrefix_nextAction_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) => latentArmStreamVisiblePrefixNextAction n sample.2) (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) ⊗ₘ algorithm.policy n

On the coupling, the actual successor reward is the latent coordinate encoded by the visible prefix and the sampled next action. This is pathwise support; conditional freshness still requires the branchwise product proof.

theorem latentArmStreamVisibleNextReward_eq_selectedCoordinate_ae {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) : ∀ᵐ sample ∂latentArmStreamTrajectoryMeasure algorithm env nu, latentArmStreamVisibleNextReward n sample.2 = UCB.armStreamCoordinate (UCB.armStreamCoordinateOfHistoryAction n (latentArmStreamVisiblePrefixNextAction n sample.2)) sample.1

The reward coordinate selected by a visible history/action condition is a measurable function of the latent stream and that condition.

theorem measurable_latentArmStreamSelectedCoordinate {K : Nat} (n : Nat) : Measurable (fun sample : UCB.ArmRewardStream K × (History.FinitePairHistory (Fin K) Real n × Fin K) => UCB.armStreamCoordinate (UCB.armStreamCoordinateOfHistoryAction n sample.2) sample.1)

On a fixed pull-count/arm branch, the dynamically selected latent reward coordinate has the restricted condition marginal times the selected arm law.

theorem latentArmStreamVisiblePrefixNextAction_selectedCoordinate_branch_eq_prod {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) (target : Nat × Fin K) : let conditionKernel := (latentArmStreamTrajectoryKernel algorithm env).map (latentArmStreamVisiblePrefixNextAction n) let fullMixed := UCB.armStreamMeasure nu ⊗ₘ conditionKernel let branch := UCB.armStreamHistoryActionCoordinateBranch n target let branchKernel := conditionKernel.restrict (UCB.measurableSet_armStreamHistoryActionCoordinateBranch n target) let branchMixed := UCB.armStreamMeasure nu ⊗ₘ branchKernel Measure.map (fun sample : UCB.ArmRewardStream K × (History.FinitePairHistory (Fin K) Real n × Fin K) => (sample.2, UCB.armStreamCoordinate (UCB.armStreamCoordinateOfHistoryAction n sample.2) sample.1)) branchMixed = ((Measure.map Prod.snd fullMixed).restrict branch).prod (nu target.2)

Summing the countable pull-count/arm partition gives the selected-coordinate joint law under the mixed latent-stream/visible-condition measure.

theorem latentArmStreamVisiblePrefixNextAction_selectedCoordinate_mixed_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) : let conditionKernel := (latentArmStreamTrajectoryKernel algorithm env).map (latentArmStreamVisiblePrefixNextAction n) let fullMixed := UCB.armStreamMeasure nu ⊗ₘ conditionKernel Measure.map (fun sample : UCB.ArmRewardStream K × (History.FinitePairHistory (Fin K) Real n × Fin K) => (sample.2, UCB.armStreamCoordinate (UCB.armStreamCoordinateOfHistoryAction n sample.2) sample.1)) fullMixed = Measure.map Prod.snd fullMixed ⊗ₘ UCB.armStreamSelectedRewardKernel n nu

Transport the selected-coordinate product law from the mixed representation back to the original latent-stream trajectory coupling.

theorem latentArmStreamVisiblePrefixNextAction_selectedCoordinate_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) => (latentArmStreamVisiblePrefixNextAction n sample.2, UCB.armStreamCoordinate (UCB.armStreamCoordinateOfHistoryAction n (latentArmStreamVisiblePrefixNextAction n sample.2)) sample.1)) (latentArmStreamTrajectoryMeasure algorithm env nu) = Measure.map (fun sample : UCB.ArmRewardStream K × ((t : Nat) -> Fin K × Real) => latentArmStreamVisiblePrefixNextAction n sample.2) (latentArmStreamTrajectoryMeasure algorithm env nu) ⊗ₘ UCB.armStreamSelectedRewardKernel n nu

Given the visible prefix through `n` and the action at `n + 1`, the actual next reward in the latent-stream coupling has exactly the selected arm law.

theorem latentArmStreamVisibleNextReward_joint_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) => (latentArmStreamVisiblePrefixNextAction n sample.2, latentArmStreamVisibleNextReward n sample.2)) (latentArmStreamTrajectoryMeasure algorithm env nu) = Measure.map (fun sample : UCB.ArmRewardStream K × ((t : Nat) -> Fin K × Real) => latentArmStreamVisiblePrefixNextAction n sample.2) (latentArmStreamTrajectoryMeasure algorithm env nu) ⊗ₘ UCB.armStreamSelectedRewardKernel n nu

Conditional-law form of one-step selected-reward freshness on the full latent-stream trajectory coupling.

theorem latentArmStreamVisibleNextReward_condDistrib_ae_eq_nu {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) : condDistrib (fun sample : UCB.ArmRewardStream K × ((t : Nat) -> Fin K × Real) => latentArmStreamVisibleNextReward n sample.2) (fun sample : UCB.ArmRewardStream K × ((t : Nat) -> Fin K × Real) => latentArmStreamVisiblePrefixNextAction n sample.2) (latentArmStreamTrajectoryMeasure algorithm env nu) =ᵐ[ (latentArmStreamTrajectoryMeasure algorithm env nu).map (fun sample => latentArmStreamVisiblePrefixNextAction n sample.2)] UCB.armStreamSelectedRewardKernel n nu

Observable-marginal form of the one-step selected-reward joint law. This removes the latent arm stream from the theorem's source space without claiming that the entire visible trajectory already equals the native construction.

theorem latentArmStreamVisibleTrajectoryMeasure_nextReward_joint_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) : let visibleMeasure := (latentArmStreamTrajectoryMeasure algorithm env nu).map Prod.snd Measure.map (fun trajectory : (t : Nat) -> Fin K × Real => (latentArmStreamVisiblePrefixNextAction n trajectory, latentArmStreamVisibleNextReward n trajectory)) visibleMeasure = Measure.map (latentArmStreamVisiblePrefixNextAction n) visibleMeasure ⊗ₘ UCB.armStreamSelectedRewardKernel n nu

Conditional-law form of one-step selected-reward freshness on the visible trajectory marginal.

theorem latentArmStreamVisibleTrajectoryMeasure_nextReward_condDistrib_ae_eq_nu {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) : let visibleMeasure := (latentArmStreamTrajectoryMeasure algorithm env nu).map Prod.snd condDistrib (latentArmStreamVisibleNextReward n) (latentArmStreamVisiblePrefixNextAction n) visibleMeasure =ᵐ[ visibleMeasure.map (latentArmStreamVisiblePrefixNextAction n)] UCB.armStreamSelectedRewardKernel n nu

Exact finite mixture law for the latent stream box and the visible SGB trajectory prefix. This is the deferred-decisions representation that the remaining native-prefix comparison must consume.

theorem latentArmStreamTrajectoryMeasure_map_stream_visiblePrefix_eq {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.1, Preorder.frestrictLe n sample.2)) (latentArmStreamTrajectoryMeasure algorithm env nu) = Measure.pi (fun _ : Finset.Iic n => Measure.infinitePi fun arm : Fin K => nu arm) ⊗ₘ latentArmStreamVisiblePrefixKernel algorithm env n