BanditRLProof.Algorithms.ThompsonCanonicalTrajectory

The canonical Ionescu-Tulcea law of the observable action/reward pairs.

noncomputable def canonicalHistoryTrajectoryMeasure {Action : Type u} {Reward : Type v} [MeasurableSpace Action] [MeasurableSpace Reward] (algorithm : HistoryAlgorithm Action Reward) (environment : HistoryEnvironment Action Reward) : Measure ((n : Nat) -> Action × Reward)

Action trace projected from the canonical pair trajectory.

def canonicalHistoryTrajectoryAction {Action : Type u} {Reward : Type v} : ((n : Nat) -> Action × Reward) -> ActionTrace Action

Reward trace projected from the canonical pair trajectory.

def canonicalHistoryTrajectoryReward {Action : Type u} {Reward : Type v} : ((n : Nat) -> Action × Reward) -> RewardTrace Reward

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

theorem measurable_canonicalHistoryTrajectoryAction_apply {Action : Type u} {Reward : Type v} [MeasurableSpace Action] [MeasurableSpace Reward] (n : Nat) : Measurable (fun trajectory : (k : Nat) -> Action × Reward => canonicalHistoryTrajectoryAction trajectory n)

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

theorem measurable_canonicalHistoryTrajectoryReward_apply {Action : Type u} {Reward : Type v} [MeasurableSpace Action] [MeasurableSpace Reward] (n : Nat) : Measurable (fun trajectory : (k : Nat) -> Action × Reward => canonicalHistoryTrajectoryReward trajectory n)

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

theorem canonicalHistoryTrajectory_initialPair_map_eq {Action : Type u} {Reward : Type v} [MeasurableSpace Action] [MeasurableSpace Reward] (algorithm : HistoryAlgorithm Action Reward) (environment : HistoryEnvironment Action Reward) : Measure.map (fun trajectory => (canonicalHistoryTrajectoryAction trajectory 0, canonicalHistoryTrajectoryReward trajectory 0)) (canonicalHistoryTrajectoryMeasure algorithm environment) = algorithm.initialAction ⊗ₘ environment.initialFeedback

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

theorem canonicalHistoryTrajectory_step_condDistrib {Action : Type u} {Reward : Type v} [MeasurableSpace Action] [StandardBorelSpace Action] [Nonempty Action] [MeasurableSpace Reward] [StandardBorelSpace Reward] [Nonempty Reward] (algorithm : HistoryAlgorithm Action Reward) (environment : HistoryEnvironment Action Reward) (n : Nat) : ProbabilityTheory.condDistrib (fun trajectory => (canonicalHistoryTrajectoryAction trajectory (n + 1), canonicalHistoryTrajectoryReward trajectory (n + 1))) (fun trajectory => History.finitePairHistoryOfTrace (canonicalHistoryTrajectoryAction trajectory) (canonicalHistoryTrajectoryReward trajectory) n) (canonicalHistoryTrajectoryMeasure algorithm environment) =ᵐ[ (canonicalHistoryTrajectoryMeasure algorithm environment).map (fun trajectory => History.finitePairHistoryOfTrace (canonicalHistoryTrajectoryAction trajectory) (canonicalHistoryTrajectoryReward trajectory) n)] historyStepKernel algorithm environment n

The canonical pair trajectory satisfies the combined history-process contract without any externally supplied law premise.

noncomputable def canonicalHistoryAlgorithmEnvironmentSequence {Action : Type u} {Reward : Type v} [MeasurableSpace Action] [StandardBorelSpace Action] [Nonempty Action] [MeasurableSpace Reward] [StandardBorelSpace Reward] [Nonempty Reward] (algorithm : HistoryAlgorithm Action Reward) (environment : HistoryEnvironment Action Reward) : IsHistoryAlgorithmEnvironmentSequence (canonicalHistoryTrajectoryMeasure algorithm environment) canonicalHistoryTrajectoryAction canonicalHistoryTrajectoryReward algorithm environment where

The combined initial pair law determines the initial action marginal.

