BanditRLProof.HistoryFiltration

Finite action histories through index `t`, represented on Mathlib's `Finset.Iic t` finite-prefix index type.

abbrev FiniteActionHistory (Action : Type v) (t : Nat)

Finite reward histories through index `t`, represented on Mathlib's `Finset.Iic t` finite-prefix index type.

abbrev FiniteRewardHistory (Reward : Type w) (t : Nat)

Pair-coordinate finite action/reward histories through index `t`.

abbrev FinitePairHistory (Action : Type v) (Reward : Type w) (t : Nat)

The paired finite action/reward history object at a finite prefix.

abbrev FiniteHistory (Action : Type v) (Reward : Type w) (t : Nat)

Restrict an infinite action trace to the finite prefix indexed by `Finset.Iic t`.

def finiteActionHistoryOfTrace {Action : Type v} (action : ActionTrace Action) (t : Nat) : FiniteActionHistory Action t

Restrict an infinite reward trace to the finite prefix indexed by `Finset.Iic t`.

def finiteRewardHistoryOfTrace {Reward : Type w} (reward : RewardTrace Reward) (t : Nat) : FiniteRewardHistory Reward t

Complete a finite reward history to an infinite trace, using `default` outside the observed prefix. The completion agrees with `history` at every coordinate through `t`. It is a deterministic history-reconstruction helper; it does not assert that the defaulted future coordinates agree with an ambient reward process.

def completeRewardTrace {Reward : Type w} (t : Nat) (history : FiniteRewardHistory Reward t) (default : Reward) : RewardTrace Reward

Restrict infinite action and reward traces to a paired finite history.

def finiteHistoryOfTrace {Action : Type v} {Reward : Type w} (action : ActionTrace Action) (reward : RewardTrace Reward) (t : Nat) : FiniteHistory Action Reward t

Restrict infinite action and reward traces to pair-coordinate history.

def finitePairHistoryOfTrace {Action : Type v} {Reward : Type w} (action : ActionTrace Action) (reward : RewardTrace Reward) (t : Nat) : FinitePairHistory Action Reward t

Extend a finite pair history from `t` to `t + 1` by appending the next pair.

def extendPairHistorySucc {Action : Type v} {Reward : Type w} {t : Nat} (history : FinitePairHistory Action Reward t) (next : Prod Action Reward) : FinitePairHistory Action Reward (t + 1)

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

theorem finiteActionHistoryOfTrace_apply {Action : Type v} (action : ActionTrace Action) (t : Nat) (i : Finset.Iic t) : finiteActionHistoryOfTrace action t i = action i.1

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

theorem finiteRewardHistoryOfTrace_apply {Reward : Type w} (reward : RewardTrace Reward) (t : Nat) (i : Finset.Iic t) : finiteRewardHistoryOfTrace reward t i = reward i.1

Completing the actual finite reward prefix recovers every original coordinate through that prefix.

theorem completeRewardTrace_finiteRewardHistoryOfTrace_apply_of_le {Reward : Type w} (reward : RewardTrace Reward) (t s : Nat) (default : Reward) (hs : s <= t) : completeRewardTrace t (finiteRewardHistoryOfTrace reward t) default s = reward s

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

theorem finiteHistoryOfTrace_fst {Action : Type v} {Reward : Type w} (action : ActionTrace Action) (reward : RewardTrace Reward) (t : Nat) : (finiteHistoryOfTrace action reward t).1 = finiteActionHistoryOfTrace action t

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

theorem finiteHistoryOfTrace_snd {Action : Type v} {Reward : Type w} (action : ActionTrace Action) (reward : RewardTrace Reward) (t : Nat) : (finiteHistoryOfTrace action reward t).2 = finiteRewardHistoryOfTrace reward t

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

theorem finitePairHistoryOfTrace_apply {Action : Type v} {Reward : Type w} (action : ActionTrace Action) (reward : RewardTrace Reward) (t : Nat) (i : Finset.Iic t) : finitePairHistoryOfTrace action reward t i = (action i.1, reward i.1)

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

