Mathlib.Data.Finset.Density

Module docstring

{"# 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. "}

Finset.dens definition

(s : Finset α) : ℚ≥0

Full source

/-- Density of a finset.

`dens s` is the number of elements of `s` divided by the size of the ambient type `α`. -/
def dens (s : Finset α) : ℚ≥0 := s.card / Fintype.card α

Density of a finite set

Informal description

The density of a finite set $s$ in a finite type $\alpha$ is defined as the ratio of the cardinality of $s$ to the cardinality of $\alpha$, expressed as a nonnegative rational number. That is, $\text{dens}(s) = \frac{|s|}{|\alpha|}$.

Finset.dens_eq_card_div_card theorem

(s : Finset α) : dens s = s.card / Fintype.card α

Full source

lemma dens_eq_card_div_card (s : Finset α) : dens s = s.card / Fintype.card α := rfl

Density of Finite Set as Cardinality Ratio

Informal description

For any finite set $s$ in a finite type $\alpha$, the density of $s$ is equal to the ratio of the cardinality of $s$ to the cardinality of $\alpha$, i.e., $\text{dens}(s) = \frac{|s|}{|\alpha|}$.

Finset.dens_empty theorem

: dens (∅ : Finset α) = 0

Full source

@[simp] lemma dens_empty : dens (∅ : Finset α) = 0 := by simp [dens]

Density of Empty Set is Zero

Informal description

The density of the empty finite set $\emptyset$ in a finite type $\alpha$ is equal to $0$.

Finset.dens_singleton theorem

(a : α) : dens ({ a } : Finset α) = (Fintype.card α : ℚ≥0)⁻¹

Full source

@[simp] lemma dens_singleton (a : α) : dens ({a} : Finset α) = (Fintype.card α : ℚ≥0)⁻¹ := by
  simp [dens]

Density of Singleton Set: $\text{dens}(\{a\}) = \frac{1}{|\alpha|}$

Informal description

For any element $a$ in a finite type $\alpha$, the density of the singleton set $\{a\}$ is equal to the reciprocal of the cardinality of $\alpha$, i.e., $\text{dens}(\{a\}) = \frac{1}{|\alpha|}$.

Finset.dens_cons theorem

(h : a ∉ s) : (s.cons a h).dens = dens s + (Fintype.card α : ℚ≥0)⁻¹

Full source

@[simp] lemma dens_cons (h : a ∉ s) : (s.cons a h).dens = dens s + (Fintype.card α : ℚ≥0)⁻¹ := by
  simp [dens, add_div]

Density of Finite Set with Added Element: $\text{dens}(s \cup \{a\}) = \text{dens}(s) + \frac{1}{|\alpha|}$

Informal description

For a finite set $s$ in a finite type $\alpha$ and an element $a \in \alpha$ not in $s$, the density of the set obtained by adding $a$ to $s$ (denoted $s \cup \{a\}$) is equal to the density of $s$ plus the reciprocal of the cardinality of $\alpha$. That is, $\text{dens}(s \cup \{a\}) = \text{dens}(s) + \frac{1}{|\alpha|}$.

Finset.dens_disjUnion theorem

(s t : Finset α) (h) : dens (s.disjUnion t h) = dens s + dens t

Full source

@[simp] lemma dens_disjUnion (s t : Finset α) (h) : dens (s.disjUnion t h) = dens s + dens t := by
  simp_rw [dens, card_disjUnion, Nat.cast_add, add_div]

Additivity of Density for Disjoint Finite Sets: $\text{dens}(s \cup t) = \text{dens}(s) + \text{dens}(t)$

Informal description

For any two disjoint finite sets $s$ and $t$ in a finite type $\alpha$, the density of their disjoint union is equal to the sum of their individual densities, i.e., $\text{dens}(s \cup t) = \text{dens}(s) + \text{dens}(t)$.

Finset.dens_eq_zero theorem

: dens s = 0 ↔ s = ∅

Full source

@[simp] lemma dens_eq_zero : densdens s = 0 ↔ s = ∅ := by
  simp +contextual [dens, Fintype.card_eq_zero_iff, eq_empty_of_isEmpty]

Density of Finite Set is Zero if and only if Empty

