{
 "cells": [
  {
   "cell_type": "markdown",
   "id": "2eaf7e55",
   "metadata": {},
   "source": [
    "# Trigonometric Identities from Complex Multiplication\n",
    "\n",
    "Euler's formula packages cosine and sine into one algebraic object,\n",
    "\n",
    "$$u(\\alpha)=\\cos\\alpha+i\\sin\\alpha=e^{i\\alpha}.$$\n",
    "\n",
    "Multiplying these objects lets the real and imaginary coefficients\n",
    "reveal several familiar identities.  This is a useful symbolic-computation\n",
    "pattern: perform one polynomial calculation and interpret its coefficients.\n"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "ea90c735",
   "metadata": {},
   "source": [
    "## Symbolic unit-circle elements\n",
    "\n",
    "We keep $\\alpha$ and $\\beta$ symbolic.  The expression `uMinusBeta`\n",
    "represents $u(-\\beta)=\\cos\\beta-i\\sin\\beta$ without asking the\n",
    "simplifier to know parity rules for sine and cosine.\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "id": "c0c532cc",
   "metadata": {},
   "outputs": [],
   "source": [
    "declare symbol α, β : MathValue\n",
    "\n",
    "def uAlpha : MathValue := cos α + i * sin α\n",
    "def uBeta : MathValue := cos β + i * sin β\n",
    "def uMinusBeta : MathValue := cos β - i * sin β\n"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "9864f158",
   "metadata": {},
   "source": [
    "## Angle-addition formulas\n",
    "\n",
    "The coefficients of $1$ and $i$ in $u(\\alpha)u(\\beta)$ are,\n",
    "respectively, $\\cos(\\alpha+\\beta)$ and $\\sin(\\alpha+\\beta)$.\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "id": "e9a733f6",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/html": [
       "$\\{-\\sin(α) \\sin(β) + \\cos(α) \\cos(β), \\cos(β) \\sin(α) + \\cos(α) \\sin(β)\\}$"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "coefficients (uAlpha * uBeta) i\n"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "c30677bd",
   "metadata": {},
   "source": [
    "Reading the two returned coefficients gives\n",
    "\n",
    "$$\n",
    "\\cos(\\alpha+\\beta)=\\cos\\alpha\\cos\\beta-\\sin\\alpha\\sin\\beta,\n",
    "$$\n",
    "$$\n",
    "\\sin(\\alpha+\\beta)=\\sin\\alpha\\cos\\beta+\\cos\\alpha\\sin\\beta.\n",
    "$$\n",
    "\n",
    "Adding $u(\\alpha)u(\\beta)$ and $u(\\alpha)u(-\\beta)$ isolates\n",
    "the product-to-sum combinations.\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "id": "a02aa852",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/html": [
       "$\\{2 \\cos(α) \\cos(β), 2 \\cos(β) \\sin(α)\\}$"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "coefficients (uAlpha * uBeta + uAlpha * uMinusBeta) i\n"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "90fe2b1c",
   "metadata": {},
   "source": [
    "The result encodes $2\\cos\\alpha\\cos\\beta$ in its real part and\n",
    "$2\\sin\\alpha\\cos\\beta$ in its imaginary part.  Dividing by two\n",
    "and replacing the two products by $u(\\alpha\\pm\\beta)$ yields the\n",
    "standard product-to-sum identities.\n",
    "\n",
    "## Triple-angle formulas\n",
    "\n",
    "Cubing one unit-circle element performs all terms of the binomial\n",
    "expansion at once.\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "id": "4852b62f",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/html": [
       "$\\{\\cos(α)^{3} - 3 \\cos(α) \\sin(α)^{2}, -\\sin(α)^{3} + 3 \\cos(α)^{2} \\sin(α)\\}$"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "coefficients (uAlpha ^ 3) i\n"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "09c68e68",
   "metadata": {},
   "source": [
    "The real and imaginary components are\n",
    "\n",
    "$$\\cos^3\\alpha-3\\cos\\alpha\\sin^2\\alpha,$$\n",
    "$$3\\cos^2\\alpha\\sin\\alpha-\\sin^3\\alpha.$$\n",
    "\n",
    "Using $\\sin^2\\alpha=1-\\cos^2\\alpha$ in the first and\n",
    "$\\cos^2\\alpha=1-\\sin^2\\alpha$ in the second gives\n",
    "\n",
    "$$\\cos(3\\alpha)=4\\cos^3\\alpha-3\\cos\\alpha,$$\n",
    "$$\\sin(3\\alpha)=3\\sin\\alpha-4\\sin^3\\alpha.$$\n",
    "\n",
    "The essential point is that Egison's coefficient extraction turns\n",
    "complex multiplication into a transparent derivation, rather than\n",
    "merely checking a pre-stated identity.\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
}