New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat: value of f (x + n * c), where f is antiperiodic with antiperiod c #11436
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thank you for this contribution, it's nice for such API gaps to get filled!
I have a few golfing suggestions, which should be quick to address.
Thanks for the feedback. I have made the changes you suggest. |
I wonder whether these theorems should all be a special case of more general theorems for |
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). |
Hello, I've redone this branch so that it deduces the facts about sin and cos from more general facts about Antiperiodic functions. |
In a field, you certainly can? |
Good point. Does that mean I should state the lemmas about trigonometric functions using |
Yes, that seems best. From my limited understanding, |
After playing around with this, I now think that For example, let Even if the API of I think part of the purpose of |
Nobody uses |
ok, I've fixed it. thanks! |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This looks alright to me but I need a second pair of eyes
maintainer merge
🚀 Pull request has been placed on the maintainer queue by YaelDillies. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
LGTM
bors merge
… 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`
Pull request successfully merged into master. Build succeeded: |
… 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`
… 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`
… 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`
… 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`
Add
@[simp]
theoremnegOnePow_two_mul_add_one
toAlgebra.GroupPower.NegOnePow
, which states that(2 * n + 1).negOnePow = -1
.Add theorems to
Algebra.Periodic
about the value off (x + n • c)
,f (x - n • c)
, andf (n • c - x)
, where we haveAntiperiodic f c
. All these theorems have variants for eithern : ℕ
orn : ℤ
, and they also have variants using*
instead of•
if the domain and codomain off
are rings.For all real numbers
x
and all integersn
. deduce the following. All these theorems are inAnalysis.SpecialFunctions.Trigonometric.Basic
, they are not@[simp]
, and they have a variation (using the notation(-1) ^ n
instead ofn.negOnePow
) for natural numbern
.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