theorem initialAction_map_eq_of_historyAlgorithmEnvironmentSequence {Omega : Type w} {Action : Type u} {Reward : Type v} [MeasurableSpace Omega] [MeasurableSpace Action] [StandardBorelSpace Action] [Nonempty Action] [MeasurableSpace Reward] [StandardBorelSpace Reward] [Nonempty Reward] (mu : Measure Omega) [IsFiniteMeasure mu] (action : Omega -> ActionTrace Action) (reward : Omega -> RewardTrace Reward) (algorithm : HistoryAlgorithm Action Reward) (environment : HistoryEnvironment Action Reward) (source : IsHistoryAlgorithmEnvironmentSequence mu action reward algorithm environment) : mu.map (fun omega => action omega 0) = algorithm.initialAction

The combined initial pair law determines the initial feedback conditional law.

theorem initialFeedback_condDistrib_of_historyAlgorithmEnvironmentSequence {Omega : Type w} {Action : Type u} {Reward : Type v} [MeasurableSpace Omega] [MeasurableSpace Action] [StandardBorelSpace Action] [Nonempty Action] [MeasurableSpace Reward] [StandardBorelSpace Reward] [Nonempty Reward] (mu : Measure Omega) [IsFiniteMeasure mu] (action : Omega -> ActionTrace Action) (reward : Omega -> RewardTrace Reward) (algorithm : HistoryAlgorithm Action Reward) (environment : HistoryEnvironment Action Reward) (source : IsHistoryAlgorithmEnvironmentSequence mu action reward algorithm environment) : ProbabilityTheory.condDistrib (fun omega => reward omega 0) (fun omega => action omega 0) mu =ᵐ[ mu.map (fun omega => action omega 0)] environment.initialFeedback

The action marginal of a history step kernel is its policy kernel.

theorem historyStepKernel_map_fst {Action : Type u} {Reward : Type v} [MeasurableSpace Action] [MeasurableSpace Reward] (algorithm : HistoryAlgorithm Action Reward) (environment : HistoryEnvironment Action Reward) (n : Nat) : (historyStepKernel algorithm environment n).map Prod.fst = algorithm.policy n

The combined successor pair law determines the successor action policy.

theorem policy_condDistrib_of_historyAlgorithmEnvironmentSequence {Omega : Type w} {Action : Type u} {Reward : Type v} [MeasurableSpace Omega] [MeasurableSpace Action] [StandardBorelSpace Action] [Nonempty Action] [MeasurableSpace Reward] [StandardBorelSpace Reward] [Nonempty Reward] (mu : Measure Omega) [IsFiniteMeasure mu] (action : Omega -> ActionTrace Action) (reward : Omega -> RewardTrace Reward) (algorithm : HistoryAlgorithm Action Reward) (environment : HistoryEnvironment Action Reward) (source : IsHistoryAlgorithmEnvironmentSequence mu action reward algorithm environment) (n : Nat) : ProbabilityTheory.condDistrib (fun omega => action omega (n + 1)) (fun omega => History.finitePairHistoryOfTrace (action omega) (reward omega) n) mu =ᵐ[ mu.map (fun omega => History.finitePairHistoryOfTrace (action omega) (reward omega) n)] algorithm.policy n

The combined successor pair law also determines the feedback conditional law given the finite history and the newly sampled action.

theorem feedback_condDistrib_of_historyAlgorithmEnvironmentSequence {Omega : Type w} {Action : Type u} {Reward : Type v} [MeasurableSpace Omega] [MeasurableSpace Action] [StandardBorelSpace Action] [Nonempty Action] [MeasurableSpace Reward] [StandardBorelSpace Reward] [Nonempty Reward] (mu : Measure Omega) [IsFiniteMeasure mu] (action : Omega -> ActionTrace Action) (reward : Omega -> RewardTrace Reward) (algorithm : HistoryAlgorithm Action Reward) (environment : HistoryEnvironment Action Reward) (source : IsHistoryAlgorithmEnvironmentSequence mu action reward algorithm environment) (n : Nat) : ProbabilityTheory.condDistrib (fun omega => reward omega (n + 1)) (fun omega => (History.finitePairHistoryOfTrace (action omega) (reward omega) n, action omega (n + 1))) mu =ᵐ[ mu.map (fun omega => (History.finitePairHistoryOfTrace (action omega) (reward omega) n, action omega (n + 1)))] environment.feedback n

