Theorem MeasureTheory.Measure.HasTemperateGrowth.exists_eLpNorm_lt_top

Modification history

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_top View 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_top View on Github →