Multiplication of tempered distributions by functions of temperate growth

Mathlib's TemperedDistribution.smulLeftCLM F g multiplies a tempered distribution by a function g of temperate growth, through its action u ↦ g • u on test functions. This file records that on the tempered distribution of a Schwartz function f, taken against any measure of temperate growth, it is the tempered distribution of the pointwise product g • f, so that it extends Mathlib's SchwartzMap.smulLeftCLM. Mathlib proves the corresponding statement for g of temperate growth lying in Lᵖ, acting on L^q functions with Hölder exponents (MeasureTheory.Lp.toTemperedDistribution_smul_eq).

Directional derivatives of such products obey the Leibniz rule ∂_v (g f) = (∂_v g) f + g ∂_v f, where ∂_v g is the classical derivative x ↦ Dg(x) v, again a function of temperate growth. By duality this is the Leibniz rule for Schwartz functions (SchwartzMap.lineDerivOp_smulLeftCLM).

Main results

• TemperedDistribution.smulLeftCLM_eq_zero_of_not_hasTemperateGrowth: for a symbol without temperate growth, smulLeftCLM is the junk value 0.
• TemperedDistribution.smulLeftCLM_toTemperedDistributionCLM_eq: multiplication by g on tempered distributions extends multiplication by g on Schwartz functions.
• TemperedDistribution.lineDerivOp_smulLeftCLM: the Leibniz rule for the product of a tempered distribution with a function of temperate growth.

@[simp]

theorem TemperedDistribution.smulLeftCLM_eq_zero_of_not_hasTemperateGrowth {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [AddCommGroup F] [Module ℂ F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousConstSMul ℂ F] {g : E → ℂ} (hg : ¬Function.HasTemperateGrowth g) : smulLeftCLM F g = 0

Multiplication by a function without temperate growth is the junk value 0, because SchwartzMap.smulLeftCLM is 0 for such a function.

theorem TemperedDistribution.lineDerivOp_smulLeftCLM {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℂ F] {g : E → ℂ} (hg : Function.HasTemperateGrowth g) (f : TemperedDistribution E F) (v : E) : LineDeriv.lineDerivOp v ((smulLeftCLM F g) f) = (smulLeftCLM F fun (x : E) => (fderiv ℝ g x) v) f + (smulLeftCLM F g) (LineDeriv.lineDerivOp v f)

The Leibniz rule for tempered distributions: for g of temperate growth, ∂_v (g f) = (∂_v g) f + g ∂_v f, where ∂_v g is the classical derivative x ↦ Dg(x) v.

theorem TemperedDistribution.smulLeftCLM_toTemperedDistributionCLM_eq {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] [NormedAddCommGroup F] [NormedSpace ℂ F] {μ : MeasureTheory.Measure E} [μ.HasTemperateGrowth] {g : E → ℂ} (f : SchwartzMap E F) : (smulLeftCLM F g) ((SchwartzMap.toTemperedDistributionCLM E F μ) f) = (SchwartzMap.toTemperedDistributionCLM E F μ) ((SchwartzMap.smulLeftCLM F g) f)

Multiplication by a function on tempered distributions extends the pointwise multiplication of Schwartz functions, for the embedding of Schwartz functions against any measure of temperate growth. (If g is not of temperate growth, both multiplications are zero.)