Commit 2023-06-26 05:48 b4ae7328

View on Github →

feat: port Analysis.SpecialFunctions.Gaussian (#5370)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/SpecialFunctions/Gaussian.lean

added theorem Complex.Gamma_one_half_eq

added theorem Complex.tsum_exp_neg_mul_int_sq

added theorem GaussianFourier.integrable_cexp_neg_mul_sq_add_real_mul_I

added theorem GaussianFourier.integral_cexp_neg_mul_sq_add_real_mul_I

added theorem GaussianFourier.norm_cexp_neg_mul_sq_add_mul_I'

added theorem GaussianFourier.norm_cexp_neg_mul_sq_add_mul_I

added theorem GaussianFourier.tendsto_verticalIntegral

added def GaussianFourier.verticalIntegral

added theorem GaussianFourier.verticalIntegral_norm_le

added theorem Real.Gamma_one_half_eq

added theorem Real.tsum_exp_neg_mul_int_sq

added theorem continuousAt_gaussian_integral

added theorem exp_neg_mul_sq_isLittleO_exp_neg

added theorem fourier_transform_gaussian

added theorem fourier_transform_gaussian_pi

added theorem integrableOn_Ioi_exp_neg_mul_sq_iff

added theorem integrableOn_rpow_mul_exp_neg_mul_sq

added theorem integrable_cexp_neg_mul_sq

added theorem integrable_exp_neg_mul_sq

added theorem integrable_exp_neg_mul_sq_iff

added theorem integrable_mul_cexp_neg_mul_sq

added theorem integrable_mul_exp_neg_mul_sq

added theorem integrable_rpow_mul_exp_neg_mul_sq

added theorem integral_cexp_neg_mul_sq_add_const

added theorem integral_gaussian

added theorem integral_gaussian_Ioi

added theorem integral_gaussian_complex

added theorem integral_gaussian_complex_Ioi

added theorem integral_gaussian_sq_complex

added theorem integral_mul_cexp_neg_mul_sq

added theorem isLittleO_exp_neg_mul_sq_cocompact

added theorem norm_cexp_neg_mul_sq

added theorem rpow_mul_exp_neg_mul_sq_isLittleO_exp_neg

added theorem tendsto_rpow_abs_mul_exp_neg_mul_sq_cocompact