1.2. Measure on sequences
To define the consistency of a stochastic iterative global optimization algorithm, we need to use the initial probability measure and the Markov kernels of an algorithm to construct a probability measure on infinite sequences of samples produced by the algorithm. We chose to use the Ionescu-Tulcea theorem (Tulcea, 1949)CT Ionescu Tulcea, 1949. “Mesures dans les espaces produits”. In Atti Accad. Naz. Lincei Rend. to define this measure. The implementation of this theorem in Mathlib is done via the Kernel.traj function, which, given a family of Markov kernels on finite sequences, returns a Markov kernel on infinite sequences.
To be able to use Kernel.traj with kernel_iter, we need to pullback each kernel in the family along a function that, given a sequence of samples u and a continuous function f, returns (u, f ∘ u). This new kernel is defined using iter_comap.
def iter_comap (n : ℕ) : Kernel (iter α n) α :=
(A.kernel_iter n).comap
(prod_eval n f)
(measurable_prod_eval n hf.measurable)
It allows to define a measure on sequences of size n + 1 by averaging the Ionescu-Tulcea kernel, given by Kernel.traj (A.iter_comap hf) 0 over the initial measure Algorithm.ν pulled back along the measurable equivalence between Iic 0 → α and α.
noncomputable def ν_mequiv : Measure (iter α 0) := A.ν.comap (MeasurableEquiv.funUnique _ _)noncomputable def measure (A : Algorithm α β) : Measure (ℕ → α) :=
(Kernel.traj (A.iter_comap hf) 0).avg A.ν_mequiv
Because ν is a probability measure, and all kernels kernel_iter are Markov kernels, measure is a also probability measure on sequences of samples.
instance : IsProbabilityMeasure (A.measure hf) := α:Type u_1β:Type u_2inst✝⁵:MeasurableSpace αinst✝⁴:TopologicalSpace αinst✝³:OpensMeasurableSpace αinst✝²:MeasurableSpace βinst✝¹:TopologicalSpace βinst✝:BorelSpace βA:Algorithm α βf:α → βhf:Continuous f⊢ IsProbabilityMeasure (measure hf A)
α:Type u_1β:Type u_2inst✝⁵:MeasurableSpace αinst✝⁴:TopologicalSpace αinst✝³:OpensMeasurableSpace αinst✝²:MeasurableSpace βinst✝¹:TopologicalSpace βinst✝:BorelSpace βA:Algorithm α βf:α → βhf:Continuous f⊢ IsProbabilityMeasure ((Kernel.traj (A.iter_comap hf) 0).avg A.ν_mequiv)
All goals completed! 🐙
Finally, we can define the measure on finite sequences of samples of size n + 1 produced by the algorithm by measuring set of infinite sequences of samples such that the first n + 1 elements are in a set of sequences of size n + 1.
noncomputable def fin_measure {n : ℕ} : Measure (iter α n) := (A.measure hf).map (frestrictLe n)