fourier transform on locally compact abelian groups

Stream: Is there code for X?

[Sahan Wijetunga]

Is there any theory about the fourier transform on locally compact abelian groups formalized in mathlib?

[Yaël Dillies]

Bhavik and I developed a theory of the Fourier transform on finite abelian groups in APAP and I am currently in the process of generalising it to locally compact abelian groups. First (baby) step is #23923.

[Junyan Xu]

See also #maths > Multi-variable Fourier analysis @ 💬

[Andrew Yang]

Had anyone made any progress on this? If not, I will try to (make Yaël) do this.

[Andrew Yang]

We might start working on this properly soon, following Ramakrishnan and Valenza's Fourier Analysis on Number Fields, and we will start with Bochner's theorem. In particular we would need the following prerequisites

• Basic theory on functions of positive type (diagonalizable etc)
• Schur's lemma for topologically irreducible unitary representations of LCA groups
• Young's convolution inequality for LCA groups (or even unimodular ones?)
• Gelfand duality theory (I think we have a fair amount in mathlib already; maybe they are enough)

Is anyone working (or planning to work) on these results?

[Sahan Wijetunga]

I am currently in an REU (doing lean stuff) but in a couple months I'd be happy to start working on it.

[Anatole Dedecker]

@Andrew Yang May I suggest following Bourbaki’s spectral theory book? I’m not sure starting with Bochner’s theorem is the most obvious thing (in Bourbaki this is deferred until much later), but I definitely plan on defining all the flavors of functions of positive types and their GNS construction in the near future.

[Anatole Dedecker]

I realize there’s no English translation, but I think the approach here has the merit of not depending on representation theory. It does depend on some spectral theory in Banach/C^*-algebras, but we should have what’s needed since everything is commutative.

[pro-Lie stabilizer]

One could also assume Hilbert's fifth problem, using pro-objects in Smooth Lie groups.

[Sahan Wijetunga]

@Akil Qasim How does this work?

[Antoine Chambert-Loir]

This might have the inconvenient of requiring to choose a description of a locally compact group as a pro-object in smooth lie groups and making it more difficult to establish functoriality properties.

[Yaël Dillies]

@Andrew Yang and I have started thinking about formalising Bourbaki's book above. We are currently stuck on the definition of the Fourier transform as the integral of a scalar function against a vector measure. I know @Oliver Butterley was thinking about this at some point. Did it get anywhere?

[Oliver Butterley]

Together with @Yoh Tanimoto, the motive was Riesz representation so we need to have integrals with respect to complex measures. We had completed a definition of total variation of any VectorMeasure. Consequently we could work with the object ∫ x, f x * μ.ang x ∂(μ.var) where μ.var is the total variation measure and μ.ang is the Radon-Nikodym derivative μ.rnDeriv μ.var. In this way we could proceed with the argument for the moment. Anyway, mathematically the argument goes like this so there is no lost effort. I assumed much wiser Lean people would soon write the full definition of the integral with respect to a VectorMeasure and then we would swap that in later! :stuck_out_tongue_wink:

[Anatole Dedecker]

Ah right, it didn't occur to me that the first issue would be "(complex) measures as a convolution algebra"...

[pro-Lie stabilizer]

@Sahan Wijetunga @Antoine Chambert-Loir that's possible, but there's a selling point, which is that it is a closer fit with the Peter-Weyl theorem (and that's how it's shown).

The Peter-Weyl theorem uses the existence of Haar integral. But one can be more specific in this sense: they are all particular kinds of pro-constructions applied to the unitary groups just as in Schur's lemma in the above.

[pro-Lie stabilizer]

@Antoine Chambert-Loir Thanks for your advice here.

Could I ask about the major functoriality properties that one could expect? I would benefit I think, as I did from the paper you wrote about A₅ (the way I thought to do that used that S₅ acts on maximal cubes inside a dodecahedron but to formalize it one would use ℚ(φ)³).

I would like to point out that Laurent series in two or more variables is not locally compact as far as I know.

Could I ask some more about what objects the functoriality should be designed to include, and what those are?

I would imaging the induced representation and frobenius reciprocity are important.

You'll find I have endless points on this issue. For another, unital Gel'fand duality, which features compact hausdorff spaces, extends to nonunital Gel'fand duality using the one point compactification and functions which converge to 0 at ∞, and the case of locally compact hausdorff groups one point compactifies to group objects under smash product, interestingly enough.

[Yaël Dillies]

Oliver Butterley said:

I assumed much wiser Lean people would soon write the full definition of the integral with respect to a VectorMeasure and then we would swap that in later!

@Andrew Yang, you know what we have to do... :wink:

[Oliver Butterley]

Yes, please! :folded_hands:

[Yoh Tanimoto]

will that be for Banach spaces, or can VectorMeasure.integral be defined in a more general setting?

[Andrew Yang]

Do you have a good reference for Banach spaces though; I don't think I know how to do it off the top of my head and Yael doesn't seem to have a reference as well.

[Yoh Tanimoto]

This book by Dinculeanu seems to be a standard reference and Banach spaces are treated in most cases, although I haven't read it.
https://www.sciencedirect.com/book/9781483197623/vector-measures

