Density of a finite set

This defines the density of a Finset and provides induction principles for finsets.

Main declarations

• Finset.dens s: Density of s : Finset α in α as a nonnegative rational number.

Implementation notes

There are many other ways to talk about the density of a finset and provide its API:

1. Use the uniform measure
2. Define finitely additive functions and generalise the Finset.card API to it. This could either be done with a. A structure FinitelyAdditiveFun b. A typeclass IsFinitelyAdditiveFun

Solution 1 would mean importing measure theory in simple files (not necessarily bad, but not amazing), and every single API lemma would require the user to prove that all the sets they are talking about are measurable in the trivial sigma-algebra (quite terrible user experience).

Solution 2 would mean that some API lemmas about density don't contain dens in their name because they are general results about finitely additive functions. But not all lemmas would be like that either since some really are dens-specific. Hence the user would need to think about whether the lemma they are looking for is generally true for finitely additive measure or whether it is dens-specific.

On top of this, solution 2.a would break dot notation on Finset.dens (possibly fixable by introducing notation for ⇑Finset.dens) and solution 2.b would run the risk of being bad performance-wise.

These considerations more generally apply to Finset.card and Finset.sum and demonstrate that overengineering basic definitions is likely to hinder user experience.

def Finset.dens {α : Type u_2} [Fintype α] (s : Finset α) : ℚ≥0

Density of a finset.

dens s is the number of elements of s divided by the size of the ambient type α.

Equations

• s.dens = ↑s.card / ↑(Fintype.card α)

theorem Finset.dens_eq_card_div_card {α : Type u_2} [Fintype α] (s : Finset α) : s.dens = ↑s.card / ↑(Fintype.card α)

@[simp]

theorem Finset.dens_empty {α : Type u_2} [Fintype α] : ∅.dens = 0

@[simp]

theorem Finset.dens_singleton {α : Type u_2} [Fintype α] (a : α) : {a}.dens = (↑(Fintype.card α))⁻¹

@[simp]

theorem Finset.dens_cons {α : Type u_2} [Fintype α] {s : Finset α} {a : α} (h : a ∉ s) : (Finset.cons a s h).dens = s.dens + (↑(Fintype.card α))⁻¹

@[simp]

theorem Finset.dens_disjUnion {α : Type u_2} [Fintype α] (s : Finset α) (t : Finset α) (h : Disjoint s t) : (s.disjUnion t h).dens = s.dens + t.dens

@[simp]

theorem Finset.dens_eq_zero {α : Type u_2} [Fintype α] {s : Finset α} : s.dens = 0 ↔ s = ∅

theorem Finset.dens_ne_zero {α : Type u_2} [Fintype α] {s : Finset α} : s.dens ≠ 0 ↔ s.Nonempty

@[simp]

theorem Finset.dens_pos {α : Type u_2} [Fintype α] {s : Finset α} : 0 < s.dens ↔ s.Nonempty

theorem Finset.Nonempty.dens_pos {α : Type u_2} [Fintype α] {s : Finset α} : s.Nonempty → 0 < s.dens

Alias of the reverse direction of Finset.dens_pos.

theorem Finset.Nonempty.dens_ne_zero {α : Type u_2} [Fintype α] {s : Finset α} : s.Nonempty → s.dens ≠ 0

Alias of the reverse direction of Finset.dens_ne_zero.

theorem Finset.dens_le_dens {α : Type u_2} [Fintype α] {s : Finset α} {t : Finset α} (h : s ⊆ t) : s.dens ≤ t.dens

theorem Finset.dens_lt_dens {α : Type u_2} [Fintype α] {s : Finset α} {t : Finset α} (h : s ⊂ t) : s.dens < t.dens

theorem Finset.dens_mono {α : Type u_2} [Fintype α] : Monotone Finset.dens

theorem Finset.dens_strictMono {α : Type u_2} [Fintype α] : StrictMono Finset.dens

theorem Finset.dens_map_le {α : Type u_2} {β : Type u_3} [Fintype α] {s : Finset α} [Fintype β] (f : α ↪ β) : (Finset.map f s).dens ≤ s.dens

@[simp]

theorem Finset.dens_map_equiv {α : Type u_2} {β : Type u_3} [Fintype α] {s : Finset α} [Fintype β] (e : α ≃ β) : (Finset.map e.toEmbedding s).dens = s.dens

theorem Finset.dens_image {α : Type u_2} {β : Type u_3} [Fintype α] [Fintype β] [DecidableEq β] {f : α → β} (hf : Function.Bijective f) (s : Finset α) : (Finset.image f s).dens = s.dens

@[simp]

theorem Finset.card_mul_dens {α : Type u_2} [Fintype α] (s : Finset α) : ↑(Fintype.card α) * s.dens = ↑s.card

