4 ms·

What do you mean? Cos is an inherently geometric function.

by aydyn 2y ago

IsTom 2y ago
There are many equivalent definitions and many of them do not refer to geometry at all. If you don't want to go through cos you can always define pi as sqrt(6 * sum from 1 to inf 1/n^2).
- TeMPOraL 2y ago
  You can also define it as `3.14159...` just because. Obviously, a π definition entirely divorced from geometry becomes irrelevant to it - instead, in geometry, you'd still use π = circumference/diameter, or π = whatever(cos), and those values would happen to be the same as a non-geometric π, but only if the geometric π is the one from Euclidean geometry.
  - Tainnor 2y ago
    > You can also define it as `3.14159...` just because. That's not a rigorous definition, though, because it doesn't tell you what those "..." expand to.
Tainnor 2y ago
To quote myself: > cos can be defined via its power series or via the exp function (if you use complex numbers).
- aydyn 2y ago
  Any function can be defined as a taylor series. That is not at all an argument against its geometric nature.
  - Tainnor 2y ago
    > 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]
    - aydyn 2y ago
      > 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.
      - Tainnor 2y ago
        > Which, _again_ is a taylor series. Mathlib defines cos x = (exp(ix)+exp(-ix))/2, which is not a definition via Taylor series (even though you can derive the Taylor series of cos quite easily from it). exp is defined as a Taylor series in mathlib, but it might just as easily be defined as the unique solution of a particular IVP, etc. Regardless of this, I have no idea why to you seemingly a definition via Taylor series is not a "true" definition, you could probably crack open half a dozen (rigorous) real or complex analysis texts, they're likely to define sin and cos in some such way (or, alternatively, as the single set of functions satisfying certain axioms), because defining them via geometry and making this rigorous is much harder. I can't argue whether cos has a "geometric nature" or not, because I don't know what that means. Undoubtedly cos is useful in geometry. It is, however, used in a wide range of other domains that make absolutely no reference to geometry. mathlib's definition of cos doesn't import a single geometry definition or theorem. Remember that the starting point of this discussion was that somebody was claiming that "pi is different in non-Euclidean geometry", which, no, even in a completely different geometry, the trigonometric functions would be useful and pi is closely related to them.

What do you mean? Cos is an inherently geometric function.

by aydyn 2y ago

What do you mean? Cos is an inherently geometric function.

There are many equivalent definitions and many of them do not refer to geometry at all. If you don't want to go through cos you can always define pi as sqrt(6 * sum from 1 to inf 1/n^2).

TeMPOraL 2y ago
You can also define it as `3.14159...` just because. Obviously, a π definition entirely divorced from geometry becomes irrelevant to it - instead, in geometry, you'd still use π = circumference/diameter, or π = whatever(cos), and those values would happen to be the same as a non-geometric π, but only if the geometric π is the one from Euclidean geometry.
- Tainnor 2y ago
  > You can also define it as `3.14159...` just because. That's not a rigorous definition, though, because it doesn't tell you what those "..." expand to.

Tainnor 2y ago

To quote myself: > cos can be defined via its power series or via the exp function (if you use complex numbers).

aydyn 2y ago
Any function can be defined as a taylor series. That is not at all an argument against its geometric nature.
- Tainnor 2y ago
  > 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]
  - aydyn 2y ago
    > 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.
    - Tainnor 2y ago
      > Which, _again_ is a taylor series. Mathlib defines cos x = (exp(ix)+exp(-ix))/2, which is not a definition via Taylor series (even though you can derive the Taylor series of cos quite easily from it). exp is defined as a Taylor series in mathlib, but it might just as easily be defined as the unique solution of a particular IVP, etc. Regardless of this, I have no idea why to you seemingly a definition via Taylor series is not a "true" definition, you could probably crack open half a dozen (rigorous) real or complex analysis texts, they're likely to define sin and cos in some such way (or, alternatively, as the single set of functions satisfying certain axioms), because defining them via geometry and making this rigorous is much harder. I can't argue whether cos has a "geometric nature" or not, because I don't know what that means. Undoubtedly cos is useful in geometry. It is, however, used in a wide range of other domains that make absolutely no reference to geometry. mathlib's definition of cos doesn't import a single geometry definition or theorem. Remember that the starting point of this discussion was that somebody was claiming that "pi is different in non-Euclidean geometry", which, no, even in a completely different geometry, the trigonometric functions would be useful and pi is closely related to them.