BanditRLProof.PolicyMeasurability

A policy whose action map is measurable from a history/context state into the action space.

structure MeasurablePolicy (State : Type u) (Action : Type v) [MeasurableSpace State] [MeasurableSpace Action] where

A measurable history/context state composed with a measurable policy is a measurable action random variable.

theorem measurable_action_of_measurable_state {Omega : Type w} {State : Type u} {Action : Type v} [MeasurableSpace Omega] [MeasurableSpace State] [MeasurableSpace Action] (policy : MeasurablePolicy State Action) (state : Omega -> State) (hstate : Measurable state) : Measurable (fun omega : Omega => policy.action (state omega))

If a history/context state is measurable with respect to a filtration at time `t`, then the action selected by a measurable policy from that state is also measurable with respect to the same filtration.

theorem measurable_action_mem_filtration_of_measurable_state {Omega : Type w} {State : Type u} {Action : Type v} [mOmega : MeasurableSpace Omega] [MeasurableSpace State] [MeasurableSpace Action] (F : MeasureTheory.Filtration Nat mOmega) (policy : MeasurablePolicy State Action) (state : Omega -> State) (t : Nat) (hstate : @Measurable Omega State (F t) inferInstance state) : @Measurable Omega Action (F t) inferInstance (fun omega : Omega => policy.action (state omega))

Specialization of policy measurability to the generated history filtration: once a policy state is measurable from the past action/reward history at time `t`, the policy-selected action is measurable from that same history.

theorem measurable_action_mem_historyFiltration_of_measurable_state {Omega : Type w} {TraceAction : Type v} {Reward : Type x} {State : Type u} {PolicyAction : Type v} [mOmega : MeasurableSpace Omega] [MeasurableSpace TraceAction] [MeasurableSingletonClass TraceAction] [MeasurableSpace Reward] [MeasurableSingletonClass Reward] [MeasurableSpace State] [MeasurableSpace PolicyAction] (traceAction : Omega -> ActionTrace TraceAction) (reward : Omega -> RewardTrace Reward) (haction : forall t : Nat, Measurable (fun omega : Omega => traceAction omega t)) (hreward : forall t : Nat, Measurable (fun omega : Omega => reward omega t)) (policy : MeasurablePolicy State PolicyAction) (state : Omega -> State) (t : Nat) (hstate : @Measurable Omega State (History.historyFiltration traceAction reward haction hreward t) inferInstance state) : @Measurable Omega PolicyAction (History.historyFiltration traceAction reward haction hreward t) inferInstance (fun omega : Omega => policy.action (state omega))

The action trace generated by applying a fixed measurable policy to a time-indexed history/context state process.

def generatedActionTrace {Omega : Type w} {State : Type u} {Action : Type v} [MeasurableSpace State] [MeasurableSpace Action] (policy : MeasurablePolicy State Action) (state : Nat -> Omega -> State) : Omega -> ActionTrace Action

If every history/context state coordinate is ambient-measurable, every coordinate of the generated policy action trace is ambient-measurable.

theorem measurable_generatedActionTrace_eval_of_measurable_state {Omega : Type w} {State : Type u} {Action : Type v} [MeasurableSpace Omega] [MeasurableSpace State] [MeasurableSpace Action] (policy : MeasurablePolicy State Action) (state : Nat -> Omega -> State) (hstate : forall t : Nat, Measurable (state t)) (t : Nat) : Measurable (fun omega : Omega => (generatedActionTrace policy state omega) t)

The shifted action trace generated by a time-indexed policy. The value at time `t + 1` is selected by `policy t` from the state available at time `t`. This matches the one-step kernel convention used later by `RewardKernel.actionRewardHistoryStepKernelFamily`.

def generatedActionTraceSucc {Omega : Type w} {State : Type u} {Action : Type v} [MeasurableSpace State] [MeasurableSpace Action] (policy : Nat -> MeasurablePolicy State Action) (state : Nat -> Omega -> State) (defaultAction : Action) : Omega -> ActionTrace Action

The initial value of the shifted generated trace is the chosen default.

theorem generatedActionTraceSucc_zero {Omega : Type w} {State : Type u} {Action : Type v} [MeasurableSpace State] [MeasurableSpace Action] (policy : Nat -> MeasurablePolicy State Action) (state : Nat -> Omega -> State) (defaultAction : Action) (omega : Omega) : (generatedActionTraceSucc policy state defaultAction omega) 0 = defaultAction

