Support of distributions

We define the support of a distribution, dsupport u, as the intersection of all closed sets for which u vanishes on the complement. For this we also define a predicate IsVanishingOn that asserts that a map f : F → V vanishes on s : Set α if for all u : F with tsupport u ⊆ s it follows that f u = 0.

These definitions work independently of a specific class of distributions (classical, tempered, or compactly supported) and all basic properties are proved in an abstract setting using FunLike.

Main definitions

• IsVanishingOn: A distribution vanishes on a set if it acts trivially on all test functions supported in that subset.
• dsupport: The support of a distribution is the intersection of all closed sets for which that distribution vanishes on the complement of the set.

Main statements

• TemperedDistribution.dsupport_delta: The support of the delta distribution is a single point.

Vanishing of distributions

def Distribution.IsVanishingOn {α : Type u_2} {β : Type u_3} {F : Type u_6} {V : Type u_10} [FunLike F α β] [TopologicalSpace α] [Zero β] [Zero V] (f : F → V) (s : Set α) : Prop

A distribution f vanishes on a set s if it vanishes for all test functions u with tsupport u ⊆ s.

To make this definition work for all types of distributions, we define it for any function from a FunLike type to a type with zero.

theorem Distribution.IsVanishingOn.mono {α : Type u_2} {β : Type u_3} {F : Type u_6} {V : Type u_10} [FunLike F α β] [TopologicalSpace α] [Zero β] {f : F → V} [Zero V] ⦃s₁ s₂ : Set α⦄ (hs : s₂ ⊆ s₁) (hf : IsVanishingOn f s₁) : IsVanishingOn f s₂

theorem Distribution.not_isVanishingOn_mono {α : Type u_2} {β : Type u_3} {F : Type u_6} {V : Type u_10} [FunLike F α β] [TopologicalSpace α] [Zero β] {f : F → V} [Zero V] ⦃s₁ s₂ : Set α⦄ (hs : s₁ ⊆ s₂) (hf : ¬IsVanishingOn f s₁) : ¬IsVanishingOn f s₂

theorem Distribution.not_isVanishingOn_iff {α : Type u_2} {β : Type u_3} {F : Type u_6} {V : Type u_10} [FunLike F α β] [TopologicalSpace α] [Zero β] {f : F → V} {s : Set α} [Zero V] : ¬IsVanishingOn f s ↔ ∃ (u : F), tsupport ⇑u ⊆ s ∧ f u ≠ 0

Support

def Distribution.dsupport {α : Type u_2} {β : Type u_3} {F : Type u_6} {V : Type u_10} [FunLike F α β] [TopologicalSpace α] [Zero β] [Zero V] (f : F → V) : Set α

The distributional support of f is the intersection of all closed sets s such that f vanishes on the complement of s.

To make this definition work for all types of distributions, we define it for any function from a FunLike type to a type with zero.

theorem Distribution.mem_dsupport_iff {α : Type u_2} {β : Type u_3} {F : Type u_6} {V : Type u_10} [FunLike F α β] [TopologicalSpace α] [Zero β] [Zero V] {f : F → V} (x : α) : x ∈ dsupport f ↔ ∀ (s : Set α), IsVanishingOn f sᶜ → IsClosed s → x ∈ s

theorem Distribution.dsupport_compl_eq {α : Type u_2} {β : Type u_3} {F : Type u_6} {V : Type u_10} [FunLike F α β] [TopologicalSpace α] [Zero β] [Zero V] {f : F → V} : (dsupport f)ᶜ = ⋃₀ {a : Set α | IsVanishingOn f a ∧ IsOpen a}

The complement of the support is the largest open set on which f vanishes.

@[simp]

theorem Distribution.notMem_dsupport_iff {α : Type u_2} {β : Type u_3} {F : Type u_6} {V : Type u_10} [FunLike F α β] [TopologicalSpace α] [Zero β] [Zero V] {f : F → V} (x : α) : x ∉ dsupport f ↔ ∃ (s : Set α), IsVanishingOn f s ∧ IsOpen s ∧ x ∈ s

theorem Distribution.mem_dsupport_iff_not_isVanishingOn {α : Type u_2} {β : Type u_3} {F : Type u_6} {V : Type u_10} [FunLike F α β] [TopologicalSpace α] [Zero β] [Zero V] {f : F → V} (x : α) : x ∈ dsupport f ↔ ∀ (s : Set α), x ∈ s → IsOpen s → ¬IsVanishingOn f s

theorem Distribution.mem_dsupport_iff_forall_exists_ne {α : Type u_2} {β : Type u_3} {F : Type u_6} {V : Type u_10} [FunLike F α β] [TopologicalSpace α] [Zero β] [Zero V] {f : F → V} (x : α) : x ∈ dsupport f ↔ ∀ (s : Set α), x ∈ s → IsOpen s → ∃ (u : F), tsupport ⇑u ⊆ s ∧ f u ≠ 0

theorem Distribution.mem_dsupport_iff_frequently {α : Type u_2} {β : Type u_3} {F : Type u_6} {V : Type u_10} [FunLike F α β] [TopologicalSpace α] [Zero β] [Zero V] {f : F → V} {x : α} : x ∈ dsupport f ↔ ∃ᶠ (u : Set α) in (nhds x).smallSets, ¬IsVanishingOn f u

