def DifferentialOperators.HasCompactSupport {n : ℕ} (u : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) : Prop

A tempered distribution u on Euclidean space has compact support if there is a compact K such that u annihilates every Schwartz function whose support is disjoint from K.

theorem DifferentialOperators.hasCompactDsupport_of_hasCompactSupport {n : ℕ} (μ : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) (hμ : HasCompactSupport μ) : HasCompactDsupport μ

If μ has compact support in the Schwartz-pairing sense, then its distributional support Distribution.dsupport μ is compact.

noncomputable def DifferentialOperators.schwNegReflCLM {n : ℕ} : SchwartzMap (EuclideanSpace ℝ (Fin n)) ℂ →L[ℂ] SchwartzMap (EuclideanSpace ℝ (Fin n)) ℂ

The reflection φ ↦ φ ∘ (-id) as a continuous linear endomorphism of the Schwartz space 𝓢(EuclideanSpace ℝ (Fin n), ℂ).

noncomputable def DifferentialOperators.crossCorrSchwartzCLM {n : ℕ} (μ : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) (hμ : HasCompactSupport μ) : SchwartzMap (EuclideanSpace ℝ (Fin n)) ℂ →L[ℂ] SchwartzMap (EuclideanSpace ℝ (Fin n)) ℂ

Cross-correlation with a compactly supported distribution μ, viewed as a continuous linear endomorphism of 𝓢(EuclideanSpace ℝ (Fin n), ℂ).

noncomputable def DifferentialOperators.convolutionSchwartzCLM {n : ℕ} (μ : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) (hμ : HasCompactSupport μ) : SchwartzMap (EuclideanSpace ℝ (Fin n)) ℂ →L[ℂ] SchwartzMap (EuclideanSpace ℝ (Fin n)) ℂ

Convolution with a compactly supported distribution μ on Schwartz functions, given as the reflection composed with cross-correlation.

noncomputable def DifferentialOperators.distribConvolution {n : ℕ} (μ f : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) (hμ : HasCompactSupport μ) : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ

The convolution μ * f of two tempered distributions, defined when the left factor μ has compact support, by precomposing f with convolution by μ on Schwartz test functions.

structure DifferentialOperators.SmoothDecomp {n : ℕ} (u : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) : Type

A decomposition of a tempered distribution u = singular + smooth into a singular part with compact support contained in supportSet and a globally smooth, compactly supported part. Used in the proof of singularSupport_convolution_subset.

• singular : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ
• smooth : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ
• supportSet : Set (EuclideanSpace ℝ (Fin n))
• supportSet_compact : IsCompact self.supportSet
• singular_supported (φ : SchwartzMap (EuclideanSpace ℝ (Fin n)) ℂ) : Function.support ⇑φ ∩ self.supportSet = ∅ → self.singular φ = 0
• singular_compactSupport : HasCompactSupport self.singular
• smooth_isSmooth (x₀ : EuclideanSpace ℝ (Fin n)) : isSmoothNear self.smooth x₀
• smooth_compactSupport : HasCompactSupport self.smooth
• sum_eq : u = self.singular + self.smooth

theorem DifferentialOperators.singularSupport_compact_of_compactSupport {n : ℕ} (u : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) (hu : HasCompactSupport u) : IsCompact (singularSupport u)

If u has compact support, then its singular support is compact (in particular, closed and contained in the support of u).

theorem DifferentialOperators.smulLeft_add_complement {n : ℕ} (χ : EuclideanSpace ℝ (Fin n) → ℂ) (u : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) (hχ : Function.HasTemperateGrowth χ := by fun_prop) : (TemperedDistribution.smulLeftCLM ℂ χ) u + (TemperedDistribution.smulLeftCLM ℂ (1 - χ)) u = u

Partition-of-unity identity for left multiplication by a tempered-growth function χ: χ · u + (1 - χ) · u = u.

