Odd and even functions

Stream: new members

[Luke Mantle]

I have been working on some definitions and properties of the Hermite polynomials. I have defined them as polynomials with a recursive relation, and as a function involving the nth derivative of a gaussian, and have shown these definitions are equivalent. One of the properties I would like to show is that the nth hermite polynomial is odd or even, depending on n. I was expecting that odd and even funcitons would already be well-established in mathlib, but when I looked around, the best I could find is this discussion where someone was asking what would be the best way to define even and odd functions to be used as part of something else they were working on: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Level.20of.20Generality.20while.20Contributing/near/276689504

Is there indeed no existing definition of even and odd functions, and if so, what's the best way to go about defining them in my case?

[Eric Wieser]

Usually, to state that a function foo is even you'd write @[simp] lemma foo_neg : foo (-x) = foo x, and similarly for odd

[Jireh Loreaux]

Eric, that's not the definition you want for polynomials though, because that would involve conflating the polynomial with its evaluation function.

[Eric Wieser]

I was tricked by the request for "even functions"!

[Eric Wieser]

I still think that proving (hermite n).eval (- x) = (hermite n).eval x and (hermite n).eval (- x) = -(hermite n).eval x and making them simp lemmas is likely all that's really needed here if the focus is just "prove the function is even"

[Jireh Loreaux]

Yeah, it could suffice for now. Probably in this circumstance that's all one might want. The weird thing is just that you can prove lemmas like that for certain polynomials without the requirement that the corresponding polynomial be even or odd (i.e., that the coefficients of odd, respectively even, degree terms are zero). For instance, when the ring has characteristic two.

[Eric Wieser]

Right, the strictly accurate statement would be (hermite n).eval (-X) = hermite n (for even-ness), I assume?

[Kevin Buzzard]

That's still always true in characteristic 2. There's a naive notion of evenness which is always true in char 2 and a stronger one saying all coefficients of all X^(2n+1) are zero. My understanding of Hermite polynomials is that they're in Z[X] so the lowbrow definition will suffice here.

[Moritz Doll]

slightly off-topic: @Luke Mantle it's great to hear that you work on Hermite functions. If you want to PR your work to mathlib (which I would highly recommend), then you probably want to start with smaller pieces. The definition and the fact that they are given by the iterated derivative of $e^{-x^2/2}$ might be enough. The PR process takes a bit getting used to, so it is less frustrating when the PR is not too big.

[Luke Mantle]

@Moritz Doll I do have a lemmas that I've worked towards, summarized here:

lemma hermite_eq_iter (n : ℕ) : hermite n = nat.iterate x_sub_dx n 1 := sorry
lemma hermite_eq_exp (n : ℕ) : (λ x, eval x (hermite n)) = λ x, (-1)^n * (inv_gaussian x) * (deriv^[n] gaussian x) := sorry
lemma hermite_coeff_recur (n k : ℕ) : coeff (hermite (n + 1)) (k + 1) = coeff (hermite n) k - (k+2)*(coeff (hermite n) (k+2)) := sorry
lemma hermite_coeff_explicit (n k : ℕ) : coeff (hermite n) k = if (even (n-k)) then (-1)^((n-k)/2) * (n-k-1)‼ * nat.choose n k else 0 := sorry
lemma hermite_coeff_explicit' (n k : ℕ) : coeff (hermite (n+k)) k = if (even n) then (-1)^(n/2) * (n-1)‼ * nat.choose (n+k) k else 0 := sorry

To start with a small piece, I could stick to the definition of hermite n, the lemma hermite_eq_iter, and a few supporting lemmas. This is my first experience with the process; where would I ask for write access to make a PR?

[Moritz Doll]

Here is a perfectly fine place (there are dedicated threads as well)

[Patrick Massot]

@Luke Mantle did you check whether all prerequisites are already in mathlib4? It seems to be a case where it makes sense to directly PR to mathlib4 in a new file.

[Moritz Doll]

