Commit 2024-04-24 06:52 29159393

View on Github →

feat: more integrability statements for iterated derivatives of Schwartz functions (#12152)

Estimated changes

Modified Mathlib/Analysis/Distribution/SchwartzSpace.lean

added def MeasureTheory.Measure.integrablePower

added def SchwartzMap.compCLMOfAntilipschitz

added theorem SchwartzMap.compCLMOfAntilipschitz_apply

added def SchwartzMap.compCLMOfContinuousLinearEquiv

added theorem SchwartzMap.compCLMOfContinuousLinearEquiv_apply

added theorem SchwartzMap.compCLM_apply

added theorem SchwartzMap.integrable_of_le_of_pow_mul_le

added theorem SchwartzMap.integrable_pow_mul_iteratedFDeriv

added theorem SchwartzMap.integrable_pow_neg_integrablePower

added theorem SchwartzMap.integral_pow_mul_iteratedFDeriv_le

added theorem SchwartzMap.integral_pow_mul_le_of_le_of_pow_mul_le

added theorem SchwartzMap.pow_mul_le_of_le_of_pow_mul_le

Modified Mathlib/MeasureTheory/Function/L1Space.lean

added theorem ContinuousLinearEquiv.integrable_comp_iff

added theorem LinearIsometryEquiv.integrable_comp_iff