L^1 as an algebra under convolution

Stream: Is there code for X?

[Jireh Loreaux]

Do we have a type synonym for L^1 with convolution as the multiplication?

[Yaël Dillies]

Not mathlib, but we have basically this in LeanAPAP: https://github.com/YaelDillies/LeanAPAP/blob/master/LeanAPAP/Prereqs/Convolution/Basic.lean

[Jireh Loreaux]

That's discrete though right? I mean, we want that too, but I was thinking the measure-theoretic L^1