Commit 2023-06-20 23:35 6f78b92d

View on Github →

feat: port Analysis.Fourier.PoissonSummation (#5306)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Fourier/PoissonSummation.lean

added theorem Real.fourierCoeff_tsum_comp_add

added theorem Real.tsum_eq_tsum_fourierIntegral

added theorem Real.tsum_eq_tsum_fourierIntegral_of_rpow_decay

added theorem Real.tsum_eq_tsum_fourierIntegral_of_rpow_decay_of_summable

added theorem SchwartzMap.tsum_eq_tsum_fourierIntegral

added theorem isBigO_norm_Icc_restrict_atBot

added theorem isBigO_norm_Icc_restrict_atTop

added theorem isBigO_norm_restrict_cocompact