:: Formalization of Wallis Infinite Product Formula for $\pi$ and the Wallis Integral
:: by Yasushige Watase
::
:: Received September 17, 2025
:: Copyright (c) 2025-2026 Association of Mizar Users

Lm11: for seq being positive-yielding Real_Sequence
for k being Nat holds seq . k > 0

proof end;

Lm9: for n being Nat holds
( (1 / PI) - (1 / ((1 + (1 / (2 * (n + 1)))) * PI)) > 0 & (1 + (1 / (2 * (n + 1)))) * PI > 0 & 1 / ((1 + (1 / (2 * (n + 1)))) * PI) > 0 )

proof end;

theorem Th39: :: WALLIS01:1

for n being Nat
for x being Real st 0 < x & x < PI / 2 holds
( 0 < sin . x & sin . x < 1 )

proof end;

theorem Th40: :: WALLIS01:2

for n, m being Nat
for x being Real st n < m & 0 < x & x < 1 holds
x |^ m < x |^ n

proof end;

theorem Th41: :: WALLIS01:3

for n being non zero Nat
for x being Real st 0 < x & x < PI / 2 holds
( (sin . x) |^ (2 * n) < (sin . x) |^ ((2 * n) -' 1) & (sin . x) |^ ((2 * n) + 1) < (sin . x) |^ (2 * n) )

proof end;

::::::::::::::::::::::::::::::::::::::
:: 1. Some results on double factorial
::::::::::::::::::::::::::::::::::::::

definition

let m be Nat;

func even-seq m -> FinSequence of INT means :Def1: :: WALLIS01:def 1
( len it = m & ( for i being Nat st i in dom it holds
it . i = 2 * i ) );

existence
ex b₁ being FinSequence of INT st
( len b₁ = m & ( for i being Nat st i in dom b₁ holds
b₁ . i = 2 * i ) )

proof end;

uniqueness
for b₁, b₂ being FinSequence of INT st len b₁ = m & ( for i being Nat st i in dom b₁ holds
b₁ . i = 2 * i ) & len b₂ = m & ( for i being Nat st i in dom b₂ holds
b₂ . i = 2 * i ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines even-seq WALLIS01:def 1 :
for m being Nat
for b₂ being FinSequence of INT holds
( b₂ = even-seq m iff ( len b₂ = m & ( for i being Nat st i in dom b₂ holds
b₂ . i = 2 * i ) ) );

definition

let m be non zero Nat;

func odd-seq m -> FinSequence of INT equals :: WALLIS01:def 2
(even-seq m) + ((dom (even-seq m)) --> (- 1));

coherence
(even-seq m) + ((dom (even-seq m)) --> (- 1)) is FinSequence of INT

proof end;

end;

:: deftheorem defines odd-seq WALLIS01:def 2 :
for m being non zero Nat holds odd-seq m = (even-seq m) + ((dom (even-seq m)) --> (- 1));

theorem Th1: :: WALLIS01:4

for n being non zero Nat holds
( dom (even-seq n) = Seg n & dom (odd-seq n) = Seg n & len (odd-seq n) = n & len (even-seq n) = n )

proof end;

theorem Th2: :: WALLIS01:5

for n being non zero Nat
for i being Nat st i in dom (odd-seq n) holds
(odd-seq n) . i = (2 * i) - 1

proof end;

Lm1: for n being non zero Nat holds even-seq n is positive-yielding

proof end;

registration

let n be non zero Nat;

cluster even-seq n -> positive-yielding ;

coherence
even-seq n is positive-yielding by Lm1;

end;

registration

let n be non zero Nat;

cluster even-seq n -> non empty ;

coherence
not even-seq n is empty

proof end;

end;

Lm2: for n being non zero Nat holds odd-seq n is positive-yielding

proof end;

registration

let n be non zero Nat;

cluster odd-seq n -> positive-yielding ;

coherence
odd-seq n is positive-yielding by Lm2;

end;

registration

let n be non zero Nat;

cluster odd-seq n -> non empty ;

coherence
not odd-seq n is empty

proof end;

end;

Lm3: for n being non zero Nat holds even-seq n is increasing

proof end;

Lm4: for n being non zero Nat holds odd-seq n is increasing

proof end;

registration

let n be non zero Nat;

cluster even-seq n -> increasing ;

coherence
even-seq n is increasing by Lm3;

cluster odd-seq n -> increasing ;

coherence
odd-seq n is increasing by Lm4;

end;

theorem Th3: :: WALLIS01:6

for n being non zero Nat holds even-seq (n + 1) = (even-seq n) ^ <*(2 * (n + 1))*>

proof end;

theorem :: WALLIS01:7

for n being non zero Nat holds Product (even-seq (n + 1)) = (2 * (n + 1)) * (Product (even-seq n))

proof end;

theorem Th5: :: WALLIS01:8

( even-seq 1 = <*2*> & even-seq 2 = <*2,4*> & even-seq 3 = <*2,4,6*> )

proof end;

theorem Th6: :: WALLIS01:9

for n being non zero Nat holds (odd-seq (n + 1)) | (Seg n) = odd-seq n

proof end;

theorem Th7: :: WALLIS01:10

for n being non zero Nat holds odd-seq (n + 1) = (odd-seq n) ^ <*((2 * n) + 1)*>

proof end;

theorem Th8: :: WALLIS01:11

( odd-seq 1 = <*1*> & odd-seq 2 = <*1,3*> & odd-seq 3 = <*1,3,5*> )

proof end;

theorem Th9: :: WALLIS01:12

for n being non zero Nat holds Product (even-seq (n + 1)) = (2 * (n + 1)) * (Product (even-seq n))

proof end;

theorem Th10: :: WALLIS01:13

for n being non zero Nat holds Product (odd-seq (n + 1)) = ((2 * n) + 1) * (Product (odd-seq n))

proof end;

theorem Th11: :: WALLIS01:14

for k being non zero Nat holds Product (even-seq k) = (2 |^ k) * (k !)

proof end;

theorem Th12: :: WALLIS01:15

for k being non zero Nat holds Product (odd-seq k) = ((2 * k) !) / ((2 |^ k) * (k !))

proof end;

::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: 2. Treating a function as Elements of $\mathbb{R}$-algebra
::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

definition

let A be set ;
let f be Element of (RAlgebra A);

func @ f -> Element of Funcs (A,REAL) equals :: WALLIS01:def 3
f;

coherence
f is Element of Funcs (A,REAL) ;

end;

:: deftheorem defines @ WALLIS01:def 3 :
for A being set
for f being Element of (RAlgebra A) holds @ f = f;

definition

let A be set ;
let f be Function of A,REAL;

func @ f -> Element of (RAlgebra A) equals :: WALLIS01:def 4
f;

coherence
f is Element of (RAlgebra A) by FUNCT_2:8;

end;

:: deftheorem defines @ WALLIS01:def 4 :
for A being set
for f being Function of A,REAL holds @ f = f;

registration

let A be set ;
let f be Element of (RAlgebra A);

reduce @ (@ f) to f;

reducibility
@ (@ f) = f ;

end;

registration

let A be set ;
let f be Function of A,REAL;

reduce @ (@ f) to f;

reducibility
@ (@ f) = f ;

end;

theorem Th13: :: WALLIS01:16

for A being non empty set
for f, g being Element of (RAlgebra A) holds
( f * g = (@ f) (#) (@ g) & @ (f * g) = (@ f) (#) (@ g) ) by FUNCSDOM:29;

theorem Th14: :: WALLIS01:17

for A being non empty set
for a being Element of REAL
for f being Element of (RAlgebra A) holds a (#) (@ f) = a * f by FUNCSDOM:30;

registration

cluster RAlgebra REAL -> scalar-unital ;

coherence
RAlgebra REAL is scalar-unital

proof end;

end;

theorem :: WALLIS01:18

RAlgebra REAL is RealLinearSpace ;

theorem :: WALLIS01:19

for A being non empty set
for f, g being Element of (RAlgebra A) holds (RealFuncAdd A) . (f,g) = (RealFuncAdd A) . ((@ f),(@ g)) ;

theorem Th17: :: WALLIS01:20

for A being non empty set
for f being Element of (RAlgebra A) holds
( (- 1) * f = (- 1) (#) (@ f) & @ ((- 1) * f) = - (@ f) & 0. (RAlgebra A) = 0 (#) (@ f) )

proof end;

theorem Th18: :: WALLIS01:21

for A being non empty set
for f, g being Element of (RAlgebra A) holds f + g = (@ f) + (@ g) by FUNCSDOM:28;

theorem Th19: :: WALLIS01:22

for f, g being Element of (RAlgebra REAL) holds f - g = (@ f) - (@ g)

proof end;

theorem Th20: :: WALLIS01:23

for M being non empty unital associative multMagma
for n being Nat
for a being Element of M holds a |^ (n + 1) = (a |^ n) * a

proof end;

Lm5: for x being Element of (RAlgebra REAL) holds x |^ 0 = REAL --> 1

proof end;

Lm6: for x being Function of REAL,REAL holds (@ x) |^ 0 = REAL --> 1

proof end;

theorem Th21: :: WALLIS01:24

for n being Nat
for x being Function of REAL,REAL st x is continuous holds
@ ((@ x) |^ n) is continuous

proof end;

theorem Th22: :: WALLIS01:25

for x being Function of REAL,REAL
for n being Nat
for a being Real st (@ (@ x)) . a > 0 holds
(@ ((@ x) |^ n)) . a = ((@ (@ x)) . a) |^ n

proof end;

theorem Th23: :: WALLIS01:26

for x being Function of REAL,REAL
for n being non zero Nat
for a being Real st (@ (@ x)) . a = 0 holds
(@ ((@ x) |^ n)) . a = 0

proof end;

theorem Th24: :: WALLIS01:27

for Z being open Subset of REAL
for n being non zero Nat
for x being Function of REAL,REAL st x is_differentiable_on Z holds
@ ((@ x) |^ n) is_differentiable_on Z

proof end;

theorem Th25: :: WALLIS01:28

for n being Nat
for I being non empty closed_interval Subset of REAL
for x being Function of REAL,REAL st x is continuous holds
( (@ ((@ x) |^ n)) | I is continuous & @ ((@ x) |^ n) is_integrable_on I & (@ ((@ x) |^ n)) | I is bounded )

proof end;

theorem Th26: :: WALLIS01:29

for r being Real
for n being Nat
for I being non empty closed_interval Subset of REAL
for x being Function of REAL,REAL st x is continuous holds
( (r (#) (@ ((@ x) |^ n))) | I is continuous & r (#) (@ ((@ x) |^ n)) is_integrable_on I & (r (#) (@ ((@ x) |^ n))) | I is bounded )

proof end;

Lm7: REAL is open Subset of REAL

proof end;

theorem Th27: :: WALLIS01:30

for n being non zero Nat holds
( (@ ((@ sin) |^ n)) . 0 = 0 & (@ ((@ sin) |^ n)) . (PI / 2) = 1 )

proof end;

theorem Th28: :: WALLIS01:31

for n being non zero Nat holds (@ ((@ sin) |^ (n + 1))) `| REAL = ((n + 1) (#) (@ ((@ sin) |^ n))) (#) (@ (@ cos))

proof end;

::::::::::::::::::::::::::::::::::::
:: 3. Recurrence relation on $\int_0^{\frac{\pi}{2}} \sin^{n} x \ dx$
:: \& Wallis Integral
:::::::::::::::::::::::::::::::::::

theorem :: WALLIS01:32

(@ ((@ sin) |^ 1)) `| REAL is_differentiable_on REAL by BINOM:8, INTEGRA8:27, SIN_COS:67;

theorem :: WALLIS01:33

for n being non zero Nat holds (@ ((@ sin) |^ (n + 1))) `| REAL is_differentiable_on REAL

proof end;

theorem Th31: :: WALLIS01:34

for n being Nat st n >= 2 holds
@ ((@ sin) |^ (n -' 1)) is_integral_of ((n -' 1) (#) (@ ((@ sin) |^ (n -' 2)))) (#) (@ (@ cos)), REAL

proof end;

theorem Th32: :: WALLIS01:35

integral ((@ ((@ sin) |^ 0)),0,(PI / 2)) = PI / 2

proof end;

theorem Th33: :: WALLIS01:36

integral ((@ ((@ sin) |^ 1)),0,(PI / 2)) = 1

proof end;

theorem Th34: :: WALLIS01:37

(sin (#) sin) + (cos (#) cos) = 1. (RAlgebra REAL)

proof end;

theorem Th35: :: WALLIS01:38

( ((@ sin) |^ 2) + ((@ cos) |^ 2) = 1. (RAlgebra REAL) & (@ sin) |^ 2 = sin (#) sin & (@ cos) |^ 2 = cos (#) cos & (@ sin) |^ 2 = (@ sin) * (@ sin) & (@ cos) |^ 2 = (@ cos) * (@ cos) )

proof end;

definition

func 'I' -> Real_Sequence means :Def6: :: WALLIS01:def 5
for m being Nat holds it . m = integral ((@ ((@ sin) |^ m)),0,(PI / 2));

correctness
existence
ex b₁ being Real_Sequence st
for m being Nat holds b₁ . m = integral ((@ ((@ sin) |^ m)),0,(PI / 2));
uniqueness
for b₁, b₂ being Real_Sequence st ( for m being Nat holds b₁ . m = integral ((@ ((@ sin) |^ m)),0,(PI / 2)) ) & ( for m being Nat holds b₂ . m = integral ((@ ((@ sin) |^ m)),0,(PI / 2)) ) holds
b₁ = b₂;

proof end;

end;

:: deftheorem Def6 defines 'I' WALLIS01:def 5 :
for b₁ being Real_Sequence holds
( b₁ = 'I' iff for m being Nat holds b₁ . m = integral ((@ ((@ sin) |^ m)),0,(PI / 2)) );

:::::::::::::::::::::::::::::::::
::4. the Wallis Product Formula
::::::::::::::::::::::::::::::::

theorem Th36: :: WALLIS01:39

for n being Nat st n >= 2 holds
((n -' 1) / n) * ('I' . (n -' 2)) = 'I' . n

proof end;

theorem Th37: :: WALLIS01:40

for n being non zero Nat holds 'I' . ((2 * n) + 1) = (Product (even-seq n)) / (Product (odd-seq (n + 1)))

proof end;

theorem Th38: :: WALLIS01:41

for n being non zero Nat holds 'I' . (2 * n) = ((Product (odd-seq n)) / (Product (even-seq n))) * (PI / 2)

proof end;

:::::::::::::::::::::::::
:: Wallis Product
::::::::::::::::::::::::

theorem Th42: :: WALLIS01:42

for n being non zero Nat
for x being Real st 0 < x & x < PI / 2 holds
( (@ ((@ sin) |^ (2 * n))) . x < (@ ((@ sin) |^ ((2 * n) -' 1))) . x & (@ ((@ sin) |^ ((2 * n) + 1))) . x < (@ ((@ sin) |^ (2 * n))) . x )

proof end;

theorem Th43: :: WALLIS01:43

for n being non zero Nat holds
( 'I' . (2 * n) <= 'I' . ((2 * n) -' 1) & 'I' . ((2 * n) + 1) <= 'I' . (2 * n) )

proof end;

theorem Th44: :: WALLIS01:44

for n being non zero Nat holds
( 1 <= ('I' . (2 * n)) / ('I' . ((2 * n) + 1)) & ('I' . (2 * n)) / ('I' . ((2 * n) + 1)) = ((((Product (odd-seq n)) |^ 2) / ((Product (even-seq n)) |^ 2)) * n) * ((1 + (1 / (2 * n))) * PI) )

proof end;

theorem Th45: :: WALLIS01:45

for n being non zero Nat holds 1 / ((1 + (1 / (2 * n))) * PI) <= (((Product (odd-seq n)) |^ 2) / ((Product (even-seq n)) |^ 2)) * n

proof end;

Lm8: for n being non zero Nat holds 0 < 'I' . ((2 * n) -' 1)

proof end;

theorem Th46: :: WALLIS01:46

for n being non zero Nat holds ('I' . (2 * n)) / ('I' . ((2 * n) + 1)) <= 1 + (1 / (2 * n))

proof end;

theorem Th47: :: WALLIS01:47

for n being non zero Nat holds (((Product (odd-seq n)) |^ 2) / ((Product (even-seq n)) |^ 2)) * n <= 1 / PI

proof end;

definition

func Wallis_Seq -> Real_Sequence means :Def7: :: WALLIS01:def 6
for k being Nat holds it . k = (((Product (odd-seq (k + 1))) |^ 2) / ((Product (even-seq (k + 1))) |^ 2)) * (k + 1);

correctness
existence
ex b₁ being Real_Sequence st
for k being Nat holds b₁ . k = (((Product (odd-seq (k + 1))) |^ 2) / ((Product (even-seq (k + 1))) |^ 2)) * (k + 1);
uniqueness
for b₁, b₂ being Real_Sequence st ( for k being Nat holds b₁ . k = (((Product (odd-seq (k + 1))) |^ 2) / ((Product (even-seq (k + 1))) |^ 2)) * (k + 1) ) & ( for k being Nat holds b₂ . k = (((Product (odd-seq (k + 1))) |^ 2) / ((Product (even-seq (k + 1))) |^ 2)) * (k + 1) ) holds
b₁ = b₂;

proof end;

end;

:: deftheorem Def7 defines Wallis_Seq WALLIS01:def 6 :
for b₁ being Real_Sequence holds
( b₁ = Wallis_Seq iff for k being Nat holds b₁ . k = (((Product (odd-seq (k + 1))) |^ 2) / ((Product (even-seq (k + 1))) |^ 2)) * (k + 1) );

definition

func w_seq -> Real_Sequence means :Def8: :: WALLIS01:def 7
for n being Nat holds it . n = 1 / ((1 + (1 / (2 * (n + 1)))) * PI);

correctness
existence
ex b₁ being Real_Sequence st
for n being Nat holds b₁ . n = 1 / ((1 + (1 / (2 * (n + 1)))) * PI);
uniqueness
for b₁, b₂ being Real_Sequence st ( for n being Nat holds b₁ . n = 1 / ((1 + (1 / (2 * (n + 1)))) * PI) ) & ( for n being Nat holds b₂ . n = 1 / ((1 + (1 / (2 * (n + 1)))) * PI) ) holds
b₁ = b₂;

proof end;

end;

:: deftheorem Def8 defines w_seq WALLIS01:def 7 :
for b₁ being Real_Sequence holds
( b₁ = w_seq iff for n being Nat holds b₁ . n = 1 / ((1 + (1 / (2 * (n + 1)))) * PI) );

Lm10: ( w_seq is convergent & lim w_seq = 1 / PI )

proof end;

theorem Th48: :: WALLIS01:48

( lim Wallis_Seq = 1 / PI & Wallis_Seq is convergent )

proof end;

theorem Th49: :: WALLIS01:49

Wallis_Seq is positive-yielding

proof end;

registration

cluster Wallis_Seq -> positive-yielding ;

coherence
Wallis_Seq is positive-yielding by Th49;

end;

theorem Th50: :: WALLIS01:50

for seq being positive-yielding Real_Sequence st seq is convergent holds
( sqrt seq is convergent & lim (sqrt seq) = sqrt (lim seq) )

proof end;

theorem :: WALLIS01:51

lim (sqrt Wallis_Seq) = 1 / (sqrt PI)

proof end;

theorem :: WALLIS01:52

for n being non zero Nat holds (sqrt Wallis_Seq) . (n -' 1) = ((sqrt n) * ((2 * n) !)) / ((4 |^ n) * ((n !) |^ 2))

proof end;