Informal description

For any finite set $s$ in a finite type $\alpha$, the density of $s$ is zero if and only if $s$ is the empty set. That is, $\text{dens}(s) = 0 \leftrightarrow s = \emptyset$.

Finset.dens_ne_zero theorem

: dens s ≠ 0 ↔ s.Nonempty

Full source

lemma dens_ne_zero : densdens s ≠ 0dens s ≠ 0 ↔ s.Nonempty := dens_eq_zero.not.trans nonempty_iff_ne_empty.symm

Nonzero Density Characterization for Finite Sets: $\text{dens}(s) \neq 0 \leftrightarrow s \text{ nonempty}$

Informal description

For any finite set $s$ in a finite type $\alpha$, the density of $s$ is nonzero if and only if $s$ is nonempty. That is, $\text{dens}(s) \neq 0 \leftrightarrow s \text{ is nonempty}$.

Finset.dens_pos theorem

: 0 < dens s ↔ s.Nonempty

Full source

@[simp] lemma dens_pos : 0 < dens s ↔ s.Nonempty := pos_iff_ne_zero.trans dens_ne_zero

Positive Density Characterization: $0 < \text{dens}(s) \leftrightarrow s \text{ nonempty}$

Informal description

For any finite set $s$ in a finite type $\alpha$, the density of $s$ is positive if and only if $s$ is nonempty. That is, $0 < \text{dens}(s) \leftrightarrow s \text{ is nonempty}$.

Finset.dens_le_dens theorem

(h : s ⊆ t) : dens s ≤ dens t

Full source

lemma dens_le_dens (h : s ⊆ t) : dens s ≤ dens t :=
  div_le_div_of_nonneg_right (mod_cast card_mono h) <| by positivity

Monotonicity of Finite Set Density under Subset Inclusion

Informal description

For any finite sets $s$ and $t$ in a finite type $\alpha$, if $s$ is a subset of $t$, then the density of $s$ is less than or equal to the density of $t$, i.e., $\frac{|s|}{|\alpha|} \leq \frac{|t|}{|\alpha|}$.

Finset.dens_lt_dens theorem

(h : s ⊂ t) : dens s < dens t

Full source

lemma dens_lt_dens (h : s ⊂ t) : dens s < dens t :=
  div_lt_div_of_pos_right (mod_cast card_strictMono h) <| by
    cases isEmpty_or_nonempty α
    · simp [Subsingleton.elim s t, ssubset_irrfl] at h
    · exact mod_cast Fintype.card_pos

Strict Monotonicity of Density under Strict Subset Inclusion: $s \subset t \implies \text{dens}(s) < \text{dens}(t)$

Informal description

For any finite subsets $s$ and $t$ of a finite type $\alpha$, if $s$ is a strict subset of $t$ (i.e., $s \subset t$), then the density of $s$ is strictly less than the density of $t$, i.e., $\text{dens}(s) < \text{dens}(t)$.

Finset.dens_mono theorem

: Monotone (dens : Finset α → ℚ≥0)

Full source

@[mono] lemma dens_mono : Monotone (dens : Finset α → ℚ≥0) := fun _ _ ↦ dens_le_dens

Monotonicity of Finite Set Density: $s \subseteq t \implies \text{dens}(s) \leq \text{dens}(t)$

Informal description

The density function $\text{dens} : \text{Finset} \alpha \to \mathbb{Q}_{\geq 0}$, which maps a finite set $s$ to its density $\frac{|s|}{|\alpha|}$, is a monotone function with respect to the subset order on finite sets. That is, for any finite sets $s$ and $t$ in $\alpha$, if $s \subseteq t$, then $\text{dens}(s) \leq \text{dens}(t)$.

Finset.dens_strictMono theorem

: StrictMono (dens : Finset α → ℚ≥0)

Full source

@[mono] lemma dens_strictMono : StrictMono (dens : Finset α → ℚ≥0) := fun _ _ ↦ dens_lt_dens

Strict Monotonicity of Finite Set Density

Informal description

The density function $\text{dens} : \text{Finset } \alpha \to \mathbb{Q}_{\geq 0}$ is strictly monotone with respect to the subset relation. That is, for any finite subsets $s, t \subseteq \alpha$, if $s \subset t$, then $\text{dens}(s) < \text{dens}(t)$.

