feat: value of f (x + n * c), where f is antiperiodic with antiperiod c

[trivial1711]

trafficstars

Add @[simp] theorem negOnePow_two_mul_add_one to Algebra.GroupPower.NegOnePow, which states that (2 * n + 1).negOnePow = -1.

Add theorems to Algebra.Periodic about the value of f (x + n • c), f (x - n • c), and f (n • c - x), where we have Antiperiodic f c. All these theorems have variants for either n : ℕ or n : ℤ, and they also have variants using * instead of • if the domain and codomain of f are rings.

For all real numbers x and all integers n. deduce the following. All these theorems are in Analysis.SpecialFunctions.Trigonometric.Basic, they are not @[simp], and they have a variation (using the notation (-1) ^ n instead of n.negOnePow) for natural number n.

• sin (x + n * π) = n.negOnePow * sin x
• sin (x - n * π) = n.negOnePow * sin x
• sin (n * π - x) = -(n.negOnePow * sin x)
• cos (x + n * π) = n.negOnePow * cos x
• cos (x - n * π) = n.negOnePow * cos x
• cos (n * π - x) = n.negOnePow * cos x

---

[trivial1711]

Thanks for the feedback. I have made the changes you suggest.

[trivial1711]

I wonder whether these theorems should all be a special case of more general theorems for Antiperiodic functions (https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Periodic.html#Function.Antiperiodic).

[grunweg]

At first thought, that certainly sounds useful. In any case, these results for anti-periodic functions would be nice to have (and the identities for sin and cos and be deduced from that).

[trivial1711]

Hello, I've redone this branch so that it deduces the facts about sin and cos from more general facts about Antiperiodic functions.

[trivial1711]

Why state half of your lemmas using negOnePow and the other half using (-1)^n?

You can't write simply (-1) ^ n if n is an integer, only if it's a natural number.

[YaelDillies]

In a field, you certainly can?

[trivial1711]

Good point. Does that mean I should state the lemmas about trigonometric functions using (-1) ^ n, but continue to use negOnePow for the general lemmas about antiperiodic functions?

[YaelDillies]

Yes, that seems best. From my limited understanding, negOnePow is meant to be used on non-field rings.

[trivial1711]

After playing around with this, I now think that Field.zpow is so difficult to work with that it would be better to leave it as negOnePow for now. Unless I am missing something, there are no lemmas in mathlib about Field.zpow at all, aside from the ones that are part of the definition of a field: https://loogle.lean-lang.org/?q=Field.zpow.

For example, let K be a field. It's almost comically difficult to prove something like (-1 : K) ^ (m + n) = (-1 : K) ^ m * (-1 : K) ^ n. On the other hand, this equation is very easy if you use negOnePow instead.

Even if the API of Field.zpow were filled out more to include the equation x ^ (m + n) = x ^ m * x ^ n for nonzero x (note that it's not true for x = 0), you'd still have to include a proof that -1 ≠ 0 every time you want to do the simplification (-1 : K) ^ (m + n) = (-1 : K) ^ m * (-1 : K) ^ n.

I think part of the purpose of negOnePow is to be able to write expressions like (-1) ^ n without using Field.zpow.

[YaelDillies]

Nobody uses Field.zpow in real life. We use ^ notation instead and the lemmas refer to it as zpow, eg x ^ (m + n) = x ^ m * x ^ n for nonzero x is zpow_add₀.

[trivial1711]

ok, I've fixed it. thanks!

[github-actions[bot]]

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Check all files imported
• Lint style