Leibniz Formula

Verify Leibniz formula using Fourier series expansion

Let's consider a sawtooth wave function as follow.

`f(x) = x`       `(-pi < x < pi)`
`f(x + 2 n pi) = f(x)`

We calculate the Fourier coefficients of this function.

`f(x) = a_0 / 2 + sum_(k=0) a_k cos(k x) + sum_(k=0) b_k sin(k x)`

In the program, we calculate the following expressions to get the Fourier coefficients.

`a_0 = 1 / pi int_(-pi)^pi f(x) dx = 0`

`a_k = 1 / pi int_(-pi)^pi f(x) cos(k x) dx = 0`

`b_k = 1 / pi int_(-pi)^pi f(x) sin(k x) dx = (2 (-1)^k) / k`

Then, we get

`f(x) = sum_(k=0) ((2 (-1)^k sin(k x)) / k)`.

If we substitute `x` with `pi / 2` in the above equation, we get Leibniz formula as follow.

`pi / 4 = 1 - 1 / 3 + 1 / 5 - 1 / 7 + 1 / 9 - ...` -- -- This file has been auto-generated by egison-translator. -- def f $x := x def multSd $x $f $G := let F := Sd x f in F * G - Sd x (f * d/d G x) multSd x (cos x) (f x) multSd x (cos (2 * x)) (f x) multSd x (cos (n * x)) (f x) multSd x (sin x) (f x) multSd x (sin (2 * x)) (f x) multSd x (sin (n * x)) (f x) def as := map (\$n -> let F := multSd x (cos (n * x)) (f x) in (substitute [(x, π)] F - substitute [(x, - π)] F) / π) nats take 10 as def bs := map (\$n -> let F := multSd x (sin (n * x)) (f x) in (substitute [(x, π)] F - substitute [(x, - π)] F) / π) (take 10 nats) take 10 bs def f' := map (\$k $b -> b * sin (k * x)) (zip nats bs) take 10 f' take 10 (map 1#(substitute [(x, π / 2)] %1) f') map 1#(%1 / 2) (take 10 (map 1#(substitute [(x, π / 2)] %1) f'))

Links

Back to the Table of Contents