Extended Cardinality

Auxiliary lemmas about Set.encard and infinite sums over ℕ∞.

The contents of this section are taken from mathlib4 PR #23503 by Peter Nelson, and should be removed once that PR is merged.

theorem ENat.hasSum {α : Type u_2} {f : α → ℕ∞} : HasSum f (⨆ (s : Finset α), ∑ a ∈ s, f a)

@[simp]

theorem ENat.summable {α : Type u_2} {f : α → ℕ∞} : Summable f

theorem ENat.tsum_eq_iSup_sum {α : Type u_2} {f : α → ℕ∞} : ∑' (x : α), f x = ⨆ (s : Finset α), ∑ a ∈ s, f a

theorem ENat.tsum_comm {α : Type u_2} {β : Type u_3} {f : α → β → ℕ∞} : ∑' (a : α) (b : β), f a b = ∑' (b : β) (a : α), f a b

theorem ENat.tsum_prod {α : Type u_2} {β : Type u_3} {f : α → β → ℕ∞} : ∑' (p : α × β), f p.1 p.2 = ∑' (a : α) (b : β), f a b

theorem ENat.tsum_add {α : Type u_2} {f g : α → ℕ∞} : ∑' (a : α), (f a + g a) = ∑' (a : α), f a + ∑' (a : α), g a

theorem ENat.tsum_le_tsum {α : Type u_2} {f g : α → ℕ∞} (h : f ≤ g) : ∑' (a : α), f a ≤ ∑' (a : α), g a

theorem ENat.sum_le_tsum {α : Type u_2} {f : α → ℕ∞} (s : Finset α) : ∑ x ∈ s, f x ≤ ∑' (x : α), f x

theorem ENat.le_tsum {α : Type u_2} {f : α → ℕ∞} (a : α) : f a ≤ ∑' (a : α), f a

theorem ENat.le_tsum_of_mem {α : Type u_2} {f : α → ℕ∞} {s : Set α} {a : α} (ha : a ∈ s) : f a ≤ ∑' (x : ↑s), f ↑x

@[simp]

theorem ENat.tsum_eq_zero {α : Type u_2} {f : α → ℕ∞} : ∑' (i : α), f i = 0 ↔ ∀ (i : α), f i = 0

theorem ENat.tsum_eq_top_of_eq_top {α : Type u_2} {f : α → ℕ∞} : (∃ (a : α), f a = ⊤) → ∑' (a : α), f a = ⊤

theorem ENat.tsum_subtype_eq_top_of_eq_top {α : Type u_2} {f : α → ℕ∞} {s : Set α} (h : ∃ a ∈ s, f a = ⊤) : ∑' (a : ↑s), f ↑a = ⊤

theorem ENat.tsum_subtype_union_disjoint {α : Type u_2} {f : α → ℕ∞} {s t : Set α} (hd : Disjoint s t) : ∑' (x : ↑(s ∪ t)), f ↑x = ∑' (x : ↑s), f ↑x + ∑' (x : ↑t), f ↑x

theorem ENat.tsum_subtype_le_of_subset {α : Type u_2} {f : α → ℕ∞} {s t : Set α} (h : s ⊆ t) : ∑' (x : ↑s), f ↑x ≤ ∑' (x : ↑t), f ↑x

theorem ENat.tsum_subtype_union_le {α : Type u_2} {f : α → ℕ∞} (s t : Set α) : ∑' (x : ↑(s ∪ t)), f ↑x ≤ ∑' (x : ↑s), f ↑x + ∑' (x : ↑t), f ↑x

theorem ENat.tsum_subtype_insert {α : Type u_2} {f : α → ℕ∞} {s : Set α} {a : α} (h : a ∉ s) : ∑' (x : ↑(insert a s)), f ↑x = f a + ∑' (x : ↑s), f ↑x

