Type of functions with locally finite support

This file defines functions with locally finite support, provides supporting API. For suitable targets, it establishes functions with locally finite support as an instance of a lattice ordered commutative group.

Throughout the present file, X denotes a topologically space and U a subset of X.

Definition, coercion to functions and basic extensionality lemmas

A function with locally finite support within U is a function X → Y whose support is locally finite within U and entirely contained in U. For T1-spaces, the theorem supportDiscreteWithin_iff_locallyFiniteWithin shows that the first condition is equivalent to the condition that the support f is discrete within U.

structure Function.locallyFinsuppWithin {X : Type u_1} [TopologicalSpace X] (U : Set X) (Y : Type u_2) [Zero Y] : Type (max u_1 u_2)

A function with locally finite support within U is a triple as specified below.

• toFun : X → Y

  A function X → Y

• supportWithinDomain' : Function.support self.toFun ⊆ U

  A proof that the support of toFun is contained in U

• supportLocallyFiniteWithinDomain' (z : X) : z ∈ U → ∃ t ∈ nhds z, (t ∩ Function.support self.toFun).Finite

  A proof that the support is locally finite within U

@[reducible, inline]

abbrev Function.locallyFinsupp (X : Type u_1) [TopologicalSpace X] (Y : Type u_2) [Zero Y] : Type (max u_1 u_2)

A function with locally finite support is a function with locally finite support within ⊤ : Set X.

