feat(Analysis/Distribution): tsupport of smulLeftCLM (leanprover-community#34595)

Author: mcdoll

Mathlib/Analysis/Distribution/SchwartzSpace/Basic.lean

@@ -722,10 +722,14 @@ def smulLeftCLM (g : E → 𝕜) : 𝓢(E, F) →L[𝕜] 𝓢(E, F) :=
     SchwartzMap.bilinLeftCLM (ContinuousLinearMap.lsmul 𝕜 𝕜).flip hg
   else 0
 
+theorem smulLeftCLM_apply {g : E → 𝕜} (hg : g.HasTemperateGrowth) (f : 𝓢(E, F)) :
+    smulLeftCLM F g f = fun x ↦ g x • f x := by
+  simp [smulLeftCLM, hg]
+
 @[simp]
 theorem smulLeftCLM_apply_apply {g : E → 𝕜} (hg : g.HasTemperateGrowth) (f : 𝓢(E, F)) (x : E) :
     smulLeftCLM F g f x = g x • f x := by
-  simp [smulLeftCLM, hg]
+  simp [smulLeftCLM_apply hg]
 
 @[simp]
 theorem smulLeftCLM_const (c : 𝕜) :
@@ -793,6 +797,13 @@ theorem smulLeftCLM_real_smul {g : E → 𝕜'} (hg : g.HasTemperateGrowth) (c :
   rw [RCLike.real_smul_eq_coe_smul (K := 𝕜') c, smulLeftCLM_smul hg,
     ← RCLike.real_smul_eq_coe_smul c]
 
+theorem tsupport_smulLeftCLM_subset (g : E → 𝕜) (f : 𝓢(E, F)) :
+    tsupport (smulLeftCLM F g f) ⊆ tsupport f ∩ tsupport g := by
+  by_cases hg : g.HasTemperateGrowth
+  · simpa [smulLeftCLM_apply hg] using
+      ⟨tsupport_smul_subset_right g f, tsupport_smul_subset_left g f⟩
+  · simp [smulLeftCLM, hg]
+
 end smul
 
 section pairing