Split action/feedback laws for one fixed history environment.

structure HistoryAlgorithmEnvironmentSplitSource {Omega : Type w} {Action : Type u} {Reward : Type v} [MeasurableSpace Omega] [MeasurableSpace Action] [StandardBorelSpace Action] [Nonempty Action] [MeasurableSpace Reward] [StandardBorelSpace Reward] [Nonempty Reward] (mu : Measure Omega) [IsFiniteMeasure mu] (action : Omega -> ActionTrace Action) (reward : Omega -> RewardTrace Reward) (algorithm : HistoryAlgorithm Action Reward) (environment : HistoryEnvironment Action Reward) : Prop where

Assemble the combined process contract from a fixed-environment split source.

noncomputable def HistoryAlgorithmEnvironmentSplitSource.toSequence {Omega : Type w} {Action : Type u} {Reward : Type v} [MeasurableSpace Omega] [MeasurableSpace Action] [StandardBorelSpace Action] [Nonempty Action] [MeasurableSpace Reward] [StandardBorelSpace Reward] [Nonempty Reward] (mu : Measure Omega) [IsFiniteMeasure mu] (action : Omega -> ActionTrace Action) (reward : Omega -> RewardTrace Reward) (algorithm : HistoryAlgorithm Action Reward) (environment : HistoryEnvironment Action Reward) (source : HistoryAlgorithmEnvironmentSplitSource mu action reward algorithm environment) : IsHistoryAlgorithmEnvironmentSequence mu action reward algorithm environment

The canonical trajectory realizes all four fixed-environment split laws.

noncomputable def canonicalHistoryAlgorithmEnvironmentSplitSource {Action : Type u} {Reward : Type v} [MeasurableSpace Action] [StandardBorelSpace Action] [Nonempty Action] [MeasurableSpace Reward] [StandardBorelSpace Reward] [Nonempty Reward] (algorithm : HistoryAlgorithm Action Reward) (environment : HistoryEnvironment Action Reward) : HistoryAlgorithmEnvironmentSplitSource (canonicalHistoryTrajectoryMeasure algorithm environment) canonicalHistoryTrajectoryAction canonicalHistoryTrajectoryReward algorithm environment where

The canonical combined process reconstructed specifically from its split laws.

noncomputable def canonicalHistoryAlgorithmEnvironmentSequence_of_split {Action : Type u} {Reward : Type v} [MeasurableSpace Action] [StandardBorelSpace Action] [Nonempty Action] [MeasurableSpace Reward] [StandardBorelSpace Reward] [Nonempty Reward] (algorithm : HistoryAlgorithm Action Reward) (environment : HistoryEnvironment Action Reward) : IsHistoryAlgorithmEnvironmentSequence (canonicalHistoryTrajectoryMeasure algorithm environment) canonicalHistoryTrajectoryAction canonicalHistoryTrajectoryReward algorithm environment

Lift a kernel to samples that retain the kernel input as their first coordinate.

noncomputable def kernelWithInput {Input : Type u} {Output : Type v} [MeasurableSpace Input] [MeasurableSpace Output] (kernel : ProbabilityTheory.Kernel Input Output) : ProbabilityTheory.Kernel Input (Input × Output)

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

theorem kernelWithInput_apply {Input : Type u} {Output : Type v} [MeasurableSpace Input] [MeasurableSingletonClass Input] [MeasurableSpace Output] (kernel : ProbabilityTheory.Kernel Input Output) [ProbabilityTheory.IsMarkovKernel kernel] (input : Input) : kernelWithInput kernel input = (kernel input).map (Prod.mk input)

For a composition-product sample, conditioning the complete sample on its first coordinate keeps that coordinate and uses the supplied second-coordinate kernel.

