Diff — Pi

Revision #1472 → #1844 · back to history

modifiedDefinition of π as ratio of circumference to diameter7bcbdcaa88ac

Field	From #1472	To #1844
anchors	[{"section":"Definition","snippet":"π is commonly defined as the ratio of a circle 's circumference C to its diameter d"},{"type":"math_alttext","value":"{\\displaystyle \\pi ={\\frac {C}{d}}.}"}]	—

modifiedDefinition via complex exponential5f45fa7c4463

Field	From #1472	To #1844
anchors	[{"section":"Definition","snippet":"π can be defined using properties of the complex exponential"},{"type":"math_alttext","value":"{\\displaystyle \\{\\dots ,-2\\pi i,0,2\\pi i,4\\pi i,\\dots \\}=\\{2\\pi ki\\mid k\\in \\mathbb {Z} \\}}"}]	—

addedAlgebraic independence of π and e (Schanuel's conjecture)a434c2e0b668

modifiedBest rational approximations from continued fraction5ba3a9ed255a

Field	From #1472	To #1844
mathlib.decl	GenContFract.of_convergents_eq_best_approximation	—
mathlib.module	Mathlib.Algebra.ContinuedFractions.Computation.ApproximationCorollaries	—
note	Mathlib has the general best-rational-approximation theorem for continued fractions, not applied to π specifically.	No best-rational-approximation theorem for continued fractions is present in Mathlib (only convergence corollaries).
status	partial	not_formalized

modifiedEuler's formula0c241b396672

Field	From #1472	To #1844
mathlib.module	Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic	Mathlib.Analysis.Complex.Trigonometric

modifiedArchimedes' polygon bounds on πdf05695ea478

Field	From #1472	To #1844
mathlib.decl	Real.pi_gt_3141592	Real.pi_gt_d6
note	Mathlib has rigorous numeric bounds on π in `Real.Pi.Bounds` but not Archimedes' specific polygon-perimeter argument.	Mathlib has rigorous numeric bounds such as `Real.pi_gt_d6 : 3.141592 < π` in `Real.Pi.Bounds` but not Archimedes' specific polygon-perimeter argument.

modifiedGauss–Legendre iterative algorithm2a6dd49584ec

Field	From #1472	To #1844
anchors	[{"section":"Computer era and iterative algorithms","snippet":"The Gauss–Legendre iterative algorithm"},{"type":"math_alttext","value":"{\\displaystyle \\textstyle a_{0}=1,\\quad b_{0}={\\frac {1}{\\sqrt {2}}},\\quad t_{0}={\\frac {1}{4}},\\quad p_{0}=1.}"},{"type":"math_alttext","value":"{\\displaystyle \\textstyle a_{n+1}={\\frac {a_{n}+b_{n}}{2}},\\quad \\quad b_{n+1}={\\sqrt {a_{n}b_{n}}},}"},{"type":"math_alttext","value":"{\\displaystyle \\textstyle t_{n+1}=t_{n}-p_{n}(a_{n}-a_{n+1})^{2},\\quad \\quad p_{n+1}=2p_{n}.}"},{"type":"math_alttext","value":"{\\displaystyle \\textstyle \\pi \\approx {\\frac {(a_{n}+b_{n})^{2}}{4t_{n}}}.}"}]	—

modifiedBBP digit extraction formula4b7575f17ab8

Field	From #1472	To #1844
anchors	[{"section":"Spigot algorithms","snippet":"the BBP digit extraction algorithm , was discovered in 1995 by Simon Plouffe"},{"type":"math_alttext","value":"{\\displaystyle \\pi =\\sum _{k=0}^{\\infty }{\\frac {1}{16^{k}}}\\left({\\frac {4}{8k+1}}-{\\frac {2}{8k+4}}-{\\frac {1}{8k+5}}-{\\frac {1}{8k+6}}\\right).}"}]	—

modifiedPeriodicity of sine and cosineffee7ae44fc7

Field	From #1472	To #1844
anchors	[{"section":"Unit of angle","snippet":"sine and cosine have period 2 π"},{"type":"math_alttext","value":"{\\displaystyle \\sin \\theta =\\sin \\left(\\theta +2\\pi k\\right){\\text{ and }}\\cos \\theta =\\cos \\left(\\theta +2\\pi k\\right).}"}]	—

modifiedFourier transforma9206f4d904c

Field	From #1472	To #1844
mathlib.decl	Real.fourierIntegral	Fourier.fourierIntegral
note	`Real.fourierIntegral` (and the more general `VectorFourier.fourierIntegral`) defines the Fourier transform with the `e^{-2πi x ξ}` convention.	`Fourier.fourierIntegral` (with the real-line wrapper `FourierTransform.fourier`) defines the Fourier transform with the `e^{-2πi x ξ}` convention.

modifiedCharacters of the circle groupe671eba4ee06

Field	From #1472	To #1844
mathlib.module	Mathlib.Analysis.Complex.Circle	Mathlib.Analysis.SpecialFunctions.Complex.Circle