theorem extendPairHistorySucc_apply_of_le {Action : Type v} {Reward : Type w} {t : Nat} (history : FinitePairHistory Action Reward t) (next : Prod Action Reward) (i : Finset.Iic (t + 1)) (hi : i.1 <= t) : extendPairHistorySucc history next i = history ⟨i.1, Finset.mem_Iic.mpr hi⟩

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

theorem extendPairHistorySucc_apply_succ {Action : Type v} {Reward : Type w} {t : Nat} (history : FinitePairHistory Action Reward t) (next : Prod Action Reward) : extendPairHistorySucc history next ⟨t + 1, Finset.mem_Iic.mpr le_rfl⟩ = next

The trace prefix at `t + 1` is the old pair prefix extended by the next action/reward pair.

theorem finitePairHistoryOfTrace_succ {Action : Type v} {Reward : Type w} (action : ActionTrace Action) (reward : RewardTrace Reward) (t : Nat) : finitePairHistoryOfTrace action reward (t + 1) = extendPairHistorySucc (finitePairHistoryOfTrace action reward t) (action (t + 1), reward (t + 1))

Project the reward coordinates from a prefix of `(Action, Reward)` pairs.

def pairHistoryRewardProjection {Action : Type v} {Reward : Type w} {t : Nat} (history : (i : Finset.Iic t) -> Prod Action Reward) : FiniteRewardHistory Reward t

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

theorem pairHistoryRewardProjection_apply {Action : Type v} {Reward : Type w} {t : Nat} (history : (i : Finset.Iic t) -> Prod Action Reward) (i : Finset.Iic t) : pairHistoryRewardProjection history i = (history i).2

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

theorem pairHistoryRewardProjection_finitePairHistoryOfTrace {Action : Type v} {Reward : Type w} (action : ActionTrace Action) (reward : RewardTrace Reward) (t : Nat) : pairHistoryRewardProjection (finitePairHistoryOfTrace action reward t) = finiteRewardHistoryOfTrace reward t

Coordinate evaluation on finite action histories is measurable.

theorem measurable_finiteActionHistory_eval {Action : Type v} [MeasurableSpace Action] (t : Nat) (i : Finset.Iic t) : Measurable (fun history : FiniteActionHistory Action t => history i)

Coordinate evaluation on finite reward histories is measurable.

theorem measurable_finiteRewardHistory_eval {Reward : Type w} [MeasurableSpace Reward] (t : Nat) (i : Finset.Iic t) : Measurable (fun history : FiniteRewardHistory Reward t => history i)

Action-coordinate evaluation on paired finite histories is measurable.

theorem measurable_finiteHistory_action_eval {Action : Type v} {Reward : Type w} [MeasurableSpace Action] [MeasurableSpace Reward] (t : Nat) (i : Finset.Iic t) : Measurable (fun history : FiniteHistory Action Reward t => history.1 i)

Reward-coordinate evaluation on paired finite histories is measurable.

theorem measurable_finiteHistory_reward_eval {Action : Type v} {Reward : Type w} [MeasurableSpace Action] [MeasurableSpace Reward] (t : Nat) (i : Finset.Iic t) : Measurable (fun history : FiniteHistory Action Reward t => history.2 i)

The reward projection from pair-coordinate histories is measurable.

theorem measurable_pairHistoryRewardProjection {Action : Type v} {Reward : Type w} [MeasurableSpace Action] [MeasurableSpace Reward] (t : Nat) : Measurable (fun history : (i : Finset.Iic t) -> Prod Action Reward => pairHistoryRewardProjection history)

Timewise measurable action and reward traces restrict to a measurable pair-coordinate finite history object.

