Commit 2024-04-02 13:07 a3021aec
View on Github →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