Equitable functions #

This file defines equitable functions.

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

TODO #

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

source

ink

def Set.EquitableOn {α : Type u_1} {β : Type u_2} [inst : LE β] [inst : Add β] [inst : One β] (s : Set α) (f : α → β) :

Prop

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

Equations

Set.EquitableOn s f = ∀ ⦃a₁ a₂ : α⦄, a₁ ∈ s → a₂ ∈ s → f a₁ ≤ f a₂ + 1

source

ink

@[simp]

theorem Set.equitableOn_empty {α : Type u_2} {β : Type u_1} [inst : LE β] [inst : Add β] [inst : One β] (f : α → β) :

Set.EquitableOn ∅ f

source

ink

theorem Set.equitableOn_iff_exists_le_le_add_one {α : Type u_1} {s : Set α} {f : α → ℕ} :

Set.EquitableOn s f ↔ ∃ b, ∀ (a : α), a ∈ s → b ≤ f a ∧ f a ≤ b + 1

source

ink

theorem Set.equitableOn_iff_exists_image_subset_icc {α : Type u_1} {s : Set α} {f : α → ℕ} :

Set.EquitableOn s f ↔ ∃ b, f '' s ⊆ Set.Icc b (b + 1)

source

ink

theorem Set.equitableOn_iff_exists_eq_eq_add_one {α : Type u_1} {s : Set α} {f : α → ℕ} :

Set.EquitableOn s f ↔ ∃ b, ∀ (a : α), a ∈ s → f a = b ∨ f a = b + 1

source

ink

theorem Set.Subsingleton.equitableOn {α : Type u_1} {β : Type u_2} [inst : OrderedSemiring β] {s : Set α} (hs : Set.Subsingleton s) (f : α → β) :

Set.EquitableOn s f

source

ink

theorem Set.equitableOn_singleton {α : Type u_1} {β : Type u_2} [inst : OrderedSemiring β] (a : α) (f : α → β) :

Set.EquitableOn {a} f

source

ink

theorem Finset.equitableOn_iff_le_le_add_one {α : Type u_1} {s : Finset α} {f : α → ℕ} :

Set.EquitableOn (↑s) f ↔ ∀ (a : α), a ∈ s → (Finset.sum s fun i => f i) / Finset.card s ≤ f a ∧ f a ≤ (Finset.sum s fun i => f i) / Finset.card s + 1

source

ink

theorem Finset.EquitableOn.le {α : Type u_1} {s : Finset α} {f : α → ℕ} {a : α} (h : Set.EquitableOn (↑s) f) (ha : a ∈ s) :

(Finset.sum s fun i => f i) / Finset.card s ≤ f a

source

ink

theorem Finset.EquitableOn.le_add_one {α : Type u_1} {s : Finset α} {f : α → ℕ} {a : α} (h : Set.EquitableOn (↑s) f) (ha : a ∈ s) :

f a ≤ (Finset.sum s fun i => f i) / Finset.card s + 1

source

ink

theorem Finset.equitableOn_iff {α : Type u_1} {s : Finset α} {f : α → ℕ} :

Set.EquitableOn (↑s) f ↔ ∀ (a : α), a ∈ s → f a = (Finset.sum s fun i => f i) / Finset.card s ∨ f a = (Finset.sum s fun i => f i) / Finset.card s + 1