At time `t + 1`, the shifted generated trace is exactly the action selected by `policy t`.

theorem generatedActionTraceSucc_succ {Omega : Type w} {State : Type u} {Action : Type v} [MeasurableSpace State] [MeasurableSpace Action] (policy : Nat -> MeasurablePolicy State Action) (state : Nat -> Omega -> State) (defaultAction : Action) (omega : Omega) (t : Nat) : (generatedActionTraceSucc policy state defaultAction omega) (t + 1) = (policy t).action (state t omega)

Function-level equality for the predictable `t + 1` coordinate.

theorem generatedActionTraceSucc_succ_eq {Omega : Type w} {State : Type u} {Action : Type v} [MeasurableSpace State] [MeasurableSpace Action] (policy : Nat -> MeasurablePolicy State Action) (state : Nat -> Omega -> State) (defaultAction : Action) (t : Nat) : (fun omega : Omega => (generatedActionTraceSucc policy state defaultAction omega) (t + 1)) = (fun omega : Omega => (policy t).action (state t omega))

If every state coordinate is ambient-measurable, every coordinate of the shifted generated policy action trace is ambient-measurable.

theorem measurable_generatedActionTraceSucc_eval_of_measurable_state {Omega : Type w} {State : Type u} {Action : Type v} [MeasurableSpace Omega] [MeasurableSpace State] [MeasurableSpace Action] (policy : Nat -> MeasurablePolicy State Action) (state : Nat -> Omega -> State) (defaultAction : Action) (hstate : forall t : Nat, Measurable (state t)) (t : Nat) : Measurable (fun omega : Omega => (generatedActionTraceSucc policy state defaultAction omega) t)

Predictable-coordinate measurability for the shifted generated action trace: if the state at time `t` is measurable in `F t`, then action coordinate `t + 1` is also measurable in `F t`.

theorem measurable_generatedActionTraceSucc_succ_mem_filtration_of_measurable_state {Omega : Type w} {State : Type u} {Action : Type v} [mOmega : MeasurableSpace Omega] [MeasurableSpace State] [MeasurableSpace Action] (F : MeasureTheory.Filtration Nat mOmega) (policy : Nat -> MeasurablePolicy State Action) (state : Nat -> Omega -> State) (defaultAction : Action) (hstate : forall t : Nat, @Measurable Omega State (F t) inferInstance (state t)) (t : Nat) : @Measurable Omega Action (F t) inferInstance (fun omega : Omega => (generatedActionTraceSucc policy state defaultAction omega) (t + 1))

If every history/context state coordinate is measurable with respect to the filtration at the same time, every coordinate of the generated policy action trace is measurable with respect to that filtration.

theorem measurable_generatedActionTrace_eval_mem_filtration_of_measurable_state {Omega : Type w} {State : Type u} {Action : Type v} [mOmega : MeasurableSpace Omega] [MeasurableSpace State] [MeasurableSpace Action] (F : MeasureTheory.Filtration Nat mOmega) (policy : MeasurablePolicy State Action) (state : Nat -> Omega -> State) (hstate : forall t : Nat, @Measurable Omega State (F t) inferInstance (state t)) (t : Nat) : @Measurable Omega Action (F t) inferInstance (fun omega : Omega => (generatedActionTrace policy state omega) t)

Specialization of generated policy trace measurability to the generated history filtration.

theorem measurable_generatedActionTrace_eval_mem_historyFiltration_of_measurable_state {Omega : Type w} {TraceAction : Type v} {Reward : Type x} {State : Type u} {PolicyAction : Type v} [mOmega : MeasurableSpace Omega] [MeasurableSpace TraceAction] [MeasurableSingletonClass TraceAction] [MeasurableSpace Reward] [MeasurableSingletonClass Reward] [MeasurableSpace State] [MeasurableSpace PolicyAction] (traceAction : Omega -> ActionTrace TraceAction) (reward : Omega -> RewardTrace Reward) (haction : forall t : Nat, Measurable (fun omega : Omega => traceAction omega t)) (hreward : forall t : Nat, Measurable (fun omega : Omega => reward omega t)) (policy : MeasurablePolicy State PolicyAction) (state : Nat -> Omega -> State) (hstate : forall t : Nat, @Measurable Omega State (History.historyFiltration traceAction reward haction hreward t) inferInstance (state t)) (t : Nat) : @Measurable Omega PolicyAction (History.historyFiltration traceAction reward haction hreward t) inferInstance (fun omega : Omega => (generatedActionTrace policy state omega) t)