BanditRLProof.Algorithms.ThompsonMeasurableTrajectory

Jointly measurable feedback environment. Freezing the first kernel input recovers the pointwise `HistoryEnvironment` consumed by the density route.

structure MeasurableHistoryEnvironment (Env : Type u) (Action : Type v) (Reward : Type w) [MeasurableSpace Env] [MeasurableSpace Action] [MeasurableSpace Reward] where

Freeze the measurable environment input to recover the pointwise API.

noncomputable def MeasurableHistoryEnvironment.at {Env : Type u} {Action : Type v} {Reward : Type w} [MeasurableSpace Env] [MeasurableSpace Action] [MeasurableSpace Reward] (environment : MeasurableHistoryEnvironment Env Action Reward) (env : Env) : HistoryEnvironment Action Reward where

Jointly measurable law of the initial action/reward pair.

noncomputable def measurableEnvironmentInitialPairKernel {Env : Type u} {Action : Type v} {Reward : Type w} [MeasurableSpace Env] [MeasurableSpace Action] [MeasurableSpace Reward] (algorithm : HistoryAlgorithm Action Reward) (environment : MeasurableHistoryEnvironment Env Action Reward) : ProbabilityTheory.Kernel Env (Action × Reward)

Jointly measurable successor pair kernel over environment and history.

noncomputable def measurableEnvironmentHistoryStepKernel {Env : Type u} {Action : Type v} {Reward : Type w} [MeasurableSpace Env] [MeasurableSpace Action] [MeasurableSpace Reward] (algorithm : HistoryAlgorithm Action Reward) (environment : MeasurableHistoryEnvironment Env Action Reward) (n : Nat) : ProbabilityTheory.Kernel (Env × History.FinitePairHistory Action Reward n) (Action × Reward)

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

theorem measurableEnvironmentInitialPairKernel_apply {Env : Type u} {Action : Type v} {Reward : Type w} [MeasurableSpace Env] [MeasurableSpace Action] [MeasurableSpace Reward] (algorithm : HistoryAlgorithm Action Reward) (environment : MeasurableHistoryEnvironment Env Action Reward) (env : Env) : measurableEnvironmentInitialPairKernel algorithm environment env = algorithm.initialAction ⊗ₘ (environment.at env).initialFeedback

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

theorem measurableEnvironmentHistoryStepKernel_apply {Env : Type u} {Action : Type v} {Reward : Type w} [MeasurableSpace Env] [MeasurableSpace Action] [MeasurableSpace Reward] (algorithm : HistoryAlgorithm Action Reward) (environment : MeasurableHistoryEnvironment Env Action Reward) (n : Nat) (env : Env) (history : History.FinitePairHistory Action Reward n) : measurableEnvironmentHistoryStepKernel algorithm environment n (env, history) = historyStepKernel algorithm (environment.at env) n history

Environment coordinate stored in a finite internal state prefix.

def measurableTrajectoryPrefixEnvironment {Env : Type u} {Action : Type v} {Reward : Type w} {n : Nat} (statePrefix : (i : Finset.Iic n) -> Env × (Action × Reward)) : Env

Pair history stored after the dummy zeroth internal state.

def measurableTrajectoryPrefixHistory {Env : Type u} {Action : Type v} {Reward : Type w} {n : Nat} (statePrefix : (i : Finset.Iic (n + 1)) -> Env × (Action × Reward)) : History.FinitePairHistory Action Reward n

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

