Commit 2026-09-08 14:44 5432597b

feat(Analysis/Convolution,MeasureTheory/Function/LpSeminorm/CompareExp): add 7 lemmas (#41557) Upstreaming from Carleson: /Carleson/ToMathlib/Analysis/Convolution.lean

PSA - this description is stale, but consider this a starting point of this PR

theorem convolution_symm
- renamed g to f' (to reuse the existing section variable)
theorem AEStronglyMeasurable.convolution (refactored)
lemma lintegral_enorm_convolution_integrand_le_eLpNorm_mul_eLpNorm (refactored)
- removed the comment "This implies both of the following theorems convolutionExists_of_memLp_memLp and enorm_convolution_le_eLpNorm_mul_eLpNorm.", because the comment would create an impression that it's an auxiliary lemma that shouldn't be used on its own
theorem ConvolutionExists.of_memLp_memLp (slightly refactored)
- (hf : AEStronglyMeasurable f μ) and (hg : AEStronglyMeasurable g μ) were removed, because we can derive those hypotheses from hfp.aestronglyMeasurable and hgq.aestronglyMeasurable respectively (which we did during refactoring)
theorem enorm_convolution_le_eLpNorm_mul_eLpNorm

lemma lintegral_enorm_convolution_integrand_le_eLpNorm_mul_eLpNorm, theorem ConvolutionExists.of_memLp_memLp, theorem enorm_convolution_le_eLpNorm_mul_eLpNorm
- turned (hpq : p.HolderConjugate q) into an instance implicit [hpq : p.HolderConjugate q] (there does exist a class HolderConjugate for ENNReals, so mathlib seems to use instance implicits in such cases, like e.g. here)
theorem AEStronglyMeasurable.convolution, lemma lintegral_enorm_convolution_integrand_le_eLpNorm_mul_eLpNorm, theorem ConvolutionExists.of_memLp_memLp, theorem enorm_convolution_le_eLpNorm_mul_eLpNorm
- L was implicit, now became explicit (to comply with existing section variables)
- changed [SigmaFinite μ] to [SFinite μ] (because it's a weaker requirement /Mathlib/MeasureTheory/Measure/Typeclasses/SFinite.lean#L191)