Finset.dens_map_le theorem

[Fintype β] (f : α ↪ β) : dens (s.map f) ≤ dens s

Full source

lemma dens_map_le [Fintype β] (f : α ↪ β) : dens (s.map f) ≤ dens s := by
  cases isEmpty_or_nonempty α
  · simp [Subsingleton.elim s ∅]
  simp_rw [dens, card_map]
  gcongr
  · positivity
  · exact mod_cast Fintype.card_pos
  · exact Fintype.card_le_of_injective _ f.2

Density Inequality under Injective Mapping: $\text{dens}(f(s)) \leq \text{dens}(s)$

Informal description

Let $\alpha$ and $\beta$ be finite types, and let $f : \alpha \hookrightarrow \beta$ be an injective function. For any finite subset $s$ of $\alpha$, the density of the image $f(s)$ in $\beta$ is less than or equal to the density of $s$ in $\alpha$. That is, $$\text{dens}(f(s)) \leq \text{dens}(s).$$

Finset.dens_map_equiv theorem

[Fintype β] (e : α ≃ β) : (s.map e.toEmbedding).dens = s.dens

Full source

@[simp] lemma dens_map_equiv [Fintype β] (e : α ≃ β) : (s.map e.toEmbedding).dens = s.dens := by
  simp [dens, Fintype.card_congr e]

Density Preservation under Bijection of Finite Types

Informal description

Let $\alpha$ and $\beta$ be finite types, and let $e : \alpha \simeq \beta$ be a bijection between them. For any finite subset $s$ of $\alpha$, the density of the image of $s$ under $e$ in $\beta$ is equal to the density of $s$ in $\alpha$. That is, $\text{dens}(e(s)) = \text{dens}(s)$.

Finset.dens_image theorem

[Fintype β] [DecidableEq β] {f : α → β} (hf : Bijective f) (s : Finset α) : (s.image f).dens = s.dens

Full source

lemma dens_image [Fintype β] [DecidableEq β] {f : α → β} (hf : Bijective f) (s : Finset α) :
    (s.image f).dens = s.dens := by
  simpa [map_eq_image, -dens_map_equiv] using dens_map_equiv (.ofBijective f hf)

Density Preservation under Bijective Image: $\text{dens}(f(s)) = \text{dens}(s)$

Informal description

Let $\alpha$ and $\beta$ be finite types, with $\beta$ having decidable equality. Given a bijective function $f : \alpha \to \beta$ and a finite subset $s$ of $\alpha$, the density of the image of $s$ under $f$ in $\beta$ is equal to the density of $s$ in $\alpha$. That is, $$\text{dens}(f(s)) = \text{dens}(s).$$

Finset.card_mul_dens theorem

(s : Finset α) : Fintype.card α * s.dens = s.card

Full source

@[simp] lemma card_mul_dens (s : Finset α) : Fintype.card α * s.dens = s.card := by
  cases isEmpty_or_nonempty α
  · simp [Subsingleton.elim s ∅]
  rw [dens, mul_div_cancel₀]
  exact mod_cast Fintype.card_ne_zero

Cardinality-Density Product Identity for Finite Sets

Informal description

For any finite set $s$ in a finite type $\alpha$, the product of the cardinality of $\alpha$ and the density of $s$ equals the cardinality of $s$. That is, $$|\alpha| \cdot \text{dens}(s) = |s|.$$

Finset.dens_mul_card theorem

(s : Finset α) : s.dens * Fintype.card α = s.card

Full source

@[simp] lemma dens_mul_card (s : Finset α) : s.dens * Fintype.card α = s.card := by
  rw [mul_comm, card_mul_dens]

Density-Cardinality Product Identity for Finite Sets

Informal description

For any finite set $s$ in a finite type $\alpha$, the product of the density of $s$ and the cardinality of $\alpha$ equals the cardinality of $s$. That is, $$\text{dens}(s) \cdot |\alpha| = |s|.$$

Finset.natCast_card_mul_nnratCast_dens theorem

(s : Finset α) : (Fintype.card α * s.dens : 𝕜) = s.card

Full source