theorem condDistrib_id_fst_compProd_ae_eq_kernelWithInput {Input : Type u} {Output : Type v} [MeasurableSpace Input] [StandardBorelSpace Input] [Nonempty Input] [MeasurableSpace Output] [StandardBorelSpace Output] [Nonempty Output] (prior : Measure Input) [IsFiniteMeasure prior] (kernel : ProbabilityTheory.Kernel Input Output) [ProbabilityTheory.IsMarkovKernel kernel] : ProbabilityTheory.condDistrib id Prod.fst (prior ⊗ₘ kernel) =ᵐ[prior] kernelWithInput kernel

Action trace of an environment/trajectory sample.

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

Reward trace of an environment/trajectory sample.

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

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

theorem measurable_environmentTrajectoryAction_apply {Env : Type u} {Action : Type v} {Reward : Type w} [MeasurableSpace Env] [MeasurableSpace Action] [MeasurableSpace Reward] (n : Nat) : Measurable (fun sample : Env × ((k : Nat) -> Action × Reward) => environmentTrajectoryAction sample n)

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

theorem measurable_environmentTrajectoryReward_apply {Env : Type u} {Action : Type v} {Reward : Type w} [MeasurableSpace Env] [MeasurableSpace Action] [MeasurableSpace Reward] (n : Nat) : Measurable (fun sample : Env × ((k : Nat) -> Action × Reward) => environmentTrajectoryReward sample n)

Transport a history-process contract across an equality of source measures.

noncomputable def historyAlgorithmEnvironmentSequence_of_measure_eq {Omega : Type w} {Action : Type u} {Reward : Type v} [MeasurableSpace Omega] [MeasurableSpace Action] [StandardBorelSpace Action] [Nonempty Action] [MeasurableSpace Reward] [StandardBorelSpace Reward] [Nonempty Reward] (mu nu : Measure Omega) [IsFiniteMeasure mu] [IsFiniteMeasure nu] (action : Omega -> ActionTrace Action) (reward : Omega -> RewardTrace Reward) (algorithm : HistoryAlgorithm Action Reward) (environment : HistoryEnvironment Action Reward) (hmeasure : mu = nu) (source : IsHistoryAlgorithmEnvironmentSequence mu action reward algorithm environment) : IsHistoryAlgorithmEnvironmentSequence nu action reward algorithm environment

Retaining a fixed environment coordinate preserves the canonical process.

noncomputable def mappedCanonicalHistoryAlgorithmEnvironmentSequence {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] (algorithm : HistoryAlgorithm Action Reward) (feedbackEnvironment : Env -> HistoryEnvironment Action Reward) (environment : Env) : IsHistoryAlgorithmEnvironmentSequence ((canonicalHistoryTrajectoryMeasure algorithm (feedbackEnvironment environment)).map (Prod.mk environment)) environmentTrajectoryAction environmentTrajectoryReward algorithm (feedbackEnvironment environment) where

A trajectory kernel whose value is the canonical fixed-environment law yields the combined history-process contract after retaining its environment input.

noncomputable def kernelWithInputHistoryAlgorithmEnvironmentSequence {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] (algorithm : HistoryAlgorithm Action Reward) (feedbackEnvironment : Env -> HistoryEnvironment Action Reward) (trajectoryKernel : ProbabilityTheory.Kernel Env ((n : Nat) -> Action × Reward)) [ProbabilityTheory.IsMarkovKernel trajectoryKernel] (environment : Env) (hkernel : trajectoryKernel environment = canonicalHistoryTrajectoryMeasure algorithm (feedbackEnvironment environment)) : IsHistoryAlgorithmEnvironmentSequence (kernelWithInput trajectoryKernel environment) environmentTrajectoryAction environmentTrajectoryReward algorithm (feedbackEnvironment environment)

The regular conditional complete-sample law of a canonical environment/ trajectory composition product satisfies the history-process contract.