theorem measurable_finitePairHistoryOfTrace {Omega : Type u} {Action : Type v} {Reward : Type w} [MeasurableSpace Omega] [MeasurableSpace Action] [MeasurableSpace Reward] (action : Omega -> ActionTrace Action) (reward : Omega -> RewardTrace Reward) (haction : forall t : Nat, Measurable (fun omega : Omega => action omega t)) (hreward : forall t : Nat, Measurable (fun omega : Omega => reward omega t)) (t : Nat) : Measurable (fun omega : Omega => finitePairHistoryOfTrace (action omega) (reward omega) t)

The successor-extension map for pair histories is measurable.

theorem measurable_extendPairHistorySucc {Action : Type v} {Reward : Type w} {t : Nat} [MeasurableSpace Action] [MeasurableSpace Reward] : Measurable (fun input : Prod (FinitePairHistory Action Reward t) (Prod Action Reward) => extendPairHistorySucc input.1 input.2)

Timewise measurable action traces restrict to measurable finite action-history objects.

theorem measurable_finiteActionHistoryOfTrace {Omega : Type u} {Action : Type v} [MeasurableSpace Omega] [MeasurableSpace Action] (action : Omega -> ActionTrace Action) (haction : forall t : Nat, Measurable (fun omega : Omega => action omega t)) (t : Nat) : Measurable (fun omega : Omega => finiteActionHistoryOfTrace (action omega) t)

Timewise measurable reward traces restrict to measurable finite reward-history objects.

theorem measurable_finiteRewardHistoryOfTrace {Omega : Type u} {Reward : Type w} [MeasurableSpace Omega] [MeasurableSpace Reward] (reward : Omega -> RewardTrace Reward) (hreward : forall t : Nat, Measurable (fun omega : Omega => reward omega t)) (t : Nat) : Measurable (fun omega : Omega => finiteRewardHistoryOfTrace (reward omega) t)

Timewise measurable action and reward traces restrict to a measurable paired finite history object.

theorem measurable_finiteHistoryOfTrace {Omega : Type u} {Action : Type v} {Reward : Type w} [MeasurableSpace Omega] [MeasurableSpace Action] [MeasurableSpace Reward] (action : Omega -> ActionTrace Action) (reward : Omega -> RewardTrace Reward) (haction : forall t : Nat, Measurable (fun omega : Omega => action omega t)) (hreward : forall t : Nat, Measurable (fun omega : Omega => reward omega t)) (t : Nat) : Measurable (fun omega : Omega => finiteHistoryOfTrace (action omega) (reward omega) t)

The singleton-valued action/reward events visible before time `t`. This is deliberately discrete: it is shaped for finite arms and discrete local reward traces such as `Rat`, where singleton events are the current compiled measurability surface.

def historyGenerators {Omega : Type u} {Action : Type v} {Reward : Type w} (action : Omega -> ActionTrace Action) (reward : Omega -> RewardTrace Reward) (t : Nat) : Set (Set Omega)

Past history generators are monotone in the horizon.

theorem historyGenerators_mono {Omega : Type u} {Action : Type v} {Reward : Type w} (action : Omega -> ActionTrace Action) (reward : Omega -> RewardTrace Reward) {t u : Nat} (htu : t <= u) : Set.Subset (historyGenerators action reward t) (historyGenerators action reward u)

The sigma-algebra generated by past action/reward singleton events.

def historyMeasurableSpace {Omega : Type u} {Action : Type v} {Reward : Type w} (action : Omega -> ActionTrace Action) (reward : Omega -> RewardTrace Reward) (t : Nat) : MeasurableSpace Omega

The history sigma-algebras are monotone.

theorem historyMeasurableSpace_mono {Omega : Type u} {Action : Type v} {Reward : Type w} (action : Omega -> ActionTrace Action) (reward : Omega -> RewardTrace Reward) {t u : Nat} (htu : t <= u) : historyMeasurableSpace action reward t <= historyMeasurableSpace action reward u

The generated history sigma-algebra is a sub-sigma-algebra of the ambient measurable space when action and reward coordinates are timewise measurable.