@[simp] lemma natCast_card_mul_nnratCast_dens (s : Finset α) :
    (Fintype.card α * s.dens : 𝕜) = s.card := mod_cast s.card_mul_dens

Cardinality-Density Product Cast Identity: $(|\alpha| \cdot \text{dens}(s) : \mathfrak{K}) = |s|$

Informal description

For any finite set $s$ in a finite type $\alpha$ and any division semiring $\mathfrak{K}$, the cast of the product of the cardinality of $\alpha$ and the density of $s$ to $\mathfrak{K}$ equals the cardinality of $s$. That is, $$(|\alpha| \cdot \text{dens}(s) : \mathfrak{K}) = |s|.$$

Finset.nnratCast_dens_mul_natCast_card theorem

(s : Finset α) : (s.dens * Fintype.card α : 𝕜) = s.card

Full source

@[simp] lemma nnratCast_dens_mul_natCast_card (s : Finset α) :
    (s.dens * Fintype.card α : 𝕜) = s.card := mod_cast s.dens_mul_card

Density-Cardinality Product Cast Identity: $(s.\text{dens} \cdot |\alpha| : \mathfrak{K}) = |s|$

Informal description

For any finite set $s$ in a finite type $\alpha$ and any division semiring $\mathfrak{K}$, the cast of the product of the density of $s$ and the cardinality of $\alpha$ to $\mathfrak{K}$ equals the cardinality of $s$. That is, $$(s.\text{dens} \cdot |\alpha| : \mathfrak{K}) = |s|.$$

Finset.nnratCast_dens theorem

(s : Finset α) : (s.dens : 𝕜) = s.card / Fintype.card α

Full source

@[norm_cast] lemma nnratCast_dens (s : Finset α) : (s.dens : 𝕜) = s.card / Fintype.card α := by
  simp [dens]

Density Cast Formula: $(s.\text{dens} : \mathfrak{K}) = \frac{|s|}{|\alpha|}$

Informal description

For any finite set $s$ in a finite type $\alpha$, the density of $s$ in $\alpha$, when cast to a division semiring $\mathfrak{K}$, is equal to the ratio of the cardinality of $s$ to the cardinality of $\alpha$. That is, $(s.\text{dens} : \mathfrak{K}) = \frac{|s|}{|\alpha|}$.

Finset.dens_univ theorem

: dens (univ : Finset α) = 1

Full source

@[simp] lemma dens_univ : dens (univ : Finset α) = 1 := by simp [dens, card_univ]

Density of Universal Finite Set is One

Informal description

For any finite type $\alpha$, the density of the universal finite set $\text{univ} : \text{Finset} \alpha$ is equal to $1$, i.e., $\text{dens}(\text{univ}) = 1$.

Finset.dens_eq_one theorem

: dens s = 1 ↔ s = univ

Full source

@[simp] lemma dens_eq_one : densdens s = 1 ↔ s = univ := by
  simp [dens, div_eq_one_iff_eq, card_eq_iff_eq_univ]

Density-One Characterization for Finite Sets: $\text{dens}(s) = 1 \leftrightarrow s = \text{univ}$

Informal description

For any finite set $s$ in a finite type $\alpha$, the density of $s$ equals $1$ if and only if $s$ is the universal set (i.e., contains all elements of $\alpha$). That is, $\text{dens}(s) = 1 \leftrightarrow s = \text{univ}$.

Finset.dens_ne_one theorem

: dens s ≠ 1 ↔ s ≠ univ

Full source

lemma dens_ne_one : densdens s ≠ 1dens s ≠ 1 ↔ s ≠ univ := dens_eq_one.not

Density Inequality: $\text{dens}(s) \neq 1 \leftrightarrow s \neq \text{univ}$

Informal description

For any finite set $s$ in a finite type $\alpha$, the density of $s$ is not equal to $1$ if and only if $s$ is not the universal set (i.e., does not contain all elements of $\alpha$). That is: \[ \text{dens}(s) \neq 1 \leftrightarrow s \neq \text{univ} \] where $\text{dens}(s) = \frac{|s|}{|\alpha|}$ is the density of $s$ in $\alpha$.

Finset.dens_le_one theorem

: s.dens ≤ 1

