nLab cosine








See at trigonometric function.


The cosine function is the function cos:\cos \;\colon\; \mathbb{R} \to \mathbb{R} from the real numbers to themselves which is characterized by the following equivalent conditions:

  1. cos\cos is the unique solution among smooth functions to the differential equation/initial value problem

    cos=cos cos'' = -cos

    (where a prime indicates the derivative) subject to the initial conditions

    cos(0) =1 cos(0) =0. \begin{aligned} cos(0) &= 1 \\ cos'(0) & = 0 \,. \end{aligned}
  2. (Euler's formula) cos\cos is the real part of the exponential function with imaginary argument

    cos(x) =Re(exp(ix)) =12(exp(ix)+exp(ix)). \begin{aligned} \cos(x) & = Re\left( \exp(i x) \right) \\ & = \frac{1}{2}\big( \exp(i x) + \exp(- i x)\big) \end{aligned} \,.
  3. cos\cos is the unique function given by the infinite series

cos(x) i=0 (1) ix 2i(2i)!\cos(x) \coloneqq \sum_{i = 0}^{\infty} \frac{(-1)^i x^{2 i}}{(2 i)!}

In arbitrary Archimedean ordered fields

In general, Archimedean ordered fields which are not sequentially Cauchy complete do not have an cosine function. Nevertheless, the cosine map is still guaranteed to be a partial function, because every Archimedean ordered field is a Hausdorff space and thus a sequentially Hausdorff space. Therefore an axiom could be added to Archimedean ordered fields FF to ensure that the cosine partial function is actually a total function:

Axiom of cosine function: For all elements xFx \in F, there exists a unique element cos(x)F\cos(x) \in F such that for all positive elements ϵF +\epsilon \in F_+, there exists a natural number NN \in \mathbb{N} such that for all natural numbers nn \in \mathbb{N}, if nNn \geq N, then ϵ<( i=0 n(1) ix 2i(2i)!)cos(x)<ϵ-\epsilon \lt \left(\sum_{i = 0}^{n} \frac{(-1)^i x^{2 i}}{(2 i)!}\right) - \cos(x) \lt \epsilon.

There is another axiom which uses the fact that derivatives of functions are well defined in the ordered local Artin F F -algebra F[ϵ]/ϵ 2F[\epsilon]/\epsilon^2 by the equation f(x+ϵ)=f(x)+f(x)ϵf(x + \epsilon) = f(x) + f'(x) \epsilon:

Axiom of sine and cosine functions: Let F[ϵ]/ϵ 2F[\epsilon]/\epsilon^2 be the ordered local Artin FF-algebra, with non-zero non-positive non-negative nilpotent element ϵF[ϵ]/ϵ 2\epsilon \in F[\epsilon]/\epsilon^2 where ϵ 2=0\epsilon^2 = 0 and canonical FF-algebra homomorphism h:FF[x]/x 2h:F \to F[x]/x^2. There exists unique functions sin:FF\sin:F \to F and cos:FF\cos:F \to F and functions sin:F[ϵ]/ϵ 2F[ϵ]/ϵ 2\sin':F[\epsilon]/\epsilon^2 \to F[\epsilon]/\epsilon^2 and cos:F[ϵ]/ϵ 2F[ϵ]/ϵ 2\cos':F[\epsilon]/\epsilon^2 \to F[\epsilon]/\epsilon^2 such that for every element xFx \in F, h(sin(x))=sin(h(x))h(\sin(x)) = \sin'(h(x)), h(cos(x))=cos(h(x))h(\cos(x)) = \cos'(h(x)), sin(x+ϵ)=sin(x)+cos(x)ϵ\sin'(x + \epsilon) = \sin'(x) + \cos'(x) \epsilon, cos(x+ϵ)=cos(x)sin(x)ϵ\cos'(x + \epsilon) = \cos'(x) - \sin'(x) \epsilon, sin(0)=0\sin'(0) = 0, and cos(0)=1\cos'(0) = 1.

In the dual numbers

The dual number real algebra 𝔻[ϵ]/ϵ 2\mathbb{D} \coloneqq \mathbb{R}[\epsilon]/\epsilon^2 has a notion of sine and cosine function, which are the solutions to the system of functional equations sin(x+ϵ)=sin(x)+cos(x)ϵ\sin(x + \epsilon) = \sin(x) + \cos(x) \epsilon and cos(x+ϵ)=cos(x)sin(x)ϵ\cos(x + \epsilon) = \cos(x) - \sin(x) \epsilon with sin(0)=1\sin(0) = 1 and cos(0)=1\cos(0) = 1.

In constructive mathematics

In classical mathematics, one could prove that the modulated Cantor real numbers C\mathbb{R}_C are sequentially Cauchy complete and equivalent to the HoTT book real numbers H\mathbb{R}_H. However, in constructive mathematics, the above cannot be proven; while the HoTT book real numbers H\mathbb{R}_H are still sequentially Cauchy complete, the modulated Cantor real numbers C\mathbb{R}_C in general cannot be proven to be sequentially Cauchy complete. In particular, this means that the sequence

i=0 n(1) ix 2i(2i)!\sum_{i = 0}^{n} \frac{(-1)^i x^{2 i}}{(2 i)!}

does not have a limit for all modulated Cantor real numbers x Cx \in \mathbb{R}_C. However, the sequence, by definition of C\mathbb{R}_C, does have a limit for all rational numbers xx \in \mathbb{Q}; this means that one could restrict the domain of the cosine function to the rational numbers cos: C\cos:\mathbb{Q} \to \mathbb{R}_C, and define it in the usual manner:

  • For all rational numbers xx \in \mathbb{Q}, there exists a unique modulated Cantor real number cos(x) C\cos(x) \in \mathbb{R}_C such that for all positive rational numbers ϵ +\epsilon \in \mathbb{Q}_+, there exists a natural number NN \in \mathbb{N} such that for all natural numbers nn \in \mathbb{N}, if nNn \geq N, then ϵ< i=0 n(1) ix 2i(2i)!cos(x)<ϵ-\epsilon \lt \sum_{i = 0}^{n} \frac{(-1)^i x^{2 i}}{(2 i)!} - \cos(x) \lt \epsilon.


Discussion in constructive analysis:

See also:

Last revised on February 8, 2023 at 19:43:01. See the history of this page for a list of all contributions to it.