Commit 2025-04-15 00:31 d8e8ad3a

View on Github →

feat(Analysis): add improper integral of complex exp (#23209) These are the infinite version of integral_exp_mul_complex.

Estimated changes

Modified Mathlib/Analysis/SpecialFunctions/ImproperIntegrals.lean

added theorem integrableOn_exp_mul_complex_Iic

added theorem integrableOn_exp_mul_complex_Ioi

added theorem integrableOn_exp_neg_Ioi

added theorem integral_exp_mul_complex_Iic

added theorem integral_exp_mul_complex_Ioi

Modified Mathlib/MeasureTheory/Group/Integral.lean

added theorem MeasureTheory.IntegrableOn.comp_inv

added theorem MeasureTheory.IntegrableOn.comp_inv_Ici

added theorem MeasureTheory.IntegrableOn.comp_inv_Iic

added theorem MeasureTheory.IntegrableOn.comp_inv_Iio

added theorem MeasureTheory.IntegrableOn.comp_inv_Ioi