BanditRLProof.ConditionalExpectationReward

Turn a trimmed-a.e. zero conditional-kernel integral into a true conditional mean-zero statement. This is the generic kernel-facing bridge for `COND-EXPECT-REWARD`. The hard future work is to prove `h_kernel_zero` from a trajectory/kernel law; this wrapper only connects that law-shaped hypothesis to Mathlib's `condExp`.

theorem condExp_eq_zero_of_condExpKernel_integral_eq_zero {Omega : Type u} [mOmega : MeasurableSpace Omega] [StandardBorelSpace Omega] (mu : Measure Omega) [IsFiniteMeasure mu] (mcond : MeasurableSpace Omega) (hm : mcond <= mOmega) (X : Omega -> Real) (h_integrable : Integrable X mu) (h_kernel_zero : Filter.Eventually (fun omega : Omega => integral (ProbabilityTheory.condExpKernel (Ω

Monotonicity of the variance proxy in Mathlib's unconditional sub-Gaussian MGF predicate. This small helper lets history-selected kernel witnesses with proxy `c` feed a conditional theorem stated with a deterministic upper proxy `d`.

theorem hasSubgaussianMGF_mono_varianceProxy {Omega : Type u} [MeasurableSpace Omega] {mu : Measure Omega} {X : Omega -> Real} {c d : NNReal} (hcd : c <= d) (h : ProbabilityTheory.HasSubgaussianMGF X c mu) : ProbabilityTheory.HasSubgaussianMGF X d mu where

A random variable measurable in the conditioning sigma-algebra is frozen by the conditional-expectation kernel. The conclusion is a kernel equality on any countably generated target, rather than a singleton reconstruction on a countable target. The proof maps the diagonal composition-product identity for `condExpKernel` through `X` and then uses Mathlib's a.e. uniqueness theorem for finite kernels.

theorem condExpKernel_map_eq_deterministic_of_measurable {Omega : Type u} {Target : Type v} [mOmega : MeasurableSpace Omega] [StandardBorelSpace Omega] [mTarget : MeasurableSpace Target] [MeasurableSpace.CountablyGenerated Target] (mu : Measure Omega) [IsFiniteMeasure mu] (mcond : MeasurableSpace Omega) (hm : mcond <= mOmega) (X : Omega -> Target) (hX : @Measurable Omega Target mcond mTarget X) : Filter.EventuallyEq (ae (mu.trim hm)) (@ProbabilityTheory.Kernel.map Omega Omega mcond mOmega Target mTarget (@ProbabilityTheory.condExpKernel Omega mOmega inferInstance mu inferInstance mcond) X) (@ProbabilityTheory.Kernel.deterministic Omega Target mcond mTarget X hX)

Pointwise measure form of `condExpKernel_map_eq_deterministic_of_measurable`.

theorem condExpKernel_map_eq_dirac_of_measurable {Omega : Type u} {Target : Type v} [mOmega : MeasurableSpace Omega] [StandardBorelSpace Omega] [mTarget : MeasurableSpace Target] [MeasurableSpace.CountablyGenerated Target] (mu : Measure Omega) [IsFiniteMeasure mu] (mcond : MeasurableSpace Omega) (hm : mcond <= mOmega) (X : Omega -> Target) (hX : @Measurable Omega Target mcond mTarget X) : Filter.Eventually (fun omega => @Measure.map Omega Target mOmega mTarget X (@ProbabilityTheory.condExpKernel Omega mOmega inferInstance mu inferInstance mcond omega) = @Measure.dirac Target mTarget (X omega)) (ae (mu.trim hm))

Convert a `condDistrib` law into a `condExpKernel` pushforward law on a countable target. Mathlib supplies eventwise equality between regular conditional distributions and `condExpKernel` pushforwards. This wrapper packages those singleton equalities into a measure equality when the target type is countable. It is a local bridge from canonical `condDistrib` trajectory laws toward the `condExpKernel` map-law consumers below; it does not itself construct the trajectory law.

theorem condExpKernel_map_eq_of_condDistrib_ae_eq_countable {Omega : Type u} {Target : Type v} {Condition : Type w} [mOmega : MeasurableSpace Omega] [StandardBorelSpace Omega] [Nonempty Omega] [mTarget : MeasurableSpace Target] [StandardBorelSpace Target] [Nonempty Target] [MeasurableSingletonClass Target] [Countable Target] [mCondition : MeasurableSpace Condition] (mu : Measure Omega) [IsFiniteMeasure mu] (X : Omega -> Target) (Y : Omega -> Condition) (hX : @Measurable Omega Target mOmega mTarget X) (hY : @Measurable Omega Condition mOmega mCondition Y) (kernel : ProbabilityTheory.Kernel Condition Target) (hcond : Filter.EventuallyEq (ae (mu.map Y)) (ProbabilityTheory.condDistrib X Y mu) kernel) : Filter.Eventually (fun omega : Omega => @Measure.map Omega Target mOmega mTarget X (@ProbabilityTheory.condExpKernel Omega mOmega _ mu _ (mCondition.comap Y) omega) = kernel (Y omega)) (ae mu)

Trim-a.e. form of the countable-target `condDistrib` to `condExpKernel.map` bridge. The ordinary bridge gives equality almost everywhere for the ambient measure. For each target singleton, both event-probability functions are measurable in the conditioning sigma-algebra. Mathlib's `ae_eq_trim_of_measurable` therefore upgrades those scalar equalities to the trimmed measure, after which countability reconstructs equality of the pushed-forward measures.

theorem condExpKernel_map_eq_of_condDistrib_ae_eq_countable_trim {Omega : Type u} {Target : Type v} {Condition : Type w} [mOmega : MeasurableSpace Omega] [StandardBorelSpace Omega] [Nonempty Omega] [mTarget : MeasurableSpace Target] [StandardBorelSpace Target] [Nonempty Target] [MeasurableSingletonClass Target] [Countable Target] [mCondition : MeasurableSpace Condition] (mu : Measure Omega) [IsFiniteMeasure mu] (X : Omega -> Target) (Y : Omega -> Condition) (hX : @Measurable Omega Target mOmega mTarget X) (hY : @Measurable Omega Condition mOmega mCondition Y) (kernel : ProbabilityTheory.Kernel Condition Target) (hcond : Filter.EventuallyEq (ae (mu.map Y)) (ProbabilityTheory.condDistrib X Y mu) kernel) : Filter.Eventually (fun omega : Omega => @Measure.map Omega Target mOmega mTarget X (@ProbabilityTheory.condExpKernel Omega mOmega _ mu _ (mCondition.comap Y) omega) = kernel (Y omega)) (ae (mu.trim hY.comap_le))

Convert a real-valued `condDistrib` law into a trimmed `condExpKernel.map` law without assuming `Countable Real`. The proof first obtains equality on every rational left ray `Iic q`, upgrades those scalar equalities to the trimmed measure using conditioning-space measurability, and then reconstructs the full Borel measure by Mathlib's countable rational-ray pi-system induction.

theorem condExpKernel_map_eq_of_condDistrib_ae_eq_real_trim {Omega : Type u} {Condition : Type v} [mOmega : MeasurableSpace Omega] [StandardBorelSpace Omega] [Nonempty Omega] [mCondition : MeasurableSpace Condition] (mu : Measure Omega) [IsFiniteMeasure mu] (X : Omega -> Real) (Y : Omega -> Condition) (hX : @Measurable Omega Real mOmega inferInstance X) (hY : @Measurable Omega Condition mOmega mCondition Y) (kernel : ProbabilityTheory.Kernel Condition Real) [ProbabilityTheory.IsMarkovKernel kernel] (hcond : Filter.EventuallyEq (ae (mu.map Y)) (ProbabilityTheory.condDistrib X Y mu) kernel) : Filter.Eventually (fun omega : Omega => @Measure.map Omega Real mOmega inferInstance X (@ProbabilityTheory.condExpKernel Omega mOmega _ mu _ (mCondition.comap Y) omega) = kernel (Y omega)) (ae (mu.trim hY.comap_le))

If a measurable pushforward law is a Dirac measure, the original random variable is a.e. constant. This is the small Mathlib bridge used to turn selected-action `condExpKernel.map = dirac ...` laws into the conditional a.e. action equality needed by the next-pair split-law route.

theorem eventuallyEq_const_of_map_eq_dirac {Omega : Type u} {Target : Type v} [mOmega : MeasurableSpace Omega] [mTarget : MeasurableSpace Target] [MeasurableSingletonClass Target] (mu : Measure Omega) (X : Omega -> Target) (x : Target) (hX : @Measurable Omega Target mOmega mTarget X) (hmap : @Measure.map Omega Target mOmega mTarget X mu = Measure.dirac x) : Filter.EventuallyEq (ae mu) X (fun _omega : Omega => x)

Build a pair pushforward law from a deterministic action side and a reward pushforward law. This is the measure-level split helper behind the next-pair route, stripped of filtration-specific hypotheses. It is useful both for canonical trajectory laws and for later ambient laws once the relevant `condExpKernel` has been identified.

theorem pair_map_eq_map_prod_mk_of_action_ae_eq_const_reward_map_eq {Omega : Type u} {Action : Type v} {Reward : Type w} [mOmega : MeasurableSpace Omega] [MeasurableSpace Action] [MeasurableSpace Reward] (mu : Measure Omega) (nextAction : Omega -> Action) (nextReward : Omega -> Reward) (selectedAction : Action) (selectedReward : Measure Reward) (h_nextReward : @Measurable Omega Reward mOmega inferInstance nextReward) (h_action_ae : Filter.EventuallyEq (ae mu) nextAction (fun _omega : Omega => selectedAction)) (h_reward_map_eq : @Measure.map Omega Reward mOmega inferInstance nextReward mu = selectedReward) : @Measure.map Omega (Prod Action Reward) mOmega inferInstance (fun omega : Omega => (nextAction omega, nextReward omega)) mu = Measure.map (Prod.mk selectedAction) selectedReward

Build a conditional next-pair product law from split action and reward laws. For each conditioning point, the action side freezes a.e. under the `condExpKernel`, while the reward side supplies the selected reward measure. This is the ambient `condExpKernel` form of `pair_map_eq_map_prod_mk_of_action_ae_eq_const_reward_map_eq`.

theorem condExpKernel_pair_map_eq_map_prod_mk_of_action_ae_reward_map_eq {Omega : Type u} {Action : Type v} {Reward : Type w} [mOmega : MeasurableSpace Omega] [StandardBorelSpace Omega] [MeasurableSpace Action] [MeasurableSpace Reward] (mu : Measure Omega) [IsFiniteMeasure mu] (F : Filtration Nat mOmega) (i : Nat) (nextAction : Omega -> Action) (nextReward : Omega -> Reward) (selectedAction : Omega -> Action) (selectedReward : Omega -> Measure Reward) (h_nextReward : @Measurable Omega Reward mOmega inferInstance nextReward) (h_action_ae : Filter.Eventually (fun omega : Omega => Filter.EventuallyEq (ae (@ProbabilityTheory.condExpKernel Omega mOmega _ mu _ (F i) omega)) nextAction (fun _y : Omega => selectedAction omega)) (ae (mu.trim (F.le i)))) (h_reward_map_eq : Filter.Eventually (fun omega : Omega => @Measure.map Omega Reward mOmega inferInstance nextReward (@ProbabilityTheory.condExpKernel Omega mOmega _ mu _ (F i) omega) = selectedReward omega) (ae (mu.trim (F.le i)))) : Filter.Eventually (fun omega : Omega => @Measure.map Omega (Prod Action Reward) mOmega inferInstance (fun y : Omega => (nextAction y, nextReward y)) (@ProbabilityTheory.condExpKernel Omega mOmega _ mu _ (F i) omega) = Measure.map (Prod.mk (selectedAction omega)) (selectedReward omega)) (ae (mu.trim (F.le i)))

Canonical reward-only `trajMeasure` selected-reward law in `condExpKernel.map` form. This applies Mathlib's `Kernel.condDistrib_trajMeasure` theorem directly to `RewardKernel.historyStepKernelFamily`, then uses the local countable-target `condDistrib`-to-`condExpKernel.map` bridge. Unlike the action/reward pair trajectory route below, the canonical process here has only reward coordinates, so its finite prefix is already the reward history consumed by the policy, context, and state maps.

theorem historyStepKernelFamily_selectedMeasure_condExpKernel_map_trajMeasure {Context : Type x} {State : Type u} {Action : Type v} {Reward : Type w} [MeasurableSpace Context] [MeasurableSpace State] [MeasurableSpace Action] [MeasurableSpace Reward] [StandardBorelSpace Reward] [StandardBorelSpace ((t : Nat) -> Reward)] [Nonempty Reward] [Nonempty ((t : Nat) -> Reward)] [MeasurableSingletonClass Reward] [Countable Reward] (mu0 : Measure Reward) [MeasureTheory.IsProbabilityMeasure mu0] (rewardKernel : RewardKernel.MarkovRewardKernel (Prod Context Action) Reward) (policy : Nat -> Policy.MeasurablePolicy State Action) (context : (n : Nat) -> ((i : Finset.Iic n) -> Reward) -> Context) (state : (n : Nat) -> ((i : Finset.Iic n) -> Reward) -> State) (hcontext : forall n : Nat, Measurable (context n)) (hstate : forall n : Nat, Measurable (state n)) (n : Nat) : let stepKernel := RewardKernel.historyStepKernelFamily rewardKernel policy context state hcontext hstate let trajMeasure := ProbabilityTheory.Kernel.trajMeasure (X

Trim-a.e. canonical reward-only `trajMeasure` selected-reward law. This is the source-facing strengthening of `historyStepKernelFamily_selectedMeasure_condExpKernel_map_trajMeasure`. It uses the trim-aware countable-target bridge, so the conclusion is stated on the finite reward-prefix conditioning sigma-algebra itself.

theorem historyStepKernelFamily_selectedMeasure_condExpKernel_map_trajMeasure_trim {Context : Type x} {State : Type u} {Action : Type v} {Reward : Type w} [MeasurableSpace Context] [MeasurableSpace State] [MeasurableSpace Action] [MeasurableSpace Reward] [StandardBorelSpace Reward] [StandardBorelSpace ((t : Nat) -> Reward)] [Nonempty Reward] [Nonempty ((t : Nat) -> Reward)] [MeasurableSingletonClass Reward] [Countable Reward] (mu0 : Measure Reward) [MeasureTheory.IsProbabilityMeasure mu0] (rewardKernel : RewardKernel.MarkovRewardKernel (Prod Context Action) Reward) (policy : Nat -> Policy.MeasurablePolicy State Action) (context : (n : Nat) -> ((i : Finset.Iic n) -> Reward) -> Context) (state : (n : Nat) -> ((i : Finset.Iic n) -> Reward) -> State) (hcontext : forall n : Nat, Measurable (context n)) (hstate : forall n : Nat, Measurable (state n)) (n : Nat) : let stepKernel := RewardKernel.historyStepKernelFamily rewardKernel policy context state hcontext hstate let trajMeasure := ProbabilityTheory.Kernel.trajMeasure (X

Identify an ambient reward trace with the canonical reward-only trajectory from its initial marginal and successor conditional distributions. The complete-law step is supplied by the foundation-level reward-trace uniqueness theorem. This wrapper specializes its kernel family to `RewardKernel.historyStepKernelFamily`, exposing the recursive process contract needed by the ambient selected-reward transport below.

theorem historyStepKernelFamily_identDistrib_trajMeasure_of_condDistrib {Omega : Type u} {Context : Type v} {State : Type w} {Action : Type x} {Reward : Type*} [mOmega : MeasurableSpace Omega] [MeasurableSpace Context] [MeasurableSpace State] [MeasurableSpace Action] [MeasurableSpace Reward] [StandardBorelSpace Reward] [Nonempty Reward] (mu : Measure Omega) [IsFiniteMeasure mu] (mu0 : Measure Reward) [IsProbabilityMeasure mu0] (rewardKernel : RewardKernel.MarkovRewardKernel (Prod Context Action) Reward) (policy : Nat -> Policy.MeasurablePolicy State Action) (context : (n : Nat) -> ((i : Finset.Iic n) -> Reward) -> Context) (state : (n : Nat) -> ((i : Finset.Iic n) -> Reward) -> State) (hcontext : forall n : Nat, Measurable (context n)) (hstate : forall n : Nat, Measurable (state n)) (reward : Omega -> ((t : Nat) -> Reward)) (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, ProbabilityTheory.condDistrib (fun omega : Omega => reward omega (i + 1)) (fun omega : Omega => Preorder.frestrictLe i (reward omega)) mu =ᵐ[mu.map (fun omega : Omega => Preorder.frestrictLe i (reward omega))] (RewardKernel.historyStepKernelFamily rewardKernel policy context state hcontext hstate i)) : ProbabilityTheory.IdentDistrib reward id mu (ProbabilityTheory.Kernel.trajMeasure (X

Transport the canonical reward-only selected-reward law to an ambient reward trace with the same complete distribution. The `IdentDistrib` contract is strictly upstream of the conditional law used by the source layer. Composing it with the finite-prefix/next-coordinate map transports the relevant joint law from Mathlib's canonical `trajMeasure`. The canonical `condDistrib_trajMeasure` factorization and disintegration uniqueness then recover the ambient conditional distribution, after which the countable-target trim bridge yields the requested `condExpKernel.map` law.

theorem historyStepKernelFamily_selectedMeasure_condExpKernel_map_of_identDistrib_trajMeasure_trim {Omega : Type u} {Context : Type v} {State : Type w} {Action : Type x} {Reward : Type*} [mOmega : MeasurableSpace Omega] [StandardBorelSpace Omega] [MeasurableSpace Context] [MeasurableSpace State] [MeasurableSpace Action] [MeasurableSpace Reward] [StandardBorelSpace Reward] [StandardBorelSpace ((t : Nat) -> Reward)] [Nonempty Omega] [Nonempty Reward] [Nonempty ((t : Nat) -> Reward)] [MeasurableSingletonClass Reward] [Countable Reward] (mu : Measure Omega) [IsFiniteMeasure mu] (mu0 : Measure Reward) [IsProbabilityMeasure mu0] (rewardKernel : RewardKernel.MarkovRewardKernel (Prod Context Action) Reward) (policy : Nat -> Policy.MeasurablePolicy State Action) (context : (n : Nat) -> ((i : Finset.Iic n) -> Reward) -> Context) (state : (n : Nat) -> ((i : Finset.Iic n) -> Reward) -> State) (hcontext : forall n : Nat, Measurable (context n)) (hstate : forall n : Nat, Measurable (state n)) (reward : Omega -> ((t : Nat) -> Reward)) (hreward : forall t : Nat, Measurable (fun omega : Omega => reward omega t)) (hident : ProbabilityTheory.IdentDistrib reward id mu (ProbabilityTheory.Kernel.trajMeasure (X

Canonical `trajMeasure` next-pair law in `condExpKernel.map` form. This is the pair-coordinate analogue of `actionRewardHistoryStepKernelFamily_reward_condExpKernel_map_trajMeasure`: on Mathlib's canonical action/reward trajectory measure, conditioning on the finite pair prefix and pushing `condExpKernel` forward by the next pair coordinate recovers the configured history-step kernel.

theorem actionRewardHistoryStepKernelFamily_pair_condExpKernel_map_trajMeasure {Context : Type x} {State : Type u} {Action : Type v} {Reward : Type w} [MeasurableSpace Context] [MeasurableSpace State] [MeasurableSpace Action] [MeasurableSpace Reward] [StandardBorelSpace (Prod Action Reward)] [StandardBorelSpace ((t : Nat) -> Prod Action Reward)] [Nonempty (Prod Action Reward)] [Nonempty ((t : Nat) -> Prod Action Reward)] [MeasurableSingletonClass (Prod Action Reward)] [Countable (Prod Action Reward)] (mu0 : Measure (Prod Action Reward)) [MeasureTheory.IsProbabilityMeasure mu0] (rewardKernel : RewardKernel.MarkovRewardKernel (Prod Context Action) Reward) (policy : Nat -> Policy.MeasurablePolicy State Action) (context : (n : Nat) -> ((i : Finset.Iic n) -> Prod Action Reward) -> Context) (state : (n : Nat) -> ((i : Finset.Iic n) -> Prod Action Reward) -> State) (hcontext : forall n : Nat, Measurable (context n)) (hstate : forall n : Nat, Measurable (state n)) (n : Nat) : let stepKernel := RewardKernel.actionRewardHistoryStepKernelFamily rewardKernel policy context state hcontext hstate let trajMeasure := ProbabilityTheory.Kernel.trajMeasure (X

Canonical `trajMeasure` next-action law in `condExpKernel.map` form. This is the action-coordinate projection of `actionRewardHistoryStepKernelFamily_pair_condExpKernel_map_trajMeasure`: on Mathlib's canonical action/reward trajectory measure, conditioning on the finite pair prefix and pushing `condExpKernel` forward by the next action coordinate recovers the Dirac law at the policy-selected action.

theorem actionRewardHistoryStepKernelFamily_action_condExpKernel_map_trajMeasure {Context : Type x} {State : Type u} {Action : Type v} {Reward : Type w} [MeasurableSpace Context] [MeasurableSpace State] [MeasurableSpace Action] [MeasurableSpace Reward] [StandardBorelSpace (Prod Action Reward)] [StandardBorelSpace ((t : Nat) -> Prod Action Reward)] [Nonempty (Prod Action Reward)] [Nonempty ((t : Nat) -> Prod Action Reward)] [MeasurableSingletonClass (Prod Action Reward)] [Countable (Prod Action Reward)] (mu0 : Measure (Prod Action Reward)) [MeasureTheory.IsProbabilityMeasure mu0] (rewardKernel : RewardKernel.MarkovRewardKernel (Prod Context Action) Reward) (policy : Nat -> Policy.MeasurablePolicy State Action) (context : (n : Nat) -> ((i : Finset.Iic n) -> Prod Action Reward) -> Context) (state : (n : Nat) -> ((i : Finset.Iic n) -> Prod Action Reward) -> State) (hcontext : forall n : Nat, Measurable (context n)) (hstate : forall n : Nat, Measurable (state n)) (n : Nat) : let stepKernel := RewardKernel.actionRewardHistoryStepKernelFamily rewardKernel policy context state hcontext hstate let trajMeasure := ProbabilityTheory.Kernel.trajMeasure (X

Canonical `trajMeasure` action-marginal law in `condExpKernel.map` form via the action-coordinate `condDistrib` route. This is the action-side analogue of `actionRewardHistoryStepKernelFamily_reward_condExpKernel_map_trajMeasure`: on the canonical action/reward trajectory measure, conditioning on the finite pair prefix and pushing `condExpKernel` forward by the next action coordinate recovers the `Prod.fst` marginal of the configured history-step kernel. The target countability contract is on `Action`, not on the whole `(Action × Reward)` pair.

theorem actionRewardHistoryStepKernelFamily_actionMarginal_condExpKernel_map_trajMeasure {Context : Type x} {State : Type u} {Action : Type v} {Reward : Type w} [MeasurableSpace Context] [MeasurableSpace State] [MeasurableSpace Action] [MeasurableSpace Reward] [StandardBorelSpace (Prod Action Reward)] [StandardBorelSpace Action] [StandardBorelSpace ((t : Nat) -> Prod Action Reward)] [Nonempty (Prod Action Reward)] [Nonempty Action] [Nonempty ((t : Nat) -> Prod Action Reward)] [MeasurableSingletonClass Action] [Countable Action] (mu0 : Measure (Prod Action Reward)) [MeasureTheory.IsProbabilityMeasure mu0] (rewardKernel : RewardKernel.MarkovRewardKernel (Prod Context Action) Reward) (policy : Nat -> Policy.MeasurablePolicy State Action) (context : (n : Nat) -> ((i : Finset.Iic n) -> Prod Action Reward) -> Context) (state : (n : Nat) -> ((i : Finset.Iic n) -> Prod Action Reward) -> State) (hcontext : forall n : Nat, Measurable (context n)) (hstate : forall n : Nat, Measurable (state n)) (n : Nat) : let stepKernel := RewardKernel.actionRewardHistoryStepKernelFamily rewardKernel policy context state hcontext hstate let trajMeasure := ProbabilityTheory.Kernel.trajMeasure (X

Canonical `trajMeasure` selected-action law in `condExpKernel.map` form via the action-coordinate `condDistrib` route. This has the same selected-action Dirac conclusion as `actionRewardHistoryStepKernelFamily_action_condExpKernel_map_trajMeasure`, but obtains it by applying the countable-target `condExpKernel_map_eq_of_condDistrib_ae_eq_countable` bridge directly to the next action coordinate. Thus the target countability contract is on `Action`, not on the whole `(Action × Reward)` pair.

theorem actionRewardHistoryStepKernelFamily_selectedAction_condExpKernel_map_trajMeasure {Context : Type x} {State : Type u} {Action : Type v} {Reward : Type w} [MeasurableSpace Context] [MeasurableSpace State] [MeasurableSpace Action] [MeasurableSpace Reward] [StandardBorelSpace (Prod Action Reward)] [StandardBorelSpace Action] [StandardBorelSpace ((t : Nat) -> Prod Action Reward)] [Nonempty (Prod Action Reward)] [Nonempty Action] [Nonempty ((t : Nat) -> Prod Action Reward)] [MeasurableSingletonClass Action] [Countable Action] (mu0 : Measure (Prod Action Reward)) [MeasureTheory.IsProbabilityMeasure mu0] (rewardKernel : RewardKernel.MarkovRewardKernel (Prod Context Action) Reward) (policy : Nat -> Policy.MeasurablePolicy State Action) (context : (n : Nat) -> ((i : Finset.Iic n) -> Prod Action Reward) -> Context) (state : (n : Nat) -> ((i : Finset.Iic n) -> Prod Action Reward) -> State) (hcontext : forall n : Nat, Measurable (context n)) (hstate : forall n : Nat, Measurable (state n)) (n : Nat) : let stepKernel := RewardKernel.actionRewardHistoryStepKernelFamily rewardKernel policy context state hcontext hstate let trajMeasure := ProbabilityTheory.Kernel.trajMeasure (X

Canonical `trajMeasure` selected-action law in conditional a.e. form. The previous theorem identifies the pushforward of the conditional kernel by the next action coordinate as a Dirac law. This wrapper turns that Dirac pushforward equality into the `Filter.EventuallyEq` shape required by the next-pair split-law route.

theorem actionRewardHistoryStepKernelFamily_selectedAction_condExpKernel_ae_trajMeasure {Context : Type x} {State : Type u} {Action : Type v} {Reward : Type w} [MeasurableSpace Context] [MeasurableSpace State] [MeasurableSpace Action] [MeasurableSpace Reward] [StandardBorelSpace (Prod Action Reward)] [StandardBorelSpace Action] [StandardBorelSpace ((t : Nat) -> Prod Action Reward)] [Nonempty (Prod Action Reward)] [Nonempty Action] [Nonempty ((t : Nat) -> Prod Action Reward)] [MeasurableSingletonClass Action] [Countable Action] (mu0 : Measure (Prod Action Reward)) [MeasureTheory.IsProbabilityMeasure mu0] (rewardKernel : RewardKernel.MarkovRewardKernel (Prod Context Action) Reward) (policy : Nat -> Policy.MeasurablePolicy State Action) (context : (n : Nat) -> ((i : Finset.Iic n) -> Prod Action Reward) -> Context) (state : (n : Nat) -> ((i : Finset.Iic n) -> Prod Action Reward) -> State) (hcontext : forall n : Nat, Measurable (context n)) (hstate : forall n : Nat, Measurable (state n)) (n : Nat) : let stepKernel := RewardKernel.actionRewardHistoryStepKernelFamily rewardKernel policy context state hcontext hstate let trajMeasure := ProbabilityTheory.Kernel.trajMeasure (X

Canonical `trajMeasure` extension-map law in `condExpKernel.map` form. This pushes `actionRewardHistoryStepKernelFamily_pair_condExpKernel_map_trajMeasure` through `History.extendPairHistorySucc`, yielding the one-step `RewardKernel.actionRewardPartialTrajectoryKernel` surface used by the extension-map consumers. It remains a canonical `trajMeasure` theorem; it does not transport an arbitrary ambient process.

theorem actionRewardPartialTrajectoryKernel_extend_condExpKernel_map_trajMeasure {Context : Type x} {State : Type u} {Action : Type v} {Reward : Type w} [MeasurableSpace Context] [MeasurableSpace State] [MeasurableSpace Action] [MeasurableSpace Reward] [StandardBorelSpace (Prod Action Reward)] [StandardBorelSpace ((t : Nat) -> Prod Action Reward)] [Nonempty (Prod Action Reward)] [Nonempty ((t : Nat) -> Prod Action Reward)] [MeasurableSingletonClass (Prod Action Reward)] [Countable (Prod Action Reward)] (mu0 : Measure (Prod Action Reward)) [MeasureTheory.IsProbabilityMeasure mu0] (rewardKernel : RewardKernel.MarkovRewardKernel (Prod Context Action) Reward) (policy : Nat -> Policy.MeasurablePolicy State Action) (context : (n : Nat) -> ((i : Finset.Iic n) -> Prod Action Reward) -> Context) (state : (n : Nat) -> ((i : Finset.Iic n) -> Prod Action Reward) -> State) (hcontext : forall n : Nat, Measurable (context n)) (hstate : forall n : Nat, Measurable (state n)) (n : Nat) : let stepKernel := RewardKernel.actionRewardHistoryStepKernelFamily rewardKernel policy context state hcontext hstate let trajMeasure := ProbabilityTheory.Kernel.trajMeasure (X

Canonical `trajMeasure` reward law in `condExpKernel.map` form. This specializes `condExpKernel_map_eq_of_condDistrib_ae_eq_countable` to the Mathlib Ionescu-Tulcea trajectory measure generated by `RewardKernel.actionRewardHistoryStepKernelFamily`. It converts the canonical next-reward `condDistrib` law into the `condExpKernel` pushforward-map shape used by the project-local conditional reward consumers.

theorem actionRewardHistoryStepKernelFamily_reward_condExpKernel_map_trajMeasure {Context : Type x} {State : Type u} {Action : Type v} {Reward : Type w} [MeasurableSpace Context] [MeasurableSpace State] [MeasurableSpace Action] [MeasurableSpace Reward] [StandardBorelSpace (Prod Action Reward)] [StandardBorelSpace Reward] [StandardBorelSpace ((t : Nat) -> Prod Action Reward)] [Nonempty (Prod Action Reward)] [Nonempty Reward] [Nonempty ((t : Nat) -> Prod Action Reward)] [MeasurableSingletonClass Reward] [Countable Reward] (mu0 : Measure (Prod Action Reward)) [MeasureTheory.IsProbabilityMeasure mu0] (rewardKernel : RewardKernel.MarkovRewardKernel (Prod Context Action) Reward) (policy : Nat -> Policy.MeasurablePolicy State Action) (context : (n : Nat) -> ((i : Finset.Iic n) -> Prod Action Reward) -> Context) (state : (n : Nat) -> ((i : Finset.Iic n) -> Prod Action Reward) -> State) (hcontext : forall n : Nat, Measurable (context n)) (hstate : forall n : Nat, Measurable (state n)) (n : Nat) : let stepKernel := RewardKernel.actionRewardHistoryStepKernelFamily rewardKernel policy context state hcontext hstate let trajMeasure := ProbabilityTheory.Kernel.trajMeasure (X

Canonical `trajMeasure` selected-reward law in `condExpKernel.map` form. This rewrites `actionRewardHistoryStepKernelFamily_reward_condExpKernel_map_trajMeasure` through `RewardKernel.actionRewardHistoryStepKernelFamily_reward_map`, yielding the selected context/action reward measure directly at the finite pair prefix.

theorem actionRewardHistoryStepKernelFamily_selectedMeasure_condExpKernel_map_trajMeasure {Context : Type x} {State : Type u} {Action : Type v} {Reward : Type w} [MeasurableSpace Context] [MeasurableSpace State] [MeasurableSpace Action] [MeasurableSpace Reward] [StandardBorelSpace (Prod Action Reward)] [StandardBorelSpace Reward] [StandardBorelSpace ((t : Nat) -> Prod Action Reward)] [Nonempty (Prod Action Reward)] [Nonempty Reward] [Nonempty ((t : Nat) -> Prod Action Reward)] [MeasurableSingletonClass Reward] [Countable Reward] (mu0 : Measure (Prod Action Reward)) [MeasureTheory.IsProbabilityMeasure mu0] (rewardKernel : RewardKernel.MarkovRewardKernel (Prod Context Action) Reward) (policy : Nat -> Policy.MeasurablePolicy State Action) (context : (n : Nat) -> ((i : Finset.Iic n) -> Prod Action Reward) -> Context) (state : (n : Nat) -> ((i : Finset.Iic n) -> Prod Action Reward) -> State) (hcontext : forall n : Nat, Measurable (context n)) (hstate : forall n : Nat, Measurable (state n)) (n : Nat) : let stepKernel := RewardKernel.actionRewardHistoryStepKernelFamily rewardKernel policy context state hcontext hstate let trajMeasure := ProbabilityTheory.Kernel.trajMeasure (X

Canonical `trajMeasure` selected-reward law in `History.finitePairHistoryOfTrace` notation. This is the same canonical Ionescu-Tulcea conditional reward law as `actionRewardHistoryStepKernelFamily_selectedMeasure_condExpKernel_map_trajMeasure`; the theorem only exposes the finite pair history prefix in the notation used by the bandit-history API.

theorem actionRewardHistoryStepKernelFamily_selectedMeasure_finitePairHistoryOfTrace_condExpKernel_map_trajMeasure {Context : Type x} {State : Type u} {Action : Type v} {Reward : Type w} [MeasurableSpace Context] [MeasurableSpace State] [MeasurableSpace Action] [MeasurableSpace Reward] [StandardBorelSpace (Prod Action Reward)] [StandardBorelSpace Reward] [StandardBorelSpace ((t : Nat) -> Prod Action Reward)] [Nonempty (Prod Action Reward)] [Nonempty Reward] [Nonempty ((t : Nat) -> Prod Action Reward)] [MeasurableSingletonClass Reward] [Countable Reward] (mu0 : Measure (Prod Action Reward)) [MeasureTheory.IsProbabilityMeasure mu0] (rewardKernel : RewardKernel.MarkovRewardKernel (Prod Context Action) Reward) (policy : Nat -> Policy.MeasurablePolicy State Action) (context : (n : Nat) -> ((i : Finset.Iic n) -> Prod Action Reward) -> Context) (state : (n : Nat) -> ((i : Finset.Iic n) -> Prod Action Reward) -> State) (hcontext : forall n : Nat, Measurable (context n)) (hstate : forall n : Nat, Measurable (state n)) (n : Nat) : let stepKernel := RewardKernel.actionRewardHistoryStepKernelFamily rewardKernel policy context state hcontext hstate let trajMeasure := ProbabilityTheory.Kernel.trajMeasure (X

Canonical `trajMeasure` selected-reward law with reward-history context/state extractors. This specializes the finite-pair-history notation wrapper to pair-context and pair-state maps obtained by projecting finite pair histories to reward histories. It is still a canonical Ionescu-Tulcea theorem, not an ambient `History.historyFiltrationSucc` transport result.

theorem actionRewardHistoryStepKernelFamily_selectedMeasure_rewardHistoryOfTrace_condExpKernel_map_trajMeasure {Context : Type x} {State : Type u} {Action : Type v} [MeasurableSpace Context] [MeasurableSpace State] [MeasurableSpace Action] [StandardBorelSpace (Prod Action Rat)] [StandardBorelSpace Rat] [StandardBorelSpace ((t : Nat) -> Prod Action Rat)] [Nonempty (Prod Action Rat)] [Nonempty Rat] [Nonempty ((t : Nat) -> Prod Action Rat)] [MeasurableSingletonClass Rat] [Countable Rat] (mu0 : Measure (Prod Action Rat)) [MeasureTheory.IsProbabilityMeasure mu0] (rewardKernel : RewardKernel.MarkovRewardKernel (Prod Context Action) Rat) (policy : Nat -> Policy.MeasurablePolicy State Action) (context : (n : Nat) -> ((i : Finset.Iic n) -> Rat) -> Context) (state : (n : Nat) -> ((i : Finset.Iic n) -> Rat) -> State) (hcontext : forall n : Nat, Measurable (context n)) (hstate : forall n : Nat, Measurable (state n)) (n : Nat) : let pairContext : (n : Nat) -> ((i : Finset.Iic n) -> Prod Action Rat) -> Context

Canonical `trajMeasure` next-pair law rebuilt from split inputs. This theorem verifies the split route on Mathlib's canonical Ionescu-Tulcea trajectory measure: the selected-action conditional a.e. law and the selected-reward pushforward law combine to recover the full `RewardKernel.actionRewardHistoryStepKernelFamily` next-pair law. Unlike the direct pair-coordinate `condDistrib` bridge, this route only needs separate countability of `Action` and `Reward`.

theorem actionRewardHistoryStepKernelFamily_pair_condExpKernel_map_trajMeasure_of_selectedAction_ae_selectedMeasure {Context : Type x} {State : Type u} {Action : Type v} {Reward : Type w} [MeasurableSpace Context] [MeasurableSpace State] [MeasurableSpace Action] [MeasurableSpace Reward] [StandardBorelSpace (Prod Action Reward)] [StandardBorelSpace Action] [StandardBorelSpace Reward] [StandardBorelSpace ((t : Nat) -> Prod Action Reward)] [Nonempty (Prod Action Reward)] [Nonempty Action] [Nonempty Reward] [Nonempty ((t : Nat) -> Prod Action Reward)] [MeasurableSingletonClass Action] [Countable Action] [MeasurableSingletonClass Reward] [Countable Reward] (mu0 : Measure (Prod Action Reward)) [MeasureTheory.IsProbabilityMeasure mu0] (rewardKernel : RewardKernel.MarkovRewardKernel (Prod Context Action) Reward) (policy : Nat -> Policy.MeasurablePolicy State Action) (context : (n : Nat) -> ((i : Finset.Iic n) -> Prod Action Reward) -> Context) (state : (n : Nat) -> ((i : Finset.Iic n) -> Prod Action Reward) -> State) (hcontext : forall n : Nat, Measurable (context n)) (hstate : forall n : Nat, Measurable (state n)) (n : Nat) : let stepKernel := RewardKernel.actionRewardHistoryStepKernelFamily rewardKernel policy context state hcontext hstate let trajMeasure := ProbabilityTheory.Kernel.trajMeasure (X

Generic `condExpKernel` map-law consumer for conditional sub-Gaussianity. If the conditional kernel pushed forward by `X` is trim-a.e. a target measure whose identity random variable is sub-Gaussian with deterministic proxy `c`, then `X` is conditionally sub-Gaussian. The target MGF bound also supplies the global exponential-integrability field: `Measure.integrable_comp_iff` combines the target laws' pointwise integrability with their common deterministic MGF bound over the finite trim measure.

theorem hasCondSubgaussianMGF_of_condExpKernel_map_eq {Omega : Type u} [mOmega : MeasurableSpace Omega] [StandardBorelSpace Omega] (mu : Measure Omega) [IsFiniteMeasure mu] (mcond : MeasurableSpace Omega) (hm : mcond <= mOmega) (X : Omega -> Real) (c : NNReal) (hX : @Measurable Omega Real mOmega inferInstance X) (target : Omega -> Measure Real) (h_kernel_map_eq : Filter.Eventually (fun omega : Omega => @Measure.map Omega Real mOmega inferInstance X (@ProbabilityTheory.condExpKernel Omega mOmega _ mu _ mcond omega) = target omega) (ae (mu.trim hm))) (h_target_subG : Filter.Eventually (fun omega : Omega => ProbabilityTheory.HasSubgaussianMGF (fun z : Real => z) c (target omega)) (ae (mu.trim hm))) : ProbabilityTheory.HasCondSubgaussianMGF mcond hm X c mu

Center a real-valued conditional reward law by a quantity measurable in the conditioning sigma-algebra. The conditional kernel freezes the center at the conditioning point. The resulting residual pushforward is therefore the centered pushforward of the supplied reward law, which can be consumed by the generic conditional sub-Gaussian map-law theorem.

theorem hasCondSubgaussianMGF_centered_of_condExpKernel_map_eq {Omega : Type u} [mOmega : MeasurableSpace Omega] [StandardBorelSpace Omega] (mu : Measure Omega) [IsFiniteMeasure mu] (mcond : MeasurableSpace Omega) (hm : mcond <= mOmega) (X center : Omega -> Real) (c : NNReal) (hX : @Measurable Omega Real mOmega inferInstance X) (hcenter : @Measurable Omega Real mcond inferInstance center) (target : Omega -> Measure Real) (h_kernel_map_eq : Filter.Eventually (fun omega : Omega => @Measure.map Omega Real mOmega inferInstance X (@ProbabilityTheory.condExpKernel Omega mOmega _ mu _ mcond omega) = target omega) (ae (mu.trim hm))) (h_target_subG : Filter.Eventually (fun omega : Omega => ProbabilityTheory.HasSubgaussianMGF (fun z : Real => z - center omega) c (target omega)) (ae (mu.trim hm))) : ProbabilityTheory.HasCondSubgaussianMGF mcond hm (fun omega => X omega - center omega) c mu

Transport conditional sub-Gaussianity across equal conditioning measurable spaces. The two inclusion proofs are propositionally irrelevant.

theorem hasCondSubgaussianMGF_congr_measurableSpace {Omega : Type u} [mOmega : MeasurableSpace Omega] [StandardBorelSpace Omega] (mu : Measure Omega) [IsFiniteMeasure mu] (mcond mcond' : MeasurableSpace Omega) (hm : mcond <= mOmega) (hm' : mcond' <= mOmega) (hspaces : mcond = mcond') (X : Omega -> Real) (c : NNReal) (h : ProbabilityTheory.HasCondSubgaussianMGF (mΩ

Centered-reward specialization of `condExp_eq_zero_of_condExpKernel_integral_eq_zero`. The statement matches the succ-indexed shape used by Mathlib's conditional tail API: the reward at `i + 1` is conditioned on filtration level `i`.

theorem centeredReward_succ_condExp_eq_zero_of_condExpKernel_integral_eq_zero {Omega : Type u} {K : Nat} [mOmega : MeasurableSpace Omega] [StandardBorelSpace Omega] (mu : Measure Omega) [IsFiniteMeasure mu] (F : Filtration Nat mOmega) (model : FiniteBanditModel K) (reward : Omega -> RewardTrace Rat) (b : Fin K) (i : Nat) (h_integrable : Integrable (fun omega : Omega => (((reward omega (i + 1) - model.mean b : Rat) : Real))) mu) (h_kernel_zero : Filter.Eventually (fun omega : Omega => integral (ProbabilityTheory.condExpKernel (Ω

Consumer bridge from a trajectory-law-shaped conditional-kernel identification to ordinary conditional mean zero. The hypothesis `h_kernel_eq` is intentionally explicit: it is the future `condExpKernel`/history-step reward-law identification, already reduced to the centered integral shape needed here. The theorem then uses the compiled `RewardKernel.historyStepKernelFamily_centeredReward_integral_eq_zero` leaf and the generic `condExpKernel` bridge above.

theorem condExp_eq_zero_of_condExpKernel_integral_eq_historyStepKernel_centeredReward {Omega : Type u} {Context : Type v} {State : Type w} {Action : Type x} [mOmega : MeasurableSpace Omega] [StandardBorelSpace Omega] [MeasurableSpace Context] [MeasurableSpace State] [MeasurableSpace Action] (mu : Measure Omega) [IsFiniteMeasure mu] (mcond : MeasurableSpace Omega) (hm : mcond <= mOmega) (rewardKernel : RewardKernel.MarkovRewardKernel (Context × Action) Rat) (policy : Nat -> Policy.MeasurablePolicy State Action) (context : (n : Nat) -> ((i : Finset.Iic n) -> Rat) -> Context) (state : (n : Nat) -> ((i : 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) (n : Nat) (history : Omega -> ((i : Finset.Iic n) -> Rat)) (X : Omega -> Real) (h_integrable : Integrable X mu) (h_kernel_eq : Filter.Eventually (fun omega : Omega => integral (ProbabilityTheory.condExpKernel (Ω

Succ-indexed selected-reward specialization of `condExp_eq_zero_of_condExpKernel_integral_eq_historyStepKernel_centeredReward`. The centered variable uses the history-selected context/action mean. The only law-identification input is `h_kernel_eq`; constructing that equality from a `partialTraj` trajectory measure is still a separate missing leaf.

theorem centeredReward_succ_condExp_eq_zero_of_historyStepKernelFamily_condExpKernel_integral_eq {Omega : Type u} {Context : Type v} {State : Type w} {Action : Type x} [mOmega : MeasurableSpace Omega] [StandardBorelSpace Omega] [MeasurableSpace Context] [MeasurableSpace State] [MeasurableSpace Action] (mu : Measure Omega) [IsFiniteMeasure mu] (F : Filtration Nat mOmega) (rewardKernel : RewardKernel.MarkovRewardKernel (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) (reward : Omega -> RewardTrace Rat) (i : Nat) (history : Omega -> ((j : Finset.Iic i) -> Rat)) (h_integrable : Integrable (fun omega : Omega => (((reward omega (i + 1) - mean (context i (history omega)) ((policy i).action (state i (history omega))) : Rat) : Real))) mu) (h_kernel_eq : Filter.Eventually (fun omega : Omega => integral (ProbabilityTheory.condExpKernel (Ω

Map-law consumer for the history-step conditional mean-zero route. Compared with the integral-equality consumer above, this theorem assumes a more structural reward-law identification: trim-a.e., the conditional kernel pushed forward by the next-reward coordinate is the corresponding `historyStepKernelFamily` reward law. The separate `h_kernel_X_eq` hypothesis records the usual "past is frozen under conditioning" obligation needed to replace the actual target variable by the centered function with the outer history fixed at `omega`. This still does not construct the `partialTraj`/`condExpKernel` identity; it only consumes a map-level version of that identity.

theorem condExp_eq_zero_of_condExpKernel_map_eq_historyStepKernel_centeredReward {Omega : Type u} {Context : Type v} {State : Type w} {Action : Type x} [mOmega : MeasurableSpace Omega] [StandardBorelSpace Omega] [MeasurableSpace Context] [MeasurableSpace State] [MeasurableSpace Action] (mu : Measure Omega) [IsFiniteMeasure mu] (mcond : MeasurableSpace Omega) (hm : mcond <= mOmega) (rewardKernel : RewardKernel.MarkovRewardKernel (Context × Action) Rat) (policy : Nat -> Policy.MeasurablePolicy State Action) (context : (n : Nat) -> ((i : Finset.Iic n) -> Rat) -> Context) (state : (n : Nat) -> ((i : 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) (n : Nat) (history : Omega -> ((i : Finset.Iic n) -> Rat)) (nextReward : Omega -> Rat) (X : Omega -> Real) (h_nextReward : @Measurable Omega Rat mOmega inferInstance nextReward) (h_integrable : Integrable X mu) (h_kernel_map_eq : Filter.Eventually (fun omega : Omega => @Measure.map Omega Rat mOmega inferInstance nextReward (ProbabilityTheory.condExpKernel (Ω

Map-law consumer for the history-step conditional sub-Gaussian route. This is the MGF analogue of `condExp_eq_zero_of_condExpKernel_map_eq_historyStepKernel_centeredReward`. It keeps two contracts explicit: `h_kernel_X_eq` freezes the history-dependent centering under the conditional kernel, and `h_variance_le` bounds the history-selected variance proxy by the deterministic proxy `c` required by Mathlib's `HasCondSubgaussianMGF`. Exponential integrability is generated by the generic integrated target-law transfer above.

theorem hasCondSubgaussianMGF_of_condExpKernel_map_eq_historyStepKernel_centeredReward {Omega : Type u} {Context : Type v} {State : Type w} {Action : Type x} [mOmega : MeasurableSpace Omega] [StandardBorelSpace Omega] [MeasurableSpace Context] [MeasurableSpace State] [MeasurableSpace Action] (mu : Measure Omega) [IsFiniteMeasure mu] (mcond : MeasurableSpace Omega) (hm : mcond <= mOmega) (rewardKernel : RewardKernel.MarkovRewardKernel (Prod Context Action) Rat) (policy : Nat -> Policy.MeasurablePolicy State Action) (context : (n : Nat) -> ((i : Finset.Iic n) -> Rat) -> Context) (state : (n : Nat) -> ((i : 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) (n : Nat) (history : Omega -> ((i : Finset.Iic n) -> Rat)) (nextReward : Omega -> Rat) (X : Omega -> Real) (c : NNReal) (h_nextReward : @Measurable Omega Rat mOmega inferInstance nextReward) (hX : @Measurable Omega Real mOmega inferInstance X) (h_kernel_map_eq : Filter.Eventually (fun omega : Omega => @Measure.map Omega Rat mOmega inferInstance nextReward (@ProbabilityTheory.condExpKernel Omega mOmega _ mu _ mcond omega) = RewardKernel.historyStepKernelFamily rewardKernel policy context state hcontext hstate n (history omega)) (ae (mu.trim hm))) (h_kernel_X_eq : Filter.Eventually (fun omega : Omega => Filter.EventuallyEq (ae (@ProbabilityTheory.condExpKernel Omega mOmega _ mu _ mcond omega)) X (fun y : Omega => (((nextReward y - mean (context n (history omega)) ((policy n).action (state n (history omega))) : Rat) : Real)))) (ae (mu.trim hm))) (h_variance_le : Filter.Eventually (fun omega : Omega => varianceProxy (context n (history omega)) ((policy n).action (state n (history omega))) <= c) (ae (mu.trim hm))) : ProbabilityTheory.HasCondSubgaussianMGF mcond hm X c mu

Succ-indexed selected-reward specialization of the conditional sub-Gaussian map-law consumer. This is the MGF analogue of `centeredReward_succ_condExp_eq_zero_of_historyStepKernelFamily_condExpKernel_map_eq`. It keeps measurability and deterministic variance domination explicit; the kernel-side sub-Gaussian law now also discharges exponential integrability via the integrated target-law transfer.

theorem centeredReward_succ_hasCondSubgaussianMGF_of_historyStepKernelFamily_condExpKernel_map_eq {Omega : Type u} {Context : Type v} {State : Type w} {Action : Type x} [mOmega : MeasurableSpace Omega] [StandardBorelSpace Omega] [MeasurableSpace Context] [MeasurableSpace State] [MeasurableSpace Action] (mu : Measure Omega) [IsFiniteMeasure mu] (F : Filtration Nat mOmega) (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) (reward : Omega -> RewardTrace Rat) (i : Nat) (history : Omega -> ((j : Finset.Iic i) -> Rat)) (c : NNReal) (h_reward : @Measurable Omega Rat mOmega inferInstance (fun omega : Omega => reward omega (i + 1))) (h_centered_meas : @Measurable Omega Real mOmega inferInstance (fun omega : Omega => (((reward omega (i + 1) - mean (context i (history omega)) ((policy i).action (state i (history omega))) : Rat) : Real)))) (h_kernel_map_eq : Filter.Eventually (fun omega : Omega => @Measure.map Omega Rat mOmega inferInstance (fun y : Omega => reward y (i + 1)) (ProbabilityTheory.condExpKernel (Ω

Event-level frozen-past canary for conditional-expectation kernels. If an event is measurable in the conditioning sigma-algebra, then trim-a.e. the conditional kernel assigns its real mass as the event indicator. This is the 0/1 event support fact used to freeze countable-valued past summaries below.

theorem condExpKernel_event_real_eq_indicator_of_measurableSet {Omega : Type u} [mOmega : MeasurableSpace Omega] [StandardBorelSpace Omega] (mu : Measure Omega) [IsFiniteMeasure mu] (mcond : MeasurableSpace Omega) (hm : mcond <= mOmega) (s : Set Omega) (hs : @MeasurableSet Omega mcond s) : Filter.Eventually (fun omega : Omega => (@ProbabilityTheory.condExpKernel Omega mOmega _ mu _ mcond omega).real s = Set.indicator s (fun _omega : Omega => (1 : Real)) omega) (ae (mu.trim hm))

Countable-valued frozen-past theorem for conditional-expectation kernels. Any countable-valued random variable measurable in the conditioning sigma-algebra is trim-a.e. constant under the corresponding conditional kernel. This packages the event-level 0/1 fact over all singleton fibers.

theorem condExpKernel_ae_eq_const_of_countable_measurable {Omega : Type u} {A : Type v} [mOmega : MeasurableSpace Omega] [StandardBorelSpace Omega] [MeasurableSpace A] [MeasurableSingletonClass A] [Countable A] (mu : Measure Omega) [IsFiniteMeasure mu] (mcond : MeasurableSpace Omega) (hm : mcond <= mOmega) (Y : Omega -> A) (hY : @Measurable Omega A mcond inferInstance Y) : Filter.Eventually (fun omega : Omega => Filter.EventuallyEq (ae (@ProbabilityTheory.condExpKernel Omega mOmega _ mu _ mcond omega)) Y (fun _y : Omega => Y omega)) (ae (mu.trim hm))

Canonical `trajMeasure` full finite-prefix law in `condExpKernel.map` form. The earlier canonical extension-map theorem states the law for the deterministic extension of the frozen prefix by the random next pair. This wrapper uses the standard `condExpKernel` frozen-prefix property for the conditioning map `Preorder.frestrictLe n`, then rewrites that extension map back to the full `Preorder.frestrictLe (n + 1)` prefix under the conditional kernel.

theorem actionRewardPartialTrajectoryKernel_prefix_condExpKernel_map_trajMeasure {Context : Type x} {State : Type u} {Action : Type v} {Reward : Type w} [MeasurableSpace Context] [MeasurableSpace State] [MeasurableSpace Action] [MeasurableSpace Reward] [StandardBorelSpace (Prod Action Reward)] [StandardBorelSpace ((t : Nat) -> Prod Action Reward)] [Nonempty (Prod Action Reward)] [Nonempty ((t : Nat) -> Prod Action Reward)] [MeasurableSingletonClass (Prod Action Reward)] [Countable (Prod Action Reward)] (mu0 : Measure (Prod Action Reward)) [MeasureTheory.IsProbabilityMeasure mu0] (rewardKernel : RewardKernel.MarkovRewardKernel (Prod Context Action) Reward) (policy : Nat -> Policy.MeasurablePolicy State Action) (context : (n : Nat) -> ((i : Finset.Iic n) -> Prod Action Reward) -> Context) (state : (n : Nat) -> ((i : Finset.Iic n) -> Prod Action Reward) -> State) (hcontext : forall n : Nat, Measurable (context n)) (hstate : forall n : Nat, Measurable (state n)) (n : Nat) : let stepKernel := RewardKernel.actionRewardHistoryStepKernelFamily rewardKernel policy context state hcontext hstate let trajMeasure := ProbabilityTheory.Kernel.trajMeasure (X

Canonical `trajMeasure` full finite-pair-history law in the project's concrete `History.finitePairHistoryOfTrace` notation. This is a notation-alignment wrapper around `actionRewardPartialTrajectoryKernel_extend_condExpKernel_map_trajMeasure`: the ambient theorem-card still needs a transport from canonical `trajMeasure` to an arbitrary generated process.

theorem actionRewardPartialTrajectoryKernel_finitePairHistoryOfTrace_condExpKernel_map_trajMeasure {Context : Type x} {State : Type u} {Action : Type v} {Reward : Type w} [MeasurableSpace Context] [MeasurableSpace State] [MeasurableSpace Action] [MeasurableSpace Reward] [StandardBorelSpace (Prod Action Reward)] [StandardBorelSpace ((t : Nat) -> Prod Action Reward)] [Nonempty (Prod Action Reward)] [Nonempty ((t : Nat) -> Prod Action Reward)] [MeasurableSingletonClass (Prod Action Reward)] [Countable (Prod Action Reward)] (mu0 : Measure (Prod Action Reward)) [MeasureTheory.IsProbabilityMeasure mu0] (rewardKernel : RewardKernel.MarkovRewardKernel (Prod Context Action) Reward) (policy : Nat -> Policy.MeasurablePolicy State Action) (context : (n : Nat) -> ((i : Finset.Iic n) -> Prod Action Reward) -> Context) (state : (n : Nat) -> ((i : Finset.Iic n) -> Prod Action Reward) -> State) (hcontext : forall n : Nat, Measurable (context n)) (hstate : forall n : Nat, Measurable (state n)) (n : Nat) : let stepKernel := RewardKernel.actionRewardHistoryStepKernelFamily rewardKernel policy context state hcontext hstate let trajMeasure := ProbabilityTheory.Kernel.trajMeasure (X

Action-freezing hookup for the next-pair split-law route. If the next action is measurable at filtration level `F i`, the conditional kernel freezes it. If that frozen action is also trim-a.e. the policy-selected action for the finite pair history, this supplies exactly the conditional a.e. action equality consumed by `actionRewardHistoryStepKernelFamily_pair_map_eq_of_action_ae_eq_policy_reward_map_eq`. It does not prove the predictability or policy-generation equality hypotheses.

theorem action_condExpKernel_ae_eq_policy_of_measurable_of_policy_eq {Omega : Type u} {State : Type w} {Action : Type x} [mOmega : MeasurableSpace Omega] [StandardBorelSpace Omega] [MeasurableSpace State] [MeasurableSpace Action] [MeasurableSingletonClass Action] [Countable Action] (mu : Measure Omega) [IsFiniteMeasure mu] (F : Filtration Nat mOmega) (policy : Nat -> Policy.MeasurablePolicy State Action) (pairState : (n : Nat) -> ((j : Finset.Iic n) -> Prod Action Rat) -> State) (action : Omega -> ActionTrace Action) (i : Nat) (pairHistory : Omega -> ((j : Finset.Iic i) -> Prod Action Rat)) (h_action_next_meas : @Measurable Omega Action (F i) inferInstance (fun omega : Omega => action omega (i + 1))) (h_action_policy_eq : Filter.Eventually (fun omega : Omega => action omega (i + 1) = (policy i).action (pairState i (pairHistory omega))) (ae (mu.trim (F.le i)))) : Filter.Eventually (fun omega : Omega => Filter.EventuallyEq (ae (@ProbabilityTheory.condExpKernel Omega mOmega _ mu _ (F i) omega)) (fun y : Omega => action y (i + 1)) (fun _y : Omega => (policy i).action (pairState i (pairHistory omega)))) (ae (mu.trim (F.le i)))

Pair-history measurability hookup for the action side of the next-pair split. If the finite pair history is visible at `F i`, the pair-state extractor is measurable, and the next action is pointwise the policy action selected from that pair state, then the previous action-freezing theorem supplies the conditional a.e. action equality consumed by the split-law builder.

theorem action_condExpKernel_ae_eq_policy_of_pairHistory_measurable_of_action_eq {Omega : Type u} {State : Type w} {Action : Type x} [mOmega : MeasurableSpace Omega] [StandardBorelSpace Omega] [MeasurableSpace State] [MeasurableSpace Action] [MeasurableSingletonClass Action] [Countable Action] (mu : Measure Omega) [IsFiniteMeasure mu] (F : Filtration Nat mOmega) (policy : Nat -> Policy.MeasurablePolicy State Action) (pairState : (n : Nat) -> ((j : Finset.Iic n) -> Prod Action Rat) -> State) (hpairState : forall n : Nat, Measurable (pairState n)) (action : Omega -> ActionTrace Action) (i : Nat) (pairHistory : Omega -> ((j : Finset.Iic i) -> Prod Action Rat)) (h_pairHistory_meas : @Measurable Omega ((j : Finset.Iic i) -> Prod Action Rat) (F i) inferInstance pairHistory) (h_action_eq : (fun omega : Omega => action omega (i + 1)) = (fun omega : Omega => (policy i).action (pairState i (pairHistory omega)))) : Filter.Eventually (fun omega : Omega => Filter.EventuallyEq (ae (@ProbabilityTheory.condExpKernel Omega mOmega _ mu _ (F i) omega)) (fun y : Omega => action y (i + 1)) (fun _y : Omega => (policy i).action (pairState i (pairHistory omega)))) (ae (mu.trim (F.le i)))

Generated-history specialization of the action side of the next-pair split. For `History.historyFiltrationSucc`, the finite action/reward pair prefix up to `i` is visible. Therefore a pointwise policy-generation equality for the next action supplies the conditional action a.e. side condition required by the split-law builder. The reward-coordinate law remains a separate input.

theorem action_condExpKernel_ae_eq_policy_historyFiltrationSucc_finitePairHistoryOfTrace_of_action_eq {Omega : Type u} {State : Type w} {Action : Type x} [mOmega : MeasurableSpace Omega] [StandardBorelSpace Omega] [MeasurableSpace State] [MeasurableSpace Action] [MeasurableSingletonClass Action] [Countable Action] (mu : Measure Omega) [IsFiniteMeasure mu] (policy : Nat -> Policy.MeasurablePolicy State Action) (pairState : (n : Nat) -> ((j : Finset.Iic n) -> Prod Action Rat) -> State) (hpairState : forall n : Nat, Measurable (pairState n)) (action : Omega -> ActionTrace Action) (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) (h_action_eq : (fun omega : Omega => action omega (i + 1)) = (fun omega : Omega => (policy i).action (pairState i (History.finitePairHistoryOfTrace (action omega) (reward omega) i)))) : Filter.Eventually (fun omega : Omega => Filter.EventuallyEq (ae (@ProbabilityTheory.condExpKernel Omega mOmega _ mu _ ((History.historyFiltrationSucc action reward haction hreward) i) omega)) (fun y : Omega => action y (i + 1)) (fun _y : Omega => (policy i).action (pairState i (History.finitePairHistoryOfTrace (action omega) (reward omega) i)))) (ae (mu.trim ((History.historyFiltrationSucc action reward haction hreward).le i)))

Generated-trace source for the action side of the next-pair split. If the action trace is the shifted policy-generated trace from finite action/reward pair histories, the pointwise policy-generation equality required by `..._finitePairHistoryOfTrace_of_action_eq` follows from the definition of `Policy.generatedActionTraceSucc`.

theorem action_condExpKernel_ae_eq_policy_historyFiltrationSucc_finitePairHistoryOfTrace_of_generatedActionTraceSucc {Omega : Type u} {State : Type w} {Action : Type x} [mOmega : MeasurableSpace Omega] [StandardBorelSpace Omega] [MeasurableSpace State] [MeasurableSpace Action] [MeasurableSingletonClass Action] [Countable Action] (mu : Measure Omega) [IsFiniteMeasure mu] (policy : Nat -> Policy.MeasurablePolicy State Action) (pairState : (n : Nat) -> ((j : Finset.Iic n) -> Prod Action Rat) -> State) (hpairState : forall n : Nat, Measurable (pairState n)) (defaultAction : Action) (action : Omega -> ActionTrace Action) (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) (h_action_generated : action = Policy.generatedActionTraceSucc policy (fun n omega => pairState n (History.finitePairHistoryOfTrace (action omega) (reward omega) n)) defaultAction) : Filter.Eventually (fun omega : Omega => Filter.EventuallyEq (ae (@ProbabilityTheory.condExpKernel Omega mOmega _ mu _ ((History.historyFiltrationSucc action reward haction hreward) i) omega)) (fun y : Omega => action y (i + 1)) (fun _y : Omega => (policy i).action (pairState i (History.finitePairHistoryOfTrace (action omega) (reward omega) i)))) (ae (mu.trim ((History.historyFiltrationSucc action reward haction hreward).le i)))

Reward-law rewrite for the next-pair split route. Some future trajectory/source theorem may naturally identify the conditional reward law using the actual next action at the conditioning point. If that actual action is trim-a.e. equal to the policy-selected action, this adapter rewrites the reward-coordinate map law into the policy-selected shape consumed by `actionRewardHistoryStepKernelFamily_pair_map_eq_of_action_ae_eq_policy_reward_map_eq`.

theorem reward_condExpKernel_map_eq_selected_policy_of_action_eq {Omega : Type u} {Context : Type v} {State : Type w} {Action : Type x} [mOmega : MeasurableSpace Omega] [StandardBorelSpace Omega] [MeasurableSpace Context] [MeasurableSpace State] [MeasurableSpace Action] (mu : Measure Omega) [IsFiniteMeasure mu] (F : Filtration Nat mOmega) (rewardKernel : RewardKernel.MarkovRewardKernel (Prod Context Action) Rat) (policy : Nat -> Policy.MeasurablePolicy State Action) (pairContext : (n : Nat) -> ((j : Finset.Iic n) -> Prod Action Rat) -> Context) (pairState : (n : Nat) -> ((j : Finset.Iic n) -> Prod Action Rat) -> State) (action : Omega -> ActionTrace Action) (reward : Omega -> RewardTrace Rat) (i : Nat) (pairHistory : Omega -> ((j : Finset.Iic i) -> Prod Action Rat)) (h_action_policy_eq : Filter.Eventually (fun omega : Omega => action omega (i + 1) = (policy i).action (pairState i (pairHistory omega))) (ae (mu.trim (F.le i)))) (h_reward_map_eq_actual_action : Filter.Eventually (fun omega : Omega => @Measure.map Omega Rat mOmega inferInstance (fun y : Omega => reward y (i + 1)) (@ProbabilityTheory.condExpKernel Omega mOmega _ mu _ (F i) omega) = RewardKernel.selectedMeasure rewardKernel (pairContext i (pairHistory omega)) (action omega (i + 1))) (ae (mu.trim (F.le i)))) : Filter.Eventually (fun omega : Omega => @Measure.map Omega Rat mOmega inferInstance (fun y : Omega => reward y (i + 1)) (@ProbabilityTheory.condExpKernel Omega mOmega _ mu _ (F i) omega) = RewardKernel.selectedMeasure rewardKernel (pairContext i (pairHistory omega)) ((policy i).action (pairState i (pairHistory omega)))) (ae (mu.trim (F.le i)))

Actual-action pair-law marginalization for the reward-coordinate route. Future trajectory-law work may identify, under the conditional kernel, the pair `(actual next action, next reward)` as a fixed-action product of the selected reward law. Mapping that pair law through `Prod.snd` gives the actual-action reward-coordinate map law consumed by the generated-action route below.

theorem reward_condExpKernel_map_eq_selected_actual_action_of_pair_map_eq {Omega : Type u} {Context : Type v} {Action : Type x} [mOmega : MeasurableSpace Omega] [StandardBorelSpace Omega] [MeasurableSpace Context] [MeasurableSpace Action] (mu : Measure Omega) [IsFiniteMeasure mu] (F : Filtration Nat mOmega) (rewardKernel : RewardKernel.MarkovRewardKernel (Prod Context Action) Rat) (pairContext : (n : Nat) -> ((j : Finset.Iic n) -> Prod Action Rat) -> Context) (action : Omega -> ActionTrace Action) (reward : Omega -> RewardTrace Rat) (i : Nat) (pairHistory : Omega -> ((j : Finset.Iic i) -> Prod Action Rat)) (h_reward_next : @Measurable Omega Rat mOmega inferInstance (fun omega : Omega => reward omega (i + 1))) (h_pair_map_eq_actual_action : Filter.Eventually (fun omega : Omega => @Measure.map Omega (Prod Action Rat) mOmega inferInstance (fun y : Omega => (action omega (i + 1), reward y (i + 1))) (@ProbabilityTheory.condExpKernel Omega mOmega _ mu _ (F i) omega) = Measure.map (Prod.mk (action omega (i + 1))) (RewardKernel.selectedMeasure rewardKernel (pairContext i (pairHistory omega)) (action omega (i + 1)))) (ae (mu.trim (F.le i)))) : Filter.Eventually (fun omega : Omega => @Measure.map Omega Rat mOmega inferInstance (fun y : Omega => reward y (i + 1)) (@ProbabilityTheory.condExpKernel Omega mOmega _ mu _ (F i) omega) = RewardKernel.selectedMeasure rewardKernel (pairContext i (pairHistory omega)) (action omega (i + 1))) (ae (mu.trim (F.le i)))

Generated-action reward-map source for the random next-pair product law. The shifted generated-action trace supplies the conditional action a.e. equality, while the hypothesis supplies the reward-coordinate selected-measure law. The conclusion is the fully random next-pair product law consumed by the trajectory-facing random-pair route.

theorem random_pair_condExpKernel_map_eq_actual_action_of_generatedActionTraceSucc_reward_map_eq_actual_action {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] (mu : Measure Omega) [IsFiniteMeasure mu] (rewardKernel : RewardKernel.MarkovRewardKernel (Prod Context Action) Rat) (policy : Nat -> Policy.MeasurablePolicy State Action) (pairContext : (n : Nat) -> ((j : Finset.Iic n) -> Prod Action Rat) -> Context) (pairState : (n : Nat) -> ((j : Finset.Iic n) -> Prod Action Rat) -> State) (hpairState : forall n : Nat, Measurable (pairState n)) (defaultAction : Action) (action : Omega -> ActionTrace Action) (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) (h_action_generated : action = Policy.generatedActionTraceSucc policy (fun n omega => pairState n (History.finitePairHistoryOfTrace (action omega) (reward omega) n)) defaultAction) (h_reward_map_eq_actual_action : Filter.Eventually (fun omega : Omega => @Measure.map Omega Rat mOmega inferInstance (fun y : Omega => reward y (i + 1)) (@ProbabilityTheory.condExpKernel Omega mOmega _ mu _ ((History.historyFiltrationSucc action reward haction hreward) i) omega) = RewardKernel.selectedMeasure rewardKernel (pairContext i (History.finitePairHistoryOfTrace (action omega) (reward omega) i)) (action omega (i + 1))) (ae (mu.trim ((History.historyFiltrationSucc action reward haction hreward).le i)))) : Filter.Eventually (fun omega : Omega => @Measure.map Omega (Prod Action Rat) mOmega inferInstance (fun y : Omega => (action y (i + 1), reward y (i + 1))) (@ProbabilityTheory.condExpKernel Omega mOmega _ mu _ ((History.historyFiltrationSucc action reward haction hreward) i) omega) = Measure.map (Prod.mk (action omega (i + 1))) (RewardKernel.selectedMeasure rewardKernel (pairContext i (History.finitePairHistoryOfTrace (action omega) (reward omega) i)) (action omega (i + 1)))) (ae (mu.trim ((History.historyFiltrationSucc action reward haction hreward).le i)))

Freeze the action coordinate in a random next-pair law. A trajectory source may identify the conditional law of the fully random pair `(action y (i+1), reward y (i+1))`, while the actual-action marginal route expects the action coordinate frozen at the conditioning point `omega`. Under the shifted generated-action trace, both action coordinates are conditionally equal to the same policy-selected action, so Mathlib's `Measure.map_congr` transfers the random-pair map law to the frozen-action map law.

theorem pair_condExpKernel_map_eq_frozen_actual_action_of_generatedActionTraceSucc_random_pair_map_eq {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] (mu : Measure Omega) [IsFiniteMeasure mu] (rewardKernel : RewardKernel.MarkovRewardKernel (Prod Context Action) Rat) (policy : Nat -> Policy.MeasurablePolicy State Action) (pairContext : (n : Nat) -> ((j : Finset.Iic n) -> Prod Action Rat) -> Context) (pairState : (n : Nat) -> ((j : Finset.Iic n) -> Prod Action Rat) -> State) (hpairState : forall n : Nat, Measurable (pairState n)) (defaultAction : Action) (action : Omega -> ActionTrace Action) (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) (h_action_generated : action = Policy.generatedActionTraceSucc policy (fun n omega => pairState n (History.finitePairHistoryOfTrace (action omega) (reward omega) n)) defaultAction) (h_random_pair_map_eq_actual_action : Filter.Eventually (fun omega : Omega => @Measure.map Omega (Prod Action Rat) mOmega inferInstance (fun y : Omega => (action y (i + 1), reward y (i + 1))) (@ProbabilityTheory.condExpKernel Omega mOmega _ mu _ ((History.historyFiltrationSucc action reward haction hreward) i) omega) = Measure.map (Prod.mk (action omega (i + 1))) (RewardKernel.selectedMeasure rewardKernel (pairContext i (History.finitePairHistoryOfTrace (action omega) (reward omega) i)) (action omega (i + 1)))) (ae (mu.trim ((History.historyFiltrationSucc action reward haction hreward).le i)))) : Filter.Eventually (fun omega : Omega => @Measure.map Omega (Prod Action Rat) mOmega inferInstance (fun y : Omega => (action omega (i + 1), reward y (i + 1))) (@ProbabilityTheory.condExpKernel Omega mOmega _ mu _ ((History.historyFiltrationSucc action reward haction hreward) i) omega) = Measure.map (Prod.mk (action omega (i + 1))) (RewardKernel.selectedMeasure rewardKernel (pairContext i (History.finitePairHistoryOfTrace (action omega) (reward omega) i)) (action omega (i + 1)))) (ae (mu.trim ((History.historyFiltrationSucc action reward haction hreward).le i)))

Random next-pair source law in canonical history-step-kernel form. This rewrites a generated-action random next-pair law whose right side is stated as `Measure.map (Prod.mk actualAction) selectedMeasure` into the standard `RewardKernel.actionRewardHistoryStepKernelFamily` form consumed by the pair-law route. It is a law-shape adapter; the random next-pair law itself remains an explicit hypothesis.

theorem actionRewardHistoryStepKernelFamily_pair_map_eq_historyFiltrationSucc_finitePairHistoryOfTrace_of_generatedActionTraceSucc_random_pair_map_eq_actual_action {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] (mu : Measure Omega) [IsFiniteMeasure mu] (rewardKernel : RewardKernel.MarkovRewardKernel (Prod Context Action) Rat) (policy : Nat -> Policy.MeasurablePolicy State Action) (pairContext : (n : Nat) -> ((j : Finset.Iic n) -> Prod Action Rat) -> Context) (pairState : (n : Nat) -> ((j : Finset.Iic n) -> Prod Action Rat) -> State) (hpairContext : forall n : Nat, Measurable (pairContext n)) (hpairState : forall n : Nat, Measurable (pairState n)) (defaultAction : Action) (action : Omega -> ActionTrace Action) (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) (h_action_generated : action = Policy.generatedActionTraceSucc policy (fun n omega => pairState n (History.finitePairHistoryOfTrace (action omega) (reward omega) n)) defaultAction) (h_random_pair_map_eq_actual_action : Filter.Eventually (fun omega : Omega => @Measure.map Omega (Prod Action Rat) mOmega inferInstance (fun y : Omega => (action y (i + 1), reward y (i + 1))) (@ProbabilityTheory.condExpKernel Omega mOmega _ mu _ ((History.historyFiltrationSucc action reward haction hreward) i) omega) = Measure.map (Prod.mk (action omega (i + 1))) (RewardKernel.selectedMeasure rewardKernel (pairContext i (History.finitePairHistoryOfTrace (action omega) (reward omega) i)) (action omega (i + 1)))) (ae (mu.trim ((History.historyFiltrationSucc action reward haction hreward).le i)))) : Filter.Eventually (fun omega : Omega => @Measure.map Omega (Prod Action Rat) mOmega inferInstance (fun y : Omega => (action y (i + 1), reward y (i + 1))) (@ProbabilityTheory.condExpKernel Omega mOmega _ mu _ ((History.historyFiltrationSucc action reward haction hreward) i) omega) = RewardKernel.actionRewardHistoryStepKernelFamily rewardKernel policy pairContext pairState hpairContext hpairState i (History.finitePairHistoryOfTrace (action omega) (reward omega) i)) (ae (mu.trim ((History.historyFiltrationSucc action reward haction hreward).le i)))

Finite reward-history frozen-past specialization. Once the finite reward history at time `i` is measurable with respect to filtration level `F i`, the conditional-expectation kernel at that level freezes the whole finite history trim-a.e. This supplies the direct `h_history_frozen` hypothesis needed by `centeredReward_succ_frozenPast_ae_of_history_frozen`.

theorem finiteRewardHistory_condExpKernel_frozen_of_measurable {Omega : Type u} [mOmega : MeasurableSpace Omega] [StandardBorelSpace Omega] (mu : Measure Omega) [IsFiniteMeasure mu] (F : Filtration Nat mOmega) (i : Nat) (history : Omega -> ((j : Finset.Iic i) -> Rat)) (hhistory : @Measurable Omega ((j : Finset.Iic i) -> Rat) (F i) inferInstance history) : Filter.Eventually (fun omega : Omega => history =ᵐ[ ProbabilityTheory.condExpKernel (Ω

Coordinate-measurability hookup for finite reward histories. If every coordinate in the finite reward prefix is measurable at filtration level `F i`, the whole `finiteRewardHistoryOfTrace` object is measurable and therefore frozen by the conditional-expectation kernel. This is still only a measurability bridge; it does not identify the conditional kernel with a trajectory/history-step reward law.

theorem finiteRewardHistory_condExpKernel_frozen_of_coordinate_measurable {Omega : Type u} [mOmega : MeasurableSpace Omega] [StandardBorelSpace Omega] (mu : Measure Omega) [IsFiniteMeasure mu] (F : Filtration Nat mOmega) (reward : Omega -> RewardTrace Rat) (i : Nat) (hreward : forall j : Finset.Iic i, @Measurable Omega Rat (F i) inferInstance (fun omega : Omega => reward omega j.1)) : Filter.Eventually (fun omega : Omega => Filter.EventuallyEq (ae (@ProbabilityTheory.condExpKernel Omega mOmega _ mu _ (F i) omega)) (fun y : Omega => History.finiteRewardHistoryOfTrace (reward y) i) (fun _y : Omega => History.finiteRewardHistoryOfTrace (reward omega) i)) (ae (mu.trim (F.le i)))

Generated-history-filtration specialization of finite reward-history freezing. For the shifted history filtration `historyFiltrationSucc`, all reward coordinates up to `i` are visible at level `i`, so the finite reward history prefix is frozen trim-a.e. under its conditional-expectation kernel. This closes the concrete finite-history measurability side of the frozen-past route; the remaining missing leaf is the reward-law/trajectory-law identification.

theorem finiteRewardHistory_condExpKernel_frozen_historyFiltrationSucc {Omega : Type u} {Action : Type v} [mOmega : MeasurableSpace Omega] [StandardBorelSpace Omega] [MeasurableSpace Action] [MeasurableSingletonClass Action] (mu : Measure Omega) [IsFiniteMeasure mu] (action : Omega -> ActionTrace Action) (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) : Filter.Eventually (fun omega : Omega => Filter.EventuallyEq (ae (@ProbabilityTheory.condExpKernel Omega mOmega _ mu _ ((History.historyFiltrationSucc action reward haction hreward) i) omega)) (fun y : Omega => History.finiteRewardHistoryOfTrace (reward y) i) (fun _y : Omega => History.finiteRewardHistoryOfTrace (reward omega) i)) (ae (mu.trim ((History.historyFiltrationSucc action reward haction hreward).le i)))

Finite action/reward pair-history frozen-past specialization. This is the pair-coordinate companion to `finiteRewardHistory_condExpKernel_frozen_of_measurable`. It needs a countable action space because the frozen object contains action coordinates.

theorem finitePairHistory_condExpKernel_frozen_of_measurable {Omega : Type u} {Action : Type v} [mOmega : MeasurableSpace Omega] [StandardBorelSpace Omega] [MeasurableSpace Action] [MeasurableSingletonClass Action] [Countable Action] (mu : Measure Omega) [IsFiniteMeasure mu] (F : Filtration Nat mOmega) (i : Nat) (history : Omega -> ((j : Finset.Iic i) -> Prod Action Rat)) (hhistory : @Measurable Omega ((j : Finset.Iic i) -> Prod Action Rat) (F i) inferInstance history) : Filter.Eventually (fun omega : Omega => Filter.EventuallyEq (ae (@ProbabilityTheory.condExpKernel Omega mOmega _ mu _ (F i) omega)) history (fun _y : Omega => history omega)) (ae (mu.trim (F.le i)))

Coordinate-measurability hookup for finite action/reward pair histories. If every action and reward coordinate in the finite pair prefix is measurable at filtration level `F i`, the whole `finitePairHistoryOfTrace` object is measurable and therefore frozen under the conditional-expectation kernel.

theorem finitePairHistory_condExpKernel_frozen_of_coordinate_measurable {Omega : Type u} {Action : Type v} [mOmega : MeasurableSpace Omega] [StandardBorelSpace Omega] [MeasurableSpace Action] [MeasurableSingletonClass Action] [Countable Action] (mu : Measure Omega) [IsFiniteMeasure mu] (F : Filtration Nat mOmega) (action : Omega -> ActionTrace Action) (reward : Omega -> RewardTrace Rat) (i : Nat) (haction : forall j : Finset.Iic i, @Measurable Omega Action (F i) inferInstance (fun omega : Omega => action omega j.1)) (hreward : forall j : Finset.Iic i, @Measurable Omega Rat (F i) inferInstance (fun omega : Omega => reward omega j.1)) : Filter.Eventually (fun omega : Omega => Filter.EventuallyEq (ae (@ProbabilityTheory.condExpKernel Omega mOmega _ mu _ (F i) omega)) (fun y : Omega => History.finitePairHistoryOfTrace (action y) (reward y) i) (fun _y : Omega => History.finitePairHistoryOfTrace (action omega) (reward omega) i)) (ae (mu.trim (F.le i)))

Generated-history-filtration specialization of finite pair-history freezing. For `History.historyFiltrationSucc`, all action and reward coordinates up to `i` are visible at level `i`, so the finite `(Action, Reward)` pair prefix is frozen trim-a.e. under its conditional-expectation kernel. This is a frozen past hook for future `partialTraj`/`condExpKernel` pair-law identification; it does not prove that law.

theorem finitePairHistory_condExpKernel_frozen_historyFiltrationSucc {Omega : Type u} {Action : Type v} [mOmega : MeasurableSpace Omega] [StandardBorelSpace Omega] [MeasurableSpace Action] [MeasurableSingletonClass Action] [Countable Action] (mu : Measure Omega) [IsFiniteMeasure mu] (action : Omega -> ActionTrace Action) (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) : Filter.Eventually (fun omega : Omega => Filter.EventuallyEq (ae (@ProbabilityTheory.condExpKernel Omega mOmega _ mu _ ((History.historyFiltrationSucc action reward haction hreward) i) omega)) (fun y : Omega => History.finitePairHistoryOfTrace (action y) (reward y) i) (fun _y : Omega => History.finitePairHistoryOfTrace (action omega) (reward omega) i)) (ae (mu.trim ((History.historyFiltrationSucc action reward haction hreward).le i)))

Successor finite-pair trace decomposition under any frozen-prefix hypothesis. If the old finite pair prefix is a.e. frozen at `omega`, then the full `i + 1` prefix is a.e. the deterministic successor extension of that frozen prefix by the random next `(Action, Reward)` pair.

theorem finitePairHistory_succ_ae_eq_extend_of_pairHistory_frozen {Omega : Type u} {Action : Type v} [mOmega : MeasurableSpace Omega] (nu : Measure Omega) (action : Omega -> ActionTrace Action) (reward : Omega -> RewardTrace Rat) (i : Nat) (omega : Omega) (h_pair_history_frozen : Filter.EventuallyEq (ae nu) (fun y : Omega => History.finitePairHistoryOfTrace (action y) (reward y) i) (fun _y : Omega => History.finitePairHistoryOfTrace (action omega) (reward omega) i)) : Filter.EventuallyEq (ae nu) (fun y : Omega => History.finitePairHistoryOfTrace (action y) (reward y) (i + 1)) (fun y : Omega => History.extendPairHistorySucc (History.finitePairHistoryOfTrace (action omega) (reward omega) i) (action y (i + 1), reward y (i + 1)))

Generated-history conditional-kernel successor decomposition for pair traces. This packages the previous frozen pair-prefix theorem into the concrete `History.historyFiltrationSucc` conditional kernel. It is not a joint law identification; it only rewrites the random `i + 1` pair trace into a frozen prefix plus random next pair under the conditional kernel.

theorem finitePairHistory_succ_condExpKernel_ae_eq_extend_historyFiltrationSucc {Omega : Type u} {Action : Type v} [mOmega : MeasurableSpace Omega] [StandardBorelSpace Omega] [MeasurableSpace Action] [MeasurableSingletonClass Action] [Countable Action] (mu : Measure Omega) [IsFiniteMeasure mu] (action : Omega -> ActionTrace Action) (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) : Filter.Eventually (fun omega : Omega => Filter.EventuallyEq (ae (@ProbabilityTheory.condExpKernel Omega mOmega _ mu _ ((History.historyFiltrationSucc action reward haction hreward) i) omega)) (fun y : Omega => History.finitePairHistoryOfTrace (action y) (reward y) (i + 1)) (fun y : Omega => History.extendPairHistorySucc (History.finitePairHistoryOfTrace (action omega) (reward omega) i) (action y (i + 1), reward y (i + 1)))) (ae (mu.trim ((History.historyFiltrationSucc action reward haction hreward).le i)))

Pushforward form of the generated-history successor decomposition. The previous theorem is an a.e. equality under the conditional kernel. This lemma upgrades it via Mathlib's `Measure.map_congr`, so later route cards can state the remaining trajectory-law input against the deterministic `extendPairHistorySucc` map instead of the full `i + 1` trace restriction.

theorem finitePairHistory_succ_condExpKernel_map_eq_extend_historyFiltrationSucc {Omega : Type u} {Action : Type v} [mOmega : MeasurableSpace Omega] [StandardBorelSpace Omega] [MeasurableSpace Action] [MeasurableSingletonClass Action] [Countable Action] (mu : Measure Omega) [IsFiniteMeasure mu] (action : Omega -> ActionTrace Action) (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) : Filter.Eventually (fun omega : Omega => @Measure.map Omega ((j : Finset.Iic (i + 1)) -> Prod Action Rat) mOmega inferInstance (fun y : Omega => History.finitePairHistoryOfTrace (action y) (reward y) (i + 1)) (@ProbabilityTheory.condExpKernel Omega mOmega _ mu _ ((History.historyFiltrationSucc action reward haction hreward) i) omega) = @Measure.map Omega ((j : Finset.Iic (i + 1)) -> Prod Action Rat) mOmega inferInstance (fun y : Omega => History.extendPairHistorySucc (History.finitePairHistoryOfTrace (action omega) (reward omega) i) (action y (i + 1), reward y (i + 1))) (@ProbabilityTheory.condExpKernel Omega mOmega _ mu _ ((History.historyFiltrationSucc action reward haction hreward) i) omega)) (ae (mu.trim ((History.historyFiltrationSucc action reward haction hreward).le i)))

Frozen-history bridge for the succ-indexed map-law route. If the finite reward history is already frozen under the conditional kernel, then the history-selected context/action mean in the centered next-reward variable is frozen as well. This is the deterministic part of the `h_kernel_X_eq` side condition consumed by the map-law conditional-expectation bridge; it deliberately does not prove that the history itself is frozen.

theorem centeredReward_succ_frozenPast_ae_of_history_frozen {Omega : Type u} {Context : Type v} {State : Type w} {Action : Type x} [mOmega : MeasurableSpace Omega] [StandardBorelSpace Omega] [MeasurableSpace State] [MeasurableSpace Action] (mu : Measure Omega) [IsFiniteMeasure mu] (F : Filtration Nat mOmega) (policy : Nat -> Policy.MeasurablePolicy State Action) (context : (n : Nat) -> ((j : Finset.Iic n) -> Rat) -> Context) (state : (n : Nat) -> ((j : Finset.Iic n) -> Rat) -> State) (mean : Context -> Action -> Rat) (reward : Omega -> RewardTrace Rat) (i : Nat) (history : Omega -> ((j : Finset.Iic i) -> Rat)) (h_history_frozen : Filter.Eventually (fun omega : Omega => history =ᵐ[ ProbabilityTheory.condExpKernel (Ω

Conditional sub-Gaussian map-law consumer with the frozen-past side condition discharged from prefix coordinate measurability. The remaining structural input is the reward-coordinate pushforward identity from `condExpKernel` to the history-step reward kernel. Ambient measurability of the centered reward and the deterministic variance-proxy upper bound remain explicit regularity contracts; exponential integrability is derived.

theorem centeredReward_succ_hasCondSubgaussianMGF_of_historyStepKernelFamily_condExpKernel_map_eq_of_coordinate_measurable {Omega : Type u} {Context : Type v} {State : Type w} {Action : Type x} [mOmega : MeasurableSpace Omega] [StandardBorelSpace Omega] [MeasurableSpace Context] [MeasurableSpace State] [MeasurableSpace Action] (mu : Measure Omega) [IsFiniteMeasure mu] (F : Filtration Nat mOmega) (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) (reward : Omega -> RewardTrace Rat) (i : Nat) (c : NNReal) (h_reward : @Measurable Omega Rat mOmega inferInstance (fun omega : Omega => reward omega (i + 1))) (h_prefix_meas : forall j : Finset.Iic i, @Measurable Omega Rat (F i) inferInstance (fun omega : Omega => reward omega j.1)) (h_centered_meas : @Measurable Omega Real mOmega inferInstance (fun omega : Omega => (((reward omega (i + 1) - mean (context i (History.finiteRewardHistoryOfTrace (reward omega) i)) ((policy i).action (state i (History.finiteRewardHistoryOfTrace (reward omega) i))) : Rat) : Real)))) (h_kernel_map_eq : Filter.Eventually (fun omega : Omega => @Measure.map Omega Rat mOmega inferInstance (fun y : Omega => reward y (i + 1)) (@ProbabilityTheory.condExpKernel Omega mOmega _ mu _ (F i) omega) = RewardKernel.historyStepKernelFamily rewardKernel policy context state hcontext hstate i (History.finiteRewardHistoryOfTrace (reward omega) i)) (ae (mu.trim (F.le i)))) (h_variance_le : 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 (F.le i)))) : ProbabilityTheory.HasCondSubgaussianMGF (F i) (F.le i) (fun omega : Omega => (((reward omega (i + 1) - mean (context i (History.finiteRewardHistoryOfTrace (reward omega) i)) ((policy i).action (state i (History.finiteRewardHistoryOfTrace (reward omega) i))) : Rat) : Real))) c mu

Generated-history-filtration specialization of the conditional sub-Gaussian map-law consumer. At filtration level `History.historyFiltrationSucc ... i`, the reward prefix up to `i` is visible by construction, so the coordinate-measurable consumer applies directly. The reward-coordinate pushforward identity and analytic measurability/variance contracts remain explicit, while exponential integrability is derived from the selected target laws.

theorem centeredReward_succ_hasCondSubgaussianMGF_of_historyStepKernelFamily_condExpKernel_map_eq_historyFiltrationSucc {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] (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) (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) (h_centered_meas : @Measurable Omega Real mOmega inferInstance (fun omega : Omega => (((reward omega (i + 1) - mean (context i (History.finiteRewardHistoryOfTrace (reward omega) i)) ((policy i).action (state i (History.finiteRewardHistoryOfTrace (reward omega) i))) : Rat) : Real)))) (h_kernel_map_eq : Filter.Eventually (fun omega : Omega => @Measure.map Omega Rat mOmega inferInstance (fun y : Omega => reward y (i + 1)) (@ProbabilityTheory.condExpKernel Omega mOmega _ mu _ ((History.historyFiltrationSucc action reward haction hreward) i) omega) = RewardKernel.historyStepKernelFamily rewardKernel policy context state hcontext hstate i (History.finiteRewardHistoryOfTrace (reward omega) i)) (ae (mu.trim ((History.historyFiltrationSucc action reward haction hreward).le i)))) (h_variance_le : 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 action reward haction hreward).le i)))) : ProbabilityTheory.HasCondSubgaussianMGF ((History.historyFiltrationSucc action reward haction hreward) i) ((History.historyFiltrationSucc action reward haction hreward).le i) (fun omega : Omega => (((reward omega (i + 1) - mean (context i (History.finiteRewardHistoryOfTrace (reward omega) i)) ((policy i).action (state i (History.finiteRewardHistoryOfTrace (reward omega) i))) : Rat) : Real))) c mu

Succ-indexed selected-reward specialization of the map-law consumer. The `h_kernel_map_eq` hypothesis is the reward-coordinate pushforward form of the future trajectory-law identification. The `h_kernel_X_eq` hypothesis is the matching frozen-past condition for the centered variable.

theorem centeredReward_succ_condExp_eq_zero_of_historyStepKernelFamily_condExpKernel_map_eq {Omega : Type u} {Context : Type v} {State : Type w} {Action : Type x} [mOmega : MeasurableSpace Omega] [StandardBorelSpace Omega] [MeasurableSpace Context] [MeasurableSpace State] [MeasurableSpace Action] (mu : Measure Omega) [IsFiniteMeasure mu] (F : Filtration Nat mOmega) (rewardKernel : RewardKernel.MarkovRewardKernel (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) (reward : Omega -> RewardTrace Rat) (i : Nat) (history : Omega -> ((j : Finset.Iic i) -> Rat)) (h_reward : @Measurable Omega Rat mOmega inferInstance (fun omega : Omega => reward omega (i + 1))) (h_integrable : Integrable (fun omega : Omega => (((reward omega (i + 1) - mean (context i (history omega)) ((policy i).action (state i (history omega))) : Rat) : Real))) mu) (h_kernel_map_eq : Filter.Eventually (fun omega : Omega => @Measure.map Omega Rat mOmega inferInstance (fun y : Omega => reward y (i + 1)) (ProbabilityTheory.condExpKernel (Ω

Map-law consumer with the frozen-past side condition discharged from prefix coordinate measurability. The remaining structural input is still `h_kernel_map_eq`: the reward-coordinate pushforward identity from `condExpKernel` to the history-step reward kernel. This theorem only removes the separate `h_kernel_X_eq` obligation by proving finite-history frozen-past from coordinate measurability at `F i`.

theorem centeredReward_succ_condExp_eq_zero_of_historyStepKernelFamily_condExpKernel_map_eq_of_coordinate_measurable {Omega : Type u} {Context : Type v} {State : Type w} {Action : Type x} [mOmega : MeasurableSpace Omega] [StandardBorelSpace Omega] [MeasurableSpace Context] [MeasurableSpace State] [MeasurableSpace Action] (mu : Measure Omega) [IsFiniteMeasure mu] (F : Filtration Nat mOmega) (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) (reward : Omega -> RewardTrace Rat) (i : Nat) (h_reward : @Measurable Omega Rat mOmega inferInstance (fun omega : Omega => reward omega (i + 1))) (h_prefix_meas : forall j : Finset.Iic i, @Measurable Omega Rat (F i) inferInstance (fun omega : Omega => reward omega j.1)) (h_integrable : Integrable (fun omega : Omega => (((reward omega (i + 1) - mean (context i (History.finiteRewardHistoryOfTrace (reward omega) i)) ((policy i).action (state i (History.finiteRewardHistoryOfTrace (reward omega) i))) : Rat) : Real))) mu) (h_kernel_map_eq : Filter.Eventually (fun omega : Omega => @Measure.map Omega Rat mOmega inferInstance (fun y : Omega => reward y (i + 1)) (@ProbabilityTheory.condExpKernel Omega mOmega _ mu _ (F i) omega) = RewardKernel.historyStepKernelFamily rewardKernel policy context state hcontext hstate i (History.finiteRewardHistoryOfTrace (reward omega) i)) (ae (mu.trim (F.le i)))) : Filter.EventuallyEq (ae mu) (@condExp Omega Real (F i) mOmega _ _ _ mu (fun omega : Omega => (((reward omega (i + 1) - mean (context i (History.finiteRewardHistoryOfTrace (reward omega) i)) ((policy i).action (state i (History.finiteRewardHistoryOfTrace (reward omega) i))) : Rat) : Real)))) (fun _omega : Omega => (0 : Real))

Generated-history-filtration specialization of the map-law consumer. At filtration level `History.historyFiltrationSucc ... i`, the reward prefix up to `i` is visible by construction, so the preceding coordinate-measurable consumer applies directly. The reward-coordinate pushforward identity remains an explicit assumption.

theorem centeredReward_succ_condExp_eq_zero_of_historyStepKernelFamily_condExpKernel_map_eq_historyFiltrationSucc {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] (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) (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) (h_integrable : Integrable (fun omega : Omega => (((reward omega (i + 1) - mean (context i (History.finiteRewardHistoryOfTrace (reward omega) i)) ((policy i).action (state i (History.finiteRewardHistoryOfTrace (reward omega) i))) : Rat) : Real))) mu) (h_kernel_map_eq : Filter.Eventually (fun omega : Omega => @Measure.map Omega Rat mOmega inferInstance (fun y : Omega => reward y (i + 1)) (@ProbabilityTheory.condExpKernel Omega mOmega _ mu _ ((History.historyFiltrationSucc action reward haction hreward) i) omega) = RewardKernel.historyStepKernelFamily rewardKernel policy context state hcontext hstate i (History.finiteRewardHistoryOfTrace (reward omega) i)) (ae (mu.trim ((History.historyFiltrationSucc action reward haction hreward).le i)))) : Filter.EventuallyEq (ae mu) (@condExp Omega Real ((History.historyFiltrationSucc action reward haction hreward) i) mOmega _ _ _ mu (fun omega : Omega => (((reward omega (i + 1) - mean (context i (History.finiteRewardHistoryOfTrace (reward omega) i)) ((policy i).action (state i (History.finiteRewardHistoryOfTrace (reward omega) i))) : Rat) : Real)))) (fun _omega : Omega => (0 : Real))

Pair-law route into the map-law conditional mean-zero consumer. If the conditional kernel has the correct next `(Action × Reward)` law, then mapping both sides through `Prod.snd` gives the reward-coordinate law consumed by the map-law conditional-expectation bridge. This theorem still assumes the pair-law identity; it only packages the marginalization step through `RewardKernel.actionRewardHistoryStepKernelFamily_reward_map`.

theorem centeredReward_succ_condExp_eq_zero_of_actionRewardHistoryStepKernelFamily_pair_map_eq_of_coordinate_measurable {Omega : Type u} {Context : Type v} {State : Type w} {Action : Type x} [mOmega : MeasurableSpace Omega] [StandardBorelSpace Omega] [MeasurableSpace Context] [MeasurableSpace State] [MeasurableSpace Action] (mu : Measure Omega) [IsFiniteMeasure mu] (F : Filtration Nat mOmega) (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)) (pairContext : (n : Nat) -> ((j : Finset.Iic n) -> Prod Action Rat) -> Context) (pairState : (n : Nat) -> ((j : Finset.Iic n) -> Prod Action Rat) -> State) (hpairContext : forall n : Nat, Measurable (pairContext n)) (hpairState : forall n : Nat, Measurable (pairState n)) (mean : Context -> Action -> Rat) (varianceProxy : Context -> Action -> NNReal) (law : RewardKernel.CenteredRewardKernelLaw rewardKernel mean varianceProxy) (action : Omega -> ActionTrace Action) (reward : Omega -> RewardTrace Rat) (i : Nat) (pairHistory : Omega -> ((j : Finset.Iic i) -> Prod Action Rat)) (h_action_next : @Measurable Omega Action mOmega inferInstance (fun omega : Omega => action omega (i + 1))) (h_reward_next : @Measurable Omega Rat mOmega inferInstance (fun omega : Omega => reward omega (i + 1))) (h_prefix_meas : forall j : Finset.Iic i, @Measurable Omega Rat (F i) inferInstance (fun omega : Omega => reward omega j.1)) (h_pair_context_eq : forall omega : Omega, pairContext i (pairHistory omega) = context i (History.finiteRewardHistoryOfTrace (reward omega) i)) (h_pair_state_eq : forall omega : Omega, pairState i (pairHistory omega) = state i (History.finiteRewardHistoryOfTrace (reward omega) i)) (h_integrable : Integrable (fun omega : Omega => (((reward omega (i + 1) - mean (context i (History.finiteRewardHistoryOfTrace (reward omega) i)) ((policy i).action (state i (History.finiteRewardHistoryOfTrace (reward omega) i))) : Rat) : Real))) mu) (h_kernel_pair_map_eq : Filter.Eventually (fun omega : Omega => @Measure.map Omega (Prod Action Rat) mOmega inferInstance (fun y : Omega => (action y (i + 1), reward y (i + 1))) (@ProbabilityTheory.condExpKernel Omega mOmega _ mu _ (F i) omega) = RewardKernel.actionRewardHistoryStepKernelFamily rewardKernel policy pairContext pairState hpairContext hpairState i (pairHistory omega)) (ae (mu.trim (F.le i)))) : Filter.EventuallyEq (ae mu) (@condExp Omega Real (F i) mOmega _ _ _ mu (fun omega : Omega => (((reward omega (i + 1) - mean (context i (History.finiteRewardHistoryOfTrace (reward omega) i)) ((policy i).action (state i (History.finiteRewardHistoryOfTrace (reward omega) i))) : Rat) : Real)))) (fun _omega : Omega => (0 : Real))

Generated-history-filtration specialization of the action/reward pair-law route. At `History.historyFiltrationSucc ... i`, the next action/reward coordinates are measurable in the ambient space and the reward prefix up to `i` is visible at filtration level `i`. Thus the coordinate-measurable pair-map consumer applies directly. The actual action/reward pair-law pushforward identity remains an explicit assumption.

theorem centeredReward_succ_condExp_eq_zero_of_actionRewardHistoryStepKernelFamily_pair_map_eq_historyFiltrationSucc {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] (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)) (pairContext : (n : Nat) -> ((j : Finset.Iic n) -> Prod Action Rat) -> Context) (pairState : (n : Nat) -> ((j : Finset.Iic n) -> Prod Action Rat) -> State) (hpairContext : forall n : Nat, Measurable (pairContext n)) (hpairState : forall n : Nat, Measurable (pairState n)) (mean : Context -> Action -> Rat) (varianceProxy : Context -> Action -> NNReal) (law : RewardKernel.CenteredRewardKernelLaw rewardKernel mean varianceProxy) (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) (pairHistory : Omega -> ((j : Finset.Iic i) -> Prod Action Rat)) (h_pair_context_eq : forall omega : Omega, pairContext i (pairHistory omega) = context i (History.finiteRewardHistoryOfTrace (reward omega) i)) (h_pair_state_eq : forall omega : Omega, pairState i (pairHistory omega) = state i (History.finiteRewardHistoryOfTrace (reward omega) i)) (h_integrable : Integrable (fun omega : Omega => (((reward omega (i + 1) - mean (context i (History.finiteRewardHistoryOfTrace (reward omega) i)) ((policy i).action (state i (History.finiteRewardHistoryOfTrace (reward omega) i))) : Rat) : Real))) mu) (h_kernel_pair_map_eq : Filter.Eventually (fun omega : Omega => @Measure.map Omega (Prod Action Rat) mOmega inferInstance (fun y : Omega => (action y (i + 1), reward y (i + 1))) (@ProbabilityTheory.condExpKernel Omega mOmega _ mu _ ((History.historyFiltrationSucc action reward haction hreward) i) omega) = RewardKernel.actionRewardHistoryStepKernelFamily rewardKernel policy pairContext pairState hpairContext hpairState i (pairHistory omega)) (ae (mu.trim ((History.historyFiltrationSucc action reward haction hreward).le i)))) : Filter.EventuallyEq (ae mu) (@condExp Omega Real ((History.historyFiltrationSucc action reward haction hreward) i) mOmega _ _ _ mu (fun omega : Omega => (((reward omega (i + 1) - mean (context i (History.finiteRewardHistoryOfTrace (reward omega) i)) ((policy i).action (state i (History.finiteRewardHistoryOfTrace (reward omega) i))) : Rat) : Real)))) (fun _omega : Omega => (0 : Real))

Generated-history pair-law route with the concrete trace pair-history. This specializes the previous generated-history consumer to the finite action/reward pair history obtained from the actual traces, and to context/state extractors that read only the reward projection of that pair history. It removes the separate pair-history compatibility hypotheses; the remaining structural assumption is exactly the generated-history `condExpKernel` pushforward equality for the next `(Action, Reward)` pair.

theorem centeredReward_succ_condExp_eq_zero_of_actionRewardHistoryStepKernelFamily_pair_map_eq_historyFiltrationSucc_projected {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] (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)) (hpairContext : forall n : Nat, Measurable (fun history : (j : Finset.Iic n) -> Prod Action Rat => context n (fun j : Finset.Iic n => (history j).2))) (hpairState : forall n : Nat, Measurable (fun history : (j : Finset.Iic n) -> Prod Action Rat => state n (fun j : Finset.Iic n => (history j).2))) (mean : Context -> Action -> Rat) (varianceProxy : Context -> Action -> NNReal) (law : RewardKernel.CenteredRewardKernelLaw rewardKernel mean varianceProxy) (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) (h_integrable : Integrable (fun omega : Omega => (((reward omega (i + 1) - mean (context i (History.finiteRewardHistoryOfTrace (reward omega) i)) ((policy i).action (state i (History.finiteRewardHistoryOfTrace (reward omega) i))) : Rat) : Real))) mu) (h_kernel_pair_map_eq : Filter.Eventually (fun omega : Omega => @Measure.map Omega (Prod Action Rat) mOmega inferInstance (fun y : Omega => (action y (i + 1), reward y (i + 1))) (@ProbabilityTheory.condExpKernel Omega mOmega _ mu _ ((History.historyFiltrationSucc action reward haction hreward) i) omega) = RewardKernel.actionRewardHistoryStepKernelFamily rewardKernel policy (fun n history => context n (fun j : Finset.Iic n => (history j).2)) (fun n history => state n (fun j : Finset.Iic n => (history j).2)) hpairContext hpairState i (fun j : Finset.Iic i => (action omega j.1, reward omega j.1))) (ae (mu.trim ((History.historyFiltrationSucc action reward haction hreward).le i)))) : Filter.EventuallyEq (ae mu) (@condExp Omega Real ((History.historyFiltrationSucc action reward haction hreward) i) mOmega _ _ _ mu (fun omega : Omega => (((reward omega (i + 1) - mean (context i (History.finiteRewardHistoryOfTrace (reward omega) i)) ((policy i).action (state i (History.finiteRewardHistoryOfTrace (reward omega) i))) : Rat) : Real)))) (fun _omega : Omega => (0 : Real))

Projected trace-pair route with projection measurability supplied locally. The remaining hypothesis is the concrete generated-history pair-law equality. The reward-projection context/state measurability proofs are derived from the original reward-history `context`/`state` measurability and `History.measurable_pairHistoryRewardProjection`.

theorem centeredReward_succ_condExp_eq_zero_of_actionRewardHistoryStepKernelFamily_pair_map_eq_historyFiltrationSucc_projected_of_context_state_measurable {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] (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) (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) (h_integrable : Integrable (fun omega : Omega => (((reward omega (i + 1) - mean (context i (History.finiteRewardHistoryOfTrace (reward omega) i)) ((policy i).action (state i (History.finiteRewardHistoryOfTrace (reward omega) i))) : Rat) : Real))) mu) (h_kernel_pair_map_eq : Filter.Eventually (fun omega : Omega => @Measure.map Omega (Prod Action Rat) mOmega inferInstance (fun y : Omega => (action y (i + 1), reward y (i + 1))) (@ProbabilityTheory.condExpKernel Omega mOmega _ mu _ ((History.historyFiltrationSucc action reward haction hreward) i) omega) = 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

Projected trace-pair route using the named finite pair-history prefix. This is the same route as `..._projected_of_context_state_measurable`, but the remaining pair-law hypothesis is stated with `History.finitePairHistoryOfTrace`. That is the finite-prefix object aligned with `RewardKernel.actionRewardPartialTrajectoryKernel`.

theorem centeredReward_succ_condExp_eq_zero_of_actionRewardHistoryStepKernelFamily_pair_map_eq_historyFiltrationSucc_finitePairHistoryOfTrace {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] (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) (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) (h_integrable : Integrable (fun omega : Omega => (((reward omega (i + 1) - mean (context i (History.finiteRewardHistoryOfTrace (reward omega) i)) ((policy i).action (state i (History.finiteRewardHistoryOfTrace (reward omega) i))) : Rat) : Real))) mu) (h_kernel_pair_map_eq : Filter.Eventually (fun omega : Omega => @Measure.map Omega (Prod Action Rat) mOmega inferInstance (fun y : Omega => (action y (i + 1), reward y (i + 1))) (@ProbabilityTheory.condExpKernel Omega mOmega _ mu _ ((History.historyFiltrationSucc action reward haction hreward) i) omega) = 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

Project a generated-history `partialTraj` trace law to the next-pair law. This names the reusable law-identification step that was previously only embedded inside the centered-reward consumer below. If the conditional kernel of the full finite pair trace at `i + 1` agrees with the one-step action/reward `partialTraj` kernel, then mapping both sides to the successor coordinate gives the concrete next `(Action, Reward)` pushforward law consumed by the pair-map route.

theorem actionRewardHistoryStepKernelFamily_pair_map_eq_of_actionRewardPartialTrajectoryKernel_map_eq_historyFiltrationSucc_finitePairHistoryOfTrace {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] (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) (h_kernel_partialtraj_map_eq : Filter.Eventually (fun omega : Omega => @Measure.map Omega ((j : Finset.Iic (i + 1)) -> Prod Action Rat) mOmega inferInstance (fun y : Omega => History.finitePairHistoryOfTrace (action y) (reward y) (i + 1)) (@ProbabilityTheory.condExpKernel Omega mOmega _ mu _ ((History.historyFiltrationSucc action reward haction hreward) i) omega) = RewardKernel.actionRewardPartialTrajectoryKernel 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

Project a history-step next-pair law to the actual-action reward law. This is the direct reward-coordinate adapter for a conditional kernel law already stated at the next `(Action, Reward)` level. Mapping both sides through `Prod.snd` reduces the target to `RewardKernel.actionRewardHistoryStepKernelFamily_reward_map`; the only remaining rewrite is the trim-a.e. successor action equality.

theorem reward_condExpKernel_map_eq_selected_actual_action_of_actionRewardHistoryStepKernelFamily_pair_map_eq {Omega : Type u} {Context : Type v} {State : Type w} {Action : Type x} [mOmega : MeasurableSpace Omega] [StandardBorelSpace Omega] [MeasurableSpace Context] [MeasurableSpace State] [MeasurableSpace Action] (mu : Measure Omega) [IsFiniteMeasure mu] (F : Filtration Nat mOmega) (rewardKernel : RewardKernel.MarkovRewardKernel (Prod Context Action) Rat) (policy : Nat -> Policy.MeasurablePolicy State Action) (pairContext : (n : Nat) -> ((j : Finset.Iic n) -> Prod Action Rat) -> Context) (pairState : (n : Nat) -> ((j : Finset.Iic n) -> Prod Action Rat) -> State) (hpairContext : forall n : Nat, Measurable (pairContext n)) (hpairState : forall n : Nat, Measurable (pairState n)) (action : Omega -> ActionTrace Action) (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) (pairHistory : Omega -> ((j : Finset.Iic i) -> Prod Action Rat)) (h_action_policy_eq : Filter.Eventually (fun omega : Omega => action omega (i + 1) = (policy i).action (pairState i (pairHistory omega))) (ae (mu.trim (F.le i)))) (h_kernel_pair_map_eq : Filter.Eventually (fun omega : Omega => @Measure.map Omega (Prod Action Rat) mOmega inferInstance (fun y : Omega => (action y (i + 1), reward y (i + 1))) (@ProbabilityTheory.condExpKernel Omega mOmega _ mu _ (F i) omega) = RewardKernel.actionRewardHistoryStepKernelFamily rewardKernel policy pairContext pairState hpairContext hpairState i (pairHistory omega)) (ae (mu.trim (F.le i)))) : Filter.Eventually (fun omega : Omega => @Measure.map Omega Rat mOmega inferInstance (fun y : Omega => reward y (i + 1)) (@ProbabilityTheory.condExpKernel Omega mOmega _ mu _ (F i) omega) = RewardKernel.selectedMeasure rewardKernel (pairContext i (pairHistory omega)) (action omega (i + 1))) (ae (mu.trim (F.le i)))

Specialize the next-pair reward adapter to generated pair histories. The hypothesis is already the history-step next-pair `condExpKernel` law for `History.finitePairHistoryOfTrace`. The theorem only projects it through the reward coordinate and rewrites the selected policy action to the actual next action by the supplied successor equality.

theorem reward_condExpKernel_map_eq_selected_actual_action_of_actionRewardHistoryStepKernelFamily_pair_map_eq_historyFiltrationSucc_finitePairHistoryOfTrace {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] (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) (h_action_policy_eq : Filter.Eventually (fun omega : Omega => action omega (i + 1) = (policy i).action (state i (History.finiteRewardHistoryOfTrace (reward omega) i))) (ae (mu.trim ((History.historyFiltrationSucc action reward haction hreward).le i)))) (h_kernel_pair_map_eq : Filter.Eventually (fun omega : Omega => @Measure.map Omega (Prod Action Rat) mOmega inferInstance (fun y : Omega => (action y (i + 1), reward y (i + 1))) (@ProbabilityTheory.condExpKernel Omega mOmega _ mu _ ((History.historyFiltrationSucc action reward haction hreward) i) omega) = 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

Generated-action wrapper for the finite-pair-history next-pair adapter. This removes the explicit successor action equality when the action trace is definitionally generated from the reward-history state.

theorem reward_condExpKernel_map_eq_selected_actual_action_of_generatedActionTraceSucc_actionRewardHistoryStepKernelFamily_pair_map_eq_historyFiltrationSucc_finitePairHistoryOfTrace {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] (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)) (defaultAction : Action) (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) (h_action_generated : action = Policy.generatedActionTraceSucc policy (fun n omega => state n (History.finiteRewardHistoryOfTrace (reward omega) n)) defaultAction) (h_kernel_pair_map_eq : Filter.Eventually (fun omega : Omega => @Measure.map Omega (Prod Action Rat) mOmega inferInstance (fun y : Omega => (action y (i + 1), reward y (i + 1))) (@ProbabilityTheory.condExpKernel Omega mOmega _ mu _ ((History.historyFiltrationSucc action reward haction hreward) i) omega) = 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

Project a full finite-pair `partialTraj` law to the actual-action reward law. The full trace law first gives the next `(Action, Reward)` marginal by the compiled `partialTraj` next-coordinate adapter. Mapping that marginal through `Prod.snd` and using `RewardKernel.actionRewardHistoryStepKernelFamily_reward_map` then gives the reward-coordinate law. The final rewrite only needs an `i + 1` action equality against the policy-selected action.

theorem reward_condExpKernel_map_eq_selected_actual_action_of_actionRewardPartialTrajectoryKernel_map_eq_historyFiltrationSucc_finitePairHistoryOfTrace {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] (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) (h_action_policy_eq : Filter.Eventually (fun omega : Omega => action omega (i + 1) = (policy i).action (state i (History.finiteRewardHistoryOfTrace (reward omega) i))) (ae (mu.trim ((History.historyFiltrationSucc action reward haction hreward).le i)))) (h_kernel_partialtraj_map_eq : Filter.Eventually (fun omega : Omega => @Measure.map Omega ((j : Finset.Iic (i + 1)) -> Prod Action Rat) mOmega inferInstance (fun y : Omega => History.finitePairHistoryOfTrace (action y) (reward y) (i + 1)) (@ProbabilityTheory.condExpKernel Omega mOmega _ mu _ ((History.historyFiltrationSucc action reward haction hreward) i) omega) = RewardKernel.actionRewardPartialTrajectoryKernel 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

Generated-action specialization of the full finite-pair `partialTraj` to actual-action reward-map adapter. `Policy.generatedActionTraceSucc` supplies the pointwise successor action equality required by `reward_condExpKernel_map_eq_selected_actual_action_of_actionRewardPartialTrajectoryKernel_map_eq_historyFiltrationSucc_finitePairHistoryOfTrace`.

theorem reward_condExpKernel_map_eq_selected_actual_action_of_generatedActionTraceSucc_actionRewardPartialTrajectoryKernel_map_eq_historyFiltrationSucc_finitePairHistoryOfTrace {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] (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)) (defaultAction : Action) (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) (h_action_generated : action = Policy.generatedActionTraceSucc policy (fun n omega => state n (History.finiteRewardHistoryOfTrace (reward omega) n)) defaultAction) (h_kernel_partialtraj_map_eq : Filter.Eventually (fun omega : Omega => @Measure.map Omega ((j : Finset.Iic (i + 1)) -> Prod Action Rat) mOmega inferInstance (fun y : Omega => History.finitePairHistoryOfTrace (action y) (reward y) (i + 1)) (@ProbabilityTheory.condExpKernel Omega mOmega _ mu _ ((History.historyFiltrationSucc action reward haction hreward) i) omega) = RewardKernel.actionRewardPartialTrajectoryKernel 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

Generated-history route from a one-step `partialTraj` law assumption. If the conditional kernel pushed forward to the extended finite pair trace agrees with the local action/reward `partialTraj` kernel from `i` to `i + 1`, then Mathlib's `partialTraj` next-coordinate marginal wrapper turns that into the concrete next `(Action, Reward)` pair-law consumed by `..._finitePairHistoryOfTrace`.

theorem centeredReward_succ_condExp_eq_zero_of_actionRewardPartialTrajectoryKernel_map_eq_historyFiltrationSucc_finitePairHistoryOfTrace {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] (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) (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) (h_integrable : Integrable (fun omega : Omega => (((reward omega (i + 1) - mean (context i (History.finiteRewardHistoryOfTrace (reward omega) i)) ((policy i).action (state i (History.finiteRewardHistoryOfTrace (reward omega) i))) : Rat) : Real))) mu) (h_kernel_partialtraj_map_eq : Filter.Eventually (fun omega : Omega => @Measure.map Omega ((j : Finset.Iic (i + 1)) -> Prod Action Rat) mOmega inferInstance (fun y : Omega => History.finitePairHistoryOfTrace (action y) (reward y) (i + 1)) (@ProbabilityTheory.condExpKernel Omega mOmega _ mu _ ((History.historyFiltrationSucc action reward haction hreward) i) omega) = RewardKernel.actionRewardPartialTrajectoryKernel 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

Build the full next `(Action, Reward)` conditional-kernel law from split action and reward laws. The action side is deterministic/predictable under the conditional kernel, and the reward side supplies the selected reward law. Together they identify the next-pair pushforward with the local history-step action/reward kernel.

theorem actionRewardHistoryStepKernelFamily_pair_map_eq_of_action_ae_eq_policy_reward_map_eq {Omega : Type u} {Context : Type v} {State : Type w} {Action : Type x} [mOmega : MeasurableSpace Omega] [StandardBorelSpace Omega] [MeasurableSpace Context] [MeasurableSpace State] [MeasurableSpace Action] (mu : Measure Omega) [IsFiniteMeasure mu] (F : Filtration Nat mOmega) (rewardKernel : RewardKernel.MarkovRewardKernel (Prod Context Action) Rat) (policy : Nat -> Policy.MeasurablePolicy State Action) (pairContext : (n : Nat) -> ((j : Finset.Iic n) -> Prod Action Rat) -> Context) (pairState : (n : Nat) -> ((j : Finset.Iic n) -> Prod Action Rat) -> State) (hpairContext : forall n : Nat, Measurable (pairContext n)) (hpairState : forall n : Nat, Measurable (pairState n)) (action : Omega -> ActionTrace Action) (reward : Omega -> RewardTrace Rat) (i : Nat) (pairHistory : Omega -> ((j : Finset.Iic i) -> Prod Action Rat)) (h_action_next : @Measurable Omega Action mOmega inferInstance (fun omega : Omega => action omega (i + 1))) (h_reward_next : @Measurable Omega Rat mOmega inferInstance (fun omega : Omega => reward omega (i + 1))) (h_action_ae_eq_policy : Filter.Eventually (fun omega : Omega => Filter.EventuallyEq (ae (@ProbabilityTheory.condExpKernel Omega mOmega _ mu _ (F i) omega)) (fun y : Omega => action y (i + 1)) (fun _y : Omega => (policy i).action (pairState i (pairHistory omega)))) (ae (mu.trim (F.le i)))) (h_reward_map_eq : Filter.Eventually (fun omega : Omega => @Measure.map Omega Rat mOmega inferInstance (fun y : Omega => reward y (i + 1)) (@ProbabilityTheory.condExpKernel Omega mOmega _ mu _ (F i) omega) = RewardKernel.selectedMeasure rewardKernel (pairContext i (pairHistory omega)) ((policy i).action (pairState i (pairHistory omega)))) (ae (mu.trim (F.le i)))) : Filter.Eventually (fun omega : Omega => @Measure.map Omega (Prod Action Rat) mOmega inferInstance (fun y : Omega => (action y (i + 1), reward y (i + 1))) (@ProbabilityTheory.condExpKernel Omega mOmega _ mu _ (F i) omega) = RewardKernel.actionRewardHistoryStepKernelFamily rewardKernel policy pairContext pairState hpairContext hpairState i (pairHistory omega)) (ae (mu.trim (F.le i)))

Generated-action source plus an actual-action reward law gives the full next-pair law. This is the generated-history specialization of the split-law builder. The action side is supplied by `Policy.generatedActionTraceSucc`; the remaining reward assumption may be stated with the actual next action at the conditioning point, and is rewritten to the policy-selected action before invoking the generic split-law theorem.

theorem actionRewardHistoryStepKernelFamily_pair_map_eq_historyFiltrationSucc_finitePairHistoryOfTrace_of_generatedActionTraceSucc_reward_map_eq_actual_action {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] (mu : Measure Omega) [IsFiniteMeasure mu] (rewardKernel : RewardKernel.MarkovRewardKernel (Prod Context Action) Rat) (policy : Nat -> Policy.MeasurablePolicy State Action) (pairContext : (n : Nat) -> ((j : Finset.Iic n) -> Prod Action Rat) -> Context) (pairState : (n : Nat) -> ((j : Finset.Iic n) -> Prod Action Rat) -> State) (hpairContext : forall n : Nat, Measurable (pairContext n)) (hpairState : forall n : Nat, Measurable (pairState n)) (defaultAction : Action) (action : Omega -> ActionTrace Action) (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) (h_action_generated : action = Policy.generatedActionTraceSucc policy (fun n omega => pairState n (History.finitePairHistoryOfTrace (action omega) (reward omega) n)) defaultAction) (h_reward_map_eq_actual_action : Filter.Eventually (fun omega : Omega => @Measure.map Omega Rat mOmega inferInstance (fun y : Omega => reward y (i + 1)) (@ProbabilityTheory.condExpKernel Omega mOmega _ mu _ ((History.historyFiltrationSucc action reward haction hreward) i) omega) = RewardKernel.selectedMeasure rewardKernel (pairContext i (History.finitePairHistoryOfTrace (action omega) (reward omega) i)) (action omega (i + 1))) (ae (mu.trim ((History.historyFiltrationSucc action reward haction hreward).le i)))) : Filter.Eventually (fun omega : Omega => @Measure.map Omega (Prod Action Rat) mOmega inferInstance (fun y : Omega => (action y (i + 1), reward y (i + 1))) (@ProbabilityTheory.condExpKernel Omega mOmega _ mu _ ((History.historyFiltrationSucc action reward haction hreward) i) omega) = RewardKernel.actionRewardHistoryStepKernelFamily rewardKernel policy pairContext pairState hpairContext hpairState i (History.finitePairHistoryOfTrace (action omega) (reward omega) i)) (ae (mu.trim ((History.historyFiltrationSucc action reward haction hreward).le i)))

Turn a next-pair `condExpKernel` law into the extension-map `partialTraj` law. This is the law-shaped bridge between the pair-map consumer and the extension-map `partialTraj` route: once the conditional kernel of the next `(Action, Reward)` pair is identified with the configured history-step kernel, pushing both sides through `History.extendPairHistorySucc` identifies the one-step finite-prefix trajectory kernel.

theorem actionRewardPartialTrajectoryKernel_extend_map_eq_of_actionRewardHistoryStepKernelFamily_pair_map_eq {Omega : Type u} {Context : Type v} {State : Type w} {Action : Type x} [mOmega : MeasurableSpace Omega] [StandardBorelSpace Omega] [MeasurableSpace Context] [MeasurableSpace State] [MeasurableSpace Action] (mu : Measure Omega) [IsFiniteMeasure mu] (F : Filtration Nat mOmega) (rewardKernel : RewardKernel.MarkovRewardKernel (Prod Context Action) Rat) (policy : Nat -> Policy.MeasurablePolicy State Action) (pairContext : (n : Nat) -> ((j : Finset.Iic n) -> Prod Action Rat) -> Context) (pairState : (n : Nat) -> ((j : Finset.Iic n) -> Prod Action Rat) -> State) (hpairContext : forall n : Nat, Measurable (pairContext n)) (hpairState : forall n : Nat, Measurable (pairState n)) (action : Omega -> ActionTrace Action) (reward : Omega -> RewardTrace Rat) (i : Nat) (pairHistory : Omega -> ((j : Finset.Iic i) -> Prod Action Rat)) (h_action_next : @Measurable Omega Action mOmega inferInstance (fun omega : Omega => action omega (i + 1))) (h_reward_next : @Measurable Omega Rat mOmega inferInstance (fun omega : Omega => reward omega (i + 1))) (h_kernel_pair_map_eq : Filter.Eventually (fun omega : Omega => @Measure.map Omega (Prod Action Rat) mOmega inferInstance (fun y : Omega => (action y (i + 1), reward y (i + 1))) (@ProbabilityTheory.condExpKernel Omega mOmega _ mu _ (F i) omega) = RewardKernel.actionRewardHistoryStepKernelFamily rewardKernel policy pairContext pairState hpairContext hpairState i (pairHistory omega)) (ae (mu.trim (F.le i)))) : Filter.Eventually (fun omega : Omega => @Measure.map Omega ((j : Finset.Iic (i + 1)) -> Prod Action Rat) mOmega inferInstance (fun y : Omega => History.extendPairHistorySucc (pairHistory omega) (action y (i + 1), reward y (i + 1))) (@ProbabilityTheory.condExpKernel Omega mOmega _ mu _ (F i) omega) = RewardKernel.actionRewardPartialTrajectoryKernel rewardKernel policy pairContext pairState hpairContext hpairState i (i + 1) (pairHistory omega)) (ae (mu.trim (F.le i)))

Generated-history finite-pair-trace specialization of the extension-map law builder. The remaining assumption is the concrete conditional next-pair law against `RewardKernel.actionRewardHistoryStepKernelFamily`; this theorem packages the pushforward through `History.extendPairHistorySucc` and the local `partialTraj` wrapper.

theorem actionRewardPartialTrajectoryKernel_extend_map_eq_of_actionRewardHistoryStepKernelFamily_pair_map_eq_historyFiltrationSucc_finitePairHistoryOfTrace {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] (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) (h_kernel_pair_map_eq : Filter.Eventually (fun omega : Omega => @Measure.map Omega (Prod Action Rat) mOmega inferInstance (fun y : Omega => (action y (i + 1), reward y (i + 1))) (@ProbabilityTheory.condExpKernel Omega mOmega _ mu _ ((History.historyFiltrationSucc action reward haction hreward) i) omega) = 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

Generated-action and actual-action reward law source for the extension-map `partialTraj` route. This composes the generated-action next-pair split-law hookup with the extension-map `partialTraj` builder. The remaining law input is only the reward-coordinate conditional map law selected by the actual next action; the wrapper rewrites that action to the policy-selected action and pushes the resulting next-pair law through `History.extendPairHistorySucc`.

theorem actionRewardPartialTrajectoryKernel_extend_map_eq_historyFiltrationSucc_finitePairHistoryOfTrace_of_generatedActionTraceSucc_reward_map_eq_actual_action {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] (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)) (defaultAction : Action) (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) (h_action_generated : action = Policy.generatedActionTraceSucc policy (fun n omega => state n (History.finiteRewardHistoryOfTrace (reward omega) n)) defaultAction) (h_reward_map_eq_actual_action : Filter.Eventually (fun omega : Omega => @Measure.map Omega Rat mOmega inferInstance (fun y : Omega => reward y (i + 1)) (@ProbabilityTheory.condExpKernel Omega mOmega _ mu _ ((History.historyFiltrationSucc action reward haction hreward) i) omega) = RewardKernel.selectedMeasure rewardKernel (context i (History.finiteRewardHistoryOfTrace (reward omega) i)) (action omega (i + 1))) (ae (mu.trim ((History.historyFiltrationSucc action reward haction hreward).le i)))) : Filter.Eventually (fun omega : Omega => @Measure.map Omega ((j : Finset.Iic (i + 1)) -> Prod Action Rat) mOmega inferInstance (fun y : Omega => History.extendPairHistorySucc (History.finitePairHistoryOfTrace (action omega) (reward omega) i) (action y (i + 1), reward y (i + 1))) (@ProbabilityTheory.condExpKernel Omega mOmega _ mu _ ((History.historyFiltrationSucc action reward haction hreward) i) omega) = RewardKernel.actionRewardPartialTrajectoryKernel 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

Turn an extension-map `partialTraj` law into the full finite-pair-trace law. The generated history filtration already freezes the old pair prefix under the conditional kernel, so the full `i + 1` trace pushforward agrees a.e. with the deterministic extension of the frozen `i` prefix by the random next pair. This adapter packages that successor decomposition separately from the centered reward consumer.

theorem actionRewardPartialTrajectoryKernel_map_eq_of_extend_map_eq_historyFiltrationSucc_finitePairHistoryOfTrace {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] (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) (h_kernel_extend_map_eq : Filter.Eventually (fun omega : Omega => @Measure.map Omega ((j : Finset.Iic (i + 1)) -> Prod Action Rat) mOmega inferInstance (fun y : Omega => History.extendPairHistorySucc (History.finitePairHistoryOfTrace (action omega) (reward omega) i) (action y (i + 1), reward y (i + 1))) (@ProbabilityTheory.condExpKernel Omega mOmega _ mu _ ((History.historyFiltrationSucc action reward haction hreward) i) omega) = RewardKernel.actionRewardPartialTrajectoryKernel 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

Project an extension-map `partialTraj` law to the actual-action reward law. This is the reward-coordinate counterpart of `actionRewardPartialTrajectoryKernel_map_eq_of_extend_map_eq_historyFiltrationSucc_finitePairHistoryOfTrace`: first lift the deterministic frozen-prefix extension law back to the full finite-pair trace law, then reuse the finite-pair trace reward-map adapter.

theorem reward_condExpKernel_map_eq_selected_actual_action_of_actionRewardPartialTrajectoryKernel_extend_map_eq_historyFiltrationSucc_finitePairHistoryOfTrace {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] (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) (h_action_policy_eq : Filter.Eventually (fun omega : Omega => action omega (i + 1) = (policy i).action (state i (History.finiteRewardHistoryOfTrace (reward omega) i))) (ae (mu.trim ((History.historyFiltrationSucc action reward haction hreward).le i)))) (h_kernel_extend_map_eq : Filter.Eventually (fun omega : Omega => @Measure.map Omega ((j : Finset.Iic (i + 1)) -> Prod Action Rat) mOmega inferInstance (fun y : Omega => History.extendPairHistorySucc (History.finitePairHistoryOfTrace (action omega) (reward omega) i) (action y (i + 1), reward y (i + 1))) (@ProbabilityTheory.condExpKernel Omega mOmega _ mu _ ((History.historyFiltrationSucc action reward haction hreward) i) omega) = RewardKernel.actionRewardPartialTrajectoryKernel 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

Generated-action specialization of the extension-map reward-coordinate adapter. The generated shifted policy trace supplies the successor action equality; the remaining hypothesis is only the frozen-prefix extension-map `partialTraj` law.

theorem reward_condExpKernel_map_eq_selected_actual_action_of_generatedActionTraceSucc_actionRewardPartialTrajectoryKernel_extend_map_eq_historyFiltrationSucc_finitePairHistoryOfTrace {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] (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)) (defaultAction : Action) (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) (h_action_generated : action = Policy.generatedActionTraceSucc policy (fun n omega => state n (History.finiteRewardHistoryOfTrace (reward omega) n)) defaultAction) (h_kernel_extend_map_eq : Filter.Eventually (fun omega : Omega => @Measure.map Omega ((j : Finset.Iic (i + 1)) -> Prod Action Rat) mOmega inferInstance (fun y : Omega => History.extendPairHistorySucc (History.finitePairHistoryOfTrace (action omega) (reward omega) i) (action y (i + 1), reward y (i + 1))) (@ProbabilityTheory.condExpKernel Omega mOmega _ mu _ ((History.historyFiltrationSucc action reward haction hreward) i) omega) = RewardKernel.actionRewardPartialTrajectoryKernel 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

Generated-action and actual-action reward law source for the full finite pair-trace `partialTraj` law. This exposes the trajectory-law part of the generated-history route without also consuming the centered-reward kernel law. The remaining external input is the actual-action reward-coordinate conditional map law.

theorem actionRewardPartialTrajectoryKernel_map_eq_historyFiltrationSucc_finitePairHistoryOfTrace_of_generatedActionTraceSucc_reward_map_eq_actual_action {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] (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)) (defaultAction : Action) (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) (h_action_generated : action = Policy.generatedActionTraceSucc policy (fun n omega => state n (History.finiteRewardHistoryOfTrace (reward omega) n)) defaultAction) (h_reward_map_eq_actual_action : Filter.Eventually (fun omega : Omega => @Measure.map Omega Rat mOmega inferInstance (fun y : Omega => reward y (i + 1)) (@ProbabilityTheory.condExpKernel Omega mOmega _ mu _ ((History.historyFiltrationSucc action reward haction hreward) i) omega) = RewardKernel.selectedMeasure rewardKernel (context i (History.finiteRewardHistoryOfTrace (reward omega) i)) (action omega (i + 1))) (ae (mu.trim ((History.historyFiltrationSucc action reward haction hreward).le i)))) : Filter.Eventually (fun omega : Omega => @Measure.map Omega ((j : Finset.Iic (i + 1)) -> Prod Action Rat) mOmega inferInstance (fun y : Omega => History.finitePairHistoryOfTrace (action y) (reward y) (i + 1)) (@ProbabilityTheory.condExpKernel Omega mOmega _ mu _ ((History.historyFiltrationSucc action reward haction hreward) i) omega) = RewardKernel.actionRewardPartialTrajectoryKernel 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

Generated-history route from an extension-map `partialTraj` law assumption. This is the next narrowing of the `partialTraj`/`condExpKernel` gap. Instead of requiring a law identity for the full `i + 1` trace restriction, it only requires the conditional kernel pushed through the deterministic extension of the frozen old pair prefix by the random next `(Action, Reward)` pair to agree with the one-step action/reward `partialTraj` kernel. The compiled successor-decomposition bridge supplies the conversion back to the existing full-trace consumer.

theorem centeredReward_succ_condExp_eq_zero_of_actionRewardPartialTrajectoryKernel_extend_map_eq_historyFiltrationSucc_finitePairHistoryOfTrace {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] (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) (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) (h_integrable : Integrable (fun omega : Omega => (((reward omega (i + 1) - mean (context i (History.finiteRewardHistoryOfTrace (reward omega) i)) ((policy i).action (state i (History.finiteRewardHistoryOfTrace (reward omega) i))) : Rat) : Real))) mu) (h_kernel_extend_map_eq : Filter.Eventually (fun omega : Omega => @Measure.map Omega ((j : Finset.Iic (i + 1)) -> Prod Action Rat) mOmega inferInstance (fun y : Omega => History.extendPairHistorySucc (History.finitePairHistoryOfTrace (action omega) (reward omega) i) (action y (i + 1), reward y (i + 1))) (@ProbabilityTheory.condExpKernel Omega mOmega _ mu _ ((History.historyFiltrationSucc action reward haction hreward) i) omega) = RewardKernel.actionRewardPartialTrajectoryKernel 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

Generated-action and actual-action reward law source for succ-indexed conditional mean-zero. This is the current narrowest compiled consumer on the adaptive pair-law route: it combines the shifted generated-action trace, an actual-action reward-coordinate conditional map law, the extension-map `partialTraj` bridge, and the centered-reward law transfer to produce ordinary conditional mean-zero. It still assumes the actual-action reward-coordinate law rather than constructing it from an ambient trajectory measure.

theorem centeredReward_succ_condExp_eq_zero_of_generatedActionTraceSucc_reward_map_eq_actual_action {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] (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) (defaultAction : Action) (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) (h_action_generated : action = Policy.generatedActionTraceSucc policy (fun n omega => state n (History.finiteRewardHistoryOfTrace (reward omega) n)) defaultAction) (h_integrable : Integrable (fun omega : Omega => (((reward omega (i + 1) - mean (context i (History.finiteRewardHistoryOfTrace (reward omega) i)) ((policy i).action (state i (History.finiteRewardHistoryOfTrace (reward omega) i))) : Rat) : Real))) mu) (h_reward_map_eq_actual_action : Filter.Eventually (fun omega : Omega => @Measure.map Omega Rat mOmega inferInstance (fun y : Omega => reward y (i + 1)) (@ProbabilityTheory.condExpKernel Omega mOmega _ mu _ ((History.historyFiltrationSucc action reward haction hreward) i) omega) = RewardKernel.selectedMeasure rewardKernel (context i (History.finiteRewardHistoryOfTrace (reward omega) i)) (action omega (i + 1))) (ae (mu.trim ((History.historyFiltrationSucc action reward haction hreward).le i)))) : Filter.EventuallyEq (ae mu) (@condExp Omega Real ((History.historyFiltrationSucc action reward haction hreward) i) mOmega _ _ _ mu (fun omega : Omega => (((reward omega (i + 1) - mean (context i (History.finiteRewardHistoryOfTrace (reward omega) i)) ((policy i).action (state i (History.finiteRewardHistoryOfTrace (reward omega) i))) : Rat) : Real)))) (fun _omega : Omega => (0 : Real))

Actual-action pair-product law source for the full finite-pair-trace `partialTraj` law. This exposes the trajectory-law layer that was previously only consumed inside the centered-reward theorem: an actual-action pair-product conditional law is first marginalized to the actual-action reward-coordinate law, then the generated-action route turns it into the full `i + 1` finite pair-trace `partialTraj` law.

theorem actionRewardPartialTrajectoryKernel_map_eq_historyFiltrationSucc_finitePairHistoryOfTrace_of_generatedActionTraceSucc_pair_map_eq_actual_action {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] (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)) (defaultAction : Action) (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) (h_action_generated : action = Policy.generatedActionTraceSucc policy (fun n omega => state n (History.finiteRewardHistoryOfTrace (reward omega) n)) defaultAction) (h_pair_map_eq_actual_action : Filter.Eventually (fun omega : Omega => @Measure.map Omega (Prod Action Rat) mOmega inferInstance (fun y : Omega => (action omega (i + 1), reward y (i + 1))) (@ProbabilityTheory.condExpKernel Omega mOmega _ mu _ ((History.historyFiltrationSucc action reward haction hreward) i) omega) = Measure.map (Prod.mk (action omega (i + 1))) (RewardKernel.selectedMeasure rewardKernel (context i (History.finiteRewardHistoryOfTrace (reward omega) i)) (action omega (i + 1)))) (ae (mu.trim ((History.historyFiltrationSucc action reward haction hreward).le i)))) : Filter.Eventually (fun omega : Omega => @Measure.map Omega ((j : Finset.Iic (i + 1)) -> Prod Action Rat) mOmega inferInstance (fun y : Omega => History.finitePairHistoryOfTrace (action y) (reward y) (i + 1)) (@ProbabilityTheory.condExpKernel Omega mOmega _ mu _ ((History.historyFiltrationSucc action reward haction hreward) i) omega) = RewardKernel.actionRewardPartialTrajectoryKernel 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

Actual-action pair-product law source for generated-action conditional mean-zero. This packages one more upstream law shape: if the conditional kernel identifies the pair `(actual next action, next reward)` with the selected reward law pushed through `Prod.mk` at the actual next action, then `Prod.snd` marginalization provides the actual-action reward-coordinate law required by `centeredReward_succ_condExp_eq_zero_of_generatedActionTraceSucc_reward_map_eq_actual_action`.

theorem centeredReward_succ_condExp_eq_zero_of_generatedActionTraceSucc_pair_map_eq_actual_action {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] (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) (defaultAction : Action) (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) (h_action_generated : action = Policy.generatedActionTraceSucc policy (fun n omega => state n (History.finiteRewardHistoryOfTrace (reward omega) n)) defaultAction) (h_integrable : Integrable (fun omega : Omega => (((reward omega (i + 1) - mean (context i (History.finiteRewardHistoryOfTrace (reward omega) i)) ((policy i).action (state i (History.finiteRewardHistoryOfTrace (reward omega) i))) : Rat) : Real))) mu) (h_pair_map_eq_actual_action : Filter.Eventually (fun omega : Omega => @Measure.map Omega (Prod Action Rat) mOmega inferInstance (fun y : Omega => (action omega (i + 1), reward y (i + 1))) (@ProbabilityTheory.condExpKernel Omega mOmega _ mu _ ((History.historyFiltrationSucc action reward haction hreward) i) omega) = Measure.map (Prod.mk (action omega (i + 1))) (RewardKernel.selectedMeasure rewardKernel (context i (History.finiteRewardHistoryOfTrace (reward omega) i)) (action omega (i + 1)))) (ae (mu.trim ((History.historyFiltrationSucc action reward haction hreward).le i)))) : Filter.EventuallyEq (ae mu) (@condExp Omega Real ((History.historyFiltrationSucc action reward haction hreward) i) mOmega _ _ _ mu (fun omega : Omega => (((reward omega (i + 1) - mean (context i (History.finiteRewardHistoryOfTrace (reward omega) i)) ((policy i).action (state i (History.finiteRewardHistoryOfTrace (reward omega) i))) : Rat) : Real)))) (fun _omega : Omega => (0 : Real))

Fully-random next-pair product law source for the full finite-pair-trace `partialTraj` law. The hypothesis may state the conditional law of the sampled pair `(action y (i+1), reward y (i+1))`. The shifted generated-action trace freezes that action coordinate to the actual/policy-selected action under the conditional kernel, after which the actual-action pair-product adapter produces the full trace law.

theorem actionRewardPartialTrajectoryKernel_map_eq_historyFiltrationSucc_finitePairHistoryOfTrace_of_generatedActionTraceSucc_random_pair_map_eq_actual_action {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] (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)) (defaultAction : Action) (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) (h_action_generated : action = Policy.generatedActionTraceSucc policy (fun n omega => state n (History.finiteRewardHistoryOfTrace (reward omega) n)) defaultAction) (h_random_pair_map_eq_actual_action : Filter.Eventually (fun omega : Omega => @Measure.map Omega (Prod Action Rat) mOmega inferInstance (fun y : Omega => (action y (i + 1), reward y (i + 1))) (@ProbabilityTheory.condExpKernel Omega mOmega _ mu _ ((History.historyFiltrationSucc action reward haction hreward) i) omega) = Measure.map (Prod.mk (action omega (i + 1))) (RewardKernel.selectedMeasure rewardKernel (context i (History.finiteRewardHistoryOfTrace (reward omega) i)) (action omega (i + 1)))) (ae (mu.trim ((History.historyFiltrationSucc action reward haction hreward).le i)))) : Filter.Eventually (fun omega : Omega => @Measure.map Omega ((j : Finset.Iic (i + 1)) -> Prod Action Rat) mOmega inferInstance (fun y : Omega => History.finitePairHistoryOfTrace (action y) (reward y) (i + 1)) (@ProbabilityTheory.condExpKernel Omega mOmega _ mu _ ((History.historyFiltrationSucc action reward haction hreward) i) omega) = RewardKernel.actionRewardPartialTrajectoryKernel 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

Random next-pair product law source for generated-action conditional mean-zero. This is a slightly more trajectory-facing consumer than `..._pair_map_eq_actual_action`: the law hypothesis may state the conditional pushforward of the fully random next pair `(action y (i+1), reward y (i+1))`. The generated-action trace freezes the action coordinate, after which the existing actual-action pair-product consumer handles the centered-reward conditional expectation.

theorem centeredReward_succ_condExp_eq_zero_of_generatedActionTraceSucc_random_pair_map_eq_actual_action {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] (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) (defaultAction : Action) (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) (h_action_generated : action = Policy.generatedActionTraceSucc policy (fun n omega => state n (History.finiteRewardHistoryOfTrace (reward omega) n)) defaultAction) (h_integrable : Integrable (fun omega : Omega => (((reward omega (i + 1) - mean (context i (History.finiteRewardHistoryOfTrace (reward omega) i)) ((policy i).action (state i (History.finiteRewardHistoryOfTrace (reward omega) i))) : Rat) : Real))) mu) (h_random_pair_map_eq_actual_action : Filter.Eventually (fun omega : Omega => @Measure.map Omega (Prod Action Rat) mOmega inferInstance (fun y : Omega => (action y (i + 1), reward y (i + 1))) (@ProbabilityTheory.condExpKernel Omega mOmega _ mu _ ((History.historyFiltrationSucc action reward haction hreward) i) omega) = Measure.map (Prod.mk (action omega (i + 1))) (RewardKernel.selectedMeasure rewardKernel (context i (History.finiteRewardHistoryOfTrace (reward omega) i)) (action omega (i + 1)))) (ae (mu.trim ((History.historyFiltrationSucc action reward haction hreward).le i)))) : Filter.EventuallyEq (ae mu) (@condExp Omega Real ((History.historyFiltrationSucc action reward haction hreward) i) mOmega _ _ _ mu (fun omega : Omega => (((reward omega (i + 1) - mean (context i (History.finiteRewardHistoryOfTrace (reward omega) i)) ((policy i).action (state i (History.finiteRewardHistoryOfTrace (reward omega) i))) : Rat) : Real)))) (fun _omega : Omega => (0 : Real))