theorem Filter.HasBasis.mem_dsupport {α : Type u_2} {β : Type u_3} {F : Type u_6} {V : Type u_10} [FunLike F α β] [TopologicalSpace α] [Zero β] [Zero V] {f : F → V} {ι : Sort u_11} {p : ι → Prop} {s : ι → Set α} {x : α} (hl : (nhds x).HasBasis p s) : x ∈ Distribution.dsupport f ↔ ∀ (i : ι), p i → ¬Distribution.IsVanishingOn f (s i)

theorem Distribution.notMem_dsupport_iff_eventually {α : Type u_2} {β : Type u_3} {F : Type u_6} {V : Type u_10} [FunLike F α β] [TopologicalSpace α] [Zero β] [Zero V] {f : F → V} {x : α} : x ∉ dsupport f ↔ ∀ᶠ (u : Set α) in (nhds x).smallSets, IsVanishingOn f u

theorem Filter.HasBasis.notMem_dsupport {α : Type u_2} {β : Type u_3} {F : Type u_6} {V : Type u_10} [FunLike F α β] [TopologicalSpace α] [Zero β] [Zero V] {f : F → V} {ι : Sort u_11} {p : ι → Prop} {s : ι → Set α} {x : α} (hl : (nhds x).HasBasis p s) : x ∉ Distribution.dsupport f ↔ ∃ (i : ι), p i ∧ Distribution.IsVanishingOn f (s i)

theorem Distribution.dsupport_subset_dsupport {α : Type u_2} {β : Type u_3} {F : Type u_6} {V : Type u_10} [FunLike F α β] [TopologicalSpace α] [Zero β] [Zero V] {f g : F → V} (h : ∀ (s : Set α), IsOpen s → IsVanishingOn g s → IsVanishingOn f s) : dsupport f ⊆ dsupport g

theorem Distribution.isClosed_dsupport {α : Type u_2} {β : Type u_3} {F : Type u_6} {V : Type u_10} [FunLike F α β] [TopologicalSpace α] [Zero β] [Zero V] {f : F → V} : IsClosed (dsupport f)

theorem Distribution.IsVanishingOn.disjoint_dsupport {α : Type u_2} {β : Type u_3} {F : Type u_6} {V : Type u_10} [FunLike F α β] [TopologicalSpace α] [Zero β] [Zero V] {f : F → V} {s : Set α} (h : IsVanishingOn f s) (s_open : IsOpen s) : Disjoint s (dsupport f)

theorem Distribution.compl_dsupport_eq_sUnion_isBounded {α : Type u_2} {β : Type u_3} {F : Type u_6} {V : Type u_10} [FunLike F α β] [PseudoMetricSpace α] [Zero β] [Zero V] {f : F → V} : (dsupport f)ᶜ = ⋃₀ {a : Set α | IsVanishingOn f a ∧ IsOpen a ∧ Bornology.IsBounded a}

The complement of the support is given by all bounded open sets on which f vanishes.

Tempered distributions

theorem Distribution.IsVanishingOn.smulLeftCLM {E : Type u_5} {F : Type u_6} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace ℂ F] {f : TemperedDistribution E F} {s : Set E} (hf : IsVanishingOn (⇑f) s) {g : E → ℂ} (hg : Function.HasTemperateGrowth g) : IsVanishingOn (⇑((TemperedDistribution.smulLeftCLM F g) f)) s

theorem Distribution.IsVanishingOn.lineDerivOp {E : Type u_5} {F : Type u_6} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace ℂ F] {f : TemperedDistribution E F} {s : Set E} (hf : IsVanishingOn (⇑f) s) (m : E) : IsVanishingOn (⇑(LineDeriv.lineDerivOp m f)) s

theorem Distribution.IsVanishingOn.iteratedLineDerivOp {E : Type u_5} {F : Type u_6} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace ℂ F] {f : TemperedDistribution E F} {s : Set E} {n : ℕ} (hf : IsVanishingOn (⇑f) s) (m : Fin n → E) : IsVanishingOn (⇑(LineDeriv.iteratedLineDerivOp m f)) s

theorem TemperedDistribution.isVanishingOn_delta {E : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] (x : E) : Distribution.IsVanishingOn ⇑(delta x) {x}ᶜ

theorem Distribution.dsupport_smulLeftCLM_subset {E : Type u_5} {F : Type u_6} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace ℂ F] {f : TemperedDistribution E F} {g : E → ℂ} (hg : Function.HasTemperateGrowth g) : dsupport ⇑((TemperedDistribution.smulLeftCLM F g) f) ⊆ dsupport ⇑f

theorem Distribution.dsupport_lineDerivOp_subset {E : Type u_5} {F : Type u_6} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace ℂ F] {f : TemperedDistribution E F} (m : E) : dsupport ⇑(LineDeriv.lineDerivOp m f) ⊆ dsupport ⇑f

theorem Distribution.dsupport_iteratedLineDerivOp_subset {E : Type u_5} {F : Type u_6} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace ℂ F] {f : TemperedDistribution E F} {n : ℕ} (m : Fin n → E) : dsupport ⇑(LineDeriv.iteratedLineDerivOp m f) ⊆ dsupport ⇑f

theorem Distribution.dsupport_delta {E : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (x : E) : dsupport ⇑(TemperedDistribution.delta x) = {x}