Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-02-10 10:20 735b22f8

View on Github →

feat(analysis/fourier): Riemann-Lebesgue lemma (part 1) (#18361) Add the Riemann-Lebesgue lemma for continuous and compactly-supported functions.

Estimated changes

Modified src/analysis/complex/basic.lean

added theorem complex.norm_exp_of_real_mul_I

Created src/analysis/fourier/riemann_lebesgue_lemma.lean

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_mul_exp_at_top_of_continuous_compact_support

Modified src/analysis/normed/group/basic.lean

added theorem has_compact_mul_support.exists_pos_le_norm

Modified src/measure_theory/integral/set_integral.lean

added theorem measure_theory.set_integral_eq_integral_of_ae_compl_eq_zero

added theorem measure_theory.set_integral_eq_integral_of_forall_compl_eq_zero

Modified src/topology/continuous_function/zero_at_infty.lean

Modified src/topology/uniform_space/compact.lean

added theorem continuous.uniform_continuous_of_tendsto_cocompact

deleted theorem continuous.uniform_continuous_of_zero_at_infty

added theorem has_compact_mul_support.is_one_at_infty

added theorem has_compact_mul_support.uniform_continuous_of_continuous