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

• mulTSupport & tsupport
• HasCompactMulSupport & HasCompactSupport

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 Function namespace, following many other topological definitions that are in the root namespace (compare Embedding vs Function.Embedding).

def tsupport {X : Type u_1} {α : Type u_2} [Zero α] [TopologicalSpace 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 nonzero.

Equations

• tsupport f = closure (Function.support f)

def mulTSupport {X : Type u_1} {α : Type u_2} [One α] [TopologicalSpace 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

• mulTSupport f = closure (Function.mulSupport f)

theorem subset_tsupport {X : Type u_1} {α : Type u_2} [Zero α] [TopologicalSpace X] (f : X → α) : Function.support f ⊆ tsupport f

theorem subset_mulTSupport {X : Type u_1} {α : Type u_2} [One α] [TopologicalSpace X] (f : X → α) : Function.mulSupport f ⊆ mulTSupport f

theorem isClosed_tsupport {X : Type u_1} {α : Type u_2} [Zero α] [TopologicalSpace X] (f : X → α) : IsClosed (tsupport f)

theorem isClosed_mulTSupport {X : Type u_1} {α : Type u_2} [One α] [TopologicalSpace X] (f : X → α) : IsClosed (mulTSupport f)

theorem tsupport_eq_empty_iff {X : Type u_1} {α : Type u_2} [Zero α] [TopologicalSpace X] {f : X → α} : tsupport f = ∅ ↔ f = 0

theorem mulTSupport_eq_empty_iff {X : Type u_1} {α : Type u_2} [One α] [TopologicalSpace X] {f : X → α} : mulTSupport f = ∅ ↔ f = 1

theorem image_eq_zero_of_nmem_tsupport {X : Type u_1} {α : Type u_2} [Zero α] [TopologicalSpace X] {f : X → α} {x : X} (hx : x ∉ tsupport f) : f x = 0

theorem image_eq_one_of_nmem_mulTSupport {X : Type u_1} {α : Type u_2} [One α] [TopologicalSpace X] {f : X → α} {x : X} (hx : x ∉ mulTSupport f) : f x = 1

theorem range_subset_insert_image_tsupport {X : Type u_1} {α : Type u_2} [Zero α] [TopologicalSpace X] (f : X → α) : Set.range f ⊆ insert 0 (f '' tsupport f)

theorem range_subset_insert_image_mulTSupport {X : Type u_1} {α : Type u_2} [One α] [TopologicalSpace X] (f : X → α) : Set.range f ⊆ insert 1 (f '' mulTSupport f)

theorem range_eq_image_tsupport_or {X : Type u_1} {α : Type u_2} [Zero α] [TopologicalSpace X] (f : X → α) : Set.range f = f '' tsupport f ∨ Set.range f = insert 0 (f '' tsupport f)

theorem range_eq_image_mulTSupport_or {X : Type u_1} {α : Type u_2} [One α] [TopologicalSpace X] (f : X → α) : Set.range f = f '' mulTSupport f ∨ Set.range f = insert 1 (f '' mulTSupport f)

theorem tsupport_mul_subset_left {X : Type u_1} [TopologicalSpace X] {α : Type u_10} [MulZeroClass α] {f : X → α} {g : X → α} : (tsupport fun (x : X) => f x * g x) ⊆ tsupport f

theorem tsupport_mul_subset_right {X : Type u_1} [TopologicalSpace X] {α : Type u_10} [MulZeroClass α] {f : X → α} {g : X → α} : (tsupport fun (x : X) => f x * g x) ⊆ tsupport g

theorem tsupport_smul_subset_left {X : Type u_1} {M : Type u_10} {α : Type u_11} [TopologicalSpace X] [Zero M] [Zero α] [SMulWithZero M α] (f : X → M) (g : X → α) : (tsupport fun (x : X) => f x • g x) ⊆ tsupport f

theorem tsupport_smul_subset_right {X : Type u_1} {M : Type u_10} {α : Type u_11} [TopologicalSpace X] [Zero α] [SMulZeroClass M α] (f : X → M) (g : X → α) : (tsupport fun (x : X) => f x • g x) ⊆ tsupport g

theorem tsupport_add {X : Type u_1} {α : Type u_2} [TopologicalSpace X] [AddMonoid α] {f : X → α} {g : X → α} : (tsupport fun (x : X) => f x + g x) ⊆ tsupport f ∪ tsupport g

theorem mulTSupport_mul {X : Type u_1} {α : Type u_2} [TopologicalSpace X] [Monoid α] {f : X → α} {g : X → α} : (mulTSupport fun (x : X) => f x * g x) ⊆ mulTSupport f ∪ mulTSupport g

theorem not_mem_tsupport_iff_eventuallyEq {α : Type u_2} {β : Type u_4} [TopologicalSpace α] [Zero β] {f : α → β} {x : α} : x ∉ tsupport f ↔ f =ᶠ[nhds x] 0

theorem not_mem_mulTSupport_iff_eventuallyEq {α : Type u_2} {β : Type u_4} [TopologicalSpace α] [One β] {f : α → β} {x : α} : x ∉ mulTSupport f ↔ f =ᶠ[nhds x] 1

theorem continuous_of_tsupport {α : Type u_2} {β : Type u_4} [TopologicalSpace α] [Zero β] [TopologicalSpace β] {f : α → β} (hf : ∀ x ∈ tsupport f, ContinuousAt f x) : Continuous f

theorem continuous_of_mulTSupport {α : Type u_2} {β : Type u_4} [TopologicalSpace α] [One β] [TopologicalSpace β] {f : α → β} (hf : ∀ x ∈ mulTSupport f, ContinuousAt f x) : Continuous f

Functions with compact support

def HasCompactSupport {α : Type u_2} {β : Type u_4} [TopologicalSpace α] [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

• HasCompactSupport f = IsCompact (tsupport f)

def HasCompactMulSupport {α : Type u_2} {β : Type u_4} [TopologicalSpace α] [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

• HasCompactMulSupport f = IsCompact (mulTSupport f)

theorem hasCompactSupport_def {α : Type u_2} {β : Type u_4} [TopologicalSpace α] [Zero β] {f : α → β} : HasCompactSupport f ↔ IsCompact (closure (Function.support f))

theorem hasCompactMulSupport_def {α : Type u_2} {β : Type u_4} [TopologicalSpace α] [One β] {f : α → β} : HasCompactMulSupport f ↔ IsCompact (closure (Function.mulSupport f))

theorem exists_compact_iff_hasCompactSupport {α : Type u_2} {β : Type u_4} [TopologicalSpace α] [Zero β] {f : α → β} [R1Space α] : (∃ (K : Set α), IsCompact K ∧ ∀ x ∉ K, f x = 0) ↔ HasCompactSupport f

theorem exists_compact_iff_hasCompactMulSupport {α : Type u_2} {β : Type u_4} [TopologicalSpace α] [One β] {f : α → β} [R1Space α] : (∃ (K : Set α), IsCompact K ∧ ∀ x ∉ K, f x = 1) ↔ HasCompactMulSupport f

theorem HasCompactSupport.intro {α : Type u_2} {β : Type u_4} [TopologicalSpace α] [Zero β] {f : α → β} [R1Space α] {K : Set α} (hK : IsCompact K) (hfK : ∀ x ∉ K, f x = 0) : HasCompactSupport f

theorem HasCompactMulSupport.intro {α : Type u_2} {β : Type u_4} [TopologicalSpace α] [One β] {f : α → β} [R1Space α] {K : Set α} (hK : IsCompact K) (hfK : ∀ x ∉ K, f x = 1) : HasCompactMulSupport f

theorem HasCompactSupport.intro' {α : Type u_2} {β : Type u_4} [TopologicalSpace α] [Zero β] {f : α → β} {K : Set α} (hK : IsCompact K) (h'K : IsClosed K) (hfK : ∀ x ∉ K, f x = 0) : HasCompactSupport f

theorem HasCompactMulSupport.intro' {α : Type u_2} {β : Type u_4} [TopologicalSpace α] [One β] {f : α → β} {K : Set α} (hK : IsCompact K) (h'K : IsClosed K) (hfK : ∀ x ∉ K, f x = 1) : HasCompactMulSupport f

theorem HasCompactSupport.of_support_subset_isCompact {α : Type u_2} {β : Type u_4} [TopologicalSpace α] [Zero β] {f : α → β} [R1Space α] {K : Set α} (hK : IsCompact K) (h : Function.support f ⊆ K) : HasCompactSupport f

theorem HasCompactMulSupport.of_mulSupport_subset_isCompact {α : Type u_2} {β : Type u_4} [TopologicalSpace α] [One β] {f : α → β} [R1Space α] {K : Set α} (hK : IsCompact K) (h : Function.mulSupport f ⊆ K) : HasCompactMulSupport f

theorem HasCompactSupport.isCompact {α : Type u_2} {β : Type u_4} [TopologicalSpace α] [Zero β] {f : α → β} (hf : HasCompactSupport f) : IsCompact (tsupport f)

theorem HasCompactMulSupport.isCompact {α : Type u_2} {β : Type u_4} [TopologicalSpace α] [One β] {f : α → β} (hf : HasCompactMulSupport f) : IsCompact (mulTSupport f)

theorem hasCompactSupport_iff_eventuallyEq {α : Type u_2} {β : Type u_4} [TopologicalSpace α] [Zero β] {f : α → β} : HasCompactSupport f ↔ f =ᶠ[Filter.coclosedCompact α] 0

theorem hasCompactMulSupport_iff_eventuallyEq {α : Type u_2} {β : Type u_4} [TopologicalSpace α] [One β] {f : α → β} : HasCompactMulSupport f ↔ f =ᶠ[Filter.coclosedCompact α] 1

theorem isCompact_range_of_support_subset_isCompact {α : Type u_2} {β : Type u_4} [TopologicalSpace α] [Zero β] {f : α → β} [TopologicalSpace β] (hf : Continuous f) {k : Set α} (hk : IsCompact k) (h'f : Function.support f ⊆ k) : IsCompact (Set.range f)

theorem isCompact_range_of_mulSupport_subset_isCompact {α : Type u_2} {β : Type u_4} [TopologicalSpace α] [One β] {f : α → β} [TopologicalSpace β] (hf : Continuous f) {k : Set α} (hk : IsCompact k) (h'f : Function.mulSupport f ⊆ k) : IsCompact (Set.range f)

theorem HasCompactSupport.isCompact_range {α : Type u_2} {β : Type u_4} [TopologicalSpace α] [Zero β] {f : α → β} [TopologicalSpace β] (h : HasCompactSupport f) (hf : Continuous f) : IsCompact (Set.range f)

theorem HasCompactMulSupport.isCompact_range {α : Type u_2} {β : Type u_4} [TopologicalSpace α] [One β] {f : α → β} [TopologicalSpace β] (h : HasCompactMulSupport f) (hf : Continuous f) : IsCompact (Set.range f)

theorem HasCompactSupport.mono' {α : Type u_2} {β : Type u_4} {γ : Type u_5} [TopologicalSpace α] [Zero β] [Zero γ] {f : α → β} {f' : α → γ} (hf : HasCompactSupport f) (hff' : Function.support f' ⊆ tsupport f) : HasCompactSupport f'

theorem HasCompactMulSupport.mono' {α : Type u_2} {β : Type u_4} {γ : Type u_5} [TopologicalSpace α] [One β] [One γ] {f : α → β} {f' : α → γ} (hf : HasCompactMulSupport f) (hff' : Function.mulSupport f' ⊆ mulTSupport f) : HasCompactMulSupport f'

theorem HasCompactSupport.mono {α : Type u_2} {β : Type u_4} {γ : Type u_5} [TopologicalSpace α] [Zero β] [Zero γ] {f : α → β} {f' : α → γ} (hf : HasCompactSupport f) (hff' : Function.support f' ⊆ Function.support f) : HasCompactSupport f'

theorem HasCompactMulSupport.mono {α : Type u_2} {β : Type u_4} {γ : Type u_5} [TopologicalSpace α] [One β] [One γ] {f : α → β} {f' : α → γ} (hf : HasCompactMulSupport f) (hff' : Function.mulSupport f' ⊆ Function.mulSupport f) : HasCompactMulSupport f'

theorem HasCompactSupport.comp_left {α : Type u_2} {β : Type u_4} {γ : Type u_5} [TopologicalSpace α] [Zero β] [Zero γ] {g : β → γ} {f : α → β} (hf : HasCompactSupport f) (hg : g 0 = 0) : HasCompactSupport (g ∘ f)

theorem HasCompactMulSupport.comp_left {α : Type u_2} {β : Type u_4} {γ : Type u_5} [TopologicalSpace α] [One β] [One γ] {g : β → γ} {f : α → β} (hf : HasCompactMulSupport f) (hg : g 1 = 1) : HasCompactMulSupport (g ∘ f)

theorem hasCompactSupport_comp_left {α : Type u_2} {β : Type u_4} {γ : Type u_5} [TopologicalSpace α] [Zero β] [Zero γ] {g : β → γ} {f : α → β} (hg : ∀ {x : β}, g x = 0 ↔ x = 0) : HasCompactSupport (g ∘ f) ↔ HasCompactSupport f

theorem hasCompactMulSupport_comp_left {α : Type u_2} {β : Type u_4} {γ : Type u_5} [TopologicalSpace α] [One β] [One γ] {g : β → γ} {f : α → β} (hg : ∀ {x : β}, g x = 1 ↔ x = 1) : HasCompactMulSupport (g ∘ f) ↔ HasCompactMulSupport f

theorem HasCompactSupport.comp_closedEmbedding {α : Type u_2} {α' : Type u_3} {β : Type u_4} [TopologicalSpace α] [TopologicalSpace α'] [Zero β] {f : α → β} (hf : HasCompactSupport f) {g : α' → α} (hg : ClosedEmbedding g) : HasCompactSupport (f ∘ g)

theorem HasCompactMulSupport.comp_closedEmbedding {α : Type u_2} {α' : Type u_3} {β : Type u_4} [TopologicalSpace α] [TopologicalSpace α'] [One β] {f : α → β} (hf : HasCompactMulSupport f) {g : α' → α} (hg : ClosedEmbedding g) : HasCompactMulSupport (f ∘ g)

theorem HasCompactSupport.comp₂_left {α : Type u_2} {β : Type u_4} {γ : Type u_5} {δ : Type u_6} [TopologicalSpace α] [Zero β] [Zero γ] [Zero δ] {f : α → β} {f₂ : α → γ} {m : β → γ → δ} (hf : HasCompactSupport f) (hf₂ : HasCompactSupport f₂) (hm : m 0 0 = 0) : HasCompactSupport fun (x : α) => m (f x) (f₂ x)

theorem HasCompactMulSupport.comp₂_left {α : Type u_2} {β : Type u_4} {γ : Type u_5} {δ : Type u_6} [TopologicalSpace α] [One β] [One γ] [One δ] {f : α → β} {f₂ : α → γ} {m : β → γ → δ} (hf : HasCompactMulSupport f) (hf₂ : HasCompactMulSupport f₂) (hm : m 1 1 = 1) : HasCompactMulSupport fun (x : α) => m (f x) (f₂ x)

theorem HasCompactSupport.isCompact_preimage {α : Type u_2} {β : Type u_4} [TopologicalSpace α] [Zero β] {f : α → β} [TopologicalSpace β] (h'f : HasCompactSupport f) (hf : Continuous f) {k : Set β} (hk : IsClosed k) (h'k : 0 ∉ k) : IsCompact (f ⁻¹' k)

theorem HasCompactMulSupport.isCompact_preimage {α : Type u_2} {β : Type u_4} [TopologicalSpace α] [One β] {f : α → β} [TopologicalSpace β] (h'f : HasCompactMulSupport f) (hf : Continuous f) {k : Set β} (hk : IsClosed k) (h'k : 1 ∉ k) : IsCompact (f ⁻¹' k)

theorem HasCompactSupport.tsupport_extend_zero_subset {α : Type u_2} {α' : Type u_3} {β : Type u_4} [TopologicalSpace α] [TopologicalSpace α'] [Zero β] {f : α → β} [T2Space α'] (hf : HasCompactSupport f) {g : α → α'} (cont : Continuous g) : tsupport (Function.extend g f 0) ⊆ g '' tsupport f

theorem HasCompactMulSupport.mulTSupport_extend_one_subset {α : Type u_2} {α' : Type u_3} {β : Type u_4} [TopologicalSpace α] [TopologicalSpace α'] [One β] {f : α → β} [T2Space α'] (hf : HasCompactMulSupport f) {g : α → α'} (cont : Continuous g) : mulTSupport (Function.extend g f 1) ⊆ g '' mulTSupport f

theorem HasCompactSupport.extend_zero {α : Type u_2} {α' : Type u_3} {β : Type u_4} [TopologicalSpace α] [TopologicalSpace α'] [Zero β] {f : α → β} [T2Space α'] (hf : HasCompactSupport f) {g : α → α'} (cont : Continuous g) : HasCompactSupport (Function.extend g f 0)

theorem HasCompactMulSupport.extend_one {α : Type u_2} {α' : Type u_3} {β : Type u_4} [TopologicalSpace α] [TopologicalSpace α'] [One β] {f : α → β} [T2Space α'] (hf : HasCompactMulSupport f) {g : α → α'} (cont : Continuous g) : HasCompactMulSupport (Function.extend g f 1)

theorem HasCompactSupport.tsupport_extend_zero {α : Type u_2} {α' : Type u_3} {β : Type u_4} [TopologicalSpace α] [TopologicalSpace α'] [Zero β] {f : α → β} [T2Space α'] (hf : HasCompactSupport f) {g : α → α'} (cont : Continuous g) (inj : Function.Injective g) : tsupport (Function.extend g f 0) = g '' tsupport f

theorem HasCompactMulSupport.mulTSupport_extend_one {α : Type u_2} {α' : Type u_3} {β : Type u_4} [TopologicalSpace α] [TopologicalSpace α'] [One β] {f : α → β} [T2Space α'] (hf : HasCompactMulSupport f) {g : α → α'} (cont : Continuous g) (inj : Function.Injective g) : mulTSupport (Function.extend g f 1) = g '' mulTSupport f

theorem HasCompactSupport.continuous_extend_zero {α' : Type u_3} {β : Type u_4} [TopologicalSpace α'] [Zero β] [T2Space α'] [TopologicalSpace β] {U : Set α'} (hU : IsOpen U) {f : ↑U → β} (cont : Continuous f) (supp : HasCompactSupport f) : Continuous (Function.extend Subtype.val f 0)

theorem HasCompactMulSupport.continuous_extend_one {α' : Type u_3} {β : Type u_4} [TopologicalSpace α'] [One β] [T2Space α'] [TopologicalSpace β] {U : Set α'} (hU : IsOpen U) {f : ↑U → β} (cont : Continuous f) (supp : HasCompactMulSupport f) : Continuous (Function.extend Subtype.val f 1)

Functions with compact support: algebraic operations

theorem HasCompactSupport.add {α : Type u_2} {β : Type u_4} [TopologicalSpace α] [AddMonoid β] {f : α → β} {f' : α → β} (hf : HasCompactSupport f) (hf' : HasCompactSupport f') : HasCompactSupport (f + f')

theorem HasCompactMulSupport.mul {α : Type u_2} {β : Type u_4} [TopologicalSpace α] [Monoid β] {f : α → β} {f' : α → β} (hf : HasCompactMulSupport f) (hf' : HasCompactMulSupport f') : HasCompactMulSupport (f * f')

theorem HasCompactSupport.smul_left {α : Type u_2} {M : Type u_7} {R : Type u_9} [TopologicalSpace α] [MonoidWithZero R] [AddMonoid M] [DistribMulAction R M] {f : α → R} {f' : α → M} (hf : HasCompactSupport f') : HasCompactSupport (f • f')

theorem HasCompactSupport.smul_right {α : Type u_2} {M : Type u_7} {R : Type u_9} [TopologicalSpace α] [Zero R] [Zero M] [SMulWithZero R M] {f : α → R} {f' : α → M} (hf : HasCompactSupport f) : HasCompactSupport (f • f')

theorem HasCompactSupport.smul_left' {α : Type u_2} {M : Type u_7} {R : Type u_9} [TopologicalSpace α] [Zero R] [Zero M] [SMulWithZero R M] {f : α → R} {f' : α → M} (hf : HasCompactSupport f') : HasCompactSupport (f • f')

theorem HasCompactSupport.mul_right {α : Type u_2} {β : Type u_4} [TopologicalSpace α] [MulZeroClass β] {f : α → β} {f' : α → β} (hf : HasCompactSupport f) : HasCompactSupport (f * f')

theorem HasCompactSupport.mul_left {α : Type u_2} {β : Type u_4} [TopologicalSpace α] [MulZeroClass β] {f : α → β} {f' : α → β} (hf : HasCompactSupport f') : HasCompactSupport (f * f')

theorem LocallyFinite.exists_finset_nhd_support_subset {X : Type u_1} {R : Type u_9} {ι : Type u_10} [TopologicalSpace X] {U : ι → Set X} [Zero R] {f : ι → X → R} (hlf : LocallyFinite fun (i : ι) => Function.support (f i)) (hso : ∀ (i : ι), tsupport (f i) ⊆ U i) (ho : ∀ (i : ι), IsOpen (U i)) (x : X) : ∃ (is : Finset ι), ∃ n ∈ nhds x, n ⊆ ⋂ i ∈ is, U i ∧ ∀ z ∈ n, (Function.support fun (i : ι) => f i z) ⊆ ↑is

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.

theorem LocallyFinite.exists_finset_nhd_mulSupport_subset {X : Type u_1} {R : Type u_9} {ι : Type u_10} [TopologicalSpace X] {U : ι → Set X} [One R] {f : ι → X → R} (hlf : LocallyFinite fun (i : ι) => Function.mulSupport (f i)) (hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i) (ho : ∀ (i : ι), IsOpen (U i)) (x : X) : ∃ (is : Finset ι), ∃ n ∈ nhds x, n ⊆ ⋂ i ∈ is, U i ∧ ∀ z ∈ n, (Function.mulSupport fun (i : ι) => f i z) ⊆ ↑is

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 locallyFinite_support_iff {X : Type u_1} {M : Type u_7} {ι : Type u_10} [TopologicalSpace X] [AddCommMonoid M] {f : ι → X → M} : (LocallyFinite fun (i : ι) => Function.support (f i)) ↔ LocallyFinite fun (i : ι) => tsupport (f i)

theorem locallyFinite_mulSupport_iff {X : Type u_1} {M : Type u_7} {ι : Type u_10} [TopologicalSpace X] [CommMonoid M] {f : ι → X → M} : (LocallyFinite fun (i : ι) => Function.mulSupport (f i)) ↔ LocallyFinite fun (i : ι) => mulTSupport (f i)

theorem LocallyFinite.smul_left {X : Type u_1} {M : Type u_7} {R : Type u_9} {ι : Type u_10} [TopologicalSpace X] [Zero R] [Zero M] [SMulWithZero R M] {s : ι → X → R} (h : LocallyFinite fun (i : ι) => Function.support (s i)) (f : ι → X → M) : LocallyFinite fun (i : ι) => Function.support (s i • f i)

theorem LocallyFinite.smul_right {X : Type u_1} {M : Type u_7} {R : Type u_9} {ι : Type u_10} [TopologicalSpace X] [Zero M] [SMulZeroClass R M] {f : ι → X → M} (h : LocallyFinite fun (i : ι) => Function.support (f i)) (s : ι → X → R) : LocallyFinite fun (i : ι) => Function.support (s i • f i)