theorem supportDiscreteWithin_iff_locallyFiniteWithin {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [T1Space X] [Zero Y] {f : X → Y} (h : Function.support f ⊆ U) : f =ᶠ[Filter.codiscreteWithin U] 0 ↔ ∀ z ∈ U, ∃ t ∈ nhds z, (t ∩ Function.support f).Finite

For T1 spaces, the condition supportLocallyFiniteWithinDomain' is equivalent to saying that the support is codiscrete within U.

instance Function.locallyFinsuppWithin.instFunLike {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [Zero Y] : FunLike (locallyFinsuppWithin U Y) X Y

Functions with locally finite support within U are FunLike: the coercion to functions is injective.

@[reducible, inline]

abbrev Function.locallyFinsuppWithin.support {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [Zero Y] (D : locallyFinsuppWithin U Y) : Set X

This allows writing D.support instead of Function.support D

theorem Function.locallyFinsuppWithin.supportWithinDomain {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [Zero Y] (D : locallyFinsuppWithin U Y) : D.support ⊆ U

theorem Function.locallyFinsuppWithin.supportLocallyFiniteWithinDomain {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [Zero Y] (D : locallyFinsuppWithin U Y) (z : X) : z ∈ U → ∃ t ∈ nhds z, (t ∩ D.support).Finite

theorem Function.locallyFinsuppWithin.ext {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [Zero Y] {D₁ D₂ : locallyFinsuppWithin U Y} (h : ∀ (a : X), D₁ a = D₂ a) : D₁ = D₂

theorem Function.locallyFinsuppWithin.ext_iff {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [Zero Y] {D₁ D₂ : locallyFinsuppWithin U Y} : D₁ = D₂ ↔ ∀ (a : X), D₁ a = D₂ a

theorem Function.locallyFinsuppWithin.coe_injective {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [Zero Y] : Injective fun (x : locallyFinsuppWithin U Y) => ⇑x

Elementary properties of the support

@[simp]

theorem Function.locallyFinsuppWithin.apply_eq_zero_of_notMem {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [Zero Y] {z : X} (D : locallyFinsuppWithin U Y) (hz : z ∉ U) : D z = 0

Simplifier lemma: Functions with locally finite support within U evaluate to zero outside of U.

theorem Function.locallyFinsuppWithin.eq_zero_codiscreteWithin {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [Zero Y] [T1Space X] (D : locallyFinsuppWithin U Y) : ⇑D =ᶠ[Filter.codiscreteWithin U] 0

On a T1 space, the support of a function with locally finite support within U is discrete within U.

theorem Function.locallyFinsuppWithin.discreteSupport {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [Zero Y] [T1Space X] (D : locallyFinsuppWithin U Y) : IsDiscrete D.support

On a T1 space, the support of a function with locally finite support within U is discrete.

theorem Function.locallyFinsuppWithin.closedSupport {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [T1Space X] [Zero Y] (D : locallyFinsuppWithin U Y) (hU : IsClosed U) : IsClosed D.support

If X is T1 and if U is closed, then the support of support of a function with locally finite support within U is also closed.

theorem Function.locallyFinsuppWithin.finiteSupport {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [T2Space X] [Zero Y] (D : locallyFinsuppWithin U Y) (hU : IsCompact U) : D.support.Finite

If X is T2 and if U is compact, then the support of a function with locally finite support within U is finite.

Lattice ordered group structure

If X is a suitable instance, this section equips functions with locally finite support within U with the standard structure of a lattice ordered group, where addition, comparison, min and max are defined pointwise.

def Function.locallyFinsuppWithin.addSubgroup {X : Type u_1} [TopologicalSpace X] (U : Set X) {Y : Type u_2} [AddCommGroup Y] : AddSubgroup (X → Y)

Functions with locally finite support within U form an additive subgroup of functions X → Y.

theorem Function.locallyFinsuppWithin.memAddSubgroup {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [AddCommGroup Y] (D : locallyFinsuppWithin U Y) : ⇑D ∈ locallyFinsuppWithin.addSubgroup U

def Function.locallyFinsuppWithin.mk_of_mem {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [AddCommGroup Y] (f : X → Y) (hf : f ∈ locallyFinsuppWithin.addSubgroup U) : locallyFinsuppWithin U Y

Assign a function with locally finite support within U to a function in the subgroup.

@[simp]

theorem Function.locallyFinsuppWithin.mk_of_mem_toFun {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [AddCommGroup Y] (f : X → Y) (hf : f ∈ locallyFinsuppWithin.addSubgroup U) (a✝ : X) : (mk_of_mem f hf) a✝ = f a✝

instance Function.locallyFinsuppWithin.instZero {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [AddCommGroup Y] : Zero (locallyFinsuppWithin U Y)

instance Function.locallyFinsuppWithin.instAdd {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [AddCommGroup Y] : Add (locallyFinsuppWithin U Y)

instance Function.locallyFinsuppWithin.instNeg {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [AddCommGroup Y] : Neg (locallyFinsuppWithin U Y)

instance Function.locallyFinsuppWithin.instSub {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [AddCommGroup Y] : Sub (locallyFinsuppWithin U Y)

instance Function.locallyFinsuppWithin.instSMulNat {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [AddCommGroup Y] : SMul ℕ (locallyFinsuppWithin U Y)

instance Function.locallyFinsuppWithin.instSMulInt {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [AddCommGroup Y] : SMul ℤ (locallyFinsuppWithin U Y)

@[simp]

theorem Function.locallyFinsuppWithin.coe_zero {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [AddCommGroup Y] : ⇑0 = 0

@[simp]

theorem Function.locallyFinsuppWithin.coe_add {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [AddCommGroup Y] (D₁ D₂ : locallyFinsuppWithin U Y) : ⇑(D₁ + D₂) = ⇑D₁ + ⇑D₂

@[simp]

theorem Function.locallyFinsuppWithin.coe_neg {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [AddCommGroup Y] (D : locallyFinsuppWithin U Y) : ⇑(-D) = -⇑D

@[simp]

theorem Function.locallyFinsuppWithin.coe_sub {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [AddCommGroup Y] (D₁ D₂ : locallyFinsuppWithin U Y) : ⇑(D₁ - D₂) = ⇑D₁ - ⇑D₂

@[simp]

theorem Function.locallyFinsuppWithin.coe_nsmul {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [AddCommGroup Y] (D : locallyFinsuppWithin U Y) (n : ℕ) : ⇑(n • D) = n • ⇑D

@[simp]

theorem Function.locallyFinsuppWithin.coe_zsmul {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [AddCommGroup Y] (D : locallyFinsuppWithin U Y) (n : ℤ) : ⇑(n • D) = n • ⇑D

instance Function.locallyFinsuppWithin.instAddCommGroup {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [AddCommGroup Y] : AddCommGroup (locallyFinsuppWithin U Y)

instance Function.locallyFinsuppWithin.instLE {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [LE Y] [Zero Y] : LE (locallyFinsuppWithin U Y)

theorem Function.locallyFinsuppWithin.le_def {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [LE Y] [Zero Y] {D₁ D₂ : locallyFinsuppWithin U Y} : D₁ ≤ D₂ ↔ ⇑D₁ ≤ ⇑D₂

instance Function.locallyFinsuppWithin.instLTOfPreorder {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [Preorder Y] [Zero Y] : LT (locallyFinsuppWithin U Y)

theorem Function.locallyFinsuppWithin.lt_def {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [Preorder Y] [Zero Y] {D₁ D₂ : locallyFinsuppWithin U Y} : D₁ < D₂ ↔ ⇑D₁ < ⇑D₂

instance Function.locallyFinsuppWithin.instMaxOfSemilatticeSup {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [SemilatticeSup Y] [Zero Y] : Max (locallyFinsuppWithin U Y)

@[simp]

theorem Function.locallyFinsuppWithin.max_apply {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [SemilatticeSup Y] [Zero Y] {D₁ D₂ : locallyFinsuppWithin U Y} {x : X} : (D₁ ⊔ D₂) x = D₁ x ⊔ D₂ x

instance Function.locallyFinsuppWithin.instMinOfSemilatticeInf {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [SemilatticeInf Y] [Zero Y] : Min (locallyFinsuppWithin U Y)

@[simp]

theorem Function.locallyFinsuppWithin.min_apply {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [SemilatticeInf Y] [Zero Y] {D₁ D₂ : locallyFinsuppWithin U Y} {x : X} : (D₁ ⊓ D₂) x = D₁ x ⊓ D₂ x

instance Function.locallyFinsuppWithin.instLattice {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [Lattice Y] [Zero Y] : Lattice (locallyFinsuppWithin U Y)

@[simp]

theorem Function.locallyFinsuppWithin.posPart_apply {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [Lattice Y] [AddCommGroup Y] (a : locallyFinsuppWithin U Y) (x : X) : a⁺ x = (a x)⁺

@[simp]

theorem Function.locallyFinsuppWithin.negPart_apply {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [Lattice Y] [AddCommGroup Y] (a : locallyFinsuppWithin U Y) (x : X) : a⁻ x = (a x)⁻

instance Function.locallyFinsuppWithin.instIsOrderedAddMonoid {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [AddCommGroup Y] [LinearOrder Y] [IsOrderedAddMonoid Y] : IsOrderedAddMonoid (locallyFinsuppWithin U Y)

Functions with locally finite support within U form an ordered commutative group.

theorem Function.locallyFinsuppWithin.posPart_add {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [AddCommGroup Y] [LinearOrder Y] [IsOrderedAddMonoid Y] (f₁ f₂ : locallyFinsuppWithin U Y) : (f₁ + f₂)⁺ ≤ f₁⁺ + f₂⁺

The positive part of a sum is less than or equal to the sum of the positive parts.

theorem Function.locallyFinsuppWithin.negPart_add {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [AddCommGroup Y] [LinearOrder Y] [IsOrderedAddMonoid Y] (f₁ f₂ : locallyFinsuppWithin U Y) : (f₁ + f₂)⁻ ≤ f₁⁻ + f₂⁻

The negative part of a sum is less than or equal to the sum of the negative parts.

@[simp]

theorem Function.locallyFinsuppWithin.nsmul_posPart {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [AddCommGroup Y] [LinearOrder Y] [IsOrderedAddMonoid Y] (n : ℕ) (f : locallyFinsuppWithin U Y) : (n • f)⁺ = n • f⁺

Taking the positive part of a function with locally finite support commutes with scalar multiplication by a natural number.

@[simp]

theorem Function.locallyFinsuppWithin.nsmul_negPart {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [AddCommGroup Y] [LinearOrder Y] [IsOrderedAddMonoid Y] (n : ℕ) (f : locallyFinsuppWithin U Y) : (n • f)⁻ = n • f⁻

Taking the negative part of a function with locally finite support commutes with scalar multiplication by a natural number.

Restriction

noncomputable def Function.locallyFinsuppWithin.restrict {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [Zero Y] {V : Set X} (D : locallyFinsuppWithin U Y) (h : V ⊆ U) : locallyFinsuppWithin V Y

If V is a subset of U, then functions with locally finite support within U restrict to functions with locally finite support within V, by setting their values to zero outside of V.

theorem Function.locallyFinsuppWithin.restrict_apply {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [Zero Y] {V : Set X} (D : locallyFinsuppWithin U Y) (h : V ⊆ U) (z : X) : (D.restrict h) z = if z ∈ V then D z else 0

theorem Function.locallyFinsuppWithin.restrict_eqOn {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [Zero Y] {V : Set X} (D : locallyFinsuppWithin U Y) (h : V ⊆ U) : Set.EqOn (⇑(D.restrict h)) (⇑D) V

theorem Function.locallyFinsuppWithin.restrict_eqOn_compl {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [Zero Y] {V : Set X} (D : locallyFinsuppWithin U Y) (h : V ⊆ U) : Set.EqOn (⇑(D.restrict h)) 0 Vᶜ

noncomputable def Function.locallyFinsuppWithin.restrictMonoidHom {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [AddCommGroup Y] {V : Set X} (h : V ⊆ U) : locallyFinsuppWithin U Y →+ locallyFinsuppWithin V Y

Restriction as a group morphism

@[simp]

theorem Function.locallyFinsuppWithin.restrictMonoidHom_apply {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [AddCommGroup Y] {V : Set X} (D : locallyFinsuppWithin U Y) (h : V ⊆ U) : (restrictMonoidHom h) D = D.restrict h

noncomputable def Function.locallyFinsuppWithin.restrictLatticeHom {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [AddCommGroup Y] [Lattice Y] {V : Set X} (h : V ⊆ U) : LatticeHom (locallyFinsuppWithin U Y) (locallyFinsuppWithin V Y)

Restriction as a lattice morphism

@[simp]

theorem Function.locallyFinsuppWithin.restrictLatticeHom_apply {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [AddCommGroup Y] [Lattice Y] {V : Set X} (D : locallyFinsuppWithin U Y) (h : V ⊆ U) : (restrictLatticeHom h) D = D.restrict h

theorem Function.locallyFinsuppWithin.restrict_posPart {X : Type u_1} [TopologicalSpace X] {U V : Set X} (D : locallyFinsuppWithin U ℤ) (h : V ⊆ U) : D⁺.restrict h = (D.restrict h)⁺

Restriction commutes with taking positive parts.

theorem Function.locallyFinsuppWithin.restrict_negPart {X : Type u_1} [TopologicalSpace X] {U V : Set X} (D : locallyFinsuppWithin U ℤ) (h : V ⊆ U) : D⁻.restrict h = (D.restrict h)⁻

Restriction commutes with taking negative parts.