BanditRLProof.ConditionalRewardPartialTrajectoryLaw

An ambient reward process satisfying the configured initial law and successor conditional-distribution recursion has the generated finite-pair `partialTraj` law on the generated history filtration. Unlike the unrestricted theorem card, the action trace here is the policy action generated from the reward history, and the model-side trajectory law is supplied by `hzero` and `hcond` rather than assumed through the conclusion.

theorem historyStepKernelFamily_actionRewardPartialTrajectoryKernel_map_eq_historyFiltrationSucc_finitePairHistoryOfTrace_of_condDistrib {Omega : Type u} {Context : Type v} {State : Type w} {Action : Type x} [mOmega : MeasurableSpace Omega] [StandardBorelSpace Omega] [MeasurableSpace Context] [MeasurableSpace State] [MeasurableSpace Action] [MeasurableSingletonClass Action] [Countable Action] [Nonempty Omega] (mu : Measure Omega) [IsFiniteMeasure mu] (mu0 : Measure Rat) [IsProbabilityMeasure mu0] (rewardKernel : RewardKernel.MarkovRewardKernel (Prod Context Action) Rat) (policy : Nat -> Policy.MeasurablePolicy State Action) (context : (n : Nat) -> ((j : Finset.Iic n) -> Rat) -> Context) (state : (n : Nat) -> ((j : Finset.Iic n) -> Rat) -> State) (hcontext : forall n : Nat, Measurable (context n)) (hstate : forall n : Nat, Measurable (state n)) (defaultAction : Action) (reward : Omega -> RewardTrace Rat) (hreward : forall t : Nat, Measurable (fun omega : Omega => reward omega t)) (hzero : Measure.map (fun omega : Omega => reward omega 0) mu = mu0) (hcond : forall i : Nat, Filter.EventuallyEq (ae (mu.map (fun omega : Omega => Preorder.frestrictLe i (reward omega)))) (ProbabilityTheory.condDistrib (fun omega : Omega => reward omega (i + 1)) (fun omega : Omega => Preorder.frestrictLe i (reward omega)) mu) (RewardKernel.historyStepKernelFamily rewardKernel policy context state hcontext hstate i)) (i : Nat) : Filter.Eventually (fun omega : Omega => @Measure.map Omega ((j : Finset.Iic (i + 1)) -> Prod Action Rat) mOmega inferInstance (fun y : Omega => History.finitePairHistoryOfTrace (generatedActionFromRewardHistory policy state defaultAction reward y) (reward y) (i + 1)) (@ProbabilityTheory.condExpKernel Omega mOmega _ mu _ ((History.historyFiltrationSucc (generatedActionFromRewardHistory policy state defaultAction reward) reward (generatedActionFromRewardHistory_measurable (policy

An arbitrary measurable action/reward process has the full finite-pair `partialTraj` law at time `i` when its successor pair regular conditional distribution given the observed finite pair prefix is the configured history-step action/reward kernel. This is the unrestricted-action theorem-card route under a genuine upstream pair `condDistrib` law. It needs neither a generated-action equality nor a complete trajectory-law assumption.

theorem actionRewardPartialTrajectoryKernel_map_eq_historyFiltrationSucc_finitePairHistoryOfTrace_of_pair_condDistrib {Omega : Type u} {Context : Type v} {State : Type w} {Action : Type x} [mOmega : MeasurableSpace Omega] [StandardBorelSpace Omega] [MeasurableSpace Context] [MeasurableSpace State] [MeasurableSpace Action] [StandardBorelSpace Action] [MeasurableSingletonClass Action] [Countable Action] [Nonempty Omega] [Nonempty Action] (mu : Measure Omega) [IsFiniteMeasure mu] (action : Omega -> ActionTrace Action) (rewardKernel : RewardKernel.MarkovRewardKernel (Prod Context Action) Rat) (policy : Nat -> Policy.MeasurablePolicy State Action) (context : (n : Nat) -> ((j : Finset.Iic n) -> Rat) -> Context) (state : (n : Nat) -> ((j : Finset.Iic n) -> Rat) -> State) (hcontext : forall n : Nat, Measurable (context n)) (hstate : forall n : Nat, Measurable (state n)) (reward : Omega -> RewardTrace Rat) (haction : forall t : Nat, Measurable (fun omega : Omega => action omega t)) (hreward : forall t : Nat, Measurable (fun omega : Omega => reward omega t)) (i : Nat) (hcond : Filter.EventuallyEq (ae (mu.map (fun omega : Omega => History.finitePairHistoryOfTrace (action omega) (reward omega) i))) (ProbabilityTheory.condDistrib (fun omega : Omega => (action omega (i + 1), reward omega (i + 1))) (fun omega : Omega => History.finitePairHistoryOfTrace (action omega) (reward omega) i) mu) (RewardKernel.actionRewardHistoryStepKernelFamily rewardKernel policy (fun n history => context n (History.pairHistoryRewardProjection history)) (fun n history => state n (History.pairHistoryRewardProjection history)) (fun n : Nat => (hcontext n).comp (History.measurable_pairHistoryRewardProjection (Action

The zero-initialized successor centered-reward process is strongly adapted to the full action/reward history filtration for any measurable action trace.

theorem centeredRewardSuccProcess_stronglyAdapted_historyFiltrationSucc {Omega : Type u} {Context : Type v} {State : Type w} {Action : Type x} [mOmega : MeasurableSpace Omega] [MeasurableSpace Context] [MeasurableSpace State] [MeasurableSpace Action] [MeasurableSingletonClass Action] (action : Omega -> ActionTrace Action) (policy : Nat -> Policy.MeasurablePolicy State Action) (context : (n : Nat) -> ((j : Finset.Iic n) -> Rat) -> Context) (state : (n : Nat) -> ((j : Finset.Iic n) -> Rat) -> State) (hcontext : forall n : Nat, Measurable (context n)) (hstate : forall n : Nat, Measurable (state n)) (mean : Context -> Action -> Rat) (hmean : Measurable (fun pair : Prod Context Action => mean pair.1 pair.2)) (reward : Omega -> RewardTrace Rat) (haction : forall t : Nat, Measurable (fun omega : Omega => action omega t)) (hreward : forall t : Nat, Measurable (fun omega : Omega => reward omega t)) : let F := History.historyFiltrationSucc action reward haction hreward let Y : Nat -> Omega -> Real := fun t omega => match t with | 0 => 0 | i + 1 => (((reward omega (i + 1) - mean (context i (History.finiteRewardHistoryOfTrace (reward omega) i)) ((policy i).action (state i (History.finiteRewardHistoryOfTrace (reward omega) i))) : Rat) : Real)) StronglyAdapted F Y

An explicit successor-pair conditional distribution and the native trimmed-a.e. selected-variance bound yield the centered-reward conditional MGF witness for an arbitrary measurable action trace.

theorem centeredReward_succ_hasCondSubgaussianMGF_of_pair_condDistrib_of_ae_variance {Omega : Type u} {Context : Type v} {State : Type w} {Action : Type x} [mOmega : MeasurableSpace Omega] [StandardBorelSpace Omega] [MeasurableSpace Context] [MeasurableSpace State] [MeasurableSpace Action] [StandardBorelSpace Action] [MeasurableSingletonClass Action] [Countable Action] [Nonempty Omega] [Nonempty Action] (mu : Measure Omega) [IsFiniteMeasure mu] (action : Omega -> ActionTrace Action) (rewardKernel : RewardKernel.MarkovRewardKernel (Prod Context Action) Rat) (policy : Nat -> Policy.MeasurablePolicy State Action) (context : (n : Nat) -> ((j : Finset.Iic n) -> Rat) -> Context) (state : (n : Nat) -> ((j : Finset.Iic n) -> Rat) -> State) (hcontext : forall n : Nat, Measurable (context n)) (hstate : forall n : Nat, Measurable (state n)) (mean : Context -> Action -> Rat) (varianceProxy : Context -> Action -> NNReal) (law : RewardKernel.CenteredRewardKernelLaw rewardKernel mean varianceProxy) (hmean : Measurable (fun pair : Prod Context Action => mean pair.1 pair.2)) (reward : Omega -> RewardTrace Rat) (haction : forall t : Nat, Measurable (fun omega : Omega => action omega t)) (hreward : forall t : Nat, Measurable (fun omega : Omega => reward omega t)) (i : Nat) (c : NNReal) (hvariance : Filter.Eventually (fun omega : Omega => varianceProxy (context i (History.finiteRewardHistoryOfTrace (reward omega) i)) ((policy i).action (state i (History.finiteRewardHistoryOfTrace (reward omega) i))) <= c) (ae (mu.trim ((History.historyFiltrationSucc (mOmega

Compatibility wrapper for a pointwise selected-history variance ceiling. The core pair-conditional-law transfer only needs the corresponding trimmed-a.e. variance event.

theorem centeredReward_succ_hasCondSubgaussianMGF_of_pair_condDistrib {Omega : Type u} {Context : Type v} {State : Type w} {Action : Type x} [mOmega : MeasurableSpace Omega] [StandardBorelSpace Omega] [MeasurableSpace Context] [MeasurableSpace State] [MeasurableSpace Action] [StandardBorelSpace Action] [MeasurableSingletonClass Action] [Countable Action] [Nonempty Omega] [Nonempty Action] (mu : Measure Omega) [IsFiniteMeasure mu] (action : Omega -> ActionTrace Action) (rewardKernel : RewardKernel.MarkovRewardKernel (Prod Context Action) Rat) (policy : Nat -> Policy.MeasurablePolicy State Action) (context : (n : Nat) -> ((j : Finset.Iic n) -> Rat) -> Context) (state : (n : Nat) -> ((j : Finset.Iic n) -> Rat) -> State) (hcontext : forall n : Nat, Measurable (context n)) (hstate : forall n : Nat, Measurable (state n)) (mean : Context -> Action -> Rat) (varianceProxy : Context -> Action -> NNReal) (law : RewardKernel.CenteredRewardKernelLaw rewardKernel mean varianceProxy) (hmean : Measurable (fun pair : Prod Context Action => mean pair.1 pair.2)) (reward : Omega -> RewardTrace Rat) (haction : forall t : Nat, Measurable (fun omega : Omega => action omega t)) (hreward : forall t : Nat, Measurable (fun omega : Omega => reward omega t)) (i : Nat) (c : NNReal) (hvariance : forall history : ((j : Finset.Iic i) -> Rat), varianceProxy (context i history) ((policy i).action (state i history)) <= c) (hcond : Filter.EventuallyEq (ae (mu.map (fun omega : Omega => History.finitePairHistoryOfTrace (action omega) (reward omega) i))) (ProbabilityTheory.condDistrib (fun omega : Omega => (action omega (i + 1), reward omega (i + 1))) (fun omega : Omega => History.finitePairHistoryOfTrace (action omega) (reward omega) i) mu) (RewardKernel.actionRewardHistoryStepKernelFamily rewardKernel policy (fun n history => context n (History.pairHistoryRewardProjection history)) (fun n history => state n (History.pairHistoryRewardProjection history)) (fun n : Nat => (hcontext n).comp (History.measurable_pairHistoryRewardProjection (Action

Azuma-Hoeffding upper tail for an arbitrary measurable action/reward process whose every successor-pair conditional law is the configured history-step kernel.

theorem actionRewardHistoryStepKernelFamily_centeredRewardSuccProcess_sum_tail_ennreal_of_pair_condDistrib {Omega : Type u} {Context : Type v} {State : Type w} {Action : Type x} [mOmega : MeasurableSpace Omega] [StandardBorelSpace Omega] [MeasurableSpace Context] [MeasurableSpace State] [MeasurableSpace Action] [StandardBorelSpace Action] [MeasurableSingletonClass Action] [Countable Action] [Nonempty Omega] [Nonempty Action] (mu : Measure Omega) [IsProbabilityMeasure mu] (action : Omega -> ActionTrace Action) (rewardKernel : RewardKernel.MarkovRewardKernel (Prod Context Action) Rat) (policy : Nat -> Policy.MeasurablePolicy State Action) (context : (n : Nat) -> ((j : Finset.Iic n) -> Rat) -> Context) (state : (n : Nat) -> ((j : Finset.Iic n) -> Rat) -> State) (hcontext : forall n : Nat, Measurable (context n)) (hstate : forall n : Nat, Measurable (state n)) (mean : Context -> Action -> Rat) (varianceProxy : Context -> Action -> NNReal) (law : RewardKernel.CenteredRewardKernelLaw rewardKernel mean varianceProxy) (hmean : Measurable (fun pair : Prod Context Action => mean pair.1 pair.2)) (reward : Omega -> RewardTrace Rat) (haction : forall t : Nat, Measurable (fun omega : Omega => action omega t)) (hreward : forall t : Nat, Measurable (fun omega : Omega => reward omega t)) (hcondLaw : forall i : Nat, Filter.EventuallyEq (ae (mu.map (fun omega : Omega => History.finitePairHistoryOfTrace (action omega) (reward omega) i))) (ProbabilityTheory.condDistrib (fun omega : Omega => (action omega (i + 1), reward omega (i + 1))) (fun omega : Omega => History.finitePairHistoryOfTrace (action omega) (reward omega) i) mu) (RewardKernel.actionRewardHistoryStepKernelFamily rewardKernel policy (fun n history => context n (History.pairHistoryRewardProjection history)) (fun n history => state n (History.pairHistoryRewardProjection history)) (fun n : Nat => (hcontext n).comp (History.measurable_pairHistoryRewardProjection (Action

Finite-horizon Azuma-Hoeffding upper tail for an arbitrary measurable action/reward process. Only successor-pair laws and trimmed-a.e. selected-variance bounds at indices `i < n - 1` are required. This is the native contract consumed by the finite-sum conditional sub-Gaussian assembler.

theorem actionRewardHistoryStepKernelFamily_centeredRewardSuccProcess_sum_tail_ennreal_of_pair_condDistrib_on_horizon {Omega : Type u} {Context : Type v} {State : Type w} {Action : Type x} [mOmega : MeasurableSpace Omega] [StandardBorelSpace Omega] [MeasurableSpace Context] [MeasurableSpace State] [MeasurableSpace Action] [StandardBorelSpace Action] [MeasurableSingletonClass Action] [Countable Action] [Nonempty Omega] [Nonempty Action] (mu : Measure Omega) [IsProbabilityMeasure mu] (action : Omega -> ActionTrace Action) (rewardKernel : RewardKernel.MarkovRewardKernel (Prod Context Action) Rat) (policy : Nat -> Policy.MeasurablePolicy State Action) (context : (n : Nat) -> ((j : Finset.Iic n) -> Rat) -> Context) (state : (n : Nat) -> ((j : Finset.Iic n) -> Rat) -> State) (hcontext : forall n : Nat, Measurable (context n)) (hstate : forall n : Nat, Measurable (state n)) (mean : Context -> Action -> Rat) (varianceProxy : Context -> Action -> NNReal) (law : RewardKernel.CenteredRewardKernelLaw rewardKernel mean varianceProxy) (hmean : Measurable (fun pair : Prod Context Action => mean pair.1 pair.2)) (reward : Omega -> RewardTrace Rat) (haction : forall t : Nat, Measurable (fun omega : Omega => action omega t)) (hreward : forall t : Nat, Measurable (fun omega : Omega => reward omega t)) (n : Nat) (hcondLaw : forall i : Nat, i < n - 1 -> Filter.EventuallyEq (ae (mu.map (fun omega : Omega => History.finitePairHistoryOfTrace (action omega) (reward omega) i))) (ProbabilityTheory.condDistrib (fun omega : Omega => (action omega (i + 1), reward omega (i + 1))) (fun omega : Omega => History.finitePairHistoryOfTrace (action omega) (reward omega) i) mu) (RewardKernel.actionRewardHistoryStepKernelFamily rewardKernel policy (fun n history => context n (History.pairHistoryRewardProjection history)) (fun n history => state n (History.pairHistoryRewardProjection history)) (fun n : Nat => (hcontext n).comp (History.measurable_pairHistoryRewardProjection (Action

Canonical action/reward `trajMeasure` Azuma-Hoeffding upper tail. The Mathlib Ionescu--Tulcea trajectory law supplies every successor-pair conditional distribution. The caller only provides the centered reward kernel law and horizon-local selected-history variance ceilings.

theorem actionRewardHistoryStepKernelFamily_centeredRewardSuccProcess_sum_tail_ennreal_trajMeasure_on_horizon {Context : Type v} {State : Type w} {Action : Type x} [MeasurableSpace Context] [MeasurableSpace State] [MeasurableSpace Action] [StandardBorelSpace Action] [MeasurableSingletonClass Action] [Countable Action] [Nonempty Action] (mu0 : Measure (Prod Action Rat)) [IsProbabilityMeasure mu0] (rewardKernel : RewardKernel.MarkovRewardKernel (Prod Context Action) Rat) (policy : Nat -> Policy.MeasurablePolicy State Action) (context : (n : Nat) -> ((j : Finset.Iic n) -> Rat) -> Context) (state : (n : Nat) -> ((j : Finset.Iic n) -> Rat) -> State) (hcontext : forall n : Nat, Measurable (context n)) (hstate : forall n : Nat, Measurable (state n)) (mean : Context -> Action -> Rat) (varianceProxy : Context -> Action -> NNReal) (law : RewardKernel.CenteredRewardKernelLaw rewardKernel mean varianceProxy) (hmean : Measurable (fun pair : Prod Context Action => mean pair.1 pair.2)) (n : Nat) (varianceCeiling : Nat -> NNReal) (hvariance : forall i : Nat, i < n - 1 -> forall history : ((j : Finset.Iic i) -> Rat), varianceProxy (context i history) ((policy i).action (state i history)) <= varianceCeiling i) {eps : Real} (heps : 0 <= eps) : let pairContext : (i : Nat) -> ((j : Finset.Iic i) -> Prod Action Rat) -> Context