Commit 2024-04-02 13:07 a3021aec

feat: value of f (x + n * c), where f is antiperiodic with antiperiod c (#11436) 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