Equitable functions

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 SuccOrder + ConditionallyCompleteMonoid, but we don't have the latter yet.

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

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

@[simp]

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

theorem Set.equitableOn_iff_exists_le_le_add_one {α : Type u_1} {s : Set α} {f : α → ℕ} : s.EquitableOn f ↔ ∃ (b : ℕ), ∀ a ∈ s, b ≤ f a ∧ f a ≤ b + 1

theorem Set.equitableOn_iff_exists_image_subset_icc {α : Type u_1} {s : Set α} {f : α → ℕ} : s.EquitableOn f ↔ ∃ (b : ℕ), f '' s ⊆ Icc b (b + 1)

theorem Set.equitableOn_iff_exists_eq_eq_add_one {α : Type u_1} {s : Set α} {f : α → ℕ} : s.EquitableOn f ↔ ∃ (b : ℕ), ∀ a ∈ s, f a = b ∨ f a = b + 1

@[simp]

theorem Set.not_equitableOn {α : Type u_1} {β : Type u_2} [LinearOrder β] [Add β] [One β] {s : Set α} {f : α → β} : ¬s.EquitableOn f ↔ ∃ a ∈ s, ∃ b ∈ s, f b + 1 < f a

theorem Set.Subsingleton.equitableOn {α : Type u_1} {β : Type u_2} [Semiring β] [PartialOrder β] [IsOrderedRing β] {s : Set α} (hs : s.Subsingleton) (f : α → β) : s.EquitableOn f

theorem Set.equitableOn_singleton {α : Type u_1} {β : Type u_2} [Semiring β] [PartialOrder β] [IsOrderedRing β] (a : α) (f : α → β) : {a}.EquitableOn f

theorem Finset.equitableOn_iff_le_le_add_one {α : Type u_1} {s : Finset α} {f : α → ℕ} : (↑s).EquitableOn f ↔ ∀ a ∈ s, (∑ i ∈ s, f i) / s.card ≤ f a ∧ f a ≤ (∑ i ∈ s, f i) / s.card + 1

theorem Finset.EquitableOn.le {α : Type u_1} {s : Finset α} {f : α → ℕ} {a : α} (h : (↑s).EquitableOn f) (ha : a ∈ s) : (∑ i ∈ s, f i) / s.card ≤ f a

theorem Finset.EquitableOn.le_add_one {α : Type u_1} {s : Finset α} {f : α → ℕ} {a : α} (h : (↑s).EquitableOn f) (ha : a ∈ s) : f a ≤ (∑ i ∈ s, f i) / s.card + 1

theorem Finset.equitableOn_iff {α : Type u_1} {s : Finset α} {f : α → ℕ} : (↑s).EquitableOn f ↔ ∀ a ∈ s, f a = (∑ i ∈ s, f i) / s.card ∨ f a = (∑ i ∈ s, f i) / s.card + 1