Change counts and sorted groups

This file proves the discrete one-dimensional lemmas of the capacity method.

• changesAtMost_of_piecesAtMost_internal: a function with at most M pieces changes at most M - 1 times along every nondecreasing sequence.
• card_nonconstant_groups_le_internal: cut the positions into consecutive groups of L; a function with at most T changes along a nondecreasing sequence is nonconstant on at most T groups, since every such group contains a change position, and distinct groups contain distinct positions.
• exists_sorted_group_internal (Lemma 1): sort P by a real key α and cut it into G consecutive groups of ⌊|P| / G⌋ elements. If each Ψ q changes at most T times, double counting gives a group on which at most T |Q| / G of the functions p ↦ Ψ q (α p) are nonconstant.

theorem Algebraic.Threshold.ChangesAtMost.mono {β : Type u_1} {Ψ : ℝ → β} {T T' : ℕ} (h : ChangesAtMost Ψ T) (hT : T ≤ T') : ChangesAtMost Ψ T'

theorem Algebraic.Threshold.ChangesAtMost.comp_add_const {β : Type u_1} {Ψ : ℝ → β} {T : ℕ} (h : ChangesAtMost Ψ T) (c : ℝ) : ChangesAtMost (fun (t : ℝ) => Ψ (t + c)) T

Translating the argument keeps the change bound.

theorem Algebraic.Threshold.PiecesAtMost.mono {β : Type u_1} {Φ : ℝ → β} {M M' : ℕ} (h : PiecesAtMost Φ M) (hM : M ≤ M') : PiecesAtMost Φ M'

theorem Algebraic.Threshold.PiecesAtMost.comp {β : Type u_1} {γ : Type u_2} {Φ : ℝ → β} {M : ℕ} (h : PiecesAtMost Φ M) (g : β → γ) : PiecesAtMost (fun (t : ℝ) => g (Φ t)) M

Post-composition keeps the pieces.

theorem Algebraic.Threshold.changesAtMost_of_piecesAtMost_internal {β : Type u_1} {Φ : ℝ → β} {M : ℕ} (h : PiecesAtMost Φ M) : ChangesAtMost Φ (M - 1)

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

theorem Algebraic.Threshold.eq_of_forall_not_change {β : Type u_1} {s : ℕ → β} {a m : ℕ} (h : ∀ (c : ℕ), a ≤ c → c < a + m → s c = s (c + 1)) (j : ℕ) : j ≤ m → s (a + j) = s a

Without a change in [a, a + m), a sequence is constant on [a, a + m].

theorem Algebraic.Threshold.card_nonconstant_groups_le_internal {β : Type u_1} {Ψ : ℝ → β} {T : ℕ} (h : ChangesAtMost Ψ T) {z : ℕ → ℝ} (hz : Monotone z) (L G : ℕ) : {g ∈ Finset.range G | ∃ j < L, ∃ j' < L, Ψ (z (g * L + j)) ≠ Ψ (z (g * L + j'))}.card ≤ T

Each function is nonconstant on few groups. Cut the positions into consecutive groups of L. A function with at most T changes along the nondecreasing sequence z is nonconstant on at most T of the first G groups.

theorem Algebraic.Threshold.exists_sorted_group_internal {β : Type u_1} {ι : Type u_2} {κ : Type u_3} (P : Finset ι) (Q : Finset κ) (α : ι → ℝ) (Ψ : κ → ℝ → β) {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 (α p) = Ψ q (α p')

Lemma 1 (sorted groups). Sort P by the real 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 (α p) are constant on P' for every q ∈ Q outside a set Qbad with G |Qbad| ≤ T |Q|.