Two lemmas about limit of Π b ∈ s, f b along

In this file we prove two auxiliary lemmas about Filter.atTop : Filter (Finset _) and ∏ b ∈ s, f b. These lemmas are useful to build the theory of absolutely convergent series.

theorem Filter.map_atTop_finsetProd_le_of_prod_eq {α : Type u_1} {β : Type u_2} {M : Type u_3} [CommMonoid M] {f : α → M} {g : β → M} (h_eq : ∀ (u : Finset β), ∃ (v : Finset α), ∀ (v' : Finset α), v ⊆ v' → ∃ (u' : Finset β), u ⊆ u' ∧ ∏ x ∈ u', g x = ∏ b ∈ v', f b) : map (fun (s : Finset α) => ∏ b ∈ s, f b) atTop ≤ map (fun (s : Finset β) => ∏ x ∈ s, g x) atTop

Let f and g be two maps to the same commutative monoid. This lemma gives a sufficient condition for comparison of the filter atTop.map (fun s ↦ ∏ b ∈ s, f b) with atTop.map (fun s ↦ ∏ b ∈ s, g b). This is useful to compare the set of limit points of Π b in s, f b as s → atTop with the similar set for g.

theorem Filter.map_atTop_finsetSum_le_of_sum_eq {α : Type u_1} {β : Type u_2} {M : Type u_3} [AddCommMonoid M] {f : α → M} {g : β → M} (h_eq : ∀ (u : Finset β), ∃ (v : Finset α), ∀ (v' : Finset α), v ⊆ v' → ∃ (u' : Finset β), u ⊆ u' ∧ ∑ x ∈ u', g x = ∑ b ∈ v', f b) : map (fun (s : Finset α) => ∑ b ∈ s, f b) atTop ≤ map (fun (s : Finset β) => ∑ x ∈ s, g x) atTop

Let f and g be two maps to the same commutative additive monoid. This lemma gives a sufficient condition for comparison of the filter atTop.map (fun s ↦ ∑ b ∈ s, f b) with atTop.map (fun s ↦ ∑ b ∈ s, g b). This is useful to compare the set of limit points of ∑ b ∈ s, f b as s → atTop with the similar set for g.

@[deprecated Filter.map_atTop_finsetSum_le_of_sum_eq (since := "2026-04-08")]

theorem Filter.map_atTop_finset_sum_le_of_sum_eq {α : Type u_1} {β : Type u_2} {M : Type u_3} [AddCommMonoid M] {f : α → M} {g : β → M} (h_eq : ∀ (u : Finset β), ∃ (v : Finset α), ∀ (v' : Finset α), v ⊆ v' → ∃ (u' : Finset β), u ⊆ u' ∧ ∑ x ∈ u', g x = ∑ b ∈ v', f b) : map (fun (s : Finset α) => ∑ b ∈ s, f b) atTop ≤ map (fun (s : Finset β) => ∑ x ∈ s, g x) atTop

Alias of Filter.map_atTop_finsetSum_le_of_sum_eq.

---

Let f and g be two maps to the same commutative additive monoid. This lemma gives a sufficient condition for comparison of the filter atTop.map (fun s ↦ ∑ b ∈ s, f b) with atTop.map (fun s ↦ ∑ b ∈ s, g b). This is useful to compare the set of limit points of ∑ b ∈ s, f b as s → atTop with the similar set for g.

@[deprecated Filter.map_atTop_finsetProd_le_of_prod_eq (since := "2026-04-08")]

theorem Filter.map_atTop_finset_prod_le_of_prod_eq {α : Type u_1} {β : Type u_2} {M : Type u_3} [CommMonoid M] {f : α → M} {g : β → M} (h_eq : ∀ (u : Finset β), ∃ (v : Finset α), ∀ (v' : Finset α), v ⊆ v' → ∃ (u' : Finset β), u ⊆ u' ∧ ∏ x ∈ u', g x = ∏ b ∈ v', f b) : map (fun (s : Finset α) => ∏ b ∈ s, f b) atTop ≤ map (fun (s : Finset β) => ∏ x ∈ s, g x) atTop

Alias of Filter.map_atTop_finsetProd_le_of_prod_eq.

---

Let f and g be two maps to the same commutative monoid. This lemma gives a sufficient condition for comparison of the filter atTop.map (fun s ↦ ∏ b ∈ s, f b) with atTop.map (fun s ↦ ∏ b ∈ s, g b). This is useful to compare the set of limit points of Π b in s, f b as s → atTop with the similar set for g.

theorem Function.Injective.map_atTop_finsetProd_eq {α : Type u_1} {β : Type u_2} {M : Type u_3} [CommMonoid M] {g : α → β} (hg : Injective g) {f : β → M} (hf : ∀ x ∉ Set.range g, f x = 1) : Filter.map (fun (s : Finset α) => ∏ i ∈ s, f (g i)) Filter.atTop = Filter.map (fun (s : Finset β) => ∏ i ∈ s, f i) Filter.atTop

Let g : γ → β be an injective function and f : β → α be a function from the codomain of g to a commutative monoid. Suppose that f x = 1 outside of the range of g. Then the filters atTop.map (fun s ↦ ∏ i ∈ s, f (g i)) and atTop.map (fun s ↦ ∏ i ∈ s, f i) coincide.

The additive version of this lemma is used to prove the equality ∑' x, f (g x) = ∑' y, f y under the same assumptions.

theorem Function.Injective.map_atTop_finsetSum_eq {α : Type u_1} {β : Type u_2} {M : Type u_3} [AddCommMonoid M] {g : α → β} (hg : Injective g) {f : β → M} (hf : ∀ x ∉ Set.range g, f x = 0) : Filter.map (fun (s : Finset α) => ∑ i ∈ s, f (g i)) Filter.atTop = Filter.map (fun (s : Finset β) => ∑ i ∈ s, f i) Filter.atTop

Let g : γ → β be an injective function and f : β → α be a function from the codomain of g to an additive commutative monoid. Suppose that f x = 0 outside of the range of g. Then the filters atTop.map (fun s ↦ ∑ i ∈ s, f (g i)) and atTop.map (fun s ↦ ∑ i ∈ s, f i) coincide.

This lemma is used to prove the equality ∑' x, f (g x) = ∑' y, f y under the same assumptions.

@[deprecated Function.Injective.map_atTop_finsetSum_eq (since := "2026-04-08")]

theorem Function.Injective.map_atTop_finset_sum_eq {α : Type u_1} {β : Type u_2} {M : Type u_3} [AddCommMonoid M] {g : α → β} (hg : Injective g) {f : β → M} (hf : ∀ x ∉ Set.range g, f x = 0) : Filter.map (fun (s : Finset α) => ∑ i ∈ s, f (g i)) Filter.atTop = Filter.map (fun (s : Finset β) => ∑ i ∈ s, f i) Filter.atTop

Alias of Function.Injective.map_atTop_finsetSum_eq.

@[deprecated Function.Injective.map_atTop_finsetProd_eq (since := "2026-04-08")]

theorem Function.Injective.map_atTop_finset_prod_eq {α : Type u_1} {β : Type u_2} {M : Type u_3} [CommMonoid M] {g : α → β} (hg : Injective g) {f : β → M} (hf : ∀ x ∉ Set.range g, f x = 1) : Filter.map (fun (s : Finset α) => ∏ i ∈ s, f (g i)) Filter.atTop = Filter.map (fun (s : Finset β) => ∏ i ∈ s, f i) Filter.atTop

Alias of Function.Injective.map_atTop_finsetProd_eq.

---

Let g : γ → β be an injective function and f : β → α be a function from the codomain of g to a commutative monoid. Suppose that f x = 1 outside of the range of g. Then the filters atTop.map (fun s ↦ ∏ i ∈ s, f (g i)) and atTop.map (fun s ↦ ∏ i ∈ s, f i) coincide.

The additive version of this lemma is used to prove the equality ∑' x, f (g x) = ∑' y, f y under the same assumptions.