
Keywords: Almost periodic functions, constructive mathematics, topological groups
A.M.S. subject classification: 03F60 Constructive and recursive analysis, 22C05 Compact groups, 43A77 Analysis on general compact groups
Finding a natural constructive treatment of the theory of almost periodic functions has long been a challenge for constructive mathematics, see [2], [5] and [7]. The present approach is similar to the one by Bishop's student Brom [2]. However, we replace his long and explicit construction by a simple definition of a new metric on the group, due to von Neumann [10](p.447), and applying Fourier and PeterWeyl theory. Thus we obtain a very similar, but much more conceptual construction.
By constructive mathematics we mean constructive in the sense of Bishop [1]. That is, using intuitionistic logic and an appropriate set theory, or type theory. Like Bishop, we will freely use the axiom of (countable) dependent choice.
To introduce the theory of almost periodic functions we first consider a periodic function f:R→C with period 2π, say. We may identify f with a function g on the unit circle, by defining g(e^{i x}): = f(x), for all x∈R. Because the circle is a compact Abelian group, Fourier theory may be used to approximate the periodic function f by finite sums of characters.
The sum
In this section we collect some results from constructive topological group theory, mostly following [1][3]. We used [6], [9] and [8] as general references for the classical theory. In this section G will denote a topological group.
Definition 1. A topological group is a group that is also a topological space in such a way that the group operations are continuous.
Any locally compact group allows a unique translation invariant measure, called Haar measure [1]. For a simple construction of Haar measure on compact groups see [3]. This construction follows von Neumann's classical existence proof.
Let G be a compact group. Let L_{1} denote L_{1}(G), the space of Haarintegrable functions on G. Define the convolution from L_{1}×L_{1} to L_{1} by
f∗g = λx.∫f(y)g(y^{  1}x)d y,  (1) 
for all f,g∈L_{1}. This map is continuous, in fact ‖f∗g‖_{1}≤‖f‖_{1}‖g‖_{1}. Define the involution f^{~}≔λx.f(x^{  1}). With this involution and convolution as multiplication L_{1} is a *algebra, called the group algebra. The group algebra contains much information about the group. For instance a group is Abelian if and only if its group algebra is Abelian. The group G is compact, so its Haar measure is finite, consequently L_{2}(G)⊂L_{1}(G), and thus, the convolution product f∗g belongs to L_{2}, for all f∈L_{1} and g∈L_{2}. Moreover, ‖f∗g‖_{2}≤‖f‖_{1}‖g‖_{2}. Thus an element f of L_{1} can be considered as an operator λg.f∗g on the Hilbert space L_{2}. These operators are compact, and thus normable, so L_{1} can thus be completed to a C*algebra. This allows us to use:
Theorem 2.
We will sometimes speak about the spectrum of a *algebra when we mean the spectrum of the C*algebra as constructed above.
Let Z denote the center of the group algebra
Theorem 3.
Following [1] we define ‘(locally) compact space' to mean (locally) compact metric space. In fact, considering the more general case of a locally compact group, Bishop and Bridges introduce a new metric ρ^{∗} on G^{∗} such that (G^{∗},ρ^{∗}) is locally compact. For compact groups this metric is equivalent to the metric induced by the norm ‖⋅‖_{∞} on C(G), see [1] (Lemma 8.3.16).
As a paradigm consider the Abelian group G: = ({e^{i t}:t∈R},⋅). The character group of this group is the space of the functions {λz.z^{n}:n∈Z}⊂C(G) with the metric and multiplication inherited from the normed space C(G) of continuous functions on G. In this case G is compact and G^{∗} is discrete. This is the general situation.
Theorem 4. Let G be a compact Abelian group. Then the character group G^{∗} is discrete.
Every inhabited discrete separable metric space is countable, since any dense subset must coincide with the whole space. If G is a compact group, then G^{∗} is locally compact, and hence separable, since moreover, G^{∗} is discrete, it is countable.
For a locally compact space X let C_{∞}(X) denote the set of functions that are ‘zero at infinity'. Bishop and Bridges [1] (p.431,p.442) proved the following Fourier theorem.
Theorem 5. Let G be a locally compact Abelian group.
There is a normdecreasing linear map
In [3] the following results were proved for a general, not necessarily Abelian, compact group G. In this context Z denotes the center of the group algebra and Σ denotes a locally compact subset of its spectrum as a C*algebra. The points of Σ are called characters. We recall that Σ is discrete.
We define the linear functional I(f): = f(e) on the group algebra and remark that f∗g(e) = (f,g^{~}), the inner product with respect to the Haar integral.
Theorem 6. Let f be an element of Z such that f^{^}≥0. Let a_{σ}: = f^{^}(σ)/‖χ_{σ}‖_{}
2 
2 
Let e_{σ}: = χ_{σ}/‖χ_{σ}‖_{2} and b_{σ}(f): = (f,e_{σ}). Then ‖e_{σ}‖_{2} = 1 and b_{σ} = f^{^}(σ)/‖χ_{σ}‖_{2}.
Corollary 7.
The main theorem in the PeterWeyl theory may be formulated as follows.
Theorem 8. For each f∈C(G), ∑_{σ}e_{σ}∗f, where σ∈Σ, converges to f in L_{2}.
Usually, the PeterWeyl theorem speaks about irreducible representations. Fortunately, these representations are in oneone correspondences with the characters above.
In this section we will prove a constructive Bohr approximation theorem for the Abelian groups.
As is wellknown, it is in general not possible to compute the norms of constructive analogues of nonseparable normed spaces. Fortunately, there are, at least, two solutions to this problem: using quasinorms, or using generalized real numbers. We repeat the definition from [1] (p.343).
Definition 9. Let X be a linear space over a scalar field F, where either F = R or F = C. A seminorm ‖⋅‖ is a map from X to R such that for all a∈F and x,y∈X, ‖x‖≥0, ‖a x‖ = a‖x‖ and ‖x + y‖≤‖x‖ + ‖y‖. A quasinorm on X is a family {‖⋅‖_{i}:i∈I} of seminorms on X such that for each x∈X, the set {‖x‖_{i}:i∈I} is bounded. Define the apartness relation ≠ on X by x≠y if and only if there exists i∈I such that ‖x  y‖_{i}>0. Likewise, define the equality x = y if and only if not x≠y,for all x,y∈X. Then (X,{‖⋅‖_{i}:i∈I}) is called a quasinormed space.
A quasinormed space may also be viewed as a normed space where the norm is a generalized real number in the sense of Richman [4]. That is, the norm is a Dedekind cut in the real numbers, but this cut does not need to be located.
Although previous constructive developments considered only almost periodic functions defined on the real numbers it is natural to consider almost periodic functions over general groups. One of von Neumann's main ideas is that the almost periodic functions allow us to mimic most of the important constructions of compact groups. Most importantly, one can define a ‘Haar measure' on the set of almost periodic functions. See [3] for a constructive proof of von Neumann's classical ‘construction' of Haar measure on compact groups.
Here, instead of mimicking these constructions, we take a slightly different path: we define a new topology on G and use the theory of compact groups directly. Classically, this would be slightly less general since we exclude noncontinuous functions. Constructively, one can not define (total) noncontinuous functions. So, like Loomis, we restrict ourselves to continuous functions.
Let F denote either R or C and let C_{b}(X, F) denote the bounded continuous Fvalued functions on the set X. We will drop the field F when it is either clear from the context, or irrelevant. The space C_{b}(X) is a quasinormed space with quasinorm {‖⋅‖_{x}: x∈X}, where ‖f‖_{x} is defined as f(x).
A subset A of a quasinormed space is called totally bounded if for each ε>0, there is a finitely enumerable set f_{1},…,f_{n}∈A such that for each f∈A, there exists i such that ‖f  f_{i}‖_{j}<ε whenever j is in I. Note that unlike in the metric case, we can not require all the elements f_{1},…,f_{n} to be distinct.
Let G be an Abelian group. Define the operator T_{s} from C_{b}(G) to C_{b}(G) by T_{s} = λf.λx.f(s + x) for all s in G.
Definition 10. A function f∈C_{b}(G) is almost periodic if the set S_{f}: = {T(s)f:s∈G} is a totally bounded subset of C_{b}(G).
In case G = R, this definition is equivalent to Bohr's original definition, which we stated on p.1. Loomis' proof [6] (41F, p.171) of this fact is constructive. We note that every almost periodic function is uniformly continuous.
Let f be an almost periodic function on G. The function v_{a}: = λg.g(a) is a uniformly continuous function from C_{b}(G) to G. Because S_{f} is totally bounded, we may define a pseudometric on G by
This metric is invariant under the action of the group (G, + ), that is, d_{f}(a + c,b + c) = d_{f}(a,b), for all a,b,c∈G. Since ‖T_{y}f  T_{z}f‖_{∞} = sup_{x}f(x + y)  f(x + z) = d_{f}(y,z), there is an isometric embedding from S_{f} into (G,d_{f}). Consequently, (G,d_{f}) is totally bounded and we let G_{f} denote the completion of (G,d_{f}), which is a compact group.
Recall from theorem 4 that the character group of a metric compact Abelian group is discrete. We obtain the following Plancherel theorem for almost periodic functions.
Theorem 11. Let f be an almost periodic function. Let Σ = G_{}
∗ 
f 
The function f is uniformly continuous. So for every ε>0, there is a δ>0, such that when a  b<δ, then f(a + x)  f(b + x)<ε for all x∈G. Hence d_{f}(a,b)≤ε. Consequently, any continuous function on G_{f } is a continuous function on G, and thus characters of G_{f} are characters of G. This shows that the space Σ in the previous theorem is the canonical choice.
The following theorem is called the Bohr approximation theorem. As we remarked before, in constructive mathematics a sum, and therefore a linear combination, of characters need not be almost periodic.
Theorem 12. Let f be an almost periodic function on G. Then f can be approximated uniformly by an almost periodic linear combination of characters.
The measure μ we used in Theorem 11 , Haar measure on G _{f} , may seem a little ad hoc. In fact μ( f ) is equal to the value of the unique constant function in closure of the convex hull of S _{f} . See the construction of Haar measure in [ 10 ] and its constructive variant [ 3 ]. In the case G = R , the number μ( f ) is also equal to M ( f ) = lim _{N→∞}
1 
2N 
In this section we extend the results from the previous section to arbitrary topological groups. Therefore, we let G denote a topological group and e denote its unit.
Definition 13. Let f be a bounded continuous function on G. Define the operators T_{s}: = λgλx.g(s x) and T_{}
s 
In the following it is often the case that the proof that S^{f} is totally bounded is symmetric to the proof that S_{f} is totally bounded. In such cases we will only prove the latter statement.
Lemma 14. Every almost periodic function f is normable.
Every continuous function f on a compact group H is almost periodic. Indeed, S_{f} is totally bounded, since it is the uniformly continuous image of the compact set H.
Let f be almost periodic on G. Define the pseudometric
on G. As before, the space (G,d_{f}) is totally bounded, and its completion G_{f} is a compact group. The function f is continuous on G_{f}, and by the PeterWeyl theorem 8 f = ∑_{χ}f∗χ in L_{2}(G_{f}); here the sum ranges over the character space Σ. For each character χ, T_{s}(f∗χ) = (T_{s}f)∗χ, so that f∗χ is almost periodic. The function f∗χ is even minimal almost invariant.
Definition 15. A function f∈C(G) is called left almost invariant if the set A of translations of f, span{T_{s}f:s∈G} is a finitedimensional subspace of C(G). It is called almost invariant if it is both left and right almost invariant.
It is called
To see that f∗χ is almost invariant we recall from [3] that λf.χ∗f is both a projection and a compact operator, so its range is finite dimensional. To see that it is minimal we need some preparations.
We consider C(G_{f}) as a *algebra with the convolution operator ∗ as multiplication and the map ()^{~} defined by f^{~}≔λx.f(x^{  1}) as involution. Then p is called a projection if p = p∗p = p^{~}.
Lemma 16.
Lemma 17. Every nonzero closed ideal I contains a nonzero central element.
Since the only central elements in the ideal I generated by a character χ are multiples of this character, we see that any nonzero closed subideal must actually be equal to I. It follows that f∗χ is minimal almost invariant.
This proves the following theorem.
Theorem 18. Let f be an almost periodic function on a topological group G. Then f = ∑f∗χ_{} in L_{2}(G_{f}) where the sum ranges over Σ. Moreover, each term f∗χ is minimal almost invariant.
The following theorem is proved in a similar way as Theorem 12. It is a Bohr approximation theorem for general topological groups.
Theorem 19. Let G be a topological group. Every almost periodic function on G can be uniformly approximated by a linear combination of minimal almost invariant functions which is almost periodic.
We have given a constructive proof of the Bohr approximation theorem for general topological groups, thus simplifying and generalizing previous constructive approaches.
Finally, Loomis [6] proves that every left almost periodic function is also right almost periodic. His proof is nonconstructive. To be precise consider his Lemma 41B. Let n be the number of elements of the family a_{i} and let n denote the finite set with n elements. Then one needs to isolate all the functions j:n→n which correspond to a given b∈G. In this way we obtain a subfinite approximation to the space of translated functions. Classically, this approximation is totally bounded, but constructively one needs a finitely enumerable set. It is unclear to me whether this can be proved constructively.
Parts of this research can already be found in my PhDthesis [?]. I would like to thank Wim Veldman for his advice during this period. Finally, I would like to thank the referees for suggestions that helped to improve the presentation of the paper.
[1] Errett Bishop and Douglas Bridges. Constructive analysis, volume 279 of Grundlehren der Mathematischen Wissenschaften. SpringerVerlag, 1985.
[2] J. Brom. The theory of almost periodic functions in constructive mathematics. Pacific Journal of Mathematics, 70:67–81, 1977.
[3] Thierry Coquand and Bas Spitters. A constructive proof of the PeterWeyl theorem. Mathematical Logic Quarterly, 4:351–359, 2005.
[4] Fred Richman. Generalized real numbers in constructive mathematics. Indagationes Mathematicae, 9:595–606, 1998.
[5] C.G. Gibson. On the almost periodicity of trigonometric polynomials in constructive mathematics. Indagationes Mathematicae, 34:355–361, 1972.
[6] Lynn H. Loomis. An introduction to abstract harmonic analysis. University Series in Higher Mathematics. van Nostrand, New York, 1953.
[7] Margenstern, Maurice. On a variant of the constructive theory of almost periodic functions. Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, 24:495–507, 1978.
[8] M.A. Naimark and A.I. Stern. Theory of group representations, volume 246 of Grundlehren der Mathematischen Wissenschaften. SpringerVerlag, 1982.
[9] S. Sternberg. Group theory and physics. Cambridge University Press, 1994.
[10] J. v. Neumann. Almost periodic functions in a group. I. Trans. Amer. Math. Soc., 36(3):445–492, 1934.