Even and odd functions

Stream: mathlib4

[David Loeffler]

I believe Mathlib doesn't currently have the notion of "even" and "odd" functions (between types with negation), i.e. functions satisfying f (-x) = f x or f (-x) = -(f x) respectively. Cf. https://en.wikipedia.org/wiki/Even_and_odd_functions.

These are pretty trivial to code up:

/-- A function `f` is _even_ if it satisfies `f (-x) = f x` for all `x`. -/
protected def Function.Even {R R' : Type*} [Neg R] (f : R → R') : Prop := ∀ (x : R), f (-x) = f x

/-- A function `f` is _odd_ if it satisfies `f (-x) = -f x` for all `x`. -/
protected def Function.Odd {R R' : Type*} [Neg R] [Neg R'] (f : R → R') : Prop :=
  ∀ (x : R), f (-x) = -(f x)

My question is: where should they go in Mathlib, given that they have virtually no prerequisites at all? Would a new file under Data, perhaps Data/EvenOddFunction.lean, be a good solution?

[Yaël Dillies]

Definitely not under Data since they import algebra if you try to prove anything non-trivial. Algebra could work

[David Loeffler]

Good point, I guess you will very soon need InvolutiveNeg and that lives in Algebra/Group. How about Algebra.Group.EvenOddFunction then?

[Yaël Dillies]

Happy with it

[Yury G. Kudryashov]

Should it come with a linter warning against _root_.Even (f : α → β)?

[Yury G. Kudryashov]

This is a valid term that means (after some simplifications) ∀ a, Even (f a).

[David Loeffler]

Yury G. Kudryashov said:

Should it come with a linter warning against _root_.Even (f : α → β)?

This sounds like a nice idea (I made that mistake several times myself) but I have no idea how to write linters myself...

[Johan Commelin]

I think such a linter can be useful (not for mathlib CI, but just as an authoring tool in VScode). But it can definitely be a separate PR.

[Damiano Testa]

I'm not sure that I understand what the linter should do: it is supposed to prevent using _root_.Even with a function? Due to the protected this means Even f where f is a function, right?

[Yaël Dillies]

Why don't you just write f.Even?

[Yaël Dillies]

Or, let's be crazy, why not call the predicates EvenFun/OddFun?

[Eric Wieser]

Johan Commelin said:

I think such a linter can be useful (not for mathlib CI, but just as an authoring tool in VScode). But it can definitely be a separate PR.

A similar linter would be good for IsCoprime on Nat

[Damiano Testa]

This linter would be a "reverse" protected, or am I misunderstanding? It should flag a selected few declarations X for which Y.X is preferred (and possibly protected)?

[Johan Commelin]

Well, I think it should also look at the t that comes after X. So for certain t it should warn about X t and suggest Y.X t.

[Johan Commelin]

And I think it should only run locally.

[Damiano Testa]

Ok, yes, I did not mention further necessary checks to trigger the linter, but I think that I have a clearer idea of what it should do!

[David Loeffler]

PR up at #16446.