feat(measure_theory/measure_space): add count_apply_infinite (#3592)

Also add some supporting lemmas about `set.infinite`.

Author: urkud

src/data/fintype/basic.lean

@@ -1003,9 +1003,14 @@ begin
   rw [h, nat_embedding_aux]
 end
 
+/-- Embedding of `ℕ` into an infinite type. -/
 noncomputable def nat_embedding (α : Type*) [infinite α] : ℕ ↪ α :=
 ⟨_, nat_embedding_aux_injective α⟩
 
+lemma exists_subset_card_eq (α : Type*) [infinite α] (n : ℕ) :
+  ∃ s : finset α, s.card = n :=
+⟨(range n).map (nat_embedding α), by rw [card_map, card_range]⟩
+
 end infinite
 
 lemma not_injective_infinite_fintype [infinite α] [fintype β] (f : α → β) :

src/data/set/finite.lean

@@ -185,6 +185,20 @@ theorem infinite_univ_iff : (@univ α).infinite ↔ _root_.infinite α :=
 theorem infinite_univ [h : _root_.infinite α] : infinite (@univ α) :=
 infinite_univ_iff.2 h
 
+theorem infinite_coe_iff {s : set α} : _root_.infinite s ↔ infinite s :=
+⟨λ ⟨h₁⟩ h₂, h₁ h₂.some, λ h₁, ⟨λ h₂, h₁ ⟨h₂⟩⟩⟩
+
+theorem infinite.to_subtype {s : set α} (h : infinite s) : _root_.infinite s :=
+infinite_coe_iff.2 h
+
+/-- Embedding of `ℕ` into an infinite set. -/
+noncomputable def infinite.nat_embedding (s : set α) (h : infinite s) : ℕ ↪ s :=
+by { haveI := h.to_subtype, exact infinite.nat_embedding s }
+
+lemma infinite.exists_subset_card_eq {s : set α} (hs : infinite s) (n : ℕ) :
+  ∃ t : finset α, ↑t ⊆ s ∧ t.card = n :=
+⟨((finset.range n).map (hs.nat_embedding _)).map (embedding.subtype _), by simp⟩
+
 instance fintype_union [decidable_eq α] (s t : set α) [fintype s] [fintype t] : fintype (s ∪ t : set α) :=
 fintype.of_finset (s.to_finset ∪ t.to_finset) $ by simp
 

src/measure_theory/measure_space.lean

@@ -1017,6 +1017,36 @@ calc count (↑s : set α) = ∑' i : (↑s : set α), (1 : α → ennreal) i :
                     ... = ∑ i in s, 1 : s.tsum_subtype 1
                     ... = s.card : by simp
 
+lemma count_apply_finite [measurable_singleton_class α] (s : set α) (hs : finite s) :
+  count s = hs.to_finset.card :=
+by rw [← count_apply_finset, finite.coe_to_finset]
+
+/-- `count` measure evaluates to infinity at infinite sets. -/
+lemma count_apply_infinite [measurable_singleton_class α] {s : set α} (hs : s.infinite) :
+  count s = ⊤ :=
+begin
+  by_contra H,
+  rcases ennreal.exists_nat_gt H with ⟨n, hn⟩,
+  rcases hs.exists_subset_card_eq n with ⟨t, ht, rfl⟩,
+  have := lt_of_le_of_lt (measure_mono ht) hn,
+  simpa [lt_irrefl] using this
+end
+
+@[simp] lemma count_apply_eq_top [measurable_singleton_class α] {s : set α} :
+  count s = ⊤ ↔ s.infinite :=
+begin
+  by_cases hs : s.finite,
+  { simp [set.infinite, hs, count_apply_finite] },
+  { change s.infinite at hs,
+    simp [hs, count_apply_infinite] }
+end
+
+@[simp] lemma count_apply_lt_top [measurable_singleton_class α] {s : set α} :
+  count s < ⊤ ↔ s.finite :=
+calc count s < ⊤ ↔ count s ≠ ⊤ : lt_top_iff_ne_top
+             ... ↔ ¬s.infinite : not_congr count_apply_eq_top
+             ... ↔ s.finite    : not_not
+
 /-- A measure is complete if every null set is also measurable.
   A null set is a subset of a measurable set with measure `0`.
   Since every measure is defined as a special case of an outer measure, we can more simply state