Comment by Tainnor
1 year ago
To quote myself:
> cos can be defined via its power series or via the exp function (if you use complex numbers).
1 year ago
To quote myself:
> cos can be defined via its power series or via the exp function (if you use complex numbers).
Any function can be defined as a taylor series. That is not at all an argument against its geometric nature.
> Any function can be defined as a taylor series.
First of all, that's wrong. It's only true for analytic functions.
Second of all, sin and cos appear in all sorts of contexts that are not primarily geometric (such as harmonic analysis).
Lean's mathlib defines pi precisely the way I've described it - cos is defined via exp, and pi is defined as the unique zero in [0,2]
> Lean's mathlib defines pi precisely the way I've described it - cos is defined via exp, and pi is defined as the unique zero in [0,2]
Which, _again_ is a taylor series. A function having a taylor series does not argue against the geometric nature of cos.
> Second of all, sin and cos appear in all sorts of contexts that are not primarily geometric (such as harmonic analysis).
I'm not sure how you can say that, there is so much material describing the geometric nature and interpretation of fourier/laplace transforms.
3 replies →