Full source

@[simp] lemma dens_le_one : s.dens ≤ 1 := by
  cases isEmpty_or_nonempty α
  · simp [Subsingleton.elim s ∅]
  · simpa using dens_le_dens s.subset_univ

Upper Bound on Finite Set Density: $\text{dens}(s) \leq 1$

Informal description

For any finite set $s$ in a finite type $\alpha$, the density of $s$ is at most $1$, i.e., $\text{dens}(s) \leq 1$.

Finset.dens_union_add_dens_inter theorem

(s t : Finset α) : dens (s ∪ t) + dens (s ∩ t) = dens s + dens t

Full source

lemma dens_union_add_dens_inter (s t : Finset α) :
    dens (s ∪ t) + dens (s ∩ t) = dens s + dens t := by
  simp_rw [dens, ← add_div, ← Nat.cast_add, card_union_add_card_inter]

Additivity of Density under Union and Intersection

Informal description

For any two finite sets $s$ and $t$ in a finite type $\alpha$, the sum of the density of their union and the density of their intersection equals the sum of their individual densities. That is: \[ \text{dens}(s \cup t) + \text{dens}(s \cap t) = \text{dens}(s) + \text{dens}(t) \] where $\text{dens}(s) = \frac{|s|}{|\alpha|}$ is the density of $s$ in $\alpha$.

Finset.dens_inter_add_dens_union theorem

(s t : Finset α) : dens (s ∩ t) + dens (s ∪ t) = dens s + dens t

Full source

lemma dens_inter_add_dens_union (s t : Finset α) :
    dens (s ∩ t) + dens (s ∪ t) = dens s + dens t := by rw [add_comm, dens_union_add_dens_inter]

Additivity of Density under Intersection and Union: $\text{dens}(s \cap t) + \text{dens}(s \cup t) = \text{dens}(s) + \text{dens}(t)$

Informal description

For any two finite sets $s$ and $t$ in a finite type $\alpha$, the sum of the density of their intersection and the density of their union equals the sum of their individual densities. That is: \[ \text{dens}(s \cap t) + \text{dens}(s \cup t) = \text{dens}(s) + \text{dens}(t) \] where $\text{dens}(s) = \frac{|s|}{|\alpha|}$ is the density of $s$ in $\alpha$.

Finset.dens_union_of_disjoint theorem

(h : Disjoint s t) : dens (s ∪ t) = dens s + dens t

Full source

@[simp] lemma dens_union_of_disjoint (h : Disjoint s t) : dens (s ∪ t) = dens s + dens t := by
  rw [← disjUnion_eq_union s t h, dens_disjUnion _ _ _]

Additivity of Density for Disjoint Union: $\text{dens}(s \cup t) = \text{dens}(s) + \text{dens}(t)$

Informal description

For any two disjoint finite sets $s$ and $t$ in a finite type $\alpha$, the density of their union equals the sum of their individual densities, i.e., \[ \text{dens}(s \cup t) = \text{dens}(s) + \text{dens}(t), \] where $\text{dens}(s) = \frac{|s|}{|\alpha|}$ is the density of $s$ in $\alpha$.

Finset.dens_sdiff_add_dens_eq_dens theorem

(h : s ⊆ t) : dens (t \ s) + dens s = dens t

Full source

lemma dens_sdiff_add_dens_eq_dens (h : s ⊆ t) : dens (t \ s) + dens s = dens t := by
  simp [dens, ← card_sdiff_add_card_eq_card h, add_div]

Additivity of Density under Set Difference: $\text{dens}(t \setminus s) + \text{dens}(s) = \text{dens}(t)$

Informal description

For any finite sets $s$ and $t$ in a finite type $\alpha$, if $s$ is a subset of $t$, then the sum of the density of the set difference $t \setminus s$ and the density of $s$ equals the density of $t$. That is, \[ \text{dens}(t \setminus s) + \text{dens}(s) = \text{dens}(t). \]

Finset.dens_sdiff_add_dens theorem

(s t : Finset α) : dens (s \ t) + dens t = (s ∪ t).dens

Full source

lemma dens_sdiff_add_dens (s t : Finset α) : dens (s \ t) + dens t = (s ∪ t).dens := by
  rw [← dens_union_of_disjoint sdiff_disjoint, sdiff_union_self_eq_union]