[Oliver Butterley]

I'm ready to do some of the leg work required if I am given guidance. However I don't have clarity on the best route to take for integral with respect to vector measures.

[Oliver Butterley]

Rudin (p.129 Real & Complex Analysis) simply defines the integral of a complex function with respect to a complex measure in the way I mentioned earlier using the rnDeriv. Of course this works well for this case and any case where there is a RN derivative with respect to the total variation measure.
image.png

[Oliver Butterley]

Dunford and Schwartz (p.322 Linear operators part 1, definition IV.10.7) defines integrals of scalar functions with respect to vector measures.
image.png

[Antoine Chambert-Loir]

I would hope the situation is be simpler than that: if you wish to follow the approach of Bourbaki in their Spectral theory book, it suffices (it is also necessary) to have a version of their notion of integration of vector-valued functions (defined as an element of the bidual in Integration, chap. 6, and for some spaces, it is proved that it belongs to the space itself) and integration of functions with respect to vector-valued measure (which, obviously, is a continuous linear map on continuous functions valued in a vector space). Apparently, at least in mathlib, docs#MeasureTheory.VectorMeasure does not give rise to an integral in full generality.

[Yoh Tanimoto]

as for the latter, for mathlib, should one start with the integral of Real-valued function against a VectorMeasure or should one aim at the integral of vector-valued functions against a VectorMeasure with some module relation?

[Antoine Chambert-Loir]

The question can only be answered with an eye on how one needs to use those vector-valued measures! @Anatole Dedecker , what do you think?

[Anatole Dedecker]

The first thing that should be emphasized is that, in Bourbaki, all measures are Radon (whatever your preferred definition is), since they essentially use Riesz' theorem as a definition. So the algebra of complex bounded measures is really an algebra of complex bounded Radon measures, and I expect a lot of things to be false if you include more general measures.

[Anatole Dedecker]

I would have to check how far you can go with $L^1$ rather than $\mathscr{M}^1$. In any case, I think it makes sense to define the $L^1$ extension of a character directly (i.e not using the embedding to complex measures).

[Yoh Tanimoto]

I think one example of vector measure applied to a vector-valued function is when one wants to show the multiplicativity of functional calculus of the same operator

[pro-Lie stabilizer]

Sahan Wijetunga said:

Akil Qasim How does this work?

I didn't fully explain in the above, but this would divide into

(1) The construction of Haar integral for $S^1$, $\mathbb{R}$, $\mathbb{Z}$, and their products.

(2) The construction of Haar integral for any smooth Lie-group

The construction of Haar integral for a smooth Lie-group is pretty standard. It's essentially described by stating that there is a unique left (or right) translation invariant differential $n$-form for $n$ the dimension of the smooth Lie-group.

(3) The construction of Haar integral for a pro-object in smooth Lie-groups.

This uses the characterization of a pro-topology using the open cosets of finite index subgroups. In the case of a profinite group this is standard: one considers the supremum over sums of characteristic functions on cosets of finite index subgroups. Characteristic functions on these cosets have an integral (again in the finite case) which is a simple summation over $1/d$ for $d$ the index of the (open) finite index subgroup.

Here is an outline of a monograph in which it is shown (or at least stated) that pro-Lie groups contain all locally compact abelian groups.

I think I should say could seem to push in a different direction than where the group here is going, but I don't intend it that way.

Together with various combinations of advanced results showing that Pro-Lie is an extensive class (generalized further by the work of Tate on Tate modules, in which for example Laurent series obtain a Haar integral as well), these constructions have the interesting consequence of using $\mathbb{R}$-linearity.

[Kevin Buzzard]

I should think that we already have the first two things in mathlib? We have Haar integrals for an arbitrary locally compact topological group. Or am I misunderstanding?

[Kevin Buzzard]

https://arxiv.org/abs/2102.07636

[pro-Lie stabilizer]

@Kevin Buzzard Thanks this satisfies what I was trying to figure out. Sorry I hadn't looked into this before posting.

In that case we surely are not far from the Fourier transform itself, since this consists in integrating against a character as a function of the Pontrjagin dual. Maybe Plancharel's theorem would be a key point of interest next.

[pro-Lie stabilizer]

Does this mean that the 2-year old code here is up-to-date?

[pro-Lie stabilizer]

Also, if anyone reading this are interested in the "reverse mathematics" in the above then you may be able to finish off what I'm trying to do: use Haar measure for Pro-Lie groups along with the Gleason-Yamabe theorem and exact sequences of group actions to extend Haar integral, somehow using that $G/G_0$ has a unique measure invariant under the action of $G$. Is this possible?

[pro-Lie stabilizer]

Oh, and $G_0$ in the above is not notation for the connected component of the identity, but instead the subgroup occuring in the Gleason-Yamabe theorem.

[pro-Lie stabilizer]

@Floris van Doorn

[Floris van Doorn]

The two-year code is not up-to-date, but you can look here for the current code:
https://github.com/leanprover-community/mathlib4/tree/master/Mathlib/MeasureTheory/Measure/Haar
Some results have been generalized by @Sébastien Gouëzel in the meantime.