Change counts, piece counts, and sorted groups

A function has at most T changes when every nondecreasing sequence has at most T adjacent positions with unequal outputs, and at most M pieces when it is constant on the level sets of a monotone rank function with values below M. Sorting a finite set by a key and splitting it into consecutive groups yields a large group on which most functions in a finite family are constant. The key may have ties, and the size bound uses natural-number division.

Main definitions

• Cslib.ChangesAtMost: a uniform bound on changes along nondecreasing sequences.
• Cslib.PiecesAtMost: a function constant on the level sets of a monotone rank function with values below M.

Main results

• Cslib.ChangesAtMost.comp_antitone: antitone precomposition preserves a change bound.
• Cslib.ChangesAtMost.pi, Cslib.ChangesAtMost.finset_pi: a finite tuple of functions changes at most the sum of the coordinate change bounds.
• Cslib.PiecesAtMost.changesAtMost: a function with at most M pieces changes at most M - 1 times.
• Cslib.ChangesAtMost.exists_sorted_group: a group of at least |P| / G points, with at most T |Q| / G exceptional functions.

References

• [S. Schlesinger, Algebraic circuit formalizations in Complexitylib, Threshold/Internal/Changes] [Sch26a]

def Cslib.ChangesAtMost {α : Type u_1} {β : Type u_2} [Preorder α] (f : α → β) (T : ℕ) : Prop

Every nondecreasing sequence has at most T adjacent changes under f.

theorem Cslib.ChangesAtMost.mono {α : Type u_1} {β : Type u_2} [Preorder α] {f : α → β} {T T' : ℕ} (h : ChangesAtMost f T) (hT : T ≤ T') : ChangesAtMost f T'

Increasing a change bound preserves it.

theorem Cslib.ChangesAtMost.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Preorder α] {f : α → β} {T : ℕ} (h : ChangesAtMost f T) (g : β → γ) : ChangesAtMost (g ∘ f) T

Post-composition preserves a change bound.

theorem Cslib.ChangesAtMost.comp_monotone {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Preorder α] [Preorder γ] {f : α → β} {T : ℕ} (h : ChangesAtMost f T) {g : γ → α} (hg : Monotone g) : ChangesAtMost (f ∘ g) T

Monotone precomposition preserves a change bound.

theorem Cslib.ChangesAtMost.comp_antitone {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Preorder α] [Preorder γ] {f : α → β} {T : ℕ} (h : ChangesAtMost f T) {g : γ → α} (hg : Antitone g) : ChangesAtMost (f ∘ g) T

Antitone precomposition preserves a change bound.

theorem Cslib.ChangesAtMost.const {α : Type u_1} {β : Type u_2} [Preorder α] (b : β) : ChangesAtMost (fun (x : α) => b) 0

A constant function has no changes.

theorem Cslib.ChangesAtMost.pi {α : Type u_1} [Preorder α] {ι : Type u_4} [Fintype ι] {β : ι → Type u_5} {f : (i : ι) → α → β i} {T : ι → ℕ} (hf : ∀ (i : ι), ChangesAtMost (f i) (T i)) : ChangesAtMost (fun (a : α) (i : ι) => f i a) (∑ i : ι, T i)

A tuple of functions indexed by a finite type changes at most the sum of the individual change bounds.

theorem Cslib.ChangesAtMost.finset_pi {α : Type u_1} [Preorder α] {ι : Type u_4} {s : Finset ι} {β : ι → Type u_5} {f : (i : ι) → α → β i} {T : ι → ℕ} (hf : ∀ i ∈ s, ChangesAtMost (f i) (T i)) : ChangesAtMost (fun (a : α) (i : ↥s) => f (↑i) a) (∑ i ∈ s, T i)

A tuple of functions indexed by a finite set changes at most the sum of the individual change bounds.

def Cslib.PiecesAtMost {α : Type u_1} {β : Type u_2} [Preorder α] (Φ : α → β) (M : ℕ) : Prop

Φ has at most M pieces when it is constant on the level sets of a monotone rank function π : α → ℕ with values below M.

theorem Cslib.PiecesAtMost.mono {α : Type u_1} {β : Type u_2} [Preorder α] {Φ : α → β} {M M' : ℕ} (h : PiecesAtMost Φ M) (hM : M ≤ M') : PiecesAtMost Φ M'

Increasing a piece bound preserves it.

theorem Cslib.PiecesAtMost.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Preorder α] {Φ : α → β} {M : ℕ} (h : PiecesAtMost Φ M) (g : β → γ) : PiecesAtMost (fun (t : α) => g (Φ t)) M

Post-composition preserves a piece bound.

theorem Cslib.PiecesAtMost.changesAtMost {α : Type u_1} {β : Type u_2} [Preorder α] {Φ : α → β} {M : ℕ} (h : PiecesAtMost Φ M) : ChangesAtMost Φ (M - 1)

A function with at most M pieces changes at most M - 1 times.

theorem Cslib.ChangesAtMost.exists_sorted_group {α : Type u_1} {β : Type u_2} [LinearOrder α] {ι : Type u_4} {κ : Type u_5} (P : Finset ι) (Q : Finset κ) (key : ι → α) (Ψ : κ → α → β) {T G : ℕ} (hG : 0 < G) (hΨ : ∀ q ∈ Q, ChangesAtMost (Ψ q) T) : ∃ P' ⊆ P, ∃ Qbad ⊆ Q, P.card / G ≤ P'.card ∧ G * Qbad.card ≤ T * Q.card ∧ ∀ q ∈ Q, q ∉ Qbad → ∀ p ∈ P', ∀ p' ∈ P', Ψ q (key p) = Ψ q (key p')

Lemma 1 (sorted groups). Sort P by the key key and cut it into G consecutive groups of ⌊|P| / G⌋ elements. If every Ψ q changes at most T times, some group P' is such that the functions p ↦ Ψ q (key p) are constant on P' for every q ∈ Q outside a set Qbad with G |Qbad| ≤ T |Q|.