Additivity of Density under Set Difference and Union: $\text{dens}(s \setminus t) + \text{dens}(t) = \text{dens}(s \cup t)$

Informal description

For any two finite sets $s$ and $t$ in a finite type $\alpha$, the sum of the density of the set difference $s \setminus t$ and the density of $t$ equals the density of their union $s \cup t$. That is, \[ \text{dens}(s \setminus t) + \text{dens}(t) = \text{dens}(s \cup t), \] where $\text{dens}(s) = \frac{|s|}{|\alpha|}$ denotes the density of $s$ in $\alpha$.

Finset.dens_sdiff_comm theorem

(h : card s = card t) : dens (s \ t) = dens (t \ s)

Full source

lemma dens_sdiff_comm (h : card s = card t) : dens (s \ t) = dens (t \ s) :=
  add_left_injective (dens t) <| by
    simp_rw [dens_sdiff_add_dens, union_comm s, ← dens_sdiff_add_dens, dens, h]

Density Equality for Set Differences of Equal-Cardinality Finite Sets: $\text{dens}(s \setminus t) = \text{dens}(t \setminus s)$

Informal description

For any two finite sets $s$ and $t$ in a finite type $\alpha$ with equal cardinalities (i.e., $|s| = |t|$), the density of the set difference $s \setminus t$ equals the density of the set difference $t \setminus s$. That is, \[ \text{dens}(s \setminus t) = \text{dens}(t \setminus s), \] where $\text{dens}(s) = \frac{|s|}{|\alpha|}$ denotes the density of $s$ in $\alpha$.

Finset.dens_sdiff_add_dens_inter theorem

(s t : Finset α) : dens (s \ t) + dens (s ∩ t) = dens s

Full source

@[simp]
lemma dens_sdiff_add_dens_inter (s t : Finset α) : dens (s \ t) + dens (s ∩ t) = dens s := by
  rw [← dens_union_of_disjoint (disjoint_sdiff_inter _ _), sdiff_union_inter]

Density Decomposition for Set Difference and Intersection: $\text{dens}(s \setminus t) + \text{dens}(s \cap t) = \text{dens}(s)$

Informal description

For any two finite sets $s$ and $t$ in a finite type $\alpha$, the sum of the density of the set difference $s \setminus t$ and the density of the intersection $s \cap t$ equals the density of $s$. That is, \[ \text{dens}(s \setminus t) + \text{dens}(s \cap t) = \text{dens}(s), \] where $\text{dens}(s) = \frac{|s|}{|\alpha|}$ denotes the density of $s$ in $\alpha$.

Finset.dens_inter_add_dens_sdiff theorem

(s t : Finset α) : dens (s ∩ t) + dens (s \ t) = dens s

Full source

@[simp]
lemma dens_inter_add_dens_sdiff (s t : Finset α) : dens (s ∩ t) + dens (s \ t) = dens s := by
  rw [add_comm, dens_sdiff_add_dens_inter]

Density Decomposition for Intersection and Set Difference: $\text{dens}(s \cap t) + \text{dens}(s \setminus t) = \text{dens}(s)$

Informal description

For any two finite sets $s$ and $t$ in a finite type $\alpha$, the sum of the density of the intersection $s \cap t$ and the density of the set difference $s \setminus t$ equals the density of $s$. That is, \[ \text{dens}(s \cap t) + \text{dens}(s \setminus t) = \text{dens}(s), \] where $\text{dens}(s) = \frac{|s|}{|\alpha|}$ denotes the density of $s$ in $\alpha$.

Finset.dens_filter_add_dens_filter_not_eq_dens theorem

 {α : Type*} [Fintype α] {s : Finset α} (p : α → Prop) [DecidablePred p] [∀ x, Decidable (¬p x)] :
  dens ({a ∈ s | p a}) + dens ({a ∈ s | ¬p a}) = dens s

Full source

lemma dens_filter_add_dens_filter_not_eq_dens {α : Type*} [Fintype α] {s : Finset α}
    (p : α → Prop) [DecidablePred p] [∀ x, Decidable (¬p x)] :
    dens {a ∈ s | p a} + dens {a ∈ s | ¬ p a} = dens s := by
  classical
  rw [← dens_union_of_disjoint (disjoint_filter_filter_neg ..), filter_union_filter_neg_eq]