@[simp]

theorem Finset.dens_mul_card {α : Type u_2} [Fintype α] (s : Finset α) : s.dens * ↑(Fintype.card α) = ↑s.card

@[simp]

theorem Finset.natCast_card_mul_nnratCast_dens {𝕜 : Type u_1} {α : Type u_2} [Fintype α] [Semifield 𝕜] [CharZero 𝕜] (s : Finset α) : ↑(Fintype.card α) * ↑s.dens = ↑s.card

@[simp]

theorem Finset.nnratCast_dens_mul_natCast_card {𝕜 : Type u_1} {α : Type u_2} [Fintype α] [Semifield 𝕜] [CharZero 𝕜] (s : Finset α) : ↑s.dens * ↑(Fintype.card α) = ↑s.card

theorem Finset.nnratCast_dens {𝕜 : Type u_1} {α : Type u_2} [Fintype α] [Semifield 𝕜] [CharZero 𝕜] (s : Finset α) : ↑s.dens = ↑s.card / ↑(Fintype.card α)

@[simp]

theorem Finset.dens_univ {α : Type u_2} [Fintype α] [Nonempty α] : Finset.univ.dens = 1

@[simp]

theorem Finset.dens_eq_one {α : Type u_2} [Fintype α] {s : Finset α} [Nonempty α] : s.dens = 1 ↔ s = Finset.univ

theorem Finset.dens_ne_one {α : Type u_2} [Fintype α] {s : Finset α} [Nonempty α] : s.dens ≠ 1 ↔ s ≠ Finset.univ

@[simp]

theorem Finset.dens_le_one {α : Type u_2} [Fintype α] {s : Finset α} : s.dens ≤ 1

theorem Finset.dens_union_add_dens_inter {α : Type u_2} [Fintype α] [DecidableEq α] (s : Finset α) (t : Finset α) : (s ∪ t).dens + (s ∩ t).dens = s.dens + t.dens

theorem Finset.dens_inter_add_dens_union {α : Type u_2} [Fintype α] [DecidableEq α] (s : Finset α) (t : Finset α) : (s ∩ t).dens + (s ∪ t).dens = s.dens + t.dens

@[simp]

theorem Finset.dens_union_of_disjoint {α : Type u_2} [Fintype α] {s : Finset α} {t : Finset α} [DecidableEq α] (h : Disjoint s t) : (s ∪ t).dens = s.dens + t.dens

theorem Finset.dens_sdiff_add_dens_eq_dens {α : Type u_2} [Fintype α] {s : Finset α} {t : Finset α} [DecidableEq α] (h : s ⊆ t) : (t \ s).dens + s.dens = t.dens

theorem Finset.dens_sdiff_add_dens {α : Type u_2} [Fintype α] [DecidableEq α] (s : Finset α) (t : Finset α) : (s \ t).dens + t.dens = (s ∪ t).dens

theorem Finset.dens_sdiff_comm {α : Type u_2} [Fintype α] {s : Finset α} {t : Finset α} [DecidableEq α] (h : s.card = t.card) : (s \ t).dens = (t \ s).dens

@[simp]

theorem Finset.dens_sdiff_add_dens_inter {α : Type u_2} [Fintype α] [DecidableEq α] (s : Finset α) (t : Finset α) : (s \ t).dens + (s ∩ t).dens = s.dens

@[simp]

theorem Finset.dens_inter_add_dens_sdiff {α : Type u_2} [Fintype α] [DecidableEq α] (s : Finset α) (t : Finset α) : (s ∩ t).dens + (s \ t).dens = s.dens

theorem Finset.dens_filter_add_dens_filter_not_eq_dens {α : Type u_4} [Fintype α] {s : Finset α} (p : α → Prop) [DecidablePred p] [(x : α) → Decidable ¬p x] : (Finset.filter p s).dens + (Finset.filter (fun (a : α) => ¬p a) s).dens = s.dens

theorem Finset.dens_union_le {α : Type u_2} [Fintype α] [DecidableEq α] (s : Finset α) (t : Finset α) : (s ∪ t).dens ≤ s.dens + t.dens

theorem Finset.dens_le_dens_sdiff_add_dens {α : Type u_2} [Fintype α] {s : Finset α} {t : Finset α} [DecidableEq α] : s.dens ≤ (s \ t).dens + t.dens

theorem Finset.dens_sdiff {α : Type u_2} [Fintype α] {s : Finset α} {t : Finset α} [DecidableEq α] (h : s ⊆ t) : (t \ s).dens = t.dens - s.dens

theorem Finset.le_dens_sdiff {α : Type u_2} [Fintype α] [DecidableEq α] (s : Finset α) (t : Finset α) : t.dens - s.dens ≤ (t \ s).dens