The topological support of a function #
In this file we define the topological support of a function f, tsupport f,
as the closure of the support of f.
Furthermore, we say that f has compact support if the topological support of f is compact.
Main definitions #
function.mul_tsupport&function.tsupportfunction.has_compact_mul_support&function.has_compact_support
Implementation Notes #
- We write all lemmas for multiplicative functions, and use
@[to_additive]to get the more common additive versions. - We do not put the definitions in the
functionnamespace, following many other topological definitions that are in the root namespace (compareembeddingvsfunction.embedding).
The topological support of a function is the closure of its support. i.e. the closure of the set of all elements where the function is nonzero.
Equations
- tsupport f = closure (function.support f)
def
mul_tsupport
{X : Type u_1}
{α : Type u_2}
[has_one α]
[topological_space X]
(f : X → α) :
set X
The topological support of a function is the closure of its support, i.e. the closure of the set of all elements where the function is not equal to 1.
Equations
theorem
subset_mul_tsupport
{X : Type u_1}
{α : Type u_2}
[has_one α]
[topological_space X]
(f : X → α) :
theorem
subset_tsupport
{X : Type u_1}
{α : Type u_2}
[has_zero α]
[topological_space X]
(f : X → α) :
theorem
is_closed_mul_tsupport
{X : Type u_1}
{α : Type u_2}
[has_one α]
[topological_space X]
(f : X → α) :
theorem
is_closed_tsupport
{X : Type u_1}
{α : Type u_2}
[has_zero α]
[topological_space X]
(f : X → α) :
theorem
mul_tsupport_eq_empty_iff
{X : Type u_1}
{α : Type u_2}
[has_one α]
[topological_space X]
{f : X → α} :
mul_tsupport f = ∅ ↔ f = 1
theorem
tsupport_eq_empty_iff
{X : Type u_1}
{α : Type u_2}
[has_zero α]
[topological_space X]
{f : X → α} :
theorem
image_eq_zero_of_nmem_mul_tsupport
{X : Type u_1}
{α : Type u_2}
[has_one α]
[topological_space X]
{f : X → α}
{x : X}
(hx : x ∉ mul_tsupport f) :
f x = 1
theorem
image_eq_zero_of_nmem_tsupport
{X : Type u_1}
{α : Type u_2}
[has_zero α]
[topological_space X]
{f : X → α}
{x : X}
(hx : x ∉ tsupport f) :
f x = 0
theorem
not_mem_closure_mul_support_iff_eventually_eq
{α : Type u_2}
{β : Type u_4}
[topological_space α]
[has_one β]
{f : α → β}
{x : α} :
theorem
not_mem_closure_support_iff_eventually_eq
{α : Type u_2}
{β : Type u_4}
[topological_space α]
[has_zero β]
{f : α → β}
{x : α} :
def
has_compact_support
{α : Type u_2}
{β : Type u_4}
[topological_space α]
[has_zero β]
(f : α → β) :
Prop
A function f has compact support or is compactly supported if the closure of the support
of f is compact. In a T₂ space this is equivalent to f being equal to 0 outside a compact
set.
Equations
def
has_compact_mul_support
{α : Type u_2}
{β : Type u_4}
[topological_space α]
[has_one β]
(f : α → β) :
Prop
A function f has compact multiplicative support or is compactly supported if the closure
of the multiplicative support of f is compact. In a T₂ space this is equivalent to f being equal
to 1 outside a compact set.
Equations
theorem
has_compact_support_def
{α : Type u_2}
{β : Type u_4}
[topological_space α]
[has_zero β]
{f : α → β} :
theorem
has_compact_mul_support_def
{α : Type u_2}
{β : Type u_4}
[topological_space α]
[has_one β]
{f : α → β} :
theorem
exists_compact_iff_has_compact_support
{α : Type u_2}
{β : Type u_4}
[topological_space α]
[has_zero β]
{f : α → β}
[t2_space α] :
(∃ (K : set α), is_compact K ∧ ∀ (x : α), x ∉ K → f x = 0) ↔ has_compact_support f
theorem
exists_compact_iff_has_compact_mul_support
{α : Type u_2}
{β : Type u_4}
[topological_space α]
[has_one β]
{f : α → β}
[t2_space α] :
(∃ (K : set α), is_compact K ∧ ∀ (x : α), x ∉ K → f x = 1) ↔ has_compact_mul_support f
theorem
has_compact_support.intro
{α : Type u_2}
{β : Type u_4}
[topological_space α]
[has_zero β]
{f : α → β}
[t2_space α]
{K : set α}
(hK : is_compact K)
(hfK : ∀ (x : α), x ∉ K → f x = 0) :
theorem
has_compact_mul_support.intro
{α : Type u_2}
{β : Type u_4}
[topological_space α]
[has_one β]
{f : α → β}
[t2_space α]
{K : set α}
(hK : is_compact K)
(hfK : ∀ (x : α), x ∉ K → f x = 1) :
theorem
has_compact_support.is_compact
{α : Type u_2}
{β : Type u_4}
[topological_space α]
[has_zero β]
{f : α → β}
(hf : has_compact_support f) :
is_compact (tsupport f)
theorem
has_compact_mul_support.is_compact
{α : Type u_2}
{β : Type u_4}
[topological_space α]
[has_one β]
{f : α → β}
(hf : has_compact_mul_support f) :
theorem
has_compact_support_iff_eventually_eq
{α : Type u_2}
{β : Type u_4}
[topological_space α]
[has_zero β]
{f : α → β} :
theorem
has_compact_mul_support_iff_eventually_eq
{α : Type u_2}
{β : Type u_4}
[topological_space α]
[has_one β]
{f : α → β} :
theorem
has_compact_support.mono'
{α : Type u_2}
{β : Type u_4}
{γ : Type u_5}
[topological_space α]
[has_zero β]
[has_zero γ]
{f : α → β}
{f' : α → γ}
(hf : has_compact_support f)
(hff' : function.support f' ⊆ tsupport f) :
theorem
has_compact_mul_support.mono'
{α : Type u_2}
{β : Type u_4}
{γ : Type u_5}
[topological_space α]
[has_one β]
[has_one γ]
{f : α → β}
{f' : α → γ}
(hf : has_compact_mul_support f)
(hff' : function.mul_support f' ⊆ mul_tsupport f) :
theorem
has_compact_mul_support.mono
{α : Type u_2}
{β : Type u_4}
{γ : Type u_5}
[topological_space α]
[has_one β]
[has_one γ]
{f : α → β}
{f' : α → γ}
(hf : has_compact_mul_support f)
(hff' : function.mul_support f' ⊆ function.mul_support f) :
theorem
has_compact_support.mono
{α : Type u_2}
{β : Type u_4}
{γ : Type u_5}
[topological_space α]
[has_zero β]
[has_zero γ]
{f : α → β}
{f' : α → γ}
(hf : has_compact_support f)
(hff' : function.support f' ⊆ function.support f) :
theorem
has_compact_mul_support.comp_left
{α : Type u_2}
{β : Type u_4}
{γ : Type u_5}
[topological_space α]
[has_one β]
[has_one γ]
{g : β → γ}
{f : α → β}
(hf : has_compact_mul_support f)
(hg : g 1 = 1) :
has_compact_mul_support (g ∘ f)
theorem
has_compact_support.comp_left
{α : Type u_2}
{β : Type u_4}
{γ : Type u_5}
[topological_space α]
[has_zero β]
[has_zero γ]
{g : β → γ}
{f : α → β}
(hf : has_compact_support f)
(hg : g 0 = 0) :
has_compact_support (g ∘ f)
theorem
has_compact_support_comp_left
{α : Type u_2}
{β : Type u_4}
{γ : Type u_5}
[topological_space α]
[has_zero β]
[has_zero γ]
{g : β → γ}
{f : α → β}
(hg : ∀ {x : β}, g x = 0 ↔ x = 0) :
has_compact_support (g ∘ f) ↔ has_compact_support f
theorem
has_compact_mul_support_comp_left
{α : Type u_2}
{β : Type u_4}
{γ : Type u_5}
[topological_space α]
[has_one β]
[has_one γ]
{g : β → γ}
{f : α → β}
(hg : ∀ {x : β}, g x = 1 ↔ x = 1) :
theorem
has_compact_support.comp_closed_embedding
{α : Type u_2}
{α' : Type u_3}
{β : Type u_4}
[topological_space α]
[topological_space α']
[has_zero β]
{f : α → β}
(hf : has_compact_support f)
{g : α' → α}
(hg : closed_embedding g) :
has_compact_support (f ∘ g)
theorem
has_compact_mul_support.comp_closed_embedding
{α : Type u_2}
{α' : Type u_3}
{β : Type u_4}
[topological_space α]
[topological_space α']
[has_one β]
{f : α → β}
(hf : has_compact_mul_support f)
{g : α' → α}
(hg : closed_embedding g) :
has_compact_mul_support (f ∘ g)
theorem
has_compact_support.comp₂_left
{α : Type u_2}
{β : Type u_4}
{γ : Type u_5}
{δ : Type u_6}
[topological_space α]
[has_zero β]
[has_zero γ]
[has_zero δ]
{f : α → β}
{f₂ : α → γ}
{m : β → γ → δ}
(hf : has_compact_support f)
(hf₂ : has_compact_support f₂)
(hm : m 0 0 = 0) :
has_compact_support (λ (x : α), m (f x) (f₂ x))
theorem
has_compact_mul_support.comp₂_left
{α : Type u_2}
{β : Type u_4}
{γ : Type u_5}
{δ : Type u_6}
[topological_space α]
[has_one β]
[has_one γ]
[has_one δ]
{f : α → β}
{f₂ : α → γ}
{m : β → γ → δ}
(hf : has_compact_mul_support f)
(hf₂ : has_compact_mul_support f₂)
(hm : m 1 1 = 1) :
has_compact_mul_support (λ (x : α), m (f x) (f₂ x))
theorem
has_compact_support.add
{α : Type u_2}
{β : Type u_4}
[topological_space α]
[add_monoid β]
{f f' : α → β}
(hf : has_compact_support f)
(hf' : has_compact_support f') :
has_compact_support (f + f')
theorem
has_compact_mul_support.mul
{α : Type u_2}
{β : Type u_4}
[topological_space α]
[monoid β]
{f f' : α → β}
(hf : has_compact_mul_support f)
(hf' : has_compact_mul_support f') :
has_compact_mul_support (f * f')
theorem
has_compact_support.smul_left
{α : Type u_2}
{M : Type u_7}
{R : Type u_9}
[topological_space α]
[monoid_with_zero R]
[add_monoid M]
[distrib_mul_action R M]
{f : α → R}
{f' : α → M}
(hf : has_compact_support f') :
has_compact_support (f • f')
theorem
has_compact_support.smul_right
{α : Type u_2}
{M : Type u_7}
{R : Type u_9}
[topological_space α]
[has_zero R]
[has_zero M]
[smul_with_zero R M]
{f : α → R}
{f' : α → M}
(hf : has_compact_support f) :
has_compact_support (f • f')
theorem
has_compact_support.smul_left'
{α : Type u_2}
{M : Type u_7}
{R : Type u_9}
[topological_space α]
[has_zero R]
[has_zero M]
[smul_with_zero R M]
{f : α → R}
{f' : α → M}
(hf : has_compact_support f') :
has_compact_support (f • f')
theorem
has_compact_support.mul_right
{α : Type u_2}
{β : Type u_4}
[topological_space α]
[mul_zero_class β]
{f f' : α → β}
(hf : has_compact_support f) :
has_compact_support (f * f')
theorem
has_compact_support.mul_left
{α : Type u_2}
{β : Type u_4}
[topological_space α]
[mul_zero_class β]
{f f' : α → β}
(hf : has_compact_support f') :
has_compact_support (f * f')
theorem
locally_finite.exists_finset_nhd_mul_support_subset
{X : Type u_1}
{R : Type u_9}
{ι : Type u_10}
{U : ι → set X}
[topological_space X]
[has_one R]
{f : ι → X → R}
(hlf : locally_finite (λ (i : ι), function.mul_support (f i)))
(hso : ∀ (i : ι), mul_tsupport (f i) ⊆ U i)
(ho : ∀ (i : ι), is_open (U i))
(x : X) :
If a family of functions f has locally-finite multiplicative support, subordinate to a family
of open sets, then for any point we can find a neighbourhood on which only finitely-many members of
f are not equal to 1.
theorem
locally_finite.exists_finset_nhd_support_subset
{X : Type u_1}
{R : Type u_9}
{ι : Type u_10}
{U : ι → set X}
[topological_space X]
[has_zero R]
{f : ι → X → R}
(hlf : locally_finite (λ (i : ι), function.support (f i)))
(hso : ∀ (i : ι), tsupport (f i) ⊆ U i)
(ho : ∀ (i : ι), is_open (U i))
(x : X) :
If a family of functions f has locally-finite support, subordinate to a family of open sets,
then for any point we can find a neighbourhood on which only finitely-many members of f are
non-zero.