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 => 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 => 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 => f x • g x) ⊆ tsupport f

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 : α), x ∈ tsupport f → ContinuousAt f x) : Continuous f

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

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 : α → β} [T2Space α] : (∃ K, IsCompact K ∧ ∀ (x : α), ¬x ∈ K → f x = 0) ↔ HasCompactSupport f

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

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

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

theorem HasCompactSupport.of_support_subset_isCompact {α : Type u_2} {β : Type u_4} [TopologicalSpace α] [Zero β] {f : α → β} [T2Space α] {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 : α → β} [T2Space α] {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)

abbrev hasCompactSupport_iff_eventuallyEq.match_1 {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [Zero β] {f : α → β} (motive : (∃ t, IsClosed t ∧ IsCompact t ∧ {x | (fun x => f x = OfNat.ofNat (α → β) 0 Zero.toOfNat0 x) x}ᶜ ⊆ t) → Prop) : (x : ∃ t, IsClosed t ∧ IsCompact t ∧ {x | (fun x => f x = OfNat.ofNat (α → β) 0 Zero.toOfNat0 x) x}ᶜ ⊆ t) → ((_C : Set α) → (hC : IsClosed _C ∧ IsCompact _C ∧ {x | (fun x => f x = OfNat.ofNat (α → β) 0 Zero.toOfNat0 x) x}ᶜ ⊆ _C) → motive (_ : ∃ t, IsClosed t ∧ IsCompact t ∧ {x | (fun x => f x = OfNat.ofNat (α → β) 0 Zero.toOfNat0 x) x}ᶜ ⊆ t)) → motive x

Equations

• hasCompactSupport_iff_eventuallyEq.match_1 motive x h_1 = Exists.casesOn x fun w h => h_1 w h

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 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.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} {U : ι → Set X} [TopologicalSpace 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 n, n ∈ nhds x ∧ n ⊆ ⋂ (i : ι) (_ : i ∈ is), U i ∧ ∀ (z : X), 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} {U : ι → Set X} [TopologicalSpace 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 n, n ∈ nhds x ∧ n ⊆ ⋂ (i : ι) (_ : i ∈ is), U i ∧ ∀ (z : X), 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.