Commit 2023-02-14 15:23 a231f964

View on Github →

feat(analysis/fourier): Basic framework for Fourier transforms (#18428) This adds a file whose purpose is to define the Fourier transform in very great generality -- this is a spinoff from #18392.

Estimated changes

Created src/analysis/fourier/fourier_transform.lean

added def fourier.fourier_integral

added theorem fourier.fourier_integral_comp_add_right

added theorem fourier.fourier_integral_def

added theorem fourier.fourier_integral_norm_le

added theorem fourier.fourier_integral_smul_const

added theorem real.continuous_fourier_char

added def real.fourier_char

added theorem real.fourier_char_apply

added def real.fourier_integral

added theorem real.fourier_integral_def

added theorem real.fourier_integral_eq_integral_exp_smul

added theorem real.vector_fourier_integral_eq_integral_exp_smul

added def vector_fourier.fourier_integral

added theorem vector_fourier.fourier_integral_add

added theorem vector_fourier.fourier_integral_comp_add_right

added theorem vector_fourier.fourier_integral_continuous

added theorem vector_fourier.fourier_integral_convergent

added theorem vector_fourier.fourier_integral_norm_le

added theorem vector_fourier.fourier_integral_smul_const

Modified src/analysis/fourier/riemann_lebesgue_lemma.lean

added theorem real.fourier_integral_zero_at_infty_of_continuous_compact_support

added theorem tendsto_integral_mul_exp_at_bot_of_continuous_compact_support

added theorem zero_at_infty_integral_mul_exp_of_continuous_compact_support