L¹-Convergence of Fejer sum

Stream: new members

[Bingyu Xia]

Hi everyone,

I've recently been working on a personal project and wanted to share it here, as I thought it might be interesting or useful to the community. I formalized the proof of L¹-Convergence of Fejer sum, which is a standard result in Fourier analysis. The complete source code is in here :
https://github.com/BryceT233/L1-convergence-of-Fejer-sum
I'm still learning, so I would appreciate any feedback on the proof structure, coding style, etc.. Thanks!

[Ruben Van de Velde]

Nice job! One comment: your theorems are too long :)

[Yaël Dillies]

All these proofs should be replaceable by calls to fun_prop: https://github.com/BryceT233/L1-convergence-of-Fejer-sum/blob/main/fejer_L1.lean#L103-L116

[Jireh Loreaux]

The proof hinges on representing the Fejér sum as the convolution of the function $f$ with the Fejér kernel $fejerKernel_n$, i.e., $\sigma_n(f) = f ⋆ fejerKernel_n$. Convergence is then established by showing that the family of Fejér kernels $\{K_n\}$ constitutes an approximation to the identity.

It seems that you didn't use docs#Filter.IsApproximateUnit though. :smiley:

[Bingyu Xia]

Yaël Dillies 发言道：

All these proofs should be replaceable by calls to fun_prop: https://github.com/BryceT233/L1-convergence-of-Fejer-sum/blob/main/fejer_L1.lean#L103-L116

I tried it out and it simplified some of the continuity/measuability checks, thanks!