Functions tending to the cofinite filter

This file introduces the typeclass Filter.TendstoCofinite, which represents functions f : α → β that tend to the cofinite filter along the cofinite filter. Functions of this class are precisely the valid index transformations for renaming variables in multivariate power series.

Main definitions

• Filter.TendstoCofinite: A typeclass for functions f satisfying Filter.Tendsto f cofinite cofinite. By Filter.tendstoCofinite_iff_finite_preimage_singleton, this is equivalent to f having finite fibers.
• Filter.TendstoCofinite.mapDomain: Given a function v : α → M into an AddCommMonoid, this is the pushforward function β → M defined by summing the values of v over the finite fibers of f.

Main results

• Filter.tendstoCofinite_iff_finite_preimage_singleton: Characterizes TendstoCofinite as exactly those functions with finite fibers.
• Basic instances of TendstoCofinite.
• Finsupp.mapDomain_tendstoCofinite: Pushing forward finitely supported functions along a TendstoCofinite function preserves the TendstoCofinite property.

class Filter.TendstoCofinite {α : Type u_1} {β : Type u_2} (f : α → β) : Prop

The class of functions f such that Tendsto f cofinite cofinite, it is equivalent to f having finite fibers, see Filter.tendstoCofinite_iff_finite_preimage_singleton.

• tendsto_cofinite : Tendsto f cofinite cofinite

theorem Filter.tendstoCofinite_iff {α : Type u_1} {β : Type u_2} (f : α → β) : TendstoCofinite f ↔ Tendsto f cofinite cofinite

theorem Filter.TendstoCofinite.finite_preimage {α : Type u_1} {β : Type u_2} (f : α → β) [TendstoCofinite f] {s : Set β} (hs : s.Finite) : (f ⁻¹' s).Finite

theorem Filter.TendstoCofinite.finite_preimage_singleton {α : Type u_1} {β : Type u_2} (f : α → β) [TendstoCofinite f] (b : β) : (f ⁻¹' {b}).Finite

theorem Filter.tendstoCofinite_iff_finite_preimage_singleton {α : Type u_1} {β : Type u_2} (f : α → β) : TendstoCofinite f ↔ ∀ (b : β), (f ⁻¹' {b}).Finite

theorem Filter.tendstoCofinite_of_injective {α : Type u_1} {β : Type u_2} {f : α → β} (h : Function.Injective f) : TendstoCofinite f

instance Filter.tendstoCofinite_of_finite {α : Type u_1} {β : Type u_2} (f : α → β) [Finite α] : TendstoCofinite f

instance Filter.TendstoCofinite.comp {α : Type u_1} {β : Type u_2} {ι : Type u_3} (f : α → β) (g : β → ι) [TendstoCofinite g] [TendstoCofinite f] : TendstoCofinite (g ∘ f)

instance Filter.TendstoCofinite.id {α : Type u_1} : TendstoCofinite _root_.id

instance Filter.TendstoCofinite.embedding {α : Type u_1} {β : Type u_2} (e : α ↪ β) : TendstoCofinite ⇑e

instance Filter.TendstoCofinite.equiv {α : Type u_1} {β : Type u_2} (e : α ≃ β) : TendstoCofinite ⇑e

noncomputable def Filter.TendstoCofinite.mapDomain {α : Type u_1} {β : Type u_2} {M : Type u_5} (f : α → β) [AddCommMonoid M] [TendstoCofinite f] (v : α → M) : β → M

Given f : α → β with Filter.TendstoCofinite f and v : α → M, Filter.TendstoCofinite.mapDomain f v : β → M is the function whose value at b : β is the sum of v x over all x such that f x = b.

Equations

• Filter.TendstoCofinite.mapDomain f v i = ⋯.toFinset.sum v

@[simp]

theorem Filter.TendstoCofinite.mapDomain_add {α : Type u_1} {β : Type u_2} {M : Type u_5} (f : α → β) [AddCommMonoid M] [TendstoCofinite f] (u v : α → M) : mapDomain f (u + v) = mapDomain f u + mapDomain f v

@[simp]

theorem Filter.TendstoCofinite.mapDomain_smul {α : Type u_1} {β : Type u_2} {R : Type u_4} {M : Type u_5} (f : α → β) [AddCommMonoid M] [TendstoCofinite f] [DistribSMul R M] (r : R) (v : α → M) : mapDomain f (r • v) = r • mapDomain f v

theorem Filter.TendstoCofinite.mapDomain_eq_zero {α : Type u_1} {β : Type u_2} {M : Type u_5} (f : α → β) [AddCommMonoid M] [TendstoCofinite f] (v : α → M) {i : β} (h' : i ∉ Set.range f) : mapDomain f v i = 0

instance Finsupp.mapDomain_tendstoCofinite {α : Type u_1} {β : Type u_2} (f : α → β) [Filter.TendstoCofinite f] : Filter.TendstoCofinite (mapDomain f)