Revision #1642 → #1972 · back to history
modifiedSix trigonometric functionsb5d803b81648
| Field | From #1642 | To #1972 |
|---|
| note | Mathlib has `Real.sin`, `Real.cos`, `Real.tan` and `Complex.cot` (see `Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent`) but does not appear to define standalone `sec`/`csc` functions. | Mathlib has `Real.sin`, `Real.cos`, `Real.tan` and `Complex.cot` but does not appear to define standalone `sec`/`csc` functions. |
modifiedUnit-circle definitions of sine and cosine44a81f351651
| Field | From #1642 | To #1972 |
|---|
| mathlib.module | Mathlib.Analysis.SpecialFunctions.Complex.Circle | Mathlib.Analysis.Complex.Circle |
modifiedPythagorean identity from unit circle65cf1b5bac8f
| Field | From #1642 | To #1972 |
|---|
| anchors | [{"section":"Unit-circle definitions","snippet":"this definition of cosine and sine also satisfies the Pythagorean identity"},{"type":"math_alttext","value":"{\\displaystyle \\cos ^{2}\\theta +\\sin ^{2}\\theta =1.}"}] | — |
addedTangent, cotangent, secant, cosecant in terms of sine and cosinee238bff72c83
modifiedSine and cosine as initial value problem3bcd33e723f4
| Field | From #1642 | To #1972 |
|---|
| anchors | [{"section":"Definition by differential equations","snippet":"can be defined as the unique solution to the initial value problem"},{"type":"math_alttext","value":"{\\displaystyle {\\frac {d}{dx}}\\sin x=\\cos x,\\ {\\frac {d}{dx}}\\cos x=-\\sin x,\\ \\sin(0)=0,\\ \\cos(0)=1.}"}] | — |
modifiedSine and cosine solve the harmonic ODE71c5e59d6c3f
| Field | From #1642 | To #1972 |
|---|
| anchors | [{"section":"Definition by differential equations","snippet":"both sine and cosine are solutions of the same ordinary differential equation"},{"type":"math_alttext","value":"{\\displaystyle y''+y=0\\,.}"}] | — |
| mathlib.module | Mathlib.Analysis.Complex.Trigonometric | Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv |
modifiedTangent ODE307ce058fa95
| Field | From #1642 | To #1972 |
|---|
| anchors | [{"section":"Definition by differential equations","snippet":"so the tangent function satisfies the ordinary differential equation"},{"type":"math_alttext","value":"{\\displaystyle {\\frac {d}{dx}}\\tan x={\\frac {\\cos ^{2}x+\\sin ^{2}x}{\\cos ^{2}x}}=1+\\tan ^{2}x\\,,}"},{"type":"math_alttext","value":"{\\displaystyle y'=1+y^{2}\\,.}"}] | — |
modifiedPower series for sine and cosine48f867f83ea2
| Field | From #1642 | To #1972 |
|---|
| anchors | [{"section":"Power series expansion","snippet":"The basic trigonometric functions can be defined by the following power series expansions"},{"type":"math_alttext","value":"{\\displaystyle {\\begin{aligned}\\sin x&=x-{\\frac {x^{3}}{3!}}+{\\frac {x^{5}}{5!}}-{\\frac {x^{7}}{7!}}+\\cdots &&=\\sum _{n=0}^{\\infty }(-1)^{n}{\\frac {x^{2n+1}}{(2n+1)!}}\\\\\\cos x&=1-{\\frac {x^{2}}{2!}}+{\\frac {x^{4}}{4!}}-{\\frac {x^{6}}{6!}}+\\cdots &&=\\sum _{n=0}^{\\infty }(-1)^{n}{\\frac {x^{2n}}{(2n)!}}\\end{aligned}}}"}] | — |
modifiedEntire extension via infinite radius of convergence0c1f8d3d6689
| Field | From #1642 | To #1972 |
|---|
| anchors | [{"section":"Power series expansion","snippet":"The radius of convergence of these series is infinite"},{"type":"math_alttext","value":"{\\displaystyle {\\begin{aligned}\\sin x&=x-{\\frac {x^{3}}{3!}}+{\\frac {x^{5}}{5!}}-{\\frac {x^{7}}{7!}}+\\cdots &&=\\sum _{n=0}^{\\infty }(-1)^{n}{\\frac {x^{2n+1}}{(2n+1)!}}\\\\\\cos x&=1-{\\frac {x^{2}}{2!}}+{\\frac {x^{4}}{4!}}-{\\frac {x^{6}}{6!}}+\\cdots &&=\\sum _{n=0}^{\\infty }(-1)^{n}{\\frac {x^{2n}}{(2n)!}}\\end{aligned}}}"}] | — |
| mathlib.module | Mathlib.Analysis.Complex.Trigonometric | Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv |
modifiedPartial fraction expansion of cotangentd7de99068910
| Field | From #1642 | To #1972 |
|---|
| anchors | [{"section":"Partial fraction expansion","snippet":"There is a series representation as partial fraction expansion where just translated reciprocal functions are summed up"},{"type":"math_alttext","value":"{\\displaystyle \\pi \\cot \\pi x=\\lim _{N\\to \\infty }\\sum _{n=-N}^{N}{\\frac {1}{x+n}}.}"},{"type":"math_alttext","value":"{\\displaystyle \\pi \\cot \\pi x={\\frac {1}{x}}+2x\\sum _{n=1}^{\\infty }{\\frac {1}{x^{2}-n^{2}}}.}"},{"type":"math_alttext","value":"{\\displaystyle \\pi \\csc \\pi x=\\sum _{n=-\\infty }^{\\infty }{\\frac {(-1)^{n}}{x+n}}={\\frac {1}{x}}+2x\\sum _{n=1}^{\\infty }{\\frac {(-1)^{n}}{x^{2}-n^{2}}},}"},{"type":"math_alttext","value":"{\\displaystyle \\pi ^{2}\\csc ^{2}\\pi x=\\sum _{n=-\\infty }^{\\infty }{\\frac {1}{(x+n)^{2}}},}"},{"type":"math_alttext","value":"{\\displaystyle \\pi \\sec \\pi x=\\sum _{n=0}^{\\infty }(-1)^{n}{\\frac {(2n+1)}{(n+{\\tfrac {1}{2}})^{2}-x^{2}}},}"},{"type":"math_alttext","value":"{\\displaystyle \\pi \\tan \\pi x=2x\\sum _{n=0}^{\\infty }{\\frac {1}{(n+{\\tfrac {1}{2}})^{2}-x^{2}}}.}"}] | — |
| mathlib.decl | Complex.pi_mul_cot_pi_q_exp | iteratedDerivWithin_cot_pi_mul_eq_mul_tsum_div_pow |
| mathlib.match_kind | exact | generalization |
| note | The Mittag-Leffler expansion `π·cot(πz) = 1/z + Σ (1/(z−n) + 1/(z+n))` is the goal of `Trigonometric/Cotangent.lean`. | Mathlib gives the iterated-derivative series expansion of `π cot(πz)` on the upper half plane and `pi_mul_cot_pi_q_exp` (q-expansion), but not the standard Mittag-Leffler form `π cot πx = 1/x + 2x Σ 1/(x²−n²)` over all of ℂ. |
| status | formalized | partial |
modifiedEuler's infinite product for sine6ebc5972abe8
| Field | From #1642 | To #1972 |
|---|
| anchors | [{"section":"Infinite product expansion","snippet":"The following infinite product for the sine is due to Leonhard Euler"},{"type":"math_alttext","value":"{\\displaystyle \\sin z=z\\prod _{n=1}^{\\infty }\\left(1-{\\frac {z^{2}}{n^{2}\\pi ^{2}}}\\right),\\quad z\\in \\mathbb {C} .}"},{"type":"math_alttext","value":"{\\displaystyle \\cos z=\\prod _{n=1}^{\\infty }\\left(1-{\\frac {z^{2}}{(n-1/2)^{2}\\pi ^{2}}}\\right),\\quad z\\in \\mathbb {C} .}"}] | — |
modifiedEuler's formulafab5b342f782
| Field | From #1642 | To #1972 |
|---|
| anchors | [{"section":"Euler's formula and the exponential function","snippet":"Euler's formula relates sine and cosine to the exponential function"},{"type":"math_alttext","value":"{\\displaystyle e^{ix}=\\cos x+i\\sin x.}"}] | — |
modifiedSine and cosine in terms of complex exponential090cee674182
| Field | From #1642 | To #1972 |
|---|
| anchors | [{"section":"Euler's formula and the exponential function","snippet":"Solving this linear system in sine and cosine, one can express them in terms of the exponential function"},{"type":"math_alttext","value":"{\\displaystyle {\\begin{aligned}\\sin x&={\\frac {e^{ix}-e^{-ix}}{2i}}\\\\[5pt]\\cos x&={\\frac {e^{ix}+e^{-ix}}{2}}.\\end{aligned}}}"}] | — |
modifiedTopological group definition of sine and cosine5e16e91d0b6f
| Field | From #1642 | To #1972 |
|---|
| anchors | [{"section":"Euler's formula and the exponential function","snippet":"Euler's formula can also be used to define the basic trigonometric function directly"},{"type":"math_alttext","value":"{\\displaystyle e:\\mathbb {R} /\\mathbb {Z} \\to U.}"}] | — |
modifiedInverse tangent via integration47a7a541c776
| Field | From #1642 | To #1972 |
|---|
| anchors | [{"section":"Definition via integration","snippet":"Another way to define the trigonometric functions in analysis is using integration"},{"type":"math_alttext","value":"{\\displaystyle \\theta (t)=\\int _{0}^{t}{\\frac {d\\tau }{1+\\tau ^{2}}}=\\arctan t}"},{"type":"math_alttext","value":"{\\displaystyle {\\frac {1}{2}}\\pi =\\int _{0}^{\\infty }{\\frac {d\\tau }{1+\\tau ^{2}}}}"}] | — |
modifiedSine and cosine by inversion8645ef4f3eac
| Field | From #1642 | To #1972 |
|---|
| anchors | [{"section":"Definition via integration","snippet":"the trigonometric functions are defined by inverting the relation"},{"type":"math_alttext","value":"{\\displaystyle \\tan \\theta =t,\\quad \\cos \\theta =(1+t^{2})^{-1/2},\\quad \\sin \\theta =t(1+t^{2})^{-1/2}}"}] | — |
modifiedAddition formulae from integral definitionfe433f780115
| Field | From #1642 | To #1972 |
|---|
| anchors | [{"section":"Definition via integration","snippet":"one may first establish the addition formulae"},{"type":"math_alttext","value":"{\\displaystyle \\arctan s+\\arctan t=\\arctan {\\frac {s+t}{1-st}}}"},{"type":"math_alttext","value":"{\\displaystyle \\arctan s+\\arctan t=\\int _{-s}^{t}{\\frac {d\\tau }{1+\\tau ^{2}}}=\\int _{0}^{\\frac {s+t}{1-st}}{\\frac {d\\tau }{1+\\tau ^{2}}}}"},{"type":"math_alttext","value":"{\\displaystyle \\arctan t+{\\frac {\\pi }{2}}=\\arctan(-1/t),\\quad t\\in (-\\infty ,0).}"},{"type":"math_alttext","value":"{\\displaystyle \\sin \\left(\\theta +{\\frac {\\pi }{2}}\\right)={\\frac {-1}{t{\\sqrt {1+(-1/t)^{2}}}}}={\\frac {-1}{\\sqrt {1+t^{2}}}}=-\\cos(\\theta )}"},{"type":"math_alttext","value":"{\\displaystyle \\cos \\left(\\theta +{\\frac {\\pi }{2}}\\right)={\\frac {1}{\\sqrt {1+(-1/t)^{2}}}}={\\frac {t}{\\sqrt {1+t^{2}}}}=\\sin(\\theta ).}"}] | — |
modifiedFunctional equation characterization of sine and cosinef893c3f16166
| Field | From #1642 | To #1972 |
|---|
| anchors | [{"section":"Definitions using functional equations","snippet":"the sine and the cosine form the unique pair of continuous functions that satisfy the difference formula"},{"type":"math_alttext","value":"{\\displaystyle \\cos(x-y)=\\cos x\\cos y+\\sin x\\sin y\\,}"},{"type":"math_alttext","value":"{\\displaystyle 0<x\\cos x<\\sin x<x\\quad {\\text{ for }}\\quad 0<x<1.}"}] | — |
modifiedComplex sine and cosine via real and hyperbolic functionsace67e3849bc
| Field | From #1642 | To #1972 |
|---|
| anchors | [{"section":"In the complex plane","snippet":"can be expressed in terms of real sines, cosines, and hyperbolic functions as follows"},{"type":"math_alttext","value":"{\\displaystyle {\\begin{aligned}\\sin z&=\\sin x\\cosh y+i\\cos x\\sinh y\\\\[5pt]\\cos z&=\\cos x\\cosh y-i\\sin x\\sinh y\\end{aligned}}}"}] | — |
modifiedPeriodicity and smallest positive periodfe30ac4d2443
| Field | From #1642 | To #1972 |
|---|
| anchors | [{"section":"Periodicity and asymptotes","snippet":"The sine and cosine functions are periodic , with period"},{"type":"math_alttext","value":"{\\displaystyle \\sin(z+2\\pi )=\\sin(z),\\quad \\cos(z+2\\pi )=\\cos(z).}"}] | — |
modifiedZeros of sine and cosine0a7a296e9435
| Field | From #1642 | To #1972 |
|---|
| anchors | [{"section":"Periodicity and asymptotes","snippet":"All of the zeros are simple zeros"},{"type":"math_alttext","value":"{\\displaystyle \\pi \\mathbb {Z} =\\left\\{\\dots ,-2\\pi ,-\\pi ,0,\\pi ,2\\pi ,\\dots \\right\\}\\subset \\mathbb {C} .}"},{"type":"math_alttext","value":"{\\displaystyle {\\frac {\\pi }{2}}+\\pi \\mathbb {Z} =\\left\\{\\dots ,-{\\frac {3\\pi }{2}},-{\\frac {\\pi }{2}},{\\frac {\\pi }{2}},{\\frac {3\\pi }{2}},\\dots \\right\\}\\subset \\mathbb {C} .}"}] | — |
modifiedTangent zeros and poles2fc9ab2f8cb8
| Field | From #1642 | To #1972 |
|---|
| anchors | [{"section":"Periodicity and asymptotes","snippet":"The tangent function"},{"type":"math_alttext","value":"{\\displaystyle \\lim _{x\\to {\\frac {\\pi }{2}}^{-}}\\tan(x)=+\\infty ,\\quad \\lim _{x\\to {\\frac {\\pi }{2}}^{+}}\\tan(x)=-\\infty .}"}] | — |
modifiedCotangent zeros and polesfce96ef6b2f5
| Field | From #1642 | To #1972 |
|---|
| anchors | [{"section":"Periodicity and asymptotes","snippet":"The cotangent function"},{"type":"math_alttext","value":"{\\displaystyle \\lim _{x\\to 0^{-}}\\cot(x)=-\\infty ,\\quad \\lim _{x\\to 0^{+}}\\cot(x)=+\\infty .}"}] | — |
| mathlib.module | Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent | Mathlib.Analysis.Complex.Trigonometric |
modifiedParity of trigonometric functions0eb65f35f736
| Field | From #1642 | To #1972 |
|---|
| anchors | [{"section":"Parity","snippet":"The cosine and the secant are even functions ; the other trigonometric functions are odd functions"},{"type":"math_alttext","value":"{\\displaystyle {\\begin{aligned}\\sin(-x)&=-\\sin x\\\\\\cos(-x)&=\\cos x\\\\\\tan(-x)&=-\\tan x\\\\\\cot(-x)&=-\\cot x\\\\\\csc(-x)&=-\\csc x\\\\\\sec(-x)&=\\sec x.\\end{aligned}}}"}] | — |
modifiedPeriods of trigonometric functions340459e07679
| Field | From #1642 | To #1972 |
|---|
| anchors | [{"section":"Periods","snippet":"All trigonometric functions are periodic functions of period 2"},{"type":"math_alttext","value":"{\\displaystyle {\\begin{array}{lrl}\\sin(x+&2k\\pi )&=\\sin x\\\\\\cos(x+&2k\\pi )&=\\cos x\\\\\\tan(x+&k\\pi )&=\\tan x\\\\\\cot(x+&k\\pi )&=\\cot x\\\\\\csc(x+&2k\\pi )&=\\csc x\\\\\\sec(x+&2k\\pi )&=\\sec x.\\end{array}}}"}] | — |
modifiedPythagorean identity95da68537935
| Field | From #1642 | To #1972 |
|---|
| anchors | [{"section":"Pythagorean identity","snippet":"The Pythagorean identity, is the expression of the Pythagorean theorem in terms of trigonometric functions"},{"type":"math_alttext","value":"{\\displaystyle \\sin ^{2}x+\\cos ^{2}x=1\\,.}"},{"type":"math_alttext","value":"{\\displaystyle \\tan ^{2}x+1=\\sec ^{2}x}"},{"type":"math_alttext","value":"{\\displaystyle 1+\\cot ^{2}x=\\csc ^{2}x}"},{"type":"math_alttext","value":"{\\displaystyle \\sec ^{2}x+\\csc ^{2}x=\\sec ^{2}x\\csc ^{2}x\\,.}"}] | — |
modifiedTangent half-angle substitution6da52494d785
| Field | From #1642 | To #1972 |
|---|
| anchors | [{"section":"Sum and difference formulas","snippet":"this is the tangent half-angle substitution , which reduces the computation of integrals and antiderivatives of trigonometric functions to that of rational fractions"},{"type":"math_alttext","value":"{\\displaystyle {\\begin{aligned}\\sin \\theta &={\\frac {2t}{1+t^{2}}},\\\\[5mu]\\cos \\theta &={\\frac {1-t^{2}}{1+t^{2}}},\\\\[5mu]\\tan \\theta &={\\frac {2t}{1-t^{2}}}.\\end{aligned}}}"},{"type":"math_alttext","value":"{\\displaystyle d\\theta ={\\frac {2}{1+t^{2}}}\\,dt,}"}] | — |
modifiedInverse trigonometric functionsdcc273525b4d
| Field | From #1642 | To #1972 |
|---|
| note | `Real.arcsin`, `Real.arccos`, and `Real.arctan` (in `Trigonometric/Arctan.lean`) are defined as restricted inverses. | `Real.arcsin`, `Real.arccos`, and `Real.arctan` are defined as restricted inverses. |
modifiedLaw of sines8741492db3e4
| Field | From #1642 | To #1972 |
|---|
| anchors | [{"section":"Law of sines","snippet":"The law of sines states that for an arbitrary triangle with sides"},{"type":"math_alttext","value":"{\\displaystyle {\\frac {\\sin A}{a}}={\\frac {\\sin B}{b}}={\\frac {\\sin C}{c}}={\\frac {2\\Delta }{abc}},}"},{"type":"math_alttext","value":"{\\displaystyle {\\frac {a}{\\sin A}}={\\frac {b}{\\sin B}}={\\frac {c}{\\sin C}}=2R,}"}] | — |
modifiedLaw of cosines30e546ab00d1
| Field | From #1642 | To #1972 |
|---|
| anchors | [{"section":"Law of cosines","snippet":"The law of cosines (also known as the cosine formula or cosine rule) is a generalization of the Pythagorean theorem"},{"type":"math_alttext","value":"{\\displaystyle c^{2}=a^{2}+b^{2}-2ab\\cos C,}"},{"type":"math_alttext","value":"{\\displaystyle \\cos C={\\frac {a^{2}+b^{2}-c^{2}}{2ab}}.}"}] | — |
modifiedLaw of tangentsa24830f25312
| Field | From #1642 | To #1972 |
|---|
| anchors | [{"section":"Law of tangents","snippet":"The law of tangents says that"},{"type":"math_alttext","value":"{\\displaystyle {\\frac {\\tan {\\frac {A-B}{2}}}{\\tan {\\frac {A+B}{2}}}}={\\frac {a-b}{a+b}}}"}] | — |
modifiedLaw of cotangentse1c4e4cdc611
| Field | From #1642 | To #1972 |
|---|
| anchors | [{"section":"Law of cotangents","snippet":"The law of cotangents says that"},{"type":"math_alttext","value":"{\\displaystyle \\cot {\\frac {A}{2}}={\\frac {s-a}{r}}.}"},{"type":"math_alttext","value":"{\\displaystyle {\\frac {\\cot {\\dfrac {A}{2}}}{s-a}}={\\frac {\\cot {\\dfrac {B}{2}}}{s-b}}={\\frac {\\cot {\\dfrac {C}{2}}}{s-c}}={\\frac {1}{r}}.}"}] | — |
modifiedFourier series of periodic functions278548e4a247
| Field | From #1642 | To #1972 |
|---|
| anchors | [{"section":"Periodic functions","snippet":"a periodic function f ( x ) can be expressed as a sum of sine waves or cosine waves in a Fourier series"},{"type":"math_alttext","value":"{\\displaystyle f(t)=\\sum _{k=1}^{\\infty }c_{k}\\varphi _{k}(t).}"}] | — |
| note | Fourier coefficients/series for L²-functions on `AddCircle` are formalised (`Mathlib.Analysis.Fourier.AddCircle`), but no general convergence-of-Fourier-series theorem for arbitrary periodic functions is identified. | Fourier coefficients/series for L²-functions on `AddCircle` are formalised, but no general convergence-of-Fourier-series theorem for arbitrary periodic functions is identified. |
modifiedSquare wave Fourier series37cc674f196b
| Field | From #1642 | To #1972 |
|---|
| anchors | [{"section":"Periodic functions","snippet":"the square wave can be written as the Fourier series"},{"type":"math_alttext","value":"{\\displaystyle f_{\\text{square}}(t)={\\frac {4}{\\pi }}\\sum _{k=1}^{\\infty }{\\sin {\\big (}(2k-1)t{\\big )} \\over 2k-1}.}"}] | — |