BanditRLProof.Algorithms.ThompsonAlgorithmDensityProcess

A stochastic policy indexed by inclusive finite action/reward histories.

structure HistoryAlgorithm (Action : Type u) (Reward : Type v) [MeasurableSpace Action] [MeasurableSpace Reward] where

A stochastic feedback environment shared by the compared algorithms.

structure HistoryEnvironment (Action : Type u) (Reward : Type v) [MeasurableSpace Action] [MeasurableSpace Reward] where

Conditional law of the next action/reward pair after a finite history.

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

Pointwise action-law absolute continuity between two algorithms.

structure HistoryAlgorithmAbsolutelyContinuous {Action : Type u} {Reward : Type v} [MeasurableSpace Action] [MeasurableSpace Reward] (algorithm referenceAlgorithm : HistoryAlgorithm Action Reward) : Prop where

The unique history at time zero containing one action/reward pair.

def singletonPairHistory {Action : Type u} {Reward : Type v} (pair : Action × Reward) : History.FinitePairHistory Action Reward 0

Remove the last coordinate from an inclusive successor history.

def pairHistoryPrefix {Action : Type u} {Reward : Type v} {n : Nat} (history : History.FinitePairHistory Action Reward (n + 1)) : History.FinitePairHistory Action Reward n

Last pair in an inclusive successor history.

def pairHistoryLast {Action : Type u} {Reward : Type v} {n : Nat} (history : History.FinitePairHistory Action Reward (n + 1)) : Action × Reward

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

theorem measurable_singletonPairHistory {Action : Type u} {Reward : Type v} [MeasurableSpace Action] [MeasurableSpace Reward] : Measurable (@singletonPairHistory Action Reward)

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

theorem measurable_pairHistoryPrefix {Action : Type u} {Reward : Type v} {n : Nat} [MeasurableSpace Action] [MeasurableSpace Reward] : Measurable (@pairHistoryPrefix Action Reward n)

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

theorem measurable_pairHistoryLast {Action : Type u} {Reward : Type v} {n : Nat} [MeasurableSpace Action] [MeasurableSpace Reward] : Measurable (@pairHistoryLast Action Reward n)

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

theorem pairHistoryPrefix_extendPairHistorySucc {Action : Type u} {Reward : Type v} {n : Nat} (history : History.FinitePairHistory Action Reward n) (next : Action × Reward) : pairHistoryPrefix (History.extendPairHistorySucc history next) = history

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

theorem pairHistoryLast_extendPairHistorySucc {Action : Type u} {Reward : Type v} {n : Nat} (history : History.FinitePairHistory Action Reward n) (next : Action × Reward) : pairHistoryLast (History.extendPairHistorySucc history next) = next

Recursive product of the initial and policy action likelihood ratios.

noncomputable def historyDensity {Action : Type u} {Reward : Type v} [MeasurableSpace Action] [MeasurableSpace Reward] [MeasurableSpace.CountablyGenerated Action] (algorithm referenceAlgorithm : HistoryAlgorithm Action Reward) : (n : Nat) -> History.FinitePairHistory Action Reward n -> ENNReal | 0, history => algorithm.initialAction.rnDeriv referenceAlgorithm.initialAction (history ⟨0, Finset.mem_Iic.mpr le_rfl⟩).1 | n + 1, history => historyDensity algorithm referenceAlgorithm n (pairHistoryPrefix history) * (algorithm.policy n).rnDeriv (referenceAlgorithm.policy n) (pairHistoryPrefix history) (pairHistoryLast history).1 theorem measurable_historyDensity {Action : Type u} {Reward : Type v} [MeasurableSpace Action] [MeasurableSpace Reward] [MeasurableSpace.CountablyGenerated Action] (algorithm referenceAlgorithm : HistoryAlgorithm Action Reward) (n : Nat) : Measurable (historyDensity algorithm referenceAlgorithm n)

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

theorem measurable_historyDensity {Action : Type u} {Reward : Type v} [MeasurableSpace Action] [MeasurableSpace Reward] [MeasurableSpace.CountablyGenerated Action] (algorithm referenceAlgorithm : HistoryAlgorithm Action Reward) (n : Nat) : Measurable (historyDensity algorithm referenceAlgorithm n)