Patrick, we certainly do not have the (analysis)-derivative in mathlib4 (I don't know about the polynomial derivative).

[Moritz Doll]

I am working on that, though.

[Moritz Doll]

(polynomial derivatives are in mathlib4)

[Eric Wieser]

This is my first experience with the process; where would I ask for write access to make a PR?

you need to give us your github username to be granted access.

[Eric Wieser]

Ah, I assume you're https://github.com/lukemantle based on the name and avatar match and "hermite" project; access granted!

[Luke Mantle]

Patrick Massot said:

Luke Mantle did you check whether all prerequisites are already in mathlib4? It seems to be a case where it makes sense to directly PR to mathlib4 in a new file.

Ah, how do you check this? I have been working in Lean 3 the whole time.

[Luke Mantle]

Eric Wieser said:

Ah, I assume you're https://github.com/lukemantle based on the name and avatar match and "hermite" project; access granted!

Yes, that's right; thanks!

[Patrick Massot]

You can simply look at the mathlib4 repository if you know which files you need.

[Luke Mantle]

Ok, I see

[Luke Mantle]

@Eric Wieser Where would be the best place in mathlib to add the hermite polynomials?

[Eric Wieser]

A new file in data/polynomial?

[Luke Mantle]

I do have multiple files (since I have multiple equivalent definitions), but I would be starting with my basic.lean. Would it be good to make a directory data/polynomial/hermite?

[Eric Wieser]

Actually, ring_theory/polynomial/hermite might be better, since that's next to ring_theory/polynomial/chebyshev

[Eric Wieser]

I think just add hermite.lean for now, renaming it to hermite/basic.lean later is easy

[Luke Mantle]

Ok, great!

[Luke Mantle]

Also, would it preferable to define hermite n as polynomials over ℝ, ℤ, or comm_ring R?

[Eric Wieser]

Why don't you make a PR with what you have, and list your questions in the description? Sometimes its easier to answer these things with the code in front of us.

[Luke Mantle]

Ok, sounds good

[Eric Wieser]

My guess would be comm_ring R, but I might change my mind when I see what you have. I would guess that $\mathbb{R}$ is not the right choice.

[Luke Mantle]

@Eric Wieser I've submitted the PR #18739

[Jake Levinson]

Question: is the statement that "a polynomial with only even terms is an even function" already in mathlib? Since @Luke Mantle has the formulas for the individual coefficients, the stronger statement (that hermite n only has even/odd powers of X) is already more or less in place.

[Jake Levinson]

Something like

lemma polynomial_even {R : Type} [comm_ring R] (p : polynomial R)
  (hp : ∀ n, odd n → p.coeff n = 0) (x) : p.eval (-x) = p.eval x := sorry

[Eric Wieser]

"has only even terms" sounds like the sort of thing that can written in a handful of ways, some of which are easier to deal with than others

[Eric Wieser]

In an extreme case, you could write something like ∃ q : polynomial R, q.aeval (X*X) = p.

[Eric Wieser]

p ∈ algebra.adjoin R {X*X} is another way

[Jake Levinson]

Jake Levinson said:

Something like

lemma polynomial_even {R : Type} [comm_ring R] (p : polynomial R)
  (hp : ∀ n, odd n → p.coeff n = 0) (x) : p.eval (-x) = p.eval x := sorry

This form is the one closest to @Luke Mantle 's repository (lemma hermite_coeff_odd_zero (n k : ℕ) (hnk : odd (n + k)) : coeff (hermite n) k = 0)

[Moritz Doll]

Honestly, I would not bother with a definition and just prove that (hermite n).eval (-x) = (-1)^n * (hermite n).eval x.

[Kevin Buzzard]

For Bernoulli polynomials it wasn't clear to me what the best base ring was, because there were denominators. But here surely the best base ring is the integers, and if so then Moritz' definition is fine. The alternative is "an arbitrary commutative ring" but it's easy to do the coercion.

[Mario Carneiro]

if there are denominators then why not Q? Or are the denominators all e.g. powers of 2 so you are thinking about rings of nonzero characteristic

[Kevin Buzzard]

Because the results relating Bernoulli polynomials to classical and p-adic zeta functions need R and Q_p versions, so another possibility is "any characteristic zero field" or "any Q-algebra"

[Mario Carneiro]

doesn't "it's easy to do the coercion" also apply to Q -> char zero field?

[Kevin Buzzard]

Yeah I should think so. So probably for Hermite you just want them over Z

[Jake Levinson]

Yes, for the Hermite polynomials, the coefficients are integers, not rationals. The only reason some standard formulas have division is because they're writing out binomial coefficients as ratios of factorials (which is unnecessary since a.choose b is an integer).

[Eric Rodriguez]

there's also desc/asc_factorial & pochhammer if that's needed