theorem ConeSupport.smulLeftCLM_schwEmbed_eq {n : ℕ} (φ : E n → ℂ) (f : SchwartzMap (E n) ℂ) : (TemperedDistribution.smulLeftCLM ℂ φ) (schwEmbed f) = schwEmbed ((SchwartzMap.smulLeftCLM ℂ φ) f)

Multiplication by φ commutes with the Schwartz embedding: the tempered distribution obtained by applying smulLeftCLM to the Schwartz embedding of f equals the Schwartz embedding of φ · f.

theorem ConeSupport.singularSupport_compactPart_empty_of_decomp {n : ℕ} {u : TemperedDistribution (E n) ℂ} (hsing : singularSupport u = ∅) (f : SchwartzMap (E n) ℂ) (g : TemperedDistribution (E n) ℂ) (hdecomp : u = schwEmbed f + g) : singularSupport g = ∅

If u = schwEmbed f + g and u has empty singular support, then the compactly supported part g also has empty singular support.

theorem ConeSupport.emptyCss_implies_schwartz_compact_decomp {n : ℕ} (u : TemperedDistribution (E n) ℂ) (hcss : ConicSingularSupportSphere u = ∅) (hsing : singularSupport u = ∅) : ∃ (f : SchwartzMap (E n) ℂ) (g : TemperedDistribution (E n) ℂ), u = schwEmbed f + g ∧ IsCompactlySupportedDistribution g ∧ singularSupport g = ∅

A tempered distribution u with empty conic singular support sphere and empty singular support decomposes as schwEmbed f + g for some Schwartz function f and compactly supported distribution g with empty singular support.

theorem ConeSupport.smulLeftCLM_comp_eq_mul {n : ℕ} (a b : E n → ℂ) (u : TemperedDistribution (E n) ℂ) (ha : Function.HasTemperateGrowth a) (hb : Function.HasTemperateGrowth b) (hab : Function.HasTemperateGrowth (a * b)) : (TemperedDistribution.smulLeftCLM ℂ a) ((TemperedDistribution.smulLeftCLM ℂ b) u) = (TemperedDistribution.smulLeftCLM ℂ (a * b)) u

Associativity of left multiplication on tempered distributions: applying smulLeftCLM a after smulLeftCLM b equals smulLeftCLM (a * b).

theorem ConeSupport.smulLeftCLM_eq_self_of_one_on_support {n : ℕ} (g : TemperedDistribution (E n) ℂ) (K : Set (E n)) (_hK : IsCompact K) (hK_supp : ∀ (f : SchwartzMap (E n) ℂ), Function.support ⇑f ∩ K = ∅ → g f = 0) (φ : E n → ℂ) (_hφ_smooth : ContDiff ℝ (↑⊤) φ) (_hφ_compact : HasCompactSupport φ) (hφ_one : ∀ x ∈ K, φ x = 1) (hφ_tg : Function.HasTemperateGrowth φ) : (TemperedDistribution.smulLeftCLM ℂ φ) g = g

If a smooth, compactly supported, temperate-growth function φ equals 1 on a compact set K containing the support of the distribution g, then multiplication by φ fixes g.

theorem ConeSupport.smulLeftCLM_schwartz_of_supported_in_smooth {n : ℕ} (g : TemperedDistribution (E n) ℂ) (φ : E n → ℂ) (hφ_smooth : ContDiff ℝ (↑⊤) φ) (hφ_compact : HasCompactSupport φ) (ψ : E n → ℂ) (hψ_smooth : ContDiff ℝ (↑⊤) ψ) (hψ_compact : HasCompactSupport ψ) (h_supp : tsupport φ ⊆ {y : E n | ψ y ≠ 0}) (f : SchwartzMap (E n) ℂ) (hf : (TemperedDistribution.smulLeftCLM ℂ ψ) g = schwEmbed f) : ∃ (s : SchwartzMap (E n) ℂ), (TemperedDistribution.smulLeftCLM ℂ φ) g = schwEmbed s

If ψ · g is given by a Schwartz function and the support of the smooth compactly supported φ lies inside the non-vanishing set of ψ, then φ · g is also given by a Schwartz function.

theorem ConeSupport.smulLeftCLM_schwartz_of_emptySingSupp {n : ℕ} (g : TemperedDistribution (E n) ℂ) (hsing : singularSupport g = ∅) (φ : E n → ℂ) (hφ_smooth : ContDiff ℝ (↑⊤) φ) (hφ_compact : HasCompactSupport φ) (_hφ_tg : Function.HasTemperateGrowth φ) : ∃ (f : SchwartzMap (E n) ℂ), (TemperedDistribution.smulLeftCLM ℂ φ) g = schwEmbed f

If g has empty singular support, then multiplying it by any smooth compactly supported φ yields a tempered distribution that is the Schwartz embedding of a Schwartz function.

theorem ConeSupport.schwEmbed_compact_support_of_distrib_compact_support {n : ℕ} (f : SchwartzMap (E n) ℂ) (K : Set (E n)) (hK : IsCompact K) (hK_supp : ∀ (ψ : SchwartzMap (E n) ℂ), Function.support ⇑ψ ∩ K = ∅ → (schwEmbed f) ψ = 0) : Function.support ⇑f ⊆ K

If the Schwartz embedding of f is supported (as a distribution) inside a compact set K, then the function support of f is contained in K.

theorem ConeSupport.compactlySupported_emptySingSupp_represented_by_smooth {n : ℕ} (g : TemperedDistribution (E n) ℂ) (hcomp : IsCompactlySupportedDistribution g) (hsing : singularSupport g = ∅) : ∃ (h : E n → ℂ), ContDiff ℝ (↑⊤) h ∧ HasCompactSupport h ∧ ∀ (ψ : SchwartzMap (E n) ℂ), g ψ = ∫ (x : E n), ψ x • h x

A compactly supported distribution with empty singular support is represented by integration against a smooth, compactly supported function.

theorem ConeSupport.compactSupport_emptySingSupp_isSchwartz {n : ℕ} (g : TemperedDistribution (E n) ℂ) (hcomp : IsCompactlySupportedDistribution g) (hsing : singularSupport g = ∅) : ∃ (f : SchwartzMap (E n) ℂ), schwEmbed f = g

A compactly supported distribution with empty singular support is the Schwartz embedding of a Schwartz function.

theorem ConeSupport.schwartz_conicSingularSupportSphere_empty {n : ℕ} (f : SchwartzMap (E n) ℂ) : ConicSingularSupportSphere (schwEmbed f) = ∅

The conic singular support sphere of any Schwartz function (viewed as a tempered distribution) is empty.

theorem ConeSupport.coneSingularSupport_eq_empty_iff {n : ℕ} (u : TemperedDistribution (E n) ℂ) : coneSingularSupport u = ∅ ↔ ∃ (f : SchwartzMap (E n) ℂ), schwEmbed f = u

Corollary 12.4 of Melrose: the cone singular support of a tempered distribution u is empty iff u is the Schwartz embedding of a Schwartz function.