theorem ENat.tsum_sub {α : Type u_2} {f g : α → ℕ∞} (hfin : ∑' (a : α), g a ≠ ⊤) (h : g ≤ f) : ∑' (a : α), (f a - g a) = ∑' (a : α), f a - ∑' (a : α), g a

theorem ENat.mul_tsum {α : Type u_2} {f : α → ℕ∞} (c : ℕ∞) : c * ∑' (a : α), f a = ∑' (a : α), c * f a

theorem ENat.tsum_mul {α : Type u_2} {f : α → ℕ∞} (c : ℕ∞) : (∑' (a : α), f a) * c = ∑' (a : α), f a * c

theorem Set.Infinite.exists_finite_subset_encard_gt {α : Type u_2} {s : Set α} (hs : s.Infinite) (b : ℕ) : ∃ t ⊆ s, ↑b < t.encard ∧ t.Finite

theorem ENat.add_ne_top {x y : ℕ∞} : x + y ≠ ⊤ ↔ x ≠ ⊤ ∧ y ≠ ⊤

theorem ENat.tsum_subtype_eq_top_iff_of_finite {α : Type u_2} {f : α → ℕ∞} {s : Set α} (hs : s.Finite) : ∑' (x : ↑s), f ↑x = ⊤ ↔ ∃ a ∈ s, f a = ⊤

theorem ENat.tsum_eq_top_of_support_infinite {α : Type u_2} {f : α → ℕ∞} (hf : (Function.support f).Infinite) : ∑' (a : α), f a = ⊤

theorem ENat.tsum_const_eq_top {ι : Type u_4} [Infinite ι] {c : ℕ∞} (hc : c ≠ 0) : ∑' (x : ι), c = ⊤

theorem ENat.tsum_eq_top_iff {α : Type u_2} {f : α → ℕ∞} : ∑' (a : α), f a = ⊤ ↔ (Function.support f).Infinite ∨ ∃ (a : α), f a = ⊤

theorem ENat.tsum_subtype_eq_top_iff {α : Type u_2} {f : α → ℕ∞} {s : Set α} : ∑' (a : ↑s), f ↑a = ⊤ ↔ (s ∩ Function.support f).Infinite ∨ ∃ a ∈ s, f a = ⊤

theorem ENat.tsum_subtype_eq_top_of_inter_support_infinite {α : Type u_2} {f : α → ℕ∞} {s : Set α} (hf : (s ∩ Function.support f).Infinite) : ∑' (a : ↑s), f ↑a = ⊤

theorem ENat.tsum_subtype_const_eq_top_of_ne_zero {α : Type u_2} {s : Set α} (hs : s.Infinite) {c : ℕ∞} (hc : c ≠ 0) : ∑' (x : ↑s), c = ⊤

theorem ENat.tsum_comp_le_tsum_of_injective {α : Type u_2} {β : Type u_3} {f : α → β} (hf : Function.Injective f) (g : β → ℕ∞) : ∑' (x : α), g (f x) ≤ ∑' (y : β), g y

theorem ENat.tsum_le_tsum_comp_of_surjective {α : Type u_2} {β : Type u_3} {f : α → β} (hf : Function.Surjective f) (g : β → ℕ∞) : ∑' (y : β), g y ≤ ∑' (x : α), g (f x)

theorem ENat.tsum_comp_eq_tsum_of_bijective {α : Type u_2} {β : Type u_3} {f : α → β} (hf : Function.Bijective f) (g : β → ℕ∞) : ∑' (x : α), g (f x) = ∑' (y : β), g y

theorem ENat.tsum_comp_eq_tsum_of_equiv {α : Type u_2} {β : Type u_3} (e : α ≃ β) (g : β → ℕ∞) : ∑' (x : α), g (e x) = ∑' (y : β), g y

theorem ENat.tsum_subtype_mono {α : Type u_2} (f : α → ℕ∞) {s t : Set α} (h : s ⊆ t) : ∑' (x : ↑s), f ↑x ≤ ∑' (x : ↑t), f ↑x

theorem ENat.tsum_subtype_sigma {α : Type u_2} {β : α → Type u_4} (f : (a : α) → β a → ℕ∞) : ∑' (p : (a : α) × β a), f p.fst p.snd = ∑' (a : α) (b : β a), f a b

theorem ENat.tsum_subtype_sigma' {α : Type u_2} {β : α → Type u_4} (f : (a : α) × β a → ℕ∞) : ∑' (p : (a : α) × β a), f p = ∑' (a : α) (b : β a), f ⟨a, b⟩

theorem ENat.tsum_subtype_iUnion_le_tsum {α : Type u_2} {ι : Type u_4} (f : α → ℕ∞) (t : ι → Set α) : ∑' (x : ↑(⋃ (i : ι), t i)), f ↑x ≤ ∑' (i : ι) (x : ↑(t i)), f ↑x

theorem ENat.tsum_subtype_biUnion_le_tsum {α : Type u_2} {ι : Type u_4} (f : α → ℕ∞) (s : Set ι) (t : ι → Set α) : ∑' (x : ↑(⋃ i ∈ s, t i)), f ↑x ≤ ∑' (i : ↑s) (x : ↑(t ↑i)), f ↑x

theorem ENat.tsum_subtype_biUnion_le {α : Type u_2} {ι : Type u_4} (f : α → ℕ∞) (s : Finset ι) (t : ι → Set α) : ∑' (x : ↑(⋃ i ∈ s, t i)), f ↑x ≤ ∑ i ∈ s, ∑' (x : ↑(t i)), f ↑x

theorem ENat.tsum_subtype_iUnion_le {α : Type u_2} {ι : Type u_4} [Fintype ι] (f : α → ℕ∞) (t : ι → Set α) : ∑' (x : ↑(⋃ (i : ι), t i)), f ↑x ≤ ∑ i : ι, ∑' (x : ↑(t i)), f ↑x

theorem ENat.tsum_subtype_iUnion_eq_tsum {α : Type u_2} {ι : Type u_4} (f : α → ℕ∞) (t : ι → Set α) (ht : Pairwise (Function.onFun Disjoint t)) : ∑' (x : ↑(⋃ (i : ι), t i)), f ↑x = ∑' (i : ι) (x : ↑(t i)), f ↑x

theorem Set.encard_iUnion_of_pairwiseDisjoint {ι : Type u_1} {α : Type u_2} {s : ι → Set α} (hs : univ.PairwiseDisjoint s) : (⋃ (i : ι), s i).encard = ∑' (i : ι), (s i).encard