Integral with values in LCTVS?

Stream: maths

[Yury G. Kudryashov]

I want to formalize the fact that an invariant measure is an average of ergodic measures. Katok and Hasselblatt use Choquet-Bishop-de Leeuw theorem to prove this, see https://en.wikipedia.org/wiki/Choquet_theory
I've tried to read Bishop&De Leeuw 1959 but they never say how do they define the integral for a function taking values in a locally convex TVS. Where can I find the definition? Does it generalize Bochner integral? Is there a proof that doesn't require this generalization of integral?

[Heather Macbeth]

I looked up some of this work about 10 years ago -- if I remember correctly it may be the Pettis integral?

[Yury G. Kudryashov]

If I want the main goal in terms of docs#MeasureTheory.Measure.join, do you suggest following Bishop-De Leeuw or there is a better direct argument?

[Heather Macbeth]

That, I can't say. The one sentence I wrote above is all I remember :)

[Sébastien Gouëzel]

Yes, I think here it's a version of the Pettis integral (but not exactly because your space is already a dual). My interpretation is that g = ∫ ω, f ω ∂η means ∀ x, g x = ∫ f ω x ∂η. And in the case of probability measures, μ = ∫ ω, ν ω ∂η means ∀ s, MeasurableSet s → μ s = ∫ ω, ν ω s ∂η

[Sébastien Gouëzel]

In the latter case, you also need that ω -> ν ω s is measurable for all measurable set s. So, in mathlib terms, nu is a kernel (with values in ergodic measures), and mu can be written as the composition of this kernel and a probability measure eta.