Density Decomposition for Filtered Finite Sets: $\text{dens}(s \cap p) + \text{dens}(s \cap \neg p) = \text{dens}(s)$

Informal description

For any finite type $\alpha$, finite set $s \subseteq \alpha$, and decidable predicate $p$ on $\alpha$ (with decidable negation), the sum of the densities of the subsets $\{a \in s \mid p(a)\}$ and $\{a \in s \mid \neg p(a)\}$ equals the density of $s$. That is, \[ \text{dens}(\{a \in s \mid p(a)\}) + \text{dens}(\{a \in s \mid \neg p(a)\}) = \text{dens}(s), \] where $\text{dens}(s) = \frac{|s|}{|\alpha|}$ is the density of $s$ in $\alpha$.

Finset.dens_union_le theorem

(s t : Finset α) : dens (s ∪ t) ≤ dens s + dens t

Full source

lemma dens_union_le (s t : Finset α) : dens (s ∪ t) ≤ dens s + dens t :=
  dens_union_add_dens_inter s t ▸ le_add_of_nonneg_right zero_le'

Subadditivity of Density under Union: $\text{dens}(s \cup t) \leq \text{dens}(s) + \text{dens}(t)$

Informal description

For any two finite sets $s$ and $t$ in a finite type $\alpha$, the density of their union satisfies the inequality: \[ \text{dens}(s \cup t) \leq \text{dens}(s) + \text{dens}(t), \] where $\text{dens}(s) = \frac{|s|}{|\alpha|}$ denotes the density of $s$ in $\alpha$.

Finset.dens_le_dens_sdiff_add_dens theorem

: dens s ≤ dens (s \ t) + dens t

Full source

lemma dens_le_dens_sdiff_add_dens : dens s ≤ dens (s \ t) + dens t :=
  dens_sdiff_add_dens s _ ▸ dens_le_dens subset_union_left

Density Inequality for Set Difference and Union: $\text{dens}(s) \leq \text{dens}(s \setminus t) + \text{dens}(t)$

Informal description

For any finite sets $s$ and $t$ in a finite type $\alpha$, the density of $s$ is less than or equal to the sum of the density of the set difference $s \setminus t$ and the density of $t$. That is, \[ \text{dens}(s) \leq \text{dens}(s \setminus t) + \text{dens}(t), \] where $\text{dens}(s) = \frac{|s|}{|\alpha|}$ denotes the density of $s$ in $\alpha$.

Finset.dens_sdiff theorem

(h : s ⊆ t) : dens (t \ s) = dens t - dens s

Full source

lemma dens_sdiff (h : s ⊆ t) : dens (t \ s) = dens t - dens s :=
  eq_tsub_of_add_eq (dens_sdiff_add_dens_eq_dens h)

Density of Set Difference Equals Difference of Densities

Informal description

For any finite sets $s$ and $t$ in a finite type $\alpha$, if $s$ is a subset of $t$, then the density of the set difference $t \setminus s$ is equal to the difference between the density of $t$ and the density of $s$. That is, \[ \text{dens}(t \setminus s) = \text{dens}(t) - \text{dens}(s). \]

Finset.le_dens_sdiff theorem

(s t : Finset α) : dens t - dens s ≤ dens (t \ s)

Full source

lemma le_dens_sdiff (s t : Finset α) : dens t - dens s ≤ dens (t \ s) :=
  tsub_le_iff_right.2 dens_le_dens_sdiff_add_dens

Density Difference Inequality: $\text{dens}(t) - \text{dens}(s) \leq \text{dens}(t \setminus s)$

Informal description

For any finite sets $s$ and $t$ in a finite type $\alpha$, the difference between the density of $t$ and the density of $s$ is less than or equal to the density of the set difference $t \setminus s$. That is, \[ \text{dens}(t) - \text{dens}(s) \leq \text{dens}(t \setminus s), \] where $\text{dens}(s) = \frac{|s|}{|\alpha|}$ denotes the density of $s$ in $\alpha$.