theorem DifferentialOperators.support_schwartz_smulLeft_subset {n : ℕ} (χ : EuclideanSpace ℝ (Fin n) → ℂ) (φ : SchwartzMap (EuclideanSpace ℝ (Fin n)) ℂ) : Function.support ⇑((SchwartzMap.smulLeftCLM ℂ χ) φ) ⊆ Function.support ⇑φ

Multiplying a Schwartz function φ by a function χ (via SchwartzMap.smulLeftCLM) can only shrink the support: supp (χ · φ) ⊆ supp φ.

theorem DifferentialOperators.smulLeft_hasCompactSupport {n : ℕ} (χ : EuclideanSpace ℝ (Fin n) → ℂ) (u : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) (hu : HasCompactSupport u) : HasCompactSupport ((TemperedDistribution.smulLeftCLM ℂ χ) u)

If u has compact support, then so does the distribution χ · u obtained by left multiplication by an arbitrary function χ.

theorem DifferentialOperators.smulLeft_supported {n : ℕ} (χ : EuclideanSpace ℝ (Fin n) → ℂ) (u : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) (S : Set (EuclideanSpace ℝ (Fin n))) (hS : tsupport χ ⊆ S) (φ : SchwartzMap (EuclideanSpace ℝ (Fin n)) ℂ) : Function.support ⇑φ ∩ S = ∅ → ((TemperedDistribution.smulLeftCLM ℂ χ) u) φ = 0

If the support of the cutoff function χ is contained in S, then the distribution χ · u annihilates every Schwartz function whose support is disjoint from S.

theorem DifferentialOperators.smulLeft_smooth_of_vanishesOnSingSupp {n : ℕ} (χ : EuclideanSpace ℝ (Fin n) → ℂ) (u : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) (hχ : ContDiff ℝ (↑⊤) χ) (hχ_vanish : ∀ x ∈ singularSupport u, χ x = 0) (x₀ : EuclideanSpace ℝ (Fin n)) : isSmoothNear ((TemperedDistribution.smulLeftCLM ℂ χ) u) x₀

If a smooth function χ vanishes on the singular support of u, then the distribution χ · u is smooth near every point.

theorem DifferentialOperators.exists_smooth_bump_subset {n : ℕ} (F K : Set (EuclideanSpace ℝ (Fin n))) (hF : IsClosed F) (hK : IsCompact K) (hFK : F ⊆ interior K) : ∃ (χ : EuclideanSpace ℝ (Fin n) → ℂ), ContDiff ℝ (↑⊤) χ ∧ _root_.HasCompactSupport χ ∧ tsupport χ ⊆ K ∧ ∃ (V : Set (EuclideanSpace ℝ (Fin n))), IsOpen V ∧ F ⊆ V ∧ ∀ x ∈ V, χ x = 1

Existence of a smooth complex-valued bump function which equals 1 on a neighbourhood of a closed set F and is supported in a given compact superset K (with F ⊆ int K).

theorem DifferentialOperators.exists_smoothDecomp {n : ℕ} (u : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) (hu : HasCompactSupport u) (K : Set (EuclideanSpace ℝ (Fin n))) (hK : IsCompact K) (hK_contains : singularSupport u ⊆ interior K) : ∃ (d : SmoothDecomp u), d.supportSet ⊆ K

Existence of a SmoothDecomp of a compactly supported tempered distribution u into a singular part supported in any compact set K containing the singular support in its interior, plus a globally smooth, compactly supported remainder.

theorem DifferentialOperators.globally_smooth_has_global_representative {n : ℕ} (f : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) (hf : ∀ (x₀ : EuclideanSpace ℝ (Fin n)), isSmoothNear f x₀) : ∃ (g : EuclideanSpace ℝ (Fin n) → ℂ), ContDiff ℝ ⊤ g ∧ ∀ (φ : SchwartzMap (EuclideanSpace ℝ (Fin n)) ℂ), f φ = ∫ (y : EuclideanSpace ℝ (Fin n)), φ y • g y

If a tempered distribution f is smooth near every point, then it is globally represented by a single smooth function g: ⟨f, φ⟩ = ∫ φ(y) • g(y) dy.

