BanditRLProof.Algorithms.ThompsonAlgorithmDensity

Weighting the base measure of a composition product is the same as weighting the product by the density pulled back through the first projection.

theorem compProd_withDensity_left {History : Type u} {Env : Type v} [MeasurableSpace History] [MeasurableSpace Env] (historyLaw : Measure History) [SFinite historyLaw] (posterior : ProbabilityTheory.Kernel History Env) [ProbabilityTheory.IsSFiniteKernel posterior] (density : History -> ENNReal) (hdensity : Measurable density) : historyLaw.withDensity density ⊗ₘ posterior = (historyLaw ⊗ₘ posterior).withDensity (density ∘ Prod.fst)

Composing a kernel weighted by a density independent of its input is the same as weighting the composed output measure.

theorem comp_withDensity_history {Env : Type u} {History : Type v} [MeasurableSpace Env] [MeasurableSpace History] (envLaw : Measure Env) (historyKernel : ProbabilityTheory.Kernel Env History) [ProbabilityTheory.IsSFiniteKernel historyKernel] (density : History -> ENNReal) (hdensity : Measurable density) : (historyKernel.withDensity (fun _ history => density history)) ∘ₘ envLaw = (historyKernel ∘ₘ envLaw).withDensity density

Swapping a joint law weighted by its second coordinate moves the density to the first coordinate of the swapped law.

theorem map_swap_withDensity_snd {Env : Type u} {History : Type v} [MeasurableSpace Env] [MeasurableSpace History] (joint : Measure (Env × History)) (density : History -> ENNReal) (hdensity : Measurable density) : (joint.withDensity (density ∘ Prod.snd)).map Prod.swap = (joint.map Prod.swap).withDensity (density ∘ Prod.fst)

Composition products transport an a.e. output-only kernel density directly, without requiring an `IsSFiniteKernel` instance for the weighted kernel.

theorem compProd_eq_compProd_withDensity_snd_of_ae_eq {Env : Type u} {History : Type v} [MeasurableSpace Env] [MeasurableSpace History] (envLaw : Measure Env) [SFinite envLaw] (actualHistoryKernel referenceHistoryKernel : ProbabilityTheory.Kernel Env History) [ProbabilityTheory.IsSFiniteKernel actualHistoryKernel] [ProbabilityTheory.IsSFiniteKernel referenceHistoryKernel] (density : History -> ENNReal) (hdensity : Measurable density) (hkernel : actualHistoryKernel =ᵐ[envLaw] referenceHistoryKernel.withDensity (fun _ history => density history)) : envLaw ⊗ₘ actualHistoryKernel = (envLaw ⊗ₘ referenceHistoryKernel).withDensity (density ∘ Prod.snd)

The exact law interface produced by an algorithm-density/change-of-algorithm argument. Both the history marginal and the history/environment joint law are weighted by the same measurable density depending only on history.

structure AlgorithmDensityPosteriorSource {Omega : Type u} {OmegaRef : Type v} {History : Type w} {Env : Type x} [MeasurableSpace Omega] [MeasurableSpace OmegaRef] [MeasurableSpace History] [MeasurableSpace Env] (mu : Measure Omega) (env : Omega -> Env) (history : Omega -> History) (referenceMu : Measure OmegaRef) (referenceEnv : OmegaRef -> Env) (referenceHistory : OmegaRef -> History) where

Construct the two algorithm-density pushforward laws from a closer-to-process interface: the actual and reference environment marginals agree, and the actual conditional history kernel is the reference conditional history kernel weighted by one history-only density.

noncomputable def algorithmDensityPosteriorSource_of_condDistrib_history_withDensity {Omega : Type u} {OmegaRef : Type v} {History : Type w} {Env : Type x} [MeasurableSpace Omega] [MeasurableSpace OmegaRef] [MeasurableSpace History] [StandardBorelSpace History] [Nonempty History] [MeasurableSpace Env] (mu : Measure Omega) [IsFiniteMeasure mu] (env : Omega -> Env) (history : Omega -> History) (henv : Measurable env) (hhistory : Measurable history) (referenceMu : Measure OmegaRef) [IsFiniteMeasure referenceMu] (referenceEnv : OmegaRef -> Env) (referenceHistory : OmegaRef -> History) (hreferenceEnv : Measurable referenceEnv) (hreferenceHistory : Measurable referenceHistory) (density : History -> ENNReal) (hdensity : Measurable density) (henvLaw : mu.map env = referenceMu.map referenceEnv) (hcond : ProbabilityTheory.condDistrib history env mu =ᵐ[mu.map env] (ProbabilityTheory.condDistrib referenceHistory referenceEnv referenceMu).withDensity (fun _ history => density history)) : AlgorithmDensityPosteriorSource mu env history referenceMu referenceEnv referenceHistory

