Decay of compactly supported mollifications

Real scalar convolution is commutative.

Convolution with a normalized compact bump preserves decay at infinity.

theorem LiebThirring.convolution_real_comm {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] (f g : E → ℝ) : MeasureTheory.convolution f g (ContinuousLinearMap.lsmul ℝ ℝ) μ = MeasureTheory.convolution g f (ContinuousLinearMap.lsmul ℝ ℝ) μ

Real scalar convolution is commutative.

theorem LiebThirring.tendsto_normed_bump_convolution_cocompact {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] {w : E → ℝ} (hw : Continuous w) (hd : Filter.Tendsto w (Filter.cocompact E) (nhds 0)) (b : ContDiffBump 0) : Filter.Tendsto (MeasureTheory.convolution (b.normed μ) w (ContinuousLinearMap.lsmul ℝ ℝ) μ) (Filter.cocompact E) (nhds 0)

Convolution with a normalized compact bump preserves decay at infinity.