theorem historyMeasurableSpace_le {Omega : Type u} {Action : Type v} {Reward : Type w} [MeasurableSpace Omega] [MeasurableSpace Action] [MeasurableSingletonClass Action] [MeasurableSpace Reward] [MeasurableSingletonClass Reward] (action : Omega -> ActionTrace Action) (reward : Omega -> RewardTrace Reward) (haction : forall t : Nat, Measurable (fun omega : Omega => action omega t)) (hreward : forall t : Nat, Measurable (fun omega : Omega => reward omega t)) (t : Nat) : historyMeasurableSpace action reward t <= (inferInstance : MeasurableSpace Omega)

The local history filtration generated by past action/reward singleton events. This is the compiled `FILTRATION-HISTORY` canary. It is intentionally only a filtration construction, not a policy/predictability or conditional-expectation theorem.

def historyFiltration {Omega : Type u} {Action : Type v} {Reward : Type w} [mOmega : MeasurableSpace Omega] [MeasurableSpace Action] [MeasurableSingletonClass Action] [MeasurableSpace Reward] [MeasurableSingletonClass Reward] (action : Omega -> ActionTrace Action) (reward : Omega -> RewardTrace Reward) (haction : forall t : Nat, Measurable (fun omega : Omega => action omega t)) (hreward : forall t : Nat, Measurable (fun omega : Omega => reward omega t)) : Filtration Nat mOmega where

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

theorem historyFiltration_apply {Omega : Type u} {Action : Type v} {Reward : Type w} [mOmega : MeasurableSpace Omega] [MeasurableSpace Action] [MeasurableSingletonClass Action] [MeasurableSpace Reward] [MeasurableSingletonClass Reward] (action : Omega -> ActionTrace Action) (reward : Omega -> RewardTrace Reward) (haction : forall t : Nat, Measurable (fun omega : Omega => action omega t)) (hreward : forall t : Nat, Measurable (fun omega : Omega => reward omega t)) (t : Nat) : (historyFiltration action reward haction hreward t : MeasurableSpace Omega) = historyMeasurableSpace action reward t

The one-step shifted history filtration. `historyFiltration` at index `t` contains observations with index `< t`. For adapted reward increments it is often more convenient to index the filtration by observations available after time `t`, i.e. `< t + 1`.

def historyFiltrationSucc {Omega : Type u} {Action : Type v} {Reward : Type w} [mOmega : MeasurableSpace Omega] [MeasurableSpace Action] [MeasurableSingletonClass Action] [MeasurableSpace Reward] [MeasurableSingletonClass Reward] (action : Omega -> ActionTrace Action) (reward : Omega -> RewardTrace Reward) (haction : forall t : Nat, Measurable (fun omega : Omega => action omega t)) (hreward : forall t : Nat, Measurable (fun omega : Omega => reward omega t)) : Filtration Nat mOmega where

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

theorem historyFiltrationSucc_apply {Omega : Type u} {Action : Type v} {Reward : Type w} [mOmega : MeasurableSpace Omega] [MeasurableSpace Action] [MeasurableSingletonClass Action] [MeasurableSpace Reward] [MeasurableSingletonClass Reward] (action : Omega -> ActionTrace Action) (reward : Omega -> RewardTrace Reward) (haction : forall t : Nat, Measurable (fun omega : Omega => action omega t)) (hreward : forall t : Nat, Measurable (fun omega : Omega => reward omega t)) (t : Nat) : (historyFiltrationSucc action reward haction hreward t : MeasurableSpace Omega) = historyFiltration action reward haction hreward (t + 1)

Past action singleton events are measurable in the generated history.