theorem DifferentialOperators.distributional_fubini_compact_support {n : ℕ} (μ : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) (hμ : HasCompactSupport μ) (g : EuclideanSpace ℝ (Fin n) → ℂ) (hg : ContDiff ℝ ⊤ g) : ∃ (ψ : SchwartzMap (EuclideanSpace ℝ (Fin n)) ℂ), ContDiff ℝ ⊤ (tempDistSchwartzConv μ ψ) ∧ ∀ (φ : SchwartzMap (EuclideanSpace ℝ (Fin n)) ℂ), ∫ (y : EuclideanSpace ℝ (Fin n)), ((convolutionSchwartzCLM μ hμ) φ) y • g y = ∫ (y : EuclideanSpace ℝ (Fin n)), φ y • tempDistSchwartzConv μ ψ y

Distributional Fubini for the convolution μ * φ of a compactly supported μ with a Schwartz function φ, tested against a smooth function g: there is a Schwartz representative ψ whose μ-convolution tempDistSchwartzConv μ ψ realises the swap-of-order integral identity.

theorem DifferentialOperators.exists_smooth_convolution_representative {n : ℕ} (μ : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) (hμ : HasCompactSupport μ) (g : EuclideanSpace ℝ (Fin n) → ℂ) (hg : ContDiff ℝ ⊤ g) : ∃ (h : EuclideanSpace ℝ (Fin n) → ℂ), ContDiff ℝ ⊤ h ∧ ∀ (φ : SchwartzMap (EuclideanSpace ℝ (Fin n)) ℂ), ∫ (y : EuclideanSpace ℝ (Fin n)), ((convolutionSchwartzCLM μ hμ) φ) y • g y = ∫ (y : EuclideanSpace ℝ (Fin n)), φ y • h y

Given a compactly supported distribution μ and a smooth function g, there is a smooth function h realising the swap-of-order identity for the μ-convolution against g. Wrapper around distributional_fubini_compact_support.

theorem DifferentialOperators.distribConvolution_of_smooth_function_isSmoothNear {n : ℕ} (μ : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) (hμ : HasCompactSupport μ) (f : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) (g : EuclideanSpace ℝ (Fin n) → ℂ) (hg : ContDiff ℝ ⊤ g) (hfg : ∀ (φ : SchwartzMap (EuclideanSpace ℝ (Fin n)) ℂ), f φ = ∫ (y : EuclideanSpace ℝ (Fin n)), φ y • g y) (x₀ : EuclideanSpace ℝ (Fin n)) : isSmoothNear (distribConvolution μ f hμ) x₀

If the right factor f of a distributional convolution μ * f is represented by a smooth function g, then μ * f is smooth near every point.

theorem DifferentialOperators.isSmoothNear_distribConvolution_of_smooth_right {n : ℕ} (μ f : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) (hμ : HasCompactSupport μ) (hf_smooth : ∀ (x₀ : EuclideanSpace ℝ (Fin n)), isSmoothNear f x₀) (x₀ : EuclideanSpace ℝ (Fin n)) : isSmoothNear (distribConvolution μ f hμ) x₀

If the right factor f is globally smooth, then the distributional convolution μ * f is smooth near every point.

theorem DifferentialOperators.distribConvolution_of_smooth_left_function_isSmoothNear {n : ℕ} (μ : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) (hμ : HasCompactSupport μ) (g_μ : EuclideanSpace ℝ (Fin n) → ℂ) (hgμ : ContDiff ℝ ⊤ g_μ) (hμg : ∀ (φ : SchwartzMap (EuclideanSpace ℝ (Fin n)) ℂ), μ φ = ∫ (y : EuclideanSpace ℝ (Fin n)), φ y • g_μ y) (f : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) (x₀ : EuclideanSpace ℝ (Fin n)) : isSmoothNear (distribConvolution μ f hμ) x₀

If the left factor μ is represented by a smooth function g_μ, then the distributional convolution μ * f is smooth near every point.