theorem conditionalHistoryAlgorithmEnvironmentSequence_of_canonicalTrajectoryKernel {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 : HistoryAlgorithm Action Reward) (feedbackEnvironment : Env -> HistoryEnvironment Action Reward) (trajectoryKernel : ProbabilityTheory.Kernel Env ((n : Nat) -> Action × Reward)) [ProbabilityTheory.IsMarkovKernel trajectoryKernel] (hkernel : forall environment, trajectoryKernel environment = canonicalHistoryTrajectoryMeasure algorithm (feedbackEnvironment environment)) : ∀ᵐ environment ∂(prior ⊗ₘ trajectoryKernel).map Prod.fst, IsHistoryAlgorithmEnvironmentSequence (ProbabilityTheory.condDistrib id Prod.fst (prior ⊗ₘ trajectoryKernel) environment) environmentTrajectoryAction environmentTrajectoryReward algorithm (feedbackEnvironment environment)

Canonical environment-indexed trajectory kernels supply all four conditional split law families required by the Thompson density route.

noncomputable def conditionalHistoryAlgorithmEnvironmentSplitSource_of_canonicalTrajectoryKernel {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 : HistoryAlgorithm Action Reward) (feedbackEnvironment : Env -> HistoryEnvironment Action Reward) (trajectoryKernel : ProbabilityTheory.Kernel Env ((n : Nat) -> Action × Reward)) [ProbabilityTheory.IsMarkovKernel trajectoryKernel] (hkernel : forall environment, trajectoryKernel environment = canonicalHistoryTrajectoryMeasure algorithm (feedbackEnvironment environment)) : ConditionalHistoryAlgorithmEnvironmentSplitSource (prior ⊗ₘ trajectoryKernel) Prod.fst environmentTrajectoryAction environmentTrajectoryReward algorithm feedbackEnvironment where

Paired canonical actual/reference trajectory kernels construct the complete conditional split source consumed by algorithm-density transport.

noncomputable def conditionalHistoryAlgorithmDensitySplitSource_of_canonicalTrajectoryKernels {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) (feedbackEnvironment : Env -> HistoryEnvironment Action Reward) (trajectoryKernel referenceTrajectoryKernel : ProbabilityTheory.Kernel Env ((n : Nat) -> Action × Reward)) [ProbabilityTheory.IsMarkovKernel trajectoryKernel] [ProbabilityTheory.IsMarkovKernel referenceTrajectoryKernel] (htrajectoryKernel : forall environment, trajectoryKernel environment = canonicalHistoryTrajectoryMeasure algorithm (feedbackEnvironment environment)) (hreferenceTrajectoryKernel : forall environment, referenceTrajectoryKernel environment = canonicalHistoryTrajectoryMeasure referenceAlgorithm (feedbackEnvironment environment)) (absolutelyContinuous : HistoryAlgorithmAbsolutelyContinuous algorithm referenceAlgorithm) : ConditionalHistoryAlgorithmDensitySplitSource (prior ⊗ₘ trajectoryKernel) Prod.fst environmentTrajectoryAction environmentTrajectoryReward (prior ⊗ₘ referenceTrajectoryKernel) Prod.fst environmentTrajectoryAction environmentTrajectoryReward algorithm referenceAlgorithm feedbackEnvironment where

Finite-prefix Thompson probability matching for paired canonical recursive trajectory kernels. The remaining producer obligation is exactly the measurable kernel family whose values are the fixed-environment canonical `trajMeasure`s.

theorem finitePairReferencePolicySampler_condDistrib_action_ae_eq_bestAction_of_canonicalTrajectoryKernels {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) (feedbackEnvironment : Env -> HistoryEnvironment Action Reward) (trajectoryKernel referenceTrajectoryKernel : ProbabilityTheory.Kernel Env ((n : Nat) -> Action × Reward)) [ProbabilityTheory.IsMarkovKernel trajectoryKernel] [ProbabilityTheory.IsMarkovKernel referenceTrajectoryKernel] (htrajectoryKernel : forall environment, trajectoryKernel environment = canonicalHistoryTrajectoryMeasure algorithm (feedbackEnvironment environment)) (hreferenceTrajectoryKernel : forall environment, referenceTrajectoryKernel environment = canonicalHistoryTrajectoryMeasure referenceAlgorithm (feedbackEnvironment environment)) (absolutelyContinuous : HistoryAlgorithmAbsolutelyContinuous algorithm referenceAlgorithm) (n : Nat) (bestAction : Env -> Action) (hbestAction : Measurable bestAction) : 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