theorem measurableSet_action_mem_historyFiltration {Omega : Type u} {Action : Type v} {Reward : Type w} [mOmega : MeasurableSpace Omega] [MeasurableSpace Action] [MeasurableSingletonClass Action] [MeasurableSpace Reward] [MeasurableSingletonClass Reward] (action : Omega -> ActionTrace Action) (reward : Omega -> RewardTrace Reward) (haction : forall t : Nat, Measurable (fun omega : Omega => action omega t)) (hreward : forall t : Nat, Measurable (fun omega : Omega => reward omega t)) {i t : Nat} (hit : i < t) (a : Action) : MeasurableSet[historyFiltration action reward haction hreward t] (Set.preimage (fun omega => action omega i) (Set.singleton a))

Past action coordinates are measurable with respect to the generated history. This is a deliberately discrete `ADAPTED-ACTION` canary: it uses countability and singleton-event measurability, not a full policy-predictability contract.

theorem measurable_action_mem_historyFiltration_of_lt {Omega : Type u} {Action : Type v} {Reward : Type w} [mOmega : MeasurableSpace Omega] [MeasurableSpace Action] [MeasurableSingletonClass Action] [Countable Action] [MeasurableSpace Reward] [MeasurableSingletonClass Reward] (action : Omega -> ActionTrace Action) (reward : Omega -> RewardTrace Reward) (haction : forall t : Nat, Measurable (fun omega : Omega => action omega t)) (hreward : forall t : Nat, Measurable (fun omega : Omega => reward omega t)) {i t : Nat} (hit : i < t) : @Measurable Omega Action (historyFiltration action reward haction hreward t) inferInstance (fun omega => action omega i)

Past reward singleton events are measurable in the generated history.

theorem measurableSet_reward_mem_historyFiltration {Omega : Type u} {Action : Type v} {Reward : Type w} [mOmega : MeasurableSpace Omega] [MeasurableSpace Action] [MeasurableSingletonClass Action] [MeasurableSpace Reward] [MeasurableSingletonClass Reward] (action : Omega -> ActionTrace Action) (reward : Omega -> RewardTrace Reward) (haction : forall t : Nat, Measurable (fun omega : Omega => action omega t)) (hreward : forall t : Nat, Measurable (fun omega : Omega => reward omega t)) {i t : Nat} (hit : i < t) (r : Reward) : MeasurableSet[historyFiltration action reward haction hreward t] (Set.preimage (fun omega => reward omega i) (Set.singleton r))

Past reward coordinates are measurable with respect to the generated history. This is the reward-side companion canary for the local history filtration; it still does not instantiate conditional reward laws or martingale differences.

theorem measurable_reward_mem_historyFiltration_of_lt {Omega : Type u} {Action : Type v} {Reward : Type w} [mOmega : MeasurableSpace Omega] [MeasurableSpace Action] [MeasurableSingletonClass Action] [MeasurableSpace Reward] [MeasurableSingletonClass Reward] [Countable Reward] (action : Omega -> ActionTrace Action) (reward : Omega -> RewardTrace Reward) (haction : forall t : Nat, Measurable (fun omega : Omega => action omega t)) (hreward : forall t : Nat, Measurable (fun omega : Omega => reward omega t)) {i t : Nat} (hit : i < t) : @Measurable Omega Reward (historyFiltration action reward haction hreward t) inferInstance (fun omega => reward omega i)

Finite pair histories up to `n` are measurable with respect to any generated history filtration level strictly after `n`. This is the product-valued counterpart of the coordinate measurability canaries above. It is intentionally countable/discrete, matching the singleton-event definition of `historyMeasurableSpace`.

