Theorem MeasureTheory.Measure.HasTemperateGrowth.exists_eLpNorm_lt_top

Modification history

2026-09-11 14:45
Mathlib/Analysis/Distribution/TemperateGrowth.lean
refactor(MeasureTheory): define `eLpNorm f` to be infinite when not `AEStronglyMeasurable` (#42406) …
Modified MeasureTheory.Measure.HasTemperateGrowth.exists_eLpNorm_lt_topView on Github →
2025-10-29 13:18
Mathlib/Analysis/Distribution/SchwartzSpace.lean
chore(Analysis/Distribution): split off functions and measures of temperate growth (#30553) …
Modified MeasureTheory.Measure.HasTemperateGrowth.exists_eLpNorm_lt_topView on Github →
2025-01-31 00:20
Mathlib/Analysis/Distribution/SchwartzSpace.lean
feat(Analysis/Distribution): Add memLp, toLp, toLpCLM, continuous_toLp for SchwartzMap (#20423)
Added MeasureTheory.Measure.HasTemperateGrowth.exists_eLpNorm_lt_topView on Github →