Commit 2025-01-31 00:20 b9c7233c

View on Github →

feat(Analysis/Distribution): Add memLp, toLp, toLpCLM, continuous_toLp for SchwartzMap (#20423)

Estimated changes

Modified Mathlib/Analysis/Distribution/SchwartzSpace.lean

added theorem MeasureTheory.Measure.HasTemperateGrowth.exists_eLpNorm_lt_top

added theorem SchwartzMap.coeFn_toLp

added theorem SchwartzMap.continuous_toLp

added theorem SchwartzMap.eLpNorm_le_seminorm

added theorem SchwartzMap.eLpNorm_lt_top

added theorem SchwartzMap.injective_toLp

added theorem SchwartzMap.memℒp

added theorem SchwartzMap.memℒp_top

added theorem SchwartzMap.norm_toLp

added theorem SchwartzMap.norm_toLp_le_seminorm

added def SchwartzMap.toLp

added def SchwartzMap.toLpCLM

added theorem SchwartzMap.toLpCLM_apply