Commit 2023-06-28 14:11 449de626

View on Github →

feat: port Analysis.Fourier.RiemannLebesgueLemma (#4950)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Fourier/RiemannLebesgueLemma.lean

added theorem Real.tendsto_integral_exp_smul_cocompact

added theorem Real.zero_at_infty_fourierIntegral

added theorem Real.zero_at_infty_vector_fourierIntegral

added theorem fourier_integral_eq_half_sub_half_period_translate

added theorem fourier_integral_half_period_translate

added theorem fourier_integrand_integrable

added theorem tendsto_integral_exp_inner_smul_cocompact

added theorem tendsto_integral_exp_inner_smul_cocompact_of_continuous_compact_support

added theorem tendsto_integral_exp_smul_cocompact

added theorem tendsto_integral_exp_smul_cocompact_of_inner_product

Modified Mathlib/Data/Real/ENNReal.lean