Leibniz Formula from a Fourier Series¶
The Leibniz series
$$ \frac{\pi}{4}=1-\frac13+\frac15-\frac17+\cdots $$
follows by evaluating the Fourier series of the sawtooth $f(x)=x$ at $x=\pi/2$. This notebook derives the coefficients symbolically before making that substitution.
The sawtooth and its coefficients¶
Since $f$ is odd, only sine terms occur:
$$ x=\sum_{k=1}^{\infty}b_k\sin(kx),\qquad b_k=\frac1\pi\int_{-\pi}^{\pi}x\sin(kx)\,dx. $$
declare symbol x, n : MathValue
def f (x : MathValue) : MathValue := x
def cosinePrimitive (k : MathValue) : MathValue :=
x * sin (k * x) / k + cos (k * x) / k^2
def sinePrimitive (k : MathValue) : MathValue :=
(- x) * cos (k * x) / k + sin (k * x) / k^2
def cosineCoefficients : [MathValue] :=
map
(\k ->
let primitive := cosinePrimitive k
in (substitute [(x, π)] primitive - substitute [(x, - π)] primitive) / π)
nats
def sineCoefficients : [MathValue] :=
map
(\k ->
let primitive := sinePrimitive k
in (substitute [(x, π)] primitive - substitute [(x, - π)] primitive) / π)
nats
take 10 sineCoefficients
Fourier terms¶
Egison now combines each coefficient with its basis function.
def fourierTerms : [MathValue] :=
map (\(k, b) -> b * sin (k * x)) (zip nats sineCoefficients)
take 10 fourierTerms
Evaluate at $x=\pi/2$¶
Even harmonics vanish, while successive odd harmonics alternate in sign. We encode the exact four-step pattern
$$ \sin(k\pi/2)=1,0,-1,0,\ldots $$
before dividing the Fourier terms by two. Thus the identity $\pi/2=2(1-1/3+1/5-\cdots)$ gives the desired series.
def sinAtHalfPi (k : Integer) : MathValue :=
if isEven k
then 0
else (-1) ^ (i.quotient (k - 1) 2)
def leibnizTerms : [MathValue] :=
map
(\(k, b) -> b * sinAtHalfPi k / 2)
(zip nats sineCoefficients)
take 10 leibnizTerms
Reading the nonzero entries yields $1,-1/3,1/5,-1/7,\ldots$. Their infinite sum is $\pi/4$; the zeros record the even Fourier modes that vanish at $\pi/2$.