theorem DifferentialOperators.isSmoothNear_distribConvolution_of_smooth_left {n : ℕ} (μ f : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) (hμ : HasCompactSupport μ) (hμ_smooth : ∀ (x₀ : EuclideanSpace ℝ (Fin n)), isSmoothNear μ x₀) (x₀ : EuclideanSpace ℝ (Fin n)) : isSmoothNear (distribConvolution μ f hμ) x₀

If the left factor μ is globally smooth, then the distributional convolution μ * f is smooth near every point.

theorem DifferentialOperators.distribConvolution_vanishesOn_compl {n : ℕ} (μ f : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) (hμ : HasCompactSupport μ) (K₁ K₂ : Set (EuclideanSpace ℝ (Fin n))) (hμK : ∀ (φ : SchwartzMap (EuclideanSpace ℝ (Fin n)) ℂ), Function.support ⇑φ ∩ K₁ = ∅ → μ φ = 0) (hfK : ∀ (φ : SchwartzMap (EuclideanSpace ℝ (Fin n)) ℂ), Function.support ⇑φ ∩ K₂ = ∅ → f φ = 0) : vanishesOn (distribConvolution μ f hμ) (K₁ + K₂)ᶜ

If μ is supported in K₁ and f is supported in K₂ (in the Schwartz-pairing sense), then distribConvolution μ f vanishes on the complement of the sum K₁ + K₂. This is the support property supp (μ * f) ⊆ supp μ + supp f.

theorem DifferentialOperators.isSmoothNear_of_vanishes_near {n : ℕ} (u : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) (p : EuclideanSpace ℝ (Fin n)) (U : Set (EuclideanSpace ℝ (Fin n))) (hU : IsOpen U) (hp : p ∈ U) (hv : vanishesOn u U) : isSmoothNear u p

If a distribution u vanishes on an open neighbourhood U of p, then it is smooth near p (with representative the zero function).

theorem DifferentialOperators.isSmoothNear_add {n : ℕ} (u₁ u₂ : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) (p : EuclideanSpace ℝ (Fin n)) (h₁ : isSmoothNear u₁ p) (h₂ : isSmoothNear u₂ p) : isSmoothNear (u₁ + u₂) p

The sum u₁ + u₂ of two tempered distributions is smooth near p whenever both summands are.

theorem DifferentialOperators.distribConvolution_add_left {n : ℕ} (μ₁ μ₂ f : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) (hμ₁ : HasCompactSupport μ₁) (hμ₂ : HasCompactSupport μ₂) (hμ : HasCompactSupport (μ₁ + μ₂)) : distribConvolution (μ₁ + μ₂) f hμ = distribConvolution μ₁ f hμ₁ + distribConvolution μ₂ f hμ₂

Additivity of distribConvolution in the left compactly-supported factor.

theorem DifferentialOperators.distribConvolution_add_right {n : ℕ} (μ f₁ f₂ : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) (hμ : HasCompactSupport μ) : distribConvolution μ (f₁ + f₂) hμ = distribConvolution μ f₁ hμ + distribConvolution μ f₂ hμ

Additivity of distribConvolution in the right factor.

theorem DifferentialOperators.exists_compact_neighborhood_disjoint_sum {n : ℕ} (K₁ K₂ : Set (EuclideanSpace ℝ (Fin n))) (hK₁ : IsCompact K₁) (hK₂ : IsCompact K₂) (p : EuclideanSpace ℝ (Fin n)) (hp : p ∉ K₁ + K₂) : ∃ (L₁ : Set (EuclideanSpace ℝ (Fin n))) (L₂ : Set (EuclideanSpace ℝ (Fin n))), IsCompact L₁ ∧ IsCompact L₂ ∧ K₁ ⊆ interior L₁ ∧ K₂ ⊆ interior L₂ ∧ p ∉ L₁ + L₂

Tube-lemma–style enlargement: given compact K₁, K₂ and a point p outside K₁ + K₂, there exist compact L₁, L₂ containing K₁, K₂ in their interiors with p ∉ L₁ + L₂.