Mapping a weighted measure transports a density pulled back by the map.

theorem map_withDensity_comp {Source : Type u} {Target : Type v} [MeasurableSpace Source] [MeasurableSpace Target] (mu : Measure Source) (map : Source -> Target) (density : Target -> ENNReal) (hmap : Measurable map) (hdensity : Measurable density) : (mu.withDensity (density ∘ map)).map map = (mu.map map).withDensity density

Weighting both a composition-product base and kernel multiplies densities.

theorem compProd_withDensity_withDensity {Base : Type u} {Target : Type v} [MeasurableSpace Base] [MeasurableSpace Target] (base : Measure Base) [SFinite base] (kernel : ProbabilityTheory.Kernel Base Target) [ProbabilityTheory.IsSFiniteKernel kernel] (baseDensity : Base -> ENNReal) (kernelDensity : Base -> Target -> ENNReal) (hbaseDensity : Measurable baseDensity) (hkernelDensity : Measurable (Function.uncurry kernelDensity)) [ProbabilityTheory.IsSFiniteKernel (kernel.withDensity kernelDensity)] : base.withDensity baseDensity ⊗ₘ kernel.withDensity kernelDensity = (base ⊗ₘ kernel).withDensity (fun pair => baseDensity pair.1 * kernelDensity pair.1 pair.2)

Kernel RN derivatives reconstruct a pointwise absolutely continuous kernel.

theorem kernel_withDensity_rnDeriv_eq_of_absolutelyContinuous {Index : Type u} {Target : Type v} [MeasurableSpace Index] [MeasurableSpace Target] [MeasurableSpace.CountableOrCountablyGenerated Index Target] (kernel referenceKernel : ProbabilityTheory.Kernel Index Target) [ProbabilityTheory.IsFiniteKernel kernel] [ProbabilityTheory.IsFiniteKernel referenceKernel] (h : forall index, kernel index ≪ referenceKernel index) : referenceKernel.withDensity (kernel.rnDeriv referenceKernel) = kernel

Weighting the left kernel of a kernel composition product.

theorem kernel_compProd_withDensity_left {Index : Type u} {Middle : Type v} {Target : Type w} [MeasurableSpace Index] [MeasurableSpace Middle] [MeasurableSpace Target] (kernel : ProbabilityTheory.Kernel Index Middle) (nextKernel : ProbabilityTheory.Kernel (Index × Middle) Target) [ProbabilityTheory.IsSFiniteKernel kernel] [ProbabilityTheory.IsSFiniteKernel nextKernel] (density : Index -> Middle -> ENNReal) (hdensity : Measurable (Function.uncurry density)) [ProbabilityTheory.IsSFiniteKernel (kernel.withDensity density)] : kernel.withDensity density ⊗ₖ nextKernel = (kernel ⊗ₖ nextKernel).withDensity (fun index pair => density index pair.1)

The actual one-step pair kernel is a density-weighted reference kernel.

theorem historyStepKernel_eq_withDensity {Action : Type u} {Reward : Type v} [MeasurableSpace Action] [MeasurableSpace Reward] (n : Nat) [MeasurableSpace.CountableOrCountablyGenerated (History.FinitePairHistory Action Reward n) Action] (algorithm referenceAlgorithm : HistoryAlgorithm Action Reward) (environment : HistoryEnvironment Action Reward) (hcontinuous : HistoryAlgorithmAbsolutelyContinuous algorithm referenceAlgorithm) : historyStepKernel algorithm environment n = (historyStepKernel referenceAlgorithm environment n).withDensity (fun history pair => (algorithm.policy n).rnDeriv (referenceAlgorithm.policy n) history pair.1)

Process contract using the combined initial and successor pair laws. Split action/feedback conditional laws are assembled into this contract below.

