BanditRLProof.PosteriorKernel

A posterior distribution over environments indexed by observed histories. The underlying object is Mathlib's `ProbabilityTheory.Kernel`; the local wrapper gives Thompson-sampling and Bayesian-regret leaves a stable project name for the regularity contract.

structure MarkovPosteriorKernel (History : Type u) (Env : Type v) [MeasurableSpace History] [MeasurableSpace Env] where

Build the local posterior-kernel contract from an existing Mathlib kernel.

def ofKernel (kernel : ProbabilityTheory.Kernel History Env) (hkernel : ProbabilityTheory.IsMarkovKernel kernel) : MarkovPosteriorKernel History Env where

Build a posterior kernel from a measurable posterior-measure selector.

def ofMeasureSelector (posterior : History -> Measure Env) (hposterior : Measurable posterior) (hprob : forall history, IsProbabilityMeasure (posterior history)) : MarkovPosteriorKernel History Env where

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

theorem ofMeasureSelector_apply (posterior : History -> Measure Env) (hposterior : Measurable posterior) (hprob : forall history, IsProbabilityMeasure (posterior history)) (history : History) : (ofMeasureSelector posterior hposterior hprob).kernel history = posterior history

Build a posterior kernel on a countable/discrete history space. Finite histories in the bandit development are typically countable/discrete, so Mathlib's `Kernel.ofFunOfCountable` can turn any probability-valued posterior selector into a Markov kernel without a separate measurability proof.

def ofCountableHistorySelector [Countable History] [MeasurableSingletonClass History] (posterior : History -> Measure Env) (hprob : forall history, IsProbabilityMeasure (posterior history)) : MarkovPosteriorKernel History Env where

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

theorem ofCountableHistorySelector_apply [Countable History] [MeasurableSingletonClass History] (posterior : History -> Measure Env) (hprob : forall history, IsProbabilityMeasure (posterior history)) (history : History) : (ofCountableHistorySelector posterior hprob).kernel history = posterior history

The posterior kernel is measurable as a map from histories to measures.

theorem measurable_kernel (posterior : MarkovPosteriorKernel History Env) : Measurable posterior.kernel

A measurable random history selects a measurable random posterior measure.

theorem measurable_apply_of_measurable_history {Omega : Type u} [MeasurableSpace Omega] (posterior : MarkovPosteriorKernel History Env) (history : Omega -> History) (hhistory : Measurable history) : Measurable (fun omega : Omega => posterior.kernel (history omega))

For every measurable environment event, the posterior event probability is a measurable scalar function of a measurable random history.

theorem measurable_eventProbability_of_measurable_history {Omega : Type u} [MeasurableSpace Omega] (posterior : MarkovPosteriorKernel History Env) (history : Omega -> History) (hhistory : Measurable history) {event : Set Env} (hevent : MeasurableSet event) : Measurable (fun omega : Omega => posterior.kernel (history omega) event)

Every measure selected by a posterior kernel is a probability measure.

theorem isProbabilityMeasure_apply (posterior : MarkovPosteriorKernel History Env) (history : History) : IsProbabilityMeasure (posterior.kernel history)

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

theorem apply_univ (posterior : MarkovPosteriorKernel History Env) (history : History) : posterior.kernel history Set.univ = 1

The Mathlib posterior of a likelihood kernel under a prior measure.

noncomputable def canonicalPosterior [StandardBorelSpace Env] [Nonempty Env] (prior : Measure Env) [IsProbabilityMeasure prior] (likelihood : ProbabilityTheory.Kernel Env History) [ProbabilityTheory.IsMarkovKernel likelihood] : MarkovPosteriorKernel History Env

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

theorem canonicalPosterior_kernel [StandardBorelSpace Env] [Nonempty Env] (prior : Measure Env) [IsProbabilityMeasure prior] (likelihood : ProbabilityTheory.Kernel Env History) [ProbabilityTheory.IsMarkovKernel likelihood] : (canonicalPosterior prior likelihood).kernel = ProbabilityTheory.posterior likelihood prior

The canonical joint law generated by a prior followed by a likelihood.

noncomputable def canonicalJointMeasure (prior : Measure Env) [IsProbabilityMeasure prior] (likelihood : ProbabilityTheory.Kernel Env History) [ProbabilityTheory.IsMarkovKernel likelihood] : Measure (Env × History)

Identify the canonical posterior on any source with the prescribed Bayesian environment/history pair law. The proof uses the defining composition-product identity for Mathlib's `posterior`. Thus the posterior conditional-law equality is produced from a joint-law transport, rather than assumed as a separate Bayes-law field.

theorem canonicalPosterior_kernel_ae_eq_condDistrib_of_pair_map_eq {Omega : Type*} [MeasurableSpace Omega] [StandardBorelSpace Env] [Nonempty Env] (mu : Measure Omega) [IsFiniteMeasure mu] (env : Omega -> Env) (history : Omega -> History) (henv : Measurable env) (hhistory : Measurable history) (prior : Measure Env) [IsProbabilityMeasure prior] (likelihood : ProbabilityTheory.Kernel Env History) [ProbabilityTheory.IsMarkovKernel likelihood] (hpair : mu.map (fun omega => (env omega, history omega)) = canonicalJointMeasure prior likelihood) : (canonicalPosterior prior likelihood).kernel =ᵐ[mu.map history] ProbabilityTheory.condDistrib env history mu

On the canonical Bayesian product space itself, the Mathlib posterior is the conditional distribution of the environment coordinate given the history coordinate.

theorem canonicalPosterior_kernel_ae_eq_condDistrib_fst_snd [StandardBorelSpace Env] [Nonempty Env] (prior : Measure Env) [IsProbabilityMeasure prior] (likelihood : ProbabilityTheory.Kernel Env History) [ProbabilityTheory.IsMarkovKernel likelihood] : (canonicalPosterior prior likelihood).kernel =ᵐ[ (canonicalJointMeasure prior likelihood).map Prod.snd] ProbabilityTheory.condDistrib Prod.fst Prod.snd (canonicalJointMeasure prior likelihood)

Minimal prior/likelihood/posterior package. This records the Bayesian objects that future Thompson-sampling leaves need to name. It does not assert that `posterior` satisfies Bayes' rule for `prior` and `likelihood`.

structure BayesianPosteriorSurface (Env : Type u) (History : Type v) [MeasurableSpace Env] [MeasurableSpace History] where

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

theorem posterior_isProbabilityMeasure_apply (surface : BayesianPosteriorSurface Env' History') (history : History') : IsProbabilityMeasure (surface.posterior.kernel history)