Extending invariant means to UAP functions

This file proves that every invariant mean extends uniquely to an invariant mean for which uniformly almost-periodic functions are measurable.

noncomputable def InvtMean.uapExtension {G : Type u_1} [Group G] (m : InvtMean G ℂ ℂ) : InvtMean G ℂ ℂ

The unique extension of an invariant mean to uniformly almost-periodic functions.

Equations

• One or more equations did not get rendered due to their size.