The reference environment posterior equals the actual posterior whenever the two algorithm-density pushforward laws use the same history density.

theorem referencePosterior_ae_eq_condDistrib_of_algorithmDensitySource {Omega : Type u} {OmegaRef : Type v} {History : Type w} {Env : Type x} [MeasurableSpace Omega] [MeasurableSpace OmegaRef] [MeasurableSpace History] [MeasurableSpace Env] [StandardBorelSpace Env] [Nonempty Env] (mu : Measure Omega) [IsFiniteMeasure mu] (env : Omega -> Env) (history : Omega -> History) (henv : Measurable env) (referenceMu : Measure OmegaRef) [IsFiniteMeasure referenceMu] (referenceEnv : OmegaRef -> Env) (referenceHistory : OmegaRef -> History) (hreferenceEnv : Measurable referenceEnv) (hreferenceHistory : Measurable referenceHistory) (source : AlgorithmDensityPosteriorSource mu env history referenceMu referenceEnv referenceHistory) : (referencePosterior referenceMu referenceEnv referenceHistory hreferenceEnv hreferenceHistory).kernel =ᵐ[mu.map history] ProbabilityTheory.condDistrib env history mu

Reference-policy Thompson probability matching with algorithm-density laws as the only process-level input.

theorem referencePolicySampler_condDistrib_action_ae_eq_bestAction_of_algorithmDensitySource {Omega : Type u} {OmegaRef : Type v} {History : Type w} {Env : Type x} {Action : Type y} [MeasurableSpace Omega] [MeasurableSpace OmegaRef] [MeasurableSpace History] [MeasurableSpace Env] [StandardBorelSpace Env] [Nonempty Env] [MeasurableSpace Action] [StandardBorelSpace Action] [Nonempty Action] (mu : Measure Omega) [IsFiniteMeasure mu] (env : Omega -> Env) (history : Omega -> History) (henv : Measurable env) (hhistory : Measurable history) (referenceMu : Measure OmegaRef) [IsFiniteMeasure referenceMu] (referenceEnv : OmegaRef -> Env) (referenceHistory : OmegaRef -> History) (hreferenceEnv : Measurable referenceEnv) (hreferenceHistory : Measurable referenceHistory) (bestAction : Env -> Action) (hbestAction : Measurable bestAction) (source : AlgorithmDensityPosteriorSource mu env history referenceMu referenceEnv referenceHistory) : let policy := referenceActionKernel referenceMu referenceEnv referenceHistory hreferenceEnv hreferenceHistory bestAction hbestAction let sampler := policySamplerMeasure mu history hhistory policy ProbabilityTheory.condDistrib policySamplerAction (policySamplerHistory history) sampler =ᵐ[ sampler.map (policySamplerHistory history)] ProbabilityTheory.condDistrib (bestAction ∘ policySamplerEnv env) (policySamplerHistory history) sampler

Reference-policy Thompson probability matching from an equal environment marginal and a conditional-history density law, without separately assuming the two algorithm-density pushforward laws.

theorem referencePolicySampler_condDistrib_action_ae_eq_bestAction_of_condDistrib_history_withDensity {Omega : Type u} {OmegaRef : Type v} {History : Type w} {Env : Type x} {Action : Type y} [MeasurableSpace Omega] [MeasurableSpace OmegaRef] [MeasurableSpace History] [StandardBorelSpace History] [Nonempty History] [MeasurableSpace Env] [StandardBorelSpace Env] [Nonempty Env] [MeasurableSpace Action] [StandardBorelSpace Action] [Nonempty Action] (mu : Measure Omega) [IsFiniteMeasure mu] (env : Omega -> Env) (history : Omega -> History) (henv : Measurable env) (hhistory : Measurable history) (referenceMu : Measure OmegaRef) [IsFiniteMeasure referenceMu] (referenceEnv : OmegaRef -> Env) (referenceHistory : OmegaRef -> History) (hreferenceEnv : Measurable referenceEnv) (hreferenceHistory : Measurable referenceHistory) (density : History -> ENNReal) (hdensity : Measurable density) (henvLaw : mu.map env = referenceMu.map referenceEnv) (hcond : ProbabilityTheory.condDistrib history env mu =ᵐ[mu.map env] (ProbabilityTheory.condDistrib referenceHistory referenceEnv referenceMu).withDensity (fun _ history => density history)) (bestAction : Env -> Action) (hbestAction : Measurable bestAction) : let policy := referenceActionKernel referenceMu referenceEnv referenceHistory hreferenceEnv hreferenceHistory bestAction hbestAction let sampler := policySamplerMeasure mu history hhistory policy ProbabilityTheory.condDistrib policySamplerAction (policySamplerHistory history) sampler =ᵐ[ sampler.map (policySamplerHistory history)] ProbabilityTheory.condDistrib (bestAction ∘ policySamplerEnv env) (policySamplerHistory history) sampler

