Commit 2024-04-15 06:46 038cb584

View on Github →

refactor(SpecialFunctions/Gaussian): shorten long pole (#12104) This splits up Analysis/SpecialFunctions/Gaussian.lean into three pieces, with the heaviest imports only needed in the later chunks. As only the first chunk is needed for many applications, including those on the critical path towards NumberTheory/Cyclotomic/PID.lean, this should improve overall build parallelism and shorten mathlib's overall compilation time.

Estimated changes

deleted theorem Complex.Gamma_one_half_eq
deleted theorem Real.Gamma_one_half_eq
deleted theorem fourierIntegral_gaussian
deleted theorem integrable_cexp_quadratic
deleted theorem integrable_exp_neg_mul_sq
deleted theorem integral_cexp_quadratic
deleted theorem integral_gaussian
deleted theorem integral_gaussian_Ioi
deleted theorem integral_gaussian_complex
deleted theorem norm_cexp_neg_mul_sq
added theorem Real.Gamma_one_half_eq
added theorem integral_gaussian
added theorem integral_gaussian_Ioi
added theorem norm_cexp_neg_mul_sq