mathlib3 documentation

data.set.equitable

Equitable functions #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines equitable functions.

A function f is equitable on a set s if f a₁ ≤ f a₂ + 1 for all a₁, a₂ ∈ s. This is mostly useful when the codomain of f is ℕ or ℤ (or more generally a successor order).

TODO #

ℕ can be replaced by any succ_order + conditionally_complete_monoid, but we don't have the latter yet.

source
def set.equitable_on {α : Type u_1} {β : Type u_2} [has_le β] [has_add β] [has_one β] (s : set α) (f : α → β) :
Prop

A set is equitable if no element value is more than one bigger than another.

Equations
source
@[simp]
theorem set.equitable_on_empty {α : Type u_1} {β : Type u_2} [has_le β] [has_add β] [has_one β] (f : α → β) :
∅.equitable_on f
source
theorem set.equitable_on_iff_exists_le_le_add_one {α : Type u_1} {s : set α} {f : α → ℕ} :
s.equitable_on f ↔ ∃ (b : ℕ), ∀ (a : α), a ∈ s → b ≤ f a ∧ f a ≤ b + 1
source
theorem set.equitable_on_iff_exists_image_subset_Icc {α : Type u_1} {s : set α} {f : α → ℕ} :
s.equitable_on f ↔ ∃ (b : ℕ), f '' s ⊆ set.Icc b (b + 1)
source
theorem set.equitable_on_iff_exists_eq_eq_add_one {α : Type u_1} {s : set α} {f : α → ℕ} :
s.equitable_on f ↔ ∃ (b : ℕ), ∀ (a : α), a ∈ s → f a = b ∨ f a = b + 1
source
theorem set.subsingleton.equitable_on {α : Type u_1} {β : Type u_2} [ordered_semiring β] {s : set α} (hs : s.subsingleton) (f : α → β) :
s.equitable_on f
source
theorem set.equitable_on_singleton {α : Type u_1} {β : Type u_2} [ordered_semiring β] (a : α) (f : α → β) :
{a}.equitable_on f
source
theorem finset.equitable_on_iff_le_le_add_one {α : Type u_1} {s : finset α} {f : α → ℕ} :
↑s.equitable_on f ↔ ∀ (a : α), a ∈ s → s.sum (λ (i : α), f i) / s.card ≤ f a ∧ f a ≤ s.sum (λ (i : α), f i) / s.card + 1
source
theorem finset.equitable_on.le {α : Type u_1} {s : finset α} {f : α → ℕ} {a : α} (h : ↑s.equitable_on f) (ha : a ∈ s) :
s.sum (λ (i : α), f i) / s.card ≤ f a
source
theorem finset.equitable_on.le_add_one {α : Type u_1} {s : finset α} {f : α → ℕ} {a : α} (h : ↑s.equitable_on f) (ha : a ∈ s) :
f a ≤ s.sum (λ (i : α), f i) / s.card + 1
source
theorem finset.equitable_on_iff {α : Type u_1} {s : finset α} {f : α → ℕ} :
↑s.equitable_on f ↔ ∀ (a : α), a ∈ s → f a = s.sum (λ (i : α), f i) / s.card ∨ f a = s.sum (λ (i : α), f i) / s.card + 1