def Distribution.IsSmoothOn' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasureTheory.MeasureSpace E] (u : TemperedDistribution E ℂ) (s : Set E) : Prop

A tempered distribution u is smooth on the set s iff its action on test functions supported in s is given by integration against a globally smooth function g.

def Distribution.singSupp {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasureTheory.MeasureSpace E] (u : TemperedDistribution E ℂ) : Set E

The singular support of a tempered distribution u: the complement of the largest open set on which u is smooth.

theorem Distribution.singSupp_compl_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasureTheory.MeasureSpace E] [BorelSpace E] {u : TemperedDistribution E ℂ} : (singSupp u)ᶜ = ⋃₀ {s : Set E | IsOpen s ∧ IsSmoothOn' u s}

The complement of the singular support equals the union of all open sets on which u is smooth.

theorem Distribution.notMem_singSupp_iff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasureTheory.MeasureSpace E] [BorelSpace E] {u : TemperedDistribution E ℂ} {x : E} : x ∉ singSupp u ↔ ∃ (s : Set E), IsOpen s ∧ IsSmoothOn' u s ∧ x ∈ s

A point x is not in the singular support iff there exists an open neighborhood of x on which u is smooth.