structure IsHistoryAlgorithmEnvironmentSequence {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

Build the pair-law process contract from LML-shaped split fields.

noncomputable def isHistoryAlgorithmEnvironmentSequence_of_split {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) (haction : forall n, Measurable (fun omega => action omega n)) (hreward : forall n, Measurable (fun omega => reward omega n)) (hinitialAction : mu.map (fun omega => action omega 0) = algorithm.initialAction) (hinitialFeedback : ProbabilityTheory.condDistrib (fun omega => reward omega 0) (fun omega => action omega 0) mu =ᵐ[ mu.map (fun omega => action omega 0)] environment.initialFeedback) (hpolicy : forall n, 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) (hfeedback : forall n, 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) : IsHistoryAlgorithmEnvironmentSequence mu action reward algorithm environment where

The process contract identifies the joint law of the current finite history and the next action/reward pair with the corresponding measure composition product.

theorem nextPairJointLaw_eq_compProd {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) : mu.map (fun omega => (History.finitePairHistoryOfTrace (action omega) (reward omega) n, (action omega (n + 1), reward omega (n + 1)))) = mu.map (fun omega => History.finitePairHistoryOfTrace (action omega) (reward omega) n) ⊗ₘ historyStepKernel algorithm environment n

Finite-history algorithm-density transport. Two history-dependent stochastic policies use the same feedback environment. Pointwise absolute continuity of the actual policy with respect to the reference policy implies that every inclusive finite pair-history law is the reference law weighted by the recursive product of action likelihood ratios.

theorem finitePairHistory_map_eq_withDensity {Omega : Type w} {OmegaRef : Type x} {Action : Type u} {Reward : Type v} [MeasurableSpace Omega] [MeasurableSpace OmegaRef] [MeasurableSpace Action] [StandardBorelSpace Action] [Nonempty Action] [MeasurableSpace Reward] [StandardBorelSpace Reward] [Nonempty Reward] (mu : Measure Omega) [IsFiniteMeasure mu] (muRef : Measure OmegaRef) [IsFiniteMeasure muRef] (action : Omega -> ActionTrace Action) (reward : Omega -> RewardTrace Reward) (actionRef : OmegaRef -> ActionTrace Action) (rewardRef : OmegaRef -> RewardTrace Reward) (algorithm referenceAlgorithm : HistoryAlgorithm Action Reward) (environment : HistoryEnvironment Action Reward) (source : IsHistoryAlgorithmEnvironmentSequence mu action reward algorithm environment) (referenceSource : IsHistoryAlgorithmEnvironmentSequence muRef actionRef rewardRef referenceAlgorithm environment) (hcontinuous : HistoryAlgorithmAbsolutelyContinuous algorithm referenceAlgorithm) (n : Nat) : mu.map (fun omega => History.finitePairHistoryOfTrace (action omega) (reward omega) n) = (muRef.map (fun omega => History.finitePairHistoryOfTrace (actionRef omega) (rewardRef omega) n)).withDensity (historyDensity algorithm referenceAlgorithm n)

Environment-indexed process realization for algorithm-density transport. The regular conditional sample laws `condDistrib id env mu` and `condDistrib id referenceEnv referenceMu` must satisfy the actual and reference process contracts almost everywhere. The compared algorithms share the same environment-indexed feedback law.

structure ConditionalHistoryAlgorithmDensitySource {Omega : Type u} {OmegaRef : Type v} {Env : Type w} {Action : Type x} {Reward : Type y} [MeasurableSpace Omega] [StandardBorelSpace Omega] [Nonempty Omega] [MeasurableSpace OmegaRef] [StandardBorelSpace OmegaRef] [Nonempty OmegaRef] [MeasurableSpace Env] [MeasurableSpace Action] [StandardBorelSpace Action] [Nonempty Action] [MeasurableSpace Reward] [StandardBorelSpace Reward] [Nonempty Reward] (mu : Measure Omega) [IsFiniteMeasure mu] (env : Omega -> Env) (action : Omega -> ActionTrace Action) (reward : Omega -> RewardTrace Reward) (referenceMu : Measure OmegaRef) [IsFiniteMeasure referenceMu] (referenceEnv : OmegaRef -> Env) (referenceAction : OmegaRef -> ActionTrace Action) (referenceReward : OmegaRef -> RewardTrace Reward) (algorithm referenceAlgorithm : HistoryAlgorithm Action Reward) (feedbackEnvironment : Env -> HistoryEnvironment Action Reward) : Prop where

The environment-indexed process realization produces the conditional finite history density law required by the posterior-invariance source constructor.

theorem condDistrib_finitePairHistory_eq_withDensity_of_conditionalProcessSource {Omega : Type u} {OmegaRef : Type v} {Env : Type w} {Action : Type x} {Reward : Type y} [MeasurableSpace Omega] [StandardBorelSpace Omega] [Nonempty Omega] [MeasurableSpace OmegaRef] [StandardBorelSpace OmegaRef] [Nonempty OmegaRef] [MeasurableSpace Env] [MeasurableSpace Action] [StandardBorelSpace Action] [Nonempty Action] [MeasurableSpace Reward] [StandardBorelSpace Reward] [Nonempty Reward] (mu : Measure Omega) [IsFiniteMeasure mu] (env : Omega -> Env) (action : Omega -> ActionTrace Action) (reward : Omega -> RewardTrace Reward) (referenceMu : Measure OmegaRef) [IsFiniteMeasure referenceMu] (referenceEnv : OmegaRef -> Env) (referenceAction : OmegaRef -> ActionTrace Action) (referenceReward : OmegaRef -> RewardTrace Reward) (algorithm referenceAlgorithm : HistoryAlgorithm Action Reward) (feedbackEnvironment : Env -> HistoryEnvironment Action Reward) (source : ConditionalHistoryAlgorithmDensitySource mu env action reward referenceMu referenceEnv referenceAction referenceReward algorithm referenceAlgorithm feedbackEnvironment) (n : Nat) : ProbabilityTheory.condDistrib (fun omega => History.finitePairHistoryOfTrace (action omega) (reward omega) n) env mu =ᵐ[mu.map env] (ProbabilityTheory.condDistrib (fun omega => History.finitePairHistoryOfTrace (referenceAction omega) (referenceReward omega) n) referenceEnv referenceMu).withDensity (fun _ history => historyDensity algorithm referenceAlgorithm n history)

Finite-prefix Thompson probability matching produced directly from the environment-indexed recursive process contracts.

theorem finitePairReferencePolicySampler_condDistrib_action_ae_eq_bestAction_of_conditionalProcessSource {Omega : Type u} {OmegaRef : Type v} {Env : Type w} {Action : Type x} {Reward : Type y} [MeasurableSpace Omega] [StandardBorelSpace Omega] [Nonempty Omega] [MeasurableSpace OmegaRef] [StandardBorelSpace OmegaRef] [Nonempty OmegaRef] [MeasurableSpace Env] [StandardBorelSpace Env] [Nonempty Env] [MeasurableSpace Action] [StandardBorelSpace Action] [Nonempty Action] [MeasurableSpace Reward] [StandardBorelSpace Reward] [Nonempty Reward] (mu : Measure Omega) [IsFiniteMeasure mu] (env : Omega -> Env) (action : Omega -> ActionTrace Action) (reward : Omega -> RewardTrace Reward) (referenceMu : Measure OmegaRef) [IsFiniteMeasure referenceMu] (referenceEnv : OmegaRef -> Env) (referenceAction : OmegaRef -> ActionTrace Action) (referenceReward : OmegaRef -> RewardTrace Reward) (algorithm referenceAlgorithm : HistoryAlgorithm Action Reward) (feedbackEnvironment : Env -> HistoryEnvironment Action Reward) (source : ConditionalHistoryAlgorithmDensitySource mu env action reward referenceMu referenceEnv referenceAction referenceReward algorithm referenceAlgorithm feedbackEnvironment) (n : Nat) (bestAction : Env -> Action) (hbestAction : Measurable bestAction) : let actualHistory := fun omega => History.finitePairHistoryOfTrace (action omega) (reward omega) n let referenceHistory := fun omega => History.finitePairHistoryOfTrace (referenceAction omega) (referenceReward omega) n let policy := referenceActionKernel referenceMu referenceEnv referenceHistory source.measurable_referenceEnv (History.measurable_finitePairHistoryOfTrace referenceAction referenceReward source.measurable_referenceAction source.measurable_referenceReward n) bestAction hbestAction let sampler := policySamplerMeasure mu actualHistory (History.measurable_finitePairHistoryOfTrace action reward source.measurable_action source.measurable_reward n) policy ProbabilityTheory.condDistrib policySamplerAction (policySamplerHistory actualHistory) sampler =ᵐ[ sampler.map (policySamplerHistory actualHistory)] ProbabilityTheory.condDistrib (bestAction ∘ policySamplerEnv env) (policySamplerHistory actualHistory) sampler

LML-shaped split laws for one algorithm/environment process under the regular conditional sample measure at almost every environment.

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

Actual/reference split conditional-process laws together with the common environment marginal and policy absolute-continuity contract.

structure ConditionalHistoryAlgorithmDensitySplitSource {Omega : Type u} {OmegaRef : Type v} {Env : Type w} {Action : Type x} {Reward : Type y} [MeasurableSpace Omega] [StandardBorelSpace Omega] [Nonempty Omega] [MeasurableSpace OmegaRef] [StandardBorelSpace OmegaRef] [Nonempty OmegaRef] [MeasurableSpace Env] [MeasurableSpace Action] [StandardBorelSpace Action] [Nonempty Action] [MeasurableSpace Reward] [StandardBorelSpace Reward] [Nonempty Reward] (mu : Measure Omega) [IsFiniteMeasure mu] (env : Omega -> Env) (action : Omega -> ActionTrace Action) (reward : Omega -> RewardTrace Reward) (referenceMu : Measure OmegaRef) [IsFiniteMeasure referenceMu] (referenceEnv : OmegaRef -> Env) (referenceAction : OmegaRef -> ActionTrace Action) (referenceReward : OmegaRef -> RewardTrace Reward) (algorithm referenceAlgorithm : HistoryAlgorithm Action Reward) (feedbackEnvironment : Env -> HistoryEnvironment Action Reward) : Prop where

Assemble the conditional process source from the four split law families for the actual and reference processes.

noncomputable def conditionalHistoryAlgorithmDensitySource_of_split {Omega : Type u} {OmegaRef : Type v} {Env : Type w} {Action : Type x} {Reward : Type y} [MeasurableSpace Omega] [StandardBorelSpace Omega] [Nonempty Omega] [MeasurableSpace OmegaRef] [StandardBorelSpace OmegaRef] [Nonempty OmegaRef] [MeasurableSpace Env] [MeasurableSpace Action] [StandardBorelSpace Action] [Nonempty Action] [MeasurableSpace Reward] [StandardBorelSpace Reward] [Nonempty Reward] (mu : Measure Omega) [IsFiniteMeasure mu] (env : Omega -> Env) (action : Omega -> ActionTrace Action) (reward : Omega -> RewardTrace Reward) (referenceMu : Measure OmegaRef) [IsFiniteMeasure referenceMu] (referenceEnv : OmegaRef -> Env) (referenceAction : OmegaRef -> ActionTrace Action) (referenceReward : OmegaRef -> RewardTrace Reward) (algorithm referenceAlgorithm : HistoryAlgorithm Action Reward) (feedbackEnvironment : Env -> HistoryEnvironment Action Reward) (source : ConditionalHistoryAlgorithmDensitySplitSource mu env action reward referenceMu referenceEnv referenceAction referenceReward algorithm referenceAlgorithm feedbackEnvironment) : ConditionalHistoryAlgorithmDensitySource mu env action reward referenceMu referenceEnv referenceAction referenceReward algorithm referenceAlgorithm feedbackEnvironment

The split conditional laws directly produce the conditional finite-history density equality.

theorem condDistrib_finitePairHistory_eq_withDensity_of_conditionalSplitSource {Omega : Type u} {OmegaRef : Type v} {Env : Type w} {Action : Type x} {Reward : Type y} [MeasurableSpace Omega] [StandardBorelSpace Omega] [Nonempty Omega] [MeasurableSpace OmegaRef] [StandardBorelSpace OmegaRef] [Nonempty OmegaRef] [MeasurableSpace Env] [MeasurableSpace Action] [StandardBorelSpace Action] [Nonempty Action] [MeasurableSpace Reward] [StandardBorelSpace Reward] [Nonempty Reward] (mu : Measure Omega) [IsFiniteMeasure mu] (env : Omega -> Env) (action : Omega -> ActionTrace Action) (reward : Omega -> RewardTrace Reward) (referenceMu : Measure OmegaRef) [IsFiniteMeasure referenceMu] (referenceEnv : OmegaRef -> Env) (referenceAction : OmegaRef -> ActionTrace Action) (referenceReward : OmegaRef -> RewardTrace Reward) (algorithm referenceAlgorithm : HistoryAlgorithm Action Reward) (feedbackEnvironment : Env -> HistoryEnvironment Action Reward) (source : ConditionalHistoryAlgorithmDensitySplitSource mu env action reward referenceMu referenceEnv referenceAction referenceReward algorithm referenceAlgorithm feedbackEnvironment) (n : Nat) : ProbabilityTheory.condDistrib (fun omega => History.finitePairHistoryOfTrace (action omega) (reward omega) n) env mu =ᵐ[mu.map env] (ProbabilityTheory.condDistrib (fun omega => History.finitePairHistoryOfTrace (referenceAction omega) (referenceReward omega) n) referenceEnv referenceMu).withDensity (fun _ history => historyDensity algorithm referenceAlgorithm n history)

Finite-prefix Thompson probability matching from the concrete four-family split conditional-law interface.

theorem finitePairReferencePolicySampler_condDistrib_action_ae_eq_bestAction_of_conditionalSplitSource {Omega : Type u} {OmegaRef : Type v} {Env : Type w} {Action : Type x} {Reward : Type y} [MeasurableSpace Omega] [StandardBorelSpace Omega] [Nonempty Omega] [MeasurableSpace OmegaRef] [StandardBorelSpace OmegaRef] [Nonempty OmegaRef] [MeasurableSpace Env] [StandardBorelSpace Env] [Nonempty Env] [MeasurableSpace Action] [StandardBorelSpace Action] [Nonempty Action] [MeasurableSpace Reward] [StandardBorelSpace Reward] [Nonempty Reward] (mu : Measure Omega) [IsFiniteMeasure mu] (env : Omega -> Env) (action : Omega -> ActionTrace Action) (reward : Omega -> RewardTrace Reward) (referenceMu : Measure OmegaRef) [IsFiniteMeasure referenceMu] (referenceEnv : OmegaRef -> Env) (referenceAction : OmegaRef -> ActionTrace Action) (referenceReward : OmegaRef -> RewardTrace Reward) (algorithm referenceAlgorithm : HistoryAlgorithm Action Reward) (feedbackEnvironment : Env -> HistoryEnvironment Action Reward) (source : ConditionalHistoryAlgorithmDensitySplitSource mu env action reward referenceMu referenceEnv referenceAction referenceReward algorithm referenceAlgorithm feedbackEnvironment) (n : Nat) (bestAction : Env -> Action) (hbestAction : Measurable bestAction) : let actualHistory := fun omega => History.finitePairHistoryOfTrace (action omega) (reward omega) n let referenceHistory := fun omega => History.finitePairHistoryOfTrace (referenceAction omega) (referenceReward omega) n let policy := referenceActionKernel referenceMu referenceEnv referenceHistory source.reference.measurable_env (History.measurable_finitePairHistoryOfTrace referenceAction referenceReward source.reference.measurable_action source.reference.measurable_reward n) bestAction hbestAction let sampler := policySamplerMeasure mu actualHistory (History.measurable_finitePairHistoryOfTrace action reward source.actual.measurable_action source.actual.measurable_reward n) policy ProbabilityTheory.condDistrib policySamplerAction (policySamplerHistory actualHistory) sampler =ᵐ[ sampler.map (policySamplerHistory actualHistory)] ProbabilityTheory.condDistrib (bestAction ∘ policySamplerEnv env) (policySamplerHistory actualHistory) sampler