Discrete analysis

Stream: maths

[Yaël Dillies]

In order to formalise the Kelley-Meka bound on Roth numbers, I have developed discrete Fourier analysis in LeanAPAP. The project has come far enough along and enough prerequisites have been upstreamed to mathlib that it is time to think about how discrete analysis should look like in mathlib.

[Yaël Dillies]

Here is what LeanAPAP currently contains (see this folder, I will update the list as PRs get opened and merged):

• NNRat.cast, the canonical embedding from ℚ≥0 to any semifield (#11203)
• Finset.dens, the density of a finset inside its ambient type (#11243)
• LeanAPAP#Finset.expect, the compact normalisation variant of Finset.sum
• Precomposition operators, like translation, dilation, conjugation-negation (LeanAPAP#translate, LeanAPAP#dilate, LeanAPAP#conjneg)
• Orthogonality of characters of finite abelian groups (LeanAPAP#AddChar.complexBasis and theorems around it)
• Pontryagin duality for finite abelian groups (LeanAPAP#AddChar.doubleDualEquiv)
• Discrete and compact Lp-norms (LeanAPAP#lpNorm, LeanAPAP#nlpNorm)
• Discrete and compact convolution (LeanAPAP#conv, LeanAPAP#dconv)
• Discrete and compact Fourier transform (LeanAPAP#dft, LeanAPAP#cft)
• The Marcinkiewicz-Zygmund inequality (LeanAPAP#complex_marcinkiewicz_zygmund)
• Rudin's inequality (LeanAPAP#rudin_ineq)
• Chang's lemma (LeanAPAP#chang)
• Almost periodicity (LeanAPAP#AlmostPeriodicity.linfty_almost_periodicity)
• Bohr sets (LeanAPAP#BohrSet)

[Yaël Dillies]

Here are some design decisions I made:

• I set everything up without measure theory. This means that all I'm dealing with are finite sums.
• I defined everything twice, once using the discrete normalisation, once using the compact normalisation. Nowadays, additive combinatorics mostly uses the convention that physical space is compact and frequency space is discrete, but not everyone agrees.
• I use docs#AddChar instead of docs#PontryaginDual to avoid assuming that my spaces have a topology.

[Yaël Dillies]

Some things are great the way I set them up:

• Lemmas have no measurability or continuity side conditions.
• Imports are pretty light as the heaviest thing I need is docs#Real.log. In particular, no measure theory is required.

[Yaël Dillies]

Some are less great:

• I had to duplicate everything in the discrete normalisation to also have them in the compact normalisation.
• My definitions don't handle discrete-but-infinite or compact-but-infinite spaces.

[Yaël Dillies]

Here are some questions that need answering:

• Are we happy with the discrete vs continuous duplication?
• Do we want the Lp-norms to be defined over more general spaces using docs#tsum and integration?
• Should we use docs#AddChar or docs#PontryaginDual ?

[Yaël Dillies]

Some people that will want to have a say are @Thomas Bloom, @Terence Tao, @David Loeffler, @Michael Stoll.

[Yaël Dillies]

@Eric Wieser, special mention to you for the precomposition operators (I can already hear you say "They are just the action of DomMulAct Gᵐᵒᵖ on G")

[David Loeffler]

I'd certainly argue strongly that rather than having special definitions for things like Lp-norms, convolution, etc in the discrete case, we should unify these with the existing material in the Mathlib analysis / measure-theory libraries. Yes, this will mean the files end up importing more of the existing hierarchy, but I don't see why that is a bad thing in itself; and eventually, we'll hopefully have things like Marcinkiewicz–Zygmund proved in their natural generality (which is much broader than discrete abelian groups) and we can just specialise them to the discrete case for the combinatorial applications.

[Eric Wieser]

LeanAPAP#lpNorm could perhaps just be notation,

[Kevin Buzzard]

Orthogonality (and even orthonormality) of characters of general finite groups is already in mathlib ,so you didn't need to do it again in the abelian case, you just had to import a whole bunch of category theory instead.

[Michael Stoll]

Where?

[Kevin Buzzard]

https://leanprover-community.github.io/mathlib4_docs/Mathlib/RepresentationTheory/Character.html#FdRep.char_orthonormal

[Michael Stoll]

Not sure that deducing the finite abelian case from that is much easier than doing it from scratch... :smile:

[Kevin Buzzard]

Yeah this was the main reason I mentioned it (that and the fact that I think this is an interesting discussion point)

[David Loeffler]

As for:

• Lemmas have no measurability or continuity side conditions,

Why would they? Any function on a finite set is continuous and Borel measurable for the discrete topology, and integrable for any locally finite measure, and mathlib knows this perfectly well (docs#discrete_of_t1_of_finite, docs#continuous_of_discreteTopology, docs#measurable_of_finite, etc). So if you want to use some general result from the measure-theory library in your discrete setting, any continuity / measurability conditions in the general case should be pretty effortless to tick off (and if not, then this is a gap in the API which should be fixed, not a reason to reinvent the wheel).

[Anatole Dedecker]

I agree with David: in a world where we all have infinite time, I see no reason not to go directly to the case of abelian locally compact groups (e.g by following Bourbaki, Théories Spectrales). I think most of the things lacking will be $L^1$ as a convolution algebra, as well as some facts about (commutative but non-unital) Banach algebras, but this is all standard material that needs to make its way into Mathlib eventually.

EDIT: Thinking about it again, I realize I significantly underestimated some things here, e.g we would need some form of Young inequality, and generally way more results about convolution.

[Yaël Dillies]

David Loeffler said:

if you want to use some general result from the measure-theory library in your discrete setting, any continuity / measurability conditions in the general case should be pretty effortless to tick off

That's true, but let me list you the ways in which you could "tick off" such a side condition:

• It's in a rw call and you fill in the side condition immediately. In practice, it is verbose and a bit wonky (on top of being annoying to write in the first place). See eg https://github.com/teorth/pfr/blob/66e620ab5bddbe4c10eac21b050fb82c637bf032/PFR/WeakPFR.lean#L323-L332 in PFR.
• It's in a rw call and you leave the side condition to the end. This is nice looking, except for the fact that you always have a bunch of goals hanging around, and some tactic calls at the end to handle them.
• It's in a simp call and the corresponding lemma is a simp lemma. That works great, except that the lemma being simp might incur a general performance penalty for all simp calls with the same type of side condition.
• It's in a simp call and the corresponding lemma isn't a simp lemma. Then again having to include the lemma in every simp call looks a bit wonky

[Terence Tao]

We certainly do perform additive combinatorics on some infinite discrete groups, such as the integers, as well as some infinite compact groups, such as the unit circle, and of course locally compact groups such as the reals that are neither discrete nor compact. So long-term we would eventually want to generalize much of the Fourier side of this subject beyond the finite case.

A few months ago there was a similar discussion within https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Should.20there.20be.20a.20ProbabilitySpace.20class.3F as to whether to set up discrete probability in a way that allows users (in say theoretical computer science) not familiar with the subtleties of measure theory to just go ahead and use these tools off the shelf. I have no strong opinion either way, as long as there are lots of helper lemmas that, for instance, relate both the compact Fourier transform and the discrete Fourier transform to the general locally compact abelian Fourier transform (when the latter becomes available in Mathlib), or to relate compact and discrete notions of L^p norms etc. to each other. I guess the main question is that of timing: do we push the restricted versions of these tools first and worry about refactoring them to special cases of a more general version later, or do we insist on doing the general version first? Mathematically I don't see a strong case either way, so it comes down to Mathlib's policy preferences I think.

[Yaël Dillies]

Here I see three reasonable non-mutually exclusive solutions:

• My current one
• Make some tactics like measurability or continuity auto-params in the relevant lemmas. Hopefully that's nice, but again it will incur an extra cost for every use of this lemma, and possibly lead to confusing error messages when users expect the side condition to appear, but instead the auto-param tactic tries to fill it and fails.
• Make a copy of every general theory lemma in a Discrete namespace, with all measurability/continuity/integrability side conditions stripped off. I find this a very attractive option, because it also lets us state things in more domain-specific terms, eg by using finite sums rather than integrals. It also solves the next problem, which I am about to explain.

[Yaël Dillies]

David Loeffler said:

Any function on a finite set is continuous and Borel measurable for the discrete topology, and integrable for any locally finite measure, and mathlib knows this perfectly well

I am being provocative, but no it doesn't:

import Mathlib

example {α β : Type*} [Finite α] (f : α → β) : Continuous f := sorry
-- failed to synthesize instance
--   TopologicalSpace α

[Yaël Dillies]

My point is that to even talk about continuity and measurability I need to assume the existence of extra data on all relevant spaces, and also assume that that data is trivial (every set is open/measurable...). This is a pain, when all you want to talk about is functions between finite types and finite sums.

[Yaël Dillies]

If we had a Discrete namespace with copies of general theory lemmas to the finite case, we would be able to nicely get rid of all these [Topological Space α] [DiscreteTopology α] and [MeasurableSpace α] [DiscreteMeasurableSpace α] assumptions by locally (to the files putting lemmas in the Discrete namespace) having instances of the form Finite α → TopologicalSpace α, Finite α → DiscreteTopology α.

[David Loeffler]

My point is that to even talk about continuity and measurability I need to assume the existence of extra data on all relevant spaces, and also assume that that data is trivial (every set is open/measurable...)

Isn't this exactly what local instance is for?

[Yaël Dillies]

That's still burden on the user.

[Anatole Dedecker]

David Loeffler said:

My point is that to even talk about continuity and measurability I need to assume the existence of extra data on all relevant spaces, and also assume that that data is trivial (every set is open/measurable...)

Isn't this exactly what local instance is for?

This yields basically unusable statements, what if you end up with a topology which is discrete but not definitionally ?

[Anatole Dedecker]

I think I would be okay with the Discrete namespace. What I don't want is to have duplicated proofs just for the sake of not importing topology.

[Yaël Dillies]

Not quite, Anatole, because I assume David is referring to uses of lemmas within the proofs.

[Anatole Dedecker]

Ah, right. But how do you even state lemmas involving the Fourier transform if you don't have any ambient topology then?

[Yaël Dillies]

Terence Tao said:

I guess the main question is that of timing: do we push the restricted versions of these tools first and worry about refactoring them to special cases of a more general version later, or do we insist on doing the general version first?

Personally, I have already spent a significant proportion of the past eight months on this project and people are starting to need discrete analysis in mathlib (eg @Daniel Weber, David himself). So I would be more than happy to get my stuff as it is now in mathlib and worry about generalising later.

[Yaël Dillies]

Anatole Dedecker said:

Ah, right. But how do you even state lemmas involving the Fourier transform if you don't have any ambient topology then?

Yep, good point... So in that case we will also need the discrete Fourier transform as a definition. If we define it as the general Fourier transform according to the discrete topology, then it's probably fine.

[Yaël Dillies]

Yaël Dillies said:

So I would be more than happy to get my stuff as it is now in mathlib and worry about generalising later.

I should also add that the amount of material I would add to mathlib is tiny compared to what would be needed for the general case, so the choice is really between:

• Have people add some random lemmas about my tiny discrete analysis API until someone comes along and generalises it all in two years time
• Have no discrete analysis at all for the coming two years

[Daniel Weber]

This isn't very relevant, but is the contrapositive of LeanAPAP#expect_le and LeanAPAP#le_expect anywhere? It's a common form of the probabilistic method, so it might be worth adding it