theorem measurable_finitePairHistoryOfTrace_mem_historyFiltration_of_lt {Omega : Type u} {Action : Type v} {Reward : Type w} [mOmega : MeasurableSpace Omega] [MeasurableSpace Action] [MeasurableSingletonClass Action] [Countable Action] [MeasurableSpace Reward] [MeasurableSingletonClass Reward] [Countable Reward] (action : Omega -> ActionTrace Action) (reward : Omega -> RewardTrace Reward) (haction : forall t : Nat, Measurable (fun omega : Omega => action omega t)) (hreward : forall t : Nat, Measurable (fun omega : Omega => reward omega t)) {n t : Nat} (hnt : n < t) : @Measurable Omega ((i : Finset.Iic n) -> Prod Action Reward) (historyFiltration (mOmega

The generated history filtration after observing indices `<= n` is exactly the comap of the finite pair-history restriction map. The forward inclusion follows from the singleton generators. The reverse inclusion follows from the previous product-valued measurability wrapper. This equality is a local bridge between the hand-rolled history filtration and Mathlib conditional-distribution statements conditioned on finite prefixes.

theorem historyFiltration_succ_eq_comap_finitePairHistoryOfTrace {Omega : Type u} {Action : Type v} {Reward : Type w} [mOmega : MeasurableSpace Omega] [MeasurableSpace Action] [MeasurableSingletonClass Action] [Countable Action] [MeasurableSpace Reward] [MeasurableSingletonClass Reward] [Countable Reward] (action : Omega -> ActionTrace Action) (reward : Omega -> RewardTrace Reward) (haction : forall t : Nat, Measurable (fun omega : Omega => action omega t)) (hreward : forall t : Nat, Measurable (fun omega : Omega => reward omega t)) (n : Nat) : (historyFiltration action reward haction hreward (n + 1) : MeasurableSpace Omega) = (inferInstance : MeasurableSpace ((i : Finset.Iic n) -> Prod Action Reward)).comap (fun omega : Omega => finitePairHistoryOfTrace (action omega) (reward omega) n)

The shifted generated-history filtration at time `n` is exactly the comap of the finite pair-history restriction through index `n`. This is the `historyFiltrationSucc`-indexed form used by the conditional-kernel source contracts.

theorem historyFiltrationSucc_eq_comap_finitePairHistoryOfTrace {Omega : Type u} {Action : Type v} {Reward : Type w} [mOmega : MeasurableSpace Omega] [MeasurableSpace Action] [MeasurableSingletonClass Action] [Countable Action] [MeasurableSpace Reward] [MeasurableSingletonClass Reward] [Countable Reward] (action : Omega -> ActionTrace Action) (reward : Omega -> RewardTrace Reward) (haction : forall t : Nat, Measurable (fun omega : Omega => action omega t)) (hreward : forall t : Nat, Measurable (fun omega : Omega => reward omega t)) (n : Nat) : (historyFiltrationSucc action reward haction hreward n : MeasurableSpace Omega) = (inferInstance : MeasurableSpace ((i : Finset.Iic n) -> Prod Action Reward)).comap (fun omega : Omega => finitePairHistoryOfTrace (action omega) (reward omega) n)

Two shifted history filtrations agree at time `n` when their action traces agree pointwise through `n` and they use the same reward trace. The proof passes through the finite-pair-history comap characterization. It is useful when an adaptive policy has a deterministic exploration prefix.

theorem historyFiltrationSucc_eq_of_action_eq_on_prefix {Omega : Type u} {Action : Type v} {Reward : Type w} [mOmega : MeasurableSpace Omega] [MeasurableSpace Action] [MeasurableSingletonClass Action] [Countable Action] [MeasurableSpace Reward] [MeasurableSingletonClass Reward] [Countable Reward] (action0 action1 : Omega -> ActionTrace Action) (reward : Omega -> RewardTrace Reward) (haction0 : forall t : Nat, Measurable (fun omega : Omega => action0 omega t)) (haction1 : forall t : Nat, Measurable (fun omega : Omega => action1 omega t)) (hreward : forall t : Nat, Measurable (fun omega : Omega => reward omega t)) (n : Nat) (haction_eq : forall omega i, i <= n -> action0 omega i = action1 omega i) : (historyFiltrationSucc action0 reward haction0 hreward n : MeasurableSpace Omega) = (historyFiltrationSucc action1 reward haction1 hreward n : MeasurableSpace Omega)