theorem measurable_measurableTrajectoryPrefixEnvironment {Env : Type u} {Action : Type v} {Reward : Type w} {n : Nat} [MeasurableSpace Env] [MeasurableSpace Action] [MeasurableSpace Reward] : Measurable (measurableTrajectoryPrefixEnvironment (Env

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

theorem measurable_measurableTrajectoryPrefixHistory {Env : Type u} {Action : Type v} {Reward : Type w} {n : Nat} [MeasurableSpace Env] [MeasurableSpace Action] [MeasurableSpace Reward] : Measurable (measurableTrajectoryPrefixHistory (Env

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

theorem measurable_measurableTrajectoryPrefixEnvironmentHistory {Env : Type u} {Action : Type v} {Reward : Type w} {n : Nat} [MeasurableSpace Env] [MeasurableSpace Action] [MeasurableSpace Reward] : Measurable (fun statePrefix : (i : Finset.Iic (n + 1)) -> Env × (Action × Reward) => (measurableTrajectoryPrefixEnvironment (n

Attach a kernel output to the environment already present in its input.

noncomputable def retainEnvironmentKernel {Input : Type u} {Env : Type v} {Output : Type w} [MeasurableSpace Input] [MeasurableSpace Env] [MeasurableSpace Output] (env : Input -> Env) (_henv : Measurable env) (kernel : ProbabilityTheory.Kernel Input Output) : ProbabilityTheory.Kernel Input (Env × Output)

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

theorem retainEnvironmentKernel_apply {Input : Type u} {Env : Type v} {Output : Type w} [MeasurableSpace Input] [MeasurableSpace Env] [MeasurableSpace Output] (env : Input -> Env) (henv : Measurable env) (kernel : ProbabilityTheory.Kernel Input Output) [ProbabilityTheory.IsMarkovKernel kernel] (input : Input) : retainEnvironmentKernel env henv kernel input = (kernel input).map (Prod.mk (env input))

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

theorem retainEnvironmentKernel_map_snd {Input : Type u} {Env : Type v} {Output : Type w} [MeasurableSpace Input] [MeasurableSpace Env] [MeasurableSpace Output] (env : Input -> Env) (henv : Measurable env) (kernel : ProbabilityTheory.Kernel Input Output) [ProbabilityTheory.IsMarkovKernel kernel] : (retainEnvironmentKernel env henv kernel).map Prod.snd = kernel

Stable internal step family used by the measurable trajectory producer.

noncomputable def canonicalMeasurableEnvironmentStepKernel {Env : Type u} {Action : Type v} {Reward : Type w} [MeasurableSpace Env] [MeasurableSpace Action] [MeasurableSpace Reward] (algorithm : HistoryAlgorithm Action Reward) (environment : MeasurableHistoryEnvironment Env Action Reward) : (n : Nat) -> ProbabilityTheory.Kernel ((i : Finset.Iic n) -> Env × (Action × Reward)) (Env × (Action × Reward)) | 0 => retainEnvironmentKernel measurableTrajectoryPrefixEnvironment measurable_measurableTrajectoryPrefixEnvironment ((measurableEnvironmentInitialPairKernel algorithm environment).comap measurableTrajectoryPrefixEnvironment measurable_measurableTrajectoryPrefixEnvironment) | n + 1 => retainEnvironmentKernel measurableTrajectoryPrefixEnvironment (measurable_measurableTrajectoryPrefixEnvironment (n

Dropping the retained environment recovers the visible pair step law.

theorem canonicalMeasurableEnvironmentStepKernel_succ_apply_map_snd {Env : Type u} {Action : Type v} {Reward : Type w} [MeasurableSpace Env] [MeasurableSpace Action] [MeasurableSpace Reward] (algorithm : HistoryAlgorithm Action Reward) (environment : MeasurableHistoryEnvironment Env Action Reward) (n : Nat) (statePrefix : (i : Finset.Iic (n + 1)) -> Env × (Action × Reward)) : (canonicalMeasurableEnvironmentStepKernel algorithm environment (n + 1) statePrefix).map Prod.snd = historyStepKernel algorithm (environment.at (measurableTrajectoryPrefixEnvironment statePrefix)) n (measurableTrajectoryPrefixHistory statePrefix)

Dummy time-zero prefix used only to seed `Kernel.traj`.

noncomputable def measurableEnvironmentInitialStatePrefix {Env : Type u} {Action : Type v} {Reward : Type w} [Nonempty Action] [Nonempty Reward] (env : Env) : (i : Finset.Iic 0) -> Env × (Action × Reward)

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

theorem measurable_measurableEnvironmentInitialStatePrefix {Env : Type u} {Action : Type v} {Reward : Type w} [MeasurableSpace Env] [MeasurableSpace Action] [MeasurableSpace Reward] [Nonempty Action] [Nonempty Reward] : Measurable (measurableEnvironmentInitialStatePrefix (Env

Pair trace obtained by dropping the dummy internal time-zero state.

def measurableEnvironmentPairTrace {Env : Type u} {Action : Type v} {Reward : Type w} (trajectory : (n : Nat) -> Env × (Action × Reward)) : (n : Nat) -> Action × Reward

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

theorem measurable_measurableEnvironmentPairTrace {Env : Type u} {Action : Type v} {Reward : Type w} [MeasurableSpace Env] [MeasurableSpace Action] [MeasurableSpace Reward] : Measurable (measurableEnvironmentPairTrace (Env

Complete measurable pair-trajectory kernel generated from the joint feedback environment, with no externally supplied trajectory-kernel premise.

noncomputable def canonicalMeasurableEnvironmentTrajectoryKernel {Env : Type u} {Action : Type v} {Reward : Type w} [MeasurableSpace Env] [MeasurableSpace Action] [MeasurableSpace Reward] [Nonempty Action] [Nonempty Reward] (algorithm : HistoryAlgorithm Action Reward) (environment : MeasurableHistoryEnvironment Env Action Reward) : ProbabilityTheory.Kernel Env ((n : Nat) -> Action × Reward)

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

theorem canonicalMeasurableEnvironmentTrajectoryKernel_apply {Env : Type u} {Action : Type v} {Reward : Type w} [MeasurableSpace Env] [MeasurableSpace Action] [MeasurableSpace Reward] [Nonempty Action] [Nonempty Reward] (algorithm : HistoryAlgorithm Action Reward) (environment : MeasurableHistoryEnvironment Env Action Reward) (env : Env) : canonicalMeasurableEnvironmentTrajectoryKernel algorithm environment env = (ProbabilityTheory.Kernel.traj (canonicalMeasurableEnvironmentStepKernel algorithm environment) 0 (measurableEnvironmentInitialStatePrefix (Action

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

theorem measurableTrajectoryPrefixEnvironment_initialStatePrefix {Env : Type u} {Action : Type v} {Reward : Type w} [Nonempty Action] [Nonempty Reward] (env : Env) : measurableTrajectoryPrefixEnvironment (measurableEnvironmentInitialStatePrefix (Action

Under a fixed input environment, every finite internal prefix retains it.

theorem measurableTrajectoryPrefixEnvironment_ae_eq_of_traj {Env : Type u} {Action : Type v} {Reward : Type w} [MeasurableSpace Env] [StandardBorelSpace Env] [MeasurableSpace Action] [MeasurableSpace Reward] [Nonempty Action] [Nonempty Reward] (algorithm : HistoryAlgorithm Action Reward) (environment : MeasurableHistoryEnvironment Env Action Reward) (env : Env) (n : Nat) : (measurableTrajectoryPrefixEnvironment (Env

The generated trajectory kernel has the configured initial pair law.

theorem canonicalMeasurableEnvironmentTrajectoryKernel_map_eval_zero {Env : Type u} {Action : Type v} {Reward : Type w} [MeasurableSpace Env] [MeasurableSpace Action] [MeasurableSpace Reward] [Nonempty Action] [Nonempty Reward] (algorithm : HistoryAlgorithm Action Reward) (environment : MeasurableHistoryEnvironment Env Action Reward) : (canonicalMeasurableEnvironmentTrajectoryKernel algorithm environment).map (fun trajectory => trajectory 0) = measurableEnvironmentInitialPairKernel algorithm environment

Joint finite-prefix/next-pair law of the projected measurable trajectory.

theorem canonicalMeasurableEnvironmentTrajectoryKernel_map_prefix_next_eq_compProd {Env : Type u} {Action : Type v} {Reward : Type w} [MeasurableSpace Env] [StandardBorelSpace Env] [MeasurableSpace Action] [StandardBorelSpace Action] [Nonempty Action] [MeasurableSpace Reward] [StandardBorelSpace Reward] [Nonempty Reward] (algorithm : HistoryAlgorithm Action Reward) (environment : MeasurableHistoryEnvironment Env Action Reward) (env : Env) (n : Nat) : (canonicalMeasurableEnvironmentTrajectoryKernel algorithm environment env).map (fun trajectory => (Preorder.frestrictLe n trajectory, trajectory (n + 1))) = (canonicalMeasurableEnvironmentTrajectoryKernel algorithm environment env).map (Preorder.frestrictLe n) ⊗ₘ historyStepKernel algorithm (environment.at env) n

The projected trajectory has the configured shifted successor pair law.

theorem canonicalMeasurableEnvironmentTrajectoryKernel_condDistrib_succ {Env : Type u} {Action : Type v} {Reward : Type w} [MeasurableSpace Env] [StandardBorelSpace Env] [MeasurableSpace Action] [StandardBorelSpace Action] [Nonempty Action] [MeasurableSpace Reward] [StandardBorelSpace Reward] [Nonempty Reward] (algorithm : HistoryAlgorithm Action Reward) (environment : MeasurableHistoryEnvironment Env Action Reward) (env : Env) (n : Nat) : ProbabilityTheory.condDistrib (fun trajectory : (k : Nat) -> Action × Reward => trajectory (n + 1)) (Preorder.frestrictLe n) (canonicalMeasurableEnvironmentTrajectoryKernel algorithm environment env) =ᵐ[ (canonicalMeasurableEnvironmentTrajectoryKernel algorithm environment env).map (Preorder.frestrictLe n)] historyStepKernel algorithm (environment.at env) n

The generated measurable trajectory kernel has the canonical fixed-environment law once its shifted successor conditional laws are identified. The initial law is discharged internally by the preceding theorem.

theorem canonicalMeasurableEnvironmentTrajectoryKernel_apply_eq_canonical_of_step_condDistrib {Env : Type u} {Action : Type v} {Reward : Type w} [MeasurableSpace Env] [MeasurableSpace Action] [StandardBorelSpace Action] [Nonempty Action] [MeasurableSpace Reward] [StandardBorelSpace Reward] [Nonempty Reward] (algorithm : HistoryAlgorithm Action Reward) (environment : MeasurableHistoryEnvironment Env Action Reward) (env : Env) (hstep : forall n, ProbabilityTheory.condDistrib (fun trajectory : (k : Nat) -> Action × Reward => trajectory (n + 1)) (Preorder.frestrictLe n) (canonicalMeasurableEnvironmentTrajectoryKernel algorithm environment env) =ᵐ[ (canonicalMeasurableEnvironmentTrajectoryKernel algorithm environment env).map (Preorder.frestrictLe n)] historyStepKernel algorithm (environment.at env) n) : canonicalMeasurableEnvironmentTrajectoryKernel algorithm environment env = canonicalHistoryTrajectoryMeasure algorithm (environment.at env)

The generated measurable trajectory kernel is pointwise canonical.

theorem canonicalMeasurableEnvironmentTrajectoryKernel_apply_eq_canonical {Env : Type u} {Action : Type v} {Reward : Type w} [MeasurableSpace Env] [StandardBorelSpace Env] [MeasurableSpace Action] [StandardBorelSpace Action] [Nonempty Action] [MeasurableSpace Reward] [StandardBorelSpace Reward] [Nonempty Reward] (algorithm : HistoryAlgorithm Action Reward) (environment : MeasurableHistoryEnvironment Env Action Reward) (env : Env) : canonicalMeasurableEnvironmentTrajectoryKernel algorithm environment env = canonicalHistoryTrajectoryMeasure algorithm (environment.at env)

Finite-prefix probability matching from jointly measurable actual/reference feedback environments. The only remaining process premise is the shifted successor conditional law of the two generated `Kernel.traj` kernels.

theorem finitePairReferencePolicySampler_condDistrib_action_ae_eq_bestAction_of_measurableEnvironment_stepCondDistrib {Env : Type u} {Action : Type v} {Reward : Type w} [MeasurableSpace Env] [StandardBorelSpace Env] [Nonempty Env] [MeasurableSpace Action] [StandardBorelSpace Action] [Nonempty Action] [MeasurableSpace Reward] [StandardBorelSpace Reward] [Nonempty Reward] (prior : Measure Env) [IsFiniteMeasure prior] (algorithm referenceAlgorithm : HistoryAlgorithm Action Reward) (environment : MeasurableHistoryEnvironment Env Action Reward) (absolutelyContinuous : HistoryAlgorithmAbsolutelyContinuous algorithm referenceAlgorithm) (hstep : forall env n, ProbabilityTheory.condDistrib (fun trajectory : (k : Nat) -> Action × Reward => trajectory (n + 1)) (Preorder.frestrictLe n) (canonicalMeasurableEnvironmentTrajectoryKernel algorithm environment env) =ᵐ[ (canonicalMeasurableEnvironmentTrajectoryKernel algorithm environment env).map (Preorder.frestrictLe n)] historyStepKernel algorithm (environment.at env) n) (hreferenceStep : forall env n, ProbabilityTheory.condDistrib (fun trajectory : (k : Nat) -> Action × Reward => trajectory (n + 1)) (Preorder.frestrictLe n) (canonicalMeasurableEnvironmentTrajectoryKernel referenceAlgorithm environment env) =ᵐ[ (canonicalMeasurableEnvironmentTrajectoryKernel referenceAlgorithm environment env).map (Preorder.frestrictLe n)] historyStepKernel referenceAlgorithm (environment.at env) n) (n : Nat) (bestAction : Env -> Action) (hbestAction : Measurable bestAction) : let trajectoryKernel := canonicalMeasurableEnvironmentTrajectoryKernel algorithm environment let referenceTrajectoryKernel := canonicalMeasurableEnvironmentTrajectoryKernel referenceAlgorithm environment let actualHistory := fun sample => History.finitePairHistoryOfTrace (environmentTrajectoryAction sample) (environmentTrajectoryReward sample) n let referenceHistory := fun sample => History.finitePairHistoryOfTrace (environmentTrajectoryAction sample) (environmentTrajectoryReward sample) n let policy := referenceActionKernel (prior ⊗ₘ referenceTrajectoryKernel) Prod.fst referenceHistory measurable_fst (History.measurable_finitePairHistoryOfTrace environmentTrajectoryAction environmentTrajectoryReward measurable_environmentTrajectoryAction_apply measurable_environmentTrajectoryReward_apply n) bestAction hbestAction let sampler := policySamplerMeasure (prior ⊗ₘ trajectoryKernel) actualHistory (History.measurable_finitePairHistoryOfTrace environmentTrajectoryAction environmentTrajectoryReward measurable_environmentTrajectoryAction_apply measurable_environmentTrajectoryReward_apply n) policy ProbabilityTheory.condDistrib policySamplerAction (policySamplerHistory actualHistory) sampler =ᵐ[ sampler.map (policySamplerHistory actualHistory)] ProbabilityTheory.condDistrib (bestAction ∘ policySamplerEnv Prod.fst) (policySamplerHistory actualHistory) sampler

Finite-prefix Thompson probability matching directly from a jointly measurable feedback environment, with both trajectory kernels and their process laws constructed internally.

theorem finitePairReferencePolicySampler_condDistrib_action_ae_eq_bestAction_of_measurableEnvironment {Env : Type u} {Action : Type v} {Reward : Type w} [MeasurableSpace Env] [StandardBorelSpace Env] [Nonempty Env] [MeasurableSpace Action] [StandardBorelSpace Action] [Nonempty Action] [MeasurableSpace Reward] [StandardBorelSpace Reward] [Nonempty Reward] (prior : Measure Env) [IsFiniteMeasure prior] (algorithm referenceAlgorithm : HistoryAlgorithm Action Reward) (environment : MeasurableHistoryEnvironment Env Action Reward) (absolutelyContinuous : HistoryAlgorithmAbsolutelyContinuous algorithm referenceAlgorithm) (n : Nat) (bestAction : Env -> Action) (hbestAction : Measurable bestAction) : let trajectoryKernel := canonicalMeasurableEnvironmentTrajectoryKernel algorithm environment let referenceTrajectoryKernel := canonicalMeasurableEnvironmentTrajectoryKernel referenceAlgorithm environment let actualHistory := fun sample => History.finitePairHistoryOfTrace (environmentTrajectoryAction sample) (environmentTrajectoryReward sample) n let referenceHistory := fun sample => History.finitePairHistoryOfTrace (environmentTrajectoryAction sample) (environmentTrajectoryReward sample) n let policy := referenceActionKernel (prior ⊗ₘ referenceTrajectoryKernel) Prod.fst referenceHistory measurable_fst (History.measurable_finitePairHistoryOfTrace environmentTrajectoryAction environmentTrajectoryReward measurable_environmentTrajectoryAction_apply measurable_environmentTrajectoryReward_apply n) bestAction hbestAction let sampler := policySamplerMeasure (prior ⊗ₘ trajectoryKernel) actualHistory (History.measurable_finitePairHistoryOfTrace environmentTrajectoryAction environmentTrajectoryReward measurable_environmentTrajectoryAction_apply measurable_environmentTrajectoryReward_apply n) policy ProbabilityTheory.condDistrib policySamplerAction (policySamplerHistory actualHistory) sampler =ᵐ[ sampler.map (policySamplerHistory actualHistory)] ProbabilityTheory.condDistrib (bestAction ∘ policySamplerEnv Prod.fst) (policySamplerHistory actualHistory) sampler