Theorem MeasureTheory.ConvolutionExists.of_memLp_memLp

Modification history

2026-09-11 14:45

Mathlib/Analysis/Convolution.lean

refactor(MeasureTheory): define `eLpNorm f` to be infinite when not `AEStronglyMeasurable` (#42406) …

Modified MeasureTheory.ConvolutionExists.of_memLp_memLp View on Github →

2026-09-08 14:44

Mathlib/Analysis/Convolution.lean

feat(Analysis/Convolution,MeasureTheory/Function/LpSeminorm/CompareExp): add 7 lemmas (#41557) …

Added MeasureTheory.ConvolutionExists.of_memLp_memLp View on Github →