{
 "cells": [
  {
   "cell_type": "markdown",
   "id": "f03132be",
   "metadata": {},
   "source": [
    "# Euler's Formula\n",
    "\n",
    "Euler's formula links the exponential function to circular motion:\n",
    "\n",
    "$$\n",
    "e^{ix}=\\cos x+i\\sin x.\n",
    "$$\n",
    "\n",
    "We verify the identity coefficient by coefficient.  Egison differentiates\n",
    "symbolic expressions to generate the Maclaurin terms on both sides.\n"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "9700a21b",
   "metadata": {},
   "source": [
    "## Maclaurin expansion of the exponential\n",
    "\n",
    "For a function $F$, the term of degree $n$ at the origin is\n",
    "\n",
    "$$\n",
    "\\frac{F^{(n)}(0)}{n!}x^n.\n",
    "$$\n",
    "\n",
    "We first ask for the first eight terms of $e^{ix}$.\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "id": "ea4aa1af",
   "metadata": {},
   "outputs": [],
   "source": [
    "declare symbol x : MathValue\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "id": "7544fc26",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/html": [
       "$\\{1, i x, \\frac{-1}{2} x^{2}, \\frac{-1}{6} i x^{3}, \\frac{1}{24} x^{4}, \\frac{1}{120} i x^{5}, \\frac{-1}{720} x^{6}, \\frac{-1}{5040} i x^{7}\\}$"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "take 8 (taylorExpansion (e^(i * x)) x 0)\n"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "3b301e54",
   "metadata": {},
   "source": [
    "## Real and imaginary parts\n",
    "\n",
    "The even powers occur in $\\cos x$, while the odd powers occur in\n",
    "$i\\sin x$.  Computing the two series separately makes this parity\n",
    "split visible.\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "id": "b930f243",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/html": [
       "$\\{1, 0, \\frac{-1}{2} x^{2}, 0, \\frac{1}{24} x^{4}, 0, \\frac{-1}{720} x^{6}, 0\\}$"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "take 8 (taylorExpansion (cos x) x 0)\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "id": "e8ad66b2",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/html": [
       "$\\{0, i x, 0, \\frac{-1}{6} i x^{3}, 0, \\frac{1}{120} i x^{5}, 0, \\frac{-1}{5040} i x^{7}\\}$"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "take 8 (taylorExpansion (i * sin x) x 0)\n"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "429b78c9",
   "metadata": {},
   "source": [
    "## Coefficient-by-coefficient comparison\n",
    "\n",
    "Adding the two lists must reproduce the exponential series through\n",
    "every displayed order.\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "id": "507f9da6",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/html": [
       "$\\{1, i x, \\frac{-1}{2} x^{2}, \\frac{-1}{6} i x^{3}, \\frac{1}{24} x^{4}, \\frac{1}{120} i x^{5}, \\frac{-1}{720} x^{6}, \\frac{-1}{5040} i x^{7}\\}$"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "take 8\n",
    "  (map2 (+)\n",
    "    (taylorExpansion (cos x) x 0)\n",
    "    (taylorExpansion (i * sin x) x 0))\n"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "ef4e7f8a",
   "metadata": {},
   "source": [
    "The final list is identical to the expansion of $e^{ix}$.  The\n",
    "calculation exhibits Euler's formula as a formal power-series\n",
    "identity, without substituting a numerical value for $x$.\n"
   ]
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "Egison",
   "language": "egison",
   "name": "egison"
  },
  "language_info": {
   "codemirror_mode": "egison",
   "file_extension": ".egi",
   "mimetype": "text/x-egison",
   "name": "egison"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 5
}