theorem DifferentialOperators.hasCompactSupport_smulLeft_of_compactSupport_function {n : ℕ} (χ : EuclideanSpace ℝ (Fin n) → ℂ) (u : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) (hχ : _root_.HasCompactSupport χ) : HasCompactSupport ((TemperedDistribution.smulLeftCLM ℂ χ) u)

If the cutoff function χ is compactly supported, then χ · u is a compactly supported distribution for every tempered u.

theorem DifferentialOperators.singularSupport_smulLeft_subset {n : ℕ} (χ : EuclideanSpace ℝ (Fin n) → ℂ) (u : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) (hχ : ContDiff ℝ (↑⊤) χ) : singularSupport ((TemperedDistribution.smulLeftCLM ℂ χ) u) ⊆ singularSupport u

Multiplying a distribution u by a smooth function χ can only shrink the singular support: singsupp (χ · u) ⊆ singsupp u.

theorem DifferentialOperators.tsupport_one_sub_subset_compl {n : ℕ} (ψ : EuclideanSpace ℝ (Fin n) → ℂ) (V : Set (EuclideanSpace ℝ (Fin n))) (hV : IsOpen V) (hψ_one : ∀ x ∈ V, ψ x = 1) : tsupport (1 - ψ) ⊆ Vᶜ

If ψ equals 1 on an open set V, then the support of 1 - ψ is contained in the complement of V.

theorem DifferentialOperators.isClosed_compact_add_closed {n : ℕ} (K C : Set (EuclideanSpace ℝ (Fin n))) (hK : IsCompact K) (hC : IsClosed C) : IsClosed (K + C)

The Minkowski sum K + C of a compact set K and a closed set C in Euclidean space is closed.

theorem DifferentialOperators.distribConvolution_reduce_to_compact_support {n : ℕ} (μ f : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) (hμ : HasCompactSupport μ) (p : EuclideanSpace ℝ (Fin n)) (hp : p ∉ singularSupport μ + singularSupport f) : ∃ (f' : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ), HasCompactSupport f' ∧ singularSupport f' ⊆ singularSupport f ∧ (isSmoothNear (distribConvolution μ f' hμ) p → isSmoothNear (distribConvolution μ f hμ) p)

Reduction step: to check smoothness of distribConvolution μ f near a point p outside singsupp μ + singsupp f, one may replace f by a compactly supported distribution f' with smaller singular support whose convolution carries the same local smoothness information.

theorem DifferentialOperators.distribConvolution_four_term_expansion {n : ℕ} (μ₁ μ₂ f₁ f₂ : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) (hμ₁ : HasCompactSupport μ₁) (hμ₂ : HasCompactSupport μ₂) (hμ : HasCompactSupport (μ₁ + μ₂)) : distribConvolution (μ₁ + μ₂) (f₁ + f₂) hμ = distribConvolution μ₁ f₁ hμ₁ + distribConvolution μ₁ f₂ hμ₁ + (distribConvolution μ₂ f₁ hμ₂ + distribConvolution μ₂ f₂ hμ₂)

Bilinear expansion (μ₁ + μ₂) * (f₁ + f₂) = μ₁ * f₁ + μ₁ * f₂ + μ₂ * f₁ + μ₂ * f₂ for distributional convolution, used in the singular-support proof.

theorem DifferentialOperators.distribConvolution_congr {n : ℕ} {a a' b b' : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ} (ha_eq : a = a') (hb_eq : b = b') (ha : HasCompactSupport a) (ha' : HasCompactSupport a') : distribConvolution a b ha = distribConvolution a' b' ha'

Congruence: replacing the arguments of distribConvolution by equal distributions gives equal results, independent of the chosen compact-support witness.

theorem DifferentialOperators.singularSupport_convolution_subset {n : ℕ} (μ f : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) (hμ : HasCompactSupport μ) : singularSupport (distribConvolution μ f hμ) ⊆ singularSupport μ + singularSupport f

The singular support of a distributional convolution is contained in the Minkowski sum of the singular supports of the factors: singsupp (μ * f) ⊆ singsupp μ + singsupp f. This is the central property underlying pseudodifferential calculus (Melrose, Section 12).