Documentation

Mathlib.Topology.Support

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 #

Implementation Notes #

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
Instances For
    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
    Instances For
      theorem subset_tsupport {X : Type u_1} {α : Type u_2} [Zero α] [TopologicalSpace X] (f : Xα) :
      theorem subset_mulTSupport {X : Type u_1} {α : Type u_2} [One α] [TopologicalSpace X] (f : Xα) :
      theorem isClosed_tsupport {X : Type u_1} {α : Type u_2} [Zero α] [TopologicalSpace X] (f : Xα) :
      theorem isClosed_mulTSupport {X : Type u_1} {α : Type u_2} [One α] [TopologicalSpace X] (f : Xα) :
      theorem tsupport_eq_empty_iff {X : Type u_1} {α : Type u_2} [Zero α] [TopologicalSpace X] {f : Xα} :
      theorem mulTSupport_eq_empty_iff {X : Type u_1} {α : Type u_2} [One α] [TopologicalSpace X] {f : Xα} :
      theorem image_eq_zero_of_nmem_tsupport {X : Type u_1} {α : Type u_2} [Zero α] [TopologicalSpace X] {f : Xα} {x : X} (hx : xtsupport 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 : xmulTSupport f) :
      f x = 1
      theorem range_subset_insert_image_tsupport {X : Type u_1} {α : Type u_2} [Zero α] [TopologicalSpace X] (f : Xα) :
      theorem range_subset_insert_image_mulTSupport {X : Type u_1} {α : Type u_2} [One α] [TopologicalSpace X] (f : Xα) :
      theorem range_eq_image_tsupport_or {X : Type u_1} {α : Type u_2} [Zero α] [TopologicalSpace X] (f : Xα) :
      theorem range_eq_image_mulTSupport_or {X : Type u_1} {α : Type u_2} [One α] [TopologicalSpace X] (f : Xα) :
      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 : XM) (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 : XM) (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 : α} :
      xtsupport f f =ᶠ[nhds x] 0
      theorem not_mem_mulTSupport_iff_eventuallyEq {α : Type u_2} {β : Type u_4} [TopologicalSpace α] [One β] {f : αβ} {x : α} :
      xmulTSupport f f =ᶠ[nhds x] 1
      theorem continuous_of_tsupport {α : Type u_2} {β : Type u_4} [TopologicalSpace α] [Zero β] [TopologicalSpace β] {f : αβ} (hf : xtsupport f, ContinuousAt f x) :
      theorem continuous_of_mulTSupport {α : Type u_2} {β : Type u_4} [TopologicalSpace α] [One β] [TopologicalSpace β] {f : αβ} (hf : xmulTSupport f, ContinuousAt f x) :

      Functions with compact support #

      def HasCompactSupport {α : Type u_2} {β : Type u_4} [TopologicalSpace α] [Zero β] (f : αβ) :

      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
      Instances For
        def HasCompactMulSupport {α : Type u_2} {β : Type u_4} [TopologicalSpace α] [One β] (f : αβ) :

        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
        Instances For
          theorem hasCompactSupport_def {α : Type u_2} {β : Type u_4} [TopologicalSpace α] [Zero β] {f : αβ} :
          theorem exists_compact_iff_hasCompactSupport {α : Type u_2} {β : Type u_4} [TopologicalSpace α] [Zero β] {f : αβ} [R1Space α] :
          (∃ (K : Set α), IsCompact K xK, f x = 0) HasCompactSupport f
          theorem exists_compact_iff_hasCompactMulSupport {α : Type u_2} {β : Type u_4} [TopologicalSpace α] [One β] {f : αβ} [R1Space α] :
          (∃ (K : Set α), IsCompact K xK, f x = 1) HasCompactMulSupport f
          theorem HasCompactSupport.intro {α : Type u_2} {β : Type u_4} [TopologicalSpace α] [Zero β] {f : αβ} [R1Space α] {K : Set α} (hK : IsCompact K) (hfK : xK, f x = 0) :
          theorem HasCompactMulSupport.intro {α : Type u_2} {β : Type u_4} [TopologicalSpace α] [One β] {f : αβ} [R1Space α] {K : Set α} (hK : IsCompact K) (hfK : xK, f x = 1) :
          theorem HasCompactSupport.intro' {α : Type u_2} {β : Type u_4} [TopologicalSpace α] [Zero β] {f : αβ} {K : Set α} (hK : IsCompact K) (h'K : IsClosed K) (hfK : xK, f x = 0) :
          theorem HasCompactMulSupport.intro' {α : Type u_2} {β : Type u_4} [TopologicalSpace α] [One β] {f : αβ} {K : Set α} (hK : IsCompact K) (h'K : IsClosed K) (hfK : xK, f x = 1) :
          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) :
          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) :
          theorem HasCompactSupport.isCompact {α : Type u_2} {β : Type u_4} [TopologicalSpace α] [Zero β] {f : αβ} (hf : HasCompactSupport f) :
          theorem HasCompactMulSupport.isCompact {α : Type u_2} {β : Type u_4} [TopologicalSpace α] [One β] {f : αβ} (hf : HasCompactMulSupport f) :
          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) :
          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) :
          theorem HasCompactSupport.isCompact_range {α : Type u_2} {β : Type u_4} [TopologicalSpace α] [Zero β] {f : αβ} [TopologicalSpace β] (h : HasCompactSupport f) (hf : Continuous f) :
          theorem HasCompactMulSupport.isCompact_range {α : Type u_2} {β : Type u_4} [TopologicalSpace α] [One β] {f : αβ} [TopologicalSpace β] (h : HasCompactMulSupport f) (hf : Continuous 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) :
          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) :
          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) :
          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) :
          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) :
          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) :
          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) :
          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) :
          theorem HasCompactSupport.comp_closedEmbedding {α : Type u_2} {α' : Type u_3} {β : Type u_4} [TopologicalSpace α] [TopologicalSpace α'] [Zero β] {f : αβ} (hf : HasCompactSupport f) {g : α'α} (hg : ClosedEmbedding 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) :
          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 : 0k) :
          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 : 1k) :
          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) :
          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) :
          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) :
          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) :
          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) :
          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) :
          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)
          theorem HasCompactSupport.is_zero_at_infty {α : Type u_2} {γ : Type u_5} [TopologicalSpace α] {f : αγ} [TopologicalSpace γ] [Zero γ] (h : HasCompactSupport f) :

          If f has compact support, then f tends to zero at infinity.

          theorem HasCompactMulSupport.is_one_at_infty {α : Type u_2} {γ : Type u_5} [TopologicalSpace α] {f : αγ} [TopologicalSpace γ] [One γ] (h : HasCompactMulSupport f) :

          If f has compact multiplicative support, then f tends to 1 at infinity.

          theorem HasCompactSupport.of_compactSpace {α : Type u_2} {γ : Type u_5} [TopologicalSpace α] [CompactSpace α] [Zero γ] (f : αγ) :
          theorem HasCompactMulSupport.of_compactSpace {α : Type u_2} {γ : Type u_5} [TopologicalSpace α] [CompactSpace α] [One γ] (f : αγ) :

          In a compact space α, any function has compact support.

          Functions with compact support: algebraic operations #

          theorem HasCompactSupport.add {α : Type u_2} {β : Type u_4} [TopologicalSpace α] [AddZeroClass β] {f : αβ} {f' : αβ} (hf : HasCompactSupport f) (hf' : HasCompactSupport f') :
          theorem HasCompactMulSupport.mul {α : Type u_2} {β : Type u_4} [TopologicalSpace α] [MulOneClass β] {f : αβ} {f' : αβ} (hf : HasCompactMulSupport f) (hf' : HasCompactMulSupport f') :
          theorem HasCompactSupport.smul_left {α : Type u_2} {M : Type u_7} {R : Type u_9} [TopologicalSpace α] [Zero M] [SMulZeroClass R M] {f : αR} {f' : αM} (hf : HasCompactSupport 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) :
          @[deprecated HasCompactSupport.smul_left]
          theorem HasCompactSupport.smul_left' {α : Type u_2} {M : Type u_7} {R : Type u_9} [TopologicalSpace α] [Zero M] [SMulZeroClass R M] {f : αR} {f' : αM} (hf : HasCompactSupport f') :

          Alias of HasCompactSupport.smul_left.

          theorem HasCompactSupport.mul_right {α : Type u_2} {β : Type u_4} [TopologicalSpace α] [MulZeroClass β] {f : αβ} {f' : αβ} (hf : HasCompactSupport f) :
          theorem HasCompactSupport.mul_left {α : Type u_2} {β : Type u_4} [TopologicalSpace α] [MulZeroClass β] {f : αβ} {f' : αβ} (hf : HasCompactSupport f') :
          theorem HasCompactSupport.abs {α : Type u_10} {β : Type u_11} [TopologicalSpace α] [AddGroup β] [Lattice β] [CovariantClass β β (fun (x x_1 : β) => x + x_1) fun (x x_1 : β) => x x_1] {f : αβ} (hf : HasCompactSupport 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 : ιXR} (hlf : LocallyFinite fun (i : ι) => Function.support (f i)) (hso : ∀ (i : ι), tsupport (f i) U i) (ho : ∀ (i : ι), IsOpen (U i)) (x : X) :
          ∃ (is : Finset ι), nnhds x, n iis, U i zn, (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 : ιXR} (hlf : LocallyFinite fun (i : ι) => Function.mulSupport (f i)) (hso : ∀ (i : ι), mulTSupport (f i) U i) (ho : ∀ (i : ι), IsOpen (U i)) (x : X) :
          ∃ (is : Finset ι), nnhds x, n iis, U i zn, (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 : ιXM} :
          (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 : ιXM} :
          (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 : ιXR} (h : LocallyFinite fun (i : ι) => Function.support (s i)) (f : ιXM) :
          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 : ιXM} (h : LocallyFinite fun (i : ι) => Function.support (f i)) (s : ιXR) :
          LocallyFinite fun (i : ι) => Function.support (s i f i)