Rolle's theorem for finitely many zeros

Rolle's theorem places a zero of f' strictly between any two zeros of a function f : ℝ → ℝ continuous between them. Applied to consecutive points of a finite set Z of zeros of f, it gives a set of #Z - 1 zeros of f' separating the points of Z (TauCeti.exists_finset_deriv_eq_zero). Iterating along a sequence of functions, each the derivative of the previous one, a finite set of zeros of f has at most k more points than some finite set of zeros of the k-th function (TauCeti.exists_card_le_card_add_of_hasDerivAt).

This is how one counts the real zeros of a function by repeatedly differentiating it, as in the zero estimate for real exponential polynomials ∑ pₖ(x) exp(γₖ x).

Main results

• TauCeti.exists_finset_deriv_eq_zero: a nonempty finite set Z of zeros of f, continuous on [min Z, max Z], is separated by a set of #Z - 1 zeros of deriv f.
• TauCeti.exists_card_le_card_add_of_hasDerivAt: if F (n + 1) is the derivative of F n for n < k, a finite set Z of zeros of F 0 gives a finite set Z' of zeros of F k with #Z ≤ #Z' + k.

References

• J.-H. Evertse, Diophantine Approximation, lecture notes (2019), ch. 4, §4.4, Exercise 4.5.

theorem TauCeti.exists_finset_deriv_eq_zero {f : ℝ → ℝ} {Z : Finset ℝ} (hZ : Z.Nonempty) (hf : ContinuousOn f (Set.Icc (Z.min' hZ) (Z.max' hZ))) (hfZ : ∀ x ∈ Z, f x = 0) : ∃ (Z' : Finset ℝ), Z'.card + 1 = Z.card ∧ (∀ z ∈ Z', deriv f z = 0) ∧ (∀ z ∈ Z', ∃ x ∈ Z, ∃ y ∈ Z, x < z ∧ z < y) ∧ ∀ x ∈ Z, ∀ y ∈ Z, x < y → ∃ z ∈ Z', x < z ∧ z < y

Rolle's theorem for finitely many zeros. If a function f : ℝ → ℝ, continuous between the smallest and largest points of a nonempty finite set Z, vanishes on Z, then deriv f vanishes on a finite set Z' with one point fewer that separates the points of Z: every point of Z' lies strictly between two points of Z, and strictly between any two points of Z lies a point of Z'.

theorem TauCeti.exists_card_le_card_add_of_hasDerivAt {F : ℕ → ℝ → ℝ} {k : ℕ} (hF : ∀ n < k, ∀ (x : ℝ), HasDerivAt (F n) (F (n + 1) x) x) {Z : Finset ℝ} (hZ : ∀ x ∈ Z, F 0 x = 0) : ∃ (Z' : Finset ℝ), (∀ x ∈ Z', F k x = 0) ∧ Z.card ≤ Z'.card + k

Iterated Rolle's theorem. Let F (n + 1) be the derivative of F n for every n < k. Then every finite set Z of zeros of F 0 has at most k more points than some finite set of zeros of F k.