Ryan Martinez

Stream: new members

[Ryan Martinez]

Hi! I'm new here; I've only just gotten started on learning lean.

I am a PhD student of Daniel Tataru studying nonlinear waves, and I was curious if I would be interfering with anyone if I wanted to formalize some results on Lp spaces and their multipliers and how I would go about contributing if I made progress. My starting point would be Riesz-Thorin and Marcinkiewicz interpolation and then try to either tackle H\"ormander's multiplier theorem and the Littlewood Paley theorem or go more in the direction of Strichartz estimates and the Christ-Kiselev lemma. I didn't see these things in mathlib, but let me know if anyone is working on them. I did see the Gagliardo-Nirenburg-Sobolev inequality, which this work would be parallel to, and a corollary of this work would be the Hardy-Littlewood-Sobolev inequality which extends GNS (outside of L1) to more general derivative multipliers.

Thanks so much!
Ryan

[Yaël Dillies]

Hey! I am interested in multipliers in the context of compact groups. I will soon develop the relevant Fourier theory over at yaeldillies.github.io/mean-fourier

[Ryan Martinez]

Very cool! I'm not super familiar with the Fourier theory of compact groups except for the torus of course. Do you know if the results are similar? I'm not super sure to what level of generality these theorems hold, probably the interpolation theorems work on any measure space. Do you have proofs of these already? Unfortunately your link sends me nowhere, so I can't look for myself.

[Ryan Martinez]

After some preliminary research there do appear to be more general multiplier theorems for locally compact groups, which probably fit better in your context. Maybe then my time would be better spent working on Strichartz estimates, but I will likely need some of your results so let me know if I can see them, or when they will be ready!

[Yaël Dillies]

My project is currently empty. I should start work on it in about two months :slight_smile:

[Ryan Martinez]

Ah I see! That makes sense! Well if I have time before then, and lean doesn't give me too much trouble, I'll ping you with the proofs of Riesz-Thorin and Marcinkiewicz interpolation for measure spaces in case you need them!

[Yongxi Lin (Aaron)]

I also want to formalize some of the stuffs you mention. You probably want to check out the Carleson' project: https://florisvandoorn.com/carleson/blueprint/. They formalized some prerequisites that you need (e.g. some APIs for weak Lp spaces). I believe they are working on upstreaming these results into Mathlib. Also I think it is probably better to formalize the more abstract versions of these two interpolation theorems in Mathlib, namely the theory about Interpolation spaces (https://en.wikipedia.org/wiki/Interpolation_space). I have seen a blueprint for the formalization of Riesz-Thorin over here: https://florisvandoorn.com/BonnAnalysis/blueprint/, but it seems like that they are not working on it right now.

Apparently you also want some results from theory of (tempered) distributions, maybe @Moritz Doll can tell you more about this part.

[Ryan Martinez]

Awesome! Thank you for the suggestions! The classical proofs of the multiplier theorems I know (for instance in the book of Duoandikoetxea) use the properties of p.v. 1/x in an essential way, but aside from that the tempered distributions end up landing in Lp and so the proofs can just be in regard to bounded linear functional on Lp’. But having done some research it does seem like there is a much more general setting over locally compact groups in which these theorems have analogs, and that’s outside my wheelhouse. So I’m not quite sure how much energy to put in that direction. But I know the Strichartz estimates are dependent on the structure of the underlying space and so is something that is definitely worth formalizing for Rn first. But yea I’ll take a look at those links!