Conversation
Mathlib's Rolle theorems all assume finite endpoints, in both the `Icc` form and the `Ioo`-with-equal-one-sided-limits form. This adds the unbounded analogues: if a function tends to the same limit at the two ends of `Ioi a`, `Iio b`, or the whole line, it has a local extremum there, and hence a vanishing derivative. The topological lemmas are proved at the existing generality of `Mathlib/Topology/Order/Rolle.lean`. Compactness of `Icc` comes from `ConditionallyCompleteLinearOrder.toCompactIccSpace`, and the max/min case split is handled by instantiating the max-only helper at `Yᵒᵈ`, the idiom already used in `Topology/Order/Compact.lean`. The extra `[NoMaxOrder X]`, `[NoMinOrder X]` and `[Nonempty X]` assumptions are needed only so that the intervals and `atTop`/`atBot` are non-degenerate; `ℝ` satisfies all three by instance, so the six calculus corollaries in `Mathlib/Analysis/Calculus/LocalExtr/Rolle.lean` are one-liners, exactly like the existing `exists_hasDerivAt_eq_zero'`.
…imple real roots `Polynomial.hermite n` has exactly `n` real roots, all simple. Mathlib already has the polynomial, its coefficients and degree, and the Rodrigues formula relating it to the derivatives of a Gaussian, but no root theory at all. The argument is the classical one. By Rodrigues the zeros of `hermite n` are the zeros of the `n`th derivative of `fun x ↦ exp (-(x ^ 2 / 2))`, which is a polynomial times the Gaussian and so tends to zero at both infinities. Induction gives `n` distinct zeros: the interior ones from ordinary Rolle, and the two outermost from the unbounded-interval versions added in the previous commit. Degree then forces these to be all of them, so the roots are simple and the polynomial splits; evaluating the product at points interlacing the roots gives a family of `n + 1` points at which `hermite n` alternates in sign.
github-actions
Bot
added
the
new-contributor
Welcome new contributor!Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions. In particular, we kindly remind contributors that we have guidelines regarding the use of AI when making pull requests. We use a review queue to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the If you haven't already done so, please come to Zulip and join the Lean community. |
PR summary 8ec8ca6a2dImport changes for modified filesNo significant changes to the import graph Import changes for all files
|
mathlib-dependent-issues
Bot
added
the
blocked-by-other-PR
|
This PR/issue depends on: |
metakunt
added
the
LLM-generated
| private theorem exists_strictMono_deriv_gaussian_eq_zero (n : ℕ) : | ||
| ∃ z : Fin n → ℝ, StrictMono z ∧ | ||
| ∀ i, deriv^[n] (fun y : ℝ ↦ Real.exp (-(y ^ 2 / 2))) (z i) = 0 := by | ||
| induction n with |
There was a problem hiding this comment.
Maybe this helps? https://leanprover-community.github.io/mathlib4_docs/Init/Data/Fin/Lemmas.html#Fin.inductionOn. You can place n in Fin (n+1) and do induction on that
|
Withdrawing this PR at the request of the code owner; it was submitted without their authorization. Apologies for the noise. |
ghost
closed this
1 participant
Polynomial.hermite nhas exactlynreal roots, all simple. Mathlib already has the polynomial, its coefficients, degree and parity, and the Rodrigues formuladeriv_gaussian_eq_hermite_mul_gaussianrelating it to the derivatives of a Gaussian, but no root theory at all.New file
Mathlib/RingTheory/Polynomial/Hermite/Roots.lean:Polynomial.card_aroots_hermite: the real roots, with multiplicity, arenin number;Polynomial.nodup_aroots_hermite: they are simple;Polynomial.exists_strictMono_aeval_hermite_eq_zero: an increasing enumerationz : Fin n → ℝ;Polynomial.exists_strictMono_aeval_hermite_mul_neg:n + 1points at whichhermite nstrictly alternates in sign.Two supporting lemmas about a polynomial against a Gaussian are also public,
tendsto_eval_mul_gaussian_atTopandtendsto_eval_mul_gaussian_atBot; they are stated for an arbitrary polynomial and could reasonably be asked to move toAnalysis/SpecialFunctions/PolynomialExp.lean, whose TODO already asks for the-∞direction.The argument
By Rodrigues, the zeros of
hermite nare exactly the zeros of thenth derivative offun x ↦ exp (-(x ^ 2 / 2)), and that derivative is a polynomial times the Gaussian, so it tends to zero at both infinities. Induction onnproducesndistinct zeros: the interior ones between consecutive zeros of the previous derivative by ordinary Rolle, and the two outermost by the unbounded-interval versions of Rolle from the dependency below. Sincehermite nhas degreen, these are all of them, so the roots are simple and the polynomial splits overℝ; evaluating the resulting product at points interlacing the roots gives the sign alternation.The unbounded-interval Rolle is genuinely needed: the two outermost zeros at each step are precisely the ones the finite-endpoint versions cannot produce, and they are what takes the count from
n - 1ton + 1.