Finite action/reward-prefix Thompson probability matching from a packaged pair of algorithm-density laws.

theorem finitePairReferencePolicySampler_condDistrib_action_ae_eq_bestAction_of_algorithmDensitySource {Omega : Type u} {OmegaRef : Type v} {Env : Type w} {Action : Type x} {Reward : Type y} [MeasurableSpace Omega] [MeasurableSpace OmegaRef] [MeasurableSpace Env] [StandardBorelSpace Env] [Nonempty Env] [MeasurableSpace Action] [StandardBorelSpace Action] [Nonempty Action] [MeasurableSpace Reward] (mu : Measure Omega) [IsFiniteMeasure mu] (env : Omega -> Env) (action : Omega -> ActionTrace Action) (reward : Omega -> RewardTrace Reward) (henv : Measurable env) (haction : forall t : Nat, Measurable (fun omega => action omega t)) (hreward : forall t : Nat, Measurable (fun omega => reward omega t)) (referenceMu : Measure OmegaRef) [IsFiniteMeasure referenceMu] (referenceEnv : OmegaRef -> Env) (referenceAction : OmegaRef -> ActionTrace Action) (referenceReward : OmegaRef -> RewardTrace Reward) (hreferenceEnv : Measurable referenceEnv) (hreferenceAction : forall t : Nat, Measurable (fun omega => referenceAction omega t)) (hreferenceReward : forall t : Nat, Measurable (fun omega => referenceReward omega t)) (n : Nat) (bestAction : Env -> Action) (hbestAction : Measurable bestAction) (source : AlgorithmDensityPosteriorSource mu env (fun omega => History.finitePairHistoryOfTrace (action omega) (reward omega) n) referenceMu referenceEnv (fun omega => History.finitePairHistoryOfTrace (referenceAction omega) (referenceReward omega) n)) : 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 hreferenceEnv (History.measurable_finitePairHistoryOfTrace referenceAction referenceReward hreferenceAction hreferenceReward n) bestAction hbestAction let sampler := policySamplerMeasure mu actualHistory (History.measurable_finitePairHistoryOfTrace action reward haction hreward n) policy ProbabilityTheory.condDistrib policySamplerAction (policySamplerHistory actualHistory) sampler =ᵐ[ sampler.map (policySamplerHistory actualHistory)] ProbabilityTheory.condDistrib (bestAction ∘ policySamplerEnv env) (policySamplerHistory actualHistory) sampler

Finite action/reward-prefix Thompson probability matching from an equal environment marginal and a conditional finite-history density law.

theorem finitePairReferencePolicySampler_condDistrib_action_ae_eq_bestAction_of_condDistrib_history_withDensity {Omega : Type u} {OmegaRef : Type v} {Env : Type w} {Action : Type x} {Reward : Type y} [MeasurableSpace Omega] [MeasurableSpace 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) (henv : Measurable env) (haction : forall t : Nat, Measurable (fun omega => action omega t)) (hreward : forall t : Nat, Measurable (fun omega => reward omega t)) (referenceMu : Measure OmegaRef) [IsFiniteMeasure referenceMu] (referenceEnv : OmegaRef -> Env) (referenceAction : OmegaRef -> ActionTrace Action) (referenceReward : OmegaRef -> RewardTrace Reward) (hreferenceEnv : Measurable referenceEnv) (hreferenceAction : forall t : Nat, Measurable (fun omega => referenceAction omega t)) (hreferenceReward : forall t : Nat, Measurable (fun omega => referenceReward omega t)) (n : Nat) (density : History.FinitePairHistory Action Reward n -> ENNReal) (hdensity : Measurable density) (henvLaw : mu.map env = referenceMu.map referenceEnv) (hcond : 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 => density history)) (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 hreferenceEnv (History.measurable_finitePairHistoryOfTrace referenceAction referenceReward hreferenceAction hreferenceReward n) bestAction hbestAction let sampler := policySamplerMeasure mu actualHistory (History.measurable_finitePairHistoryOfTrace action reward haction hreward n) policy ProbabilityTheory.condDistrib policySamplerAction (policySamplerHistory actualHistory) sampler =ᵐ[ sampler.map (policySamplerHistory actualHistory)] ProbabilityTheory.condDistrib (bestAction ∘ policySamplerEnv env) (policySamplerHistory actualHistory) sampler