Density of a finite set #
This defines the density of a Finset and provides induction principles for finsets.
Main declarations #
Finset.dens t:dens s : ℕreturns the density ofs : Finset α.
Notation #
If you need to specify the field the density is valued in, dens[𝕜] s is notation for
(dens s : 𝕜). Note that no dot notation is allowed.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Finset.card_div_card_eq_dens
{𝕜 : Type u_1}
{α : Type u_2}
[Fintype α]
[Semifield 𝕜]
(s : Finset α)
:
s.dens = ↑s.card / ↑(Fintype.card α)
@[simp]
theorem
Finset.dens_singleton
{𝕜 : Type u_1}
{α : Type u_2}
[Fintype α]
[Semifield 𝕜]
(a : α)
:
{a}.dens = (↑(Fintype.card α))⁻¹
@[simp]
theorem
Finset.dens_cons
{𝕜 : Type u_1}
{α : Type u_2}
[Fintype α]
[Semifield 𝕜]
{s : Finset α}
{a : α}
(h : a ∉ s)
:
(Finset.cons a s h).dens = s.dens + (↑(Fintype.card α))⁻¹
theorem
Finset.dens_sdiff_comm
{𝕜 : Type u_1}
{α : Type u_2}
[Fintype α]
[Semifield 𝕜]
{s : Finset α}
{t : Finset α}
[DecidableEq α]
[IsCancelAdd 𝕜]
(h : s.card = t.card)
:
theorem
Finset.dens_filter_add_dens_filter_not_eq_dens
{𝕜 : Type u_1}
{α : Type u_2}
[Fintype α]
[Semifield 𝕜]
{s : Finset α}
[DecidableEq α]
(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.Nonempty.dens_ne_zero
{𝕜 : Type u_1}
{α : Type u_2}
[Fintype α]
[Semifield 𝕜]
{s : Finset α}
[CharZero 𝕜]
:
s.Nonempty → s.dens ≠ 0
Alias of the reverse direction of Finset.dens_ne_zero.
@[simp]
theorem
Finset.dens_nonneg
{𝕜 : Type u_1}
{α : Type u_2}
[Fintype α]
[LinearOrderedSemifield 𝕜]
{s : Finset α}
:
0 ≤ s.dens
theorem
Finset.dens_le_dens
{𝕜 : Type u_1}
{α : Type u_2}
[Fintype α]
[LinearOrderedSemifield 𝕜]
{s : Finset α}
{t : Finset α}
(h : s ⊆ t)
:
s.dens ≤ t.dens
theorem
Finset.dens_lt_dens
{𝕜 : Type u_1}
{α : Type u_2}
[Fintype α]
[LinearOrderedSemifield 𝕜]
{s : Finset α}
{t : Finset α}
(h : s ⊂ t)
:
s.dens < t.dens
theorem
Finset.dens_mono
{𝕜 : Type u_1}
{α : Type u_2}
[Fintype α]
[LinearOrderedSemifield 𝕜]
:
Monotone Finset.dens
theorem
Finset.dens_strictMono
{𝕜 : Type u_1}
{α : Type u_2}
[Fintype α]
[LinearOrderedSemifield 𝕜]
:
StrictMono Finset.dens
theorem
Finset.dens_map_le
{𝕜 : Type u_1}
{α : Type u_2}
{β : Type u_3}
[Fintype α]
[LinearOrderedSemifield 𝕜]
{s : Finset α}
[Fintype β]
(f : α ↪ β)
:
(Finset.map f s).dens ≤ s.dens
theorem
Finset.dens_union_le
{𝕜 : Type u_1}
{α : Type u_2}
[Fintype α]
[LinearOrderedSemifield 𝕜]
[DecidableEq α]
(s : Finset α)
(t : Finset α)
:
theorem
Finset.dens_le_dens_sdiff_add_dens
{𝕜 : Type u_1}
{α : Type u_2}
[Fintype α]
[LinearOrderedSemifield 𝕜]
{s : Finset α}
{t : Finset α}
[DecidableEq α]
:
theorem
Finset.dens_sdiff
{𝕜 : Type u_1}
{α : Type u_2}
[Fintype α]
[LinearOrderedSemifield 𝕜]
{s : Finset α}
{t : Finset α}
[DecidableEq α]
[Sub 𝕜]
[OrderedSub 𝕜]
(h : s ⊆ t)
:
theorem
Finset.le_dens_sdiff
{𝕜 : Type u_1}
{α : Type u_2}
[Fintype α]
[LinearOrderedSemifield 𝕜]
[DecidableEq α]
[Sub 𝕜]
[OrderedSub 𝕜]
(s : Finset α)
(t : Finset α)
:
@[simp]
theorem
Finset.dens_pos
{𝕜 : Type u_1}
{α : Type u_2}
[Fintype α]
[LinearOrderedSemifield 𝕜]
{s : Finset α}
[CharZero 𝕜]
:
theorem
Finset.Nonempty.dens_pos
{𝕜 : Type u_1}
{α : Type u_2}
[Fintype α]
[LinearOrderedSemifield 𝕜]
{s : Finset α}
[CharZero 𝕜]
:
s.Nonempty → 0 < s.dens
Alias of the reverse direction of Finset.dens_pos.