:: A Formal Proof of {S}tirling's Formula
:: by Yasushige Watase
::
:: Received September 17, 2025
:: Copyright (c) 2025-2026 Association of Mizar Users

Lm1: for n being Nat holds divset ((EqDiv (['0,1'],(n + 1))),1) = [.0,(1 / (n + 1)).]

proof end;

theorem Th1: :: STIRLIN1:1

for n, k being Nat st k in Seg (n + 1) holds
divset ((EqDiv (['0,1'],(n + 1))),k) = [.((k -' 1) / (n + 1)),(k / (n + 1)).]

proof end;

definition

func D[01] -> sequence of (divs ['0,1']) means :Def1: :: STIRLIN1:def 1
for n being Element of NAT holds it . n = EqDiv (['0,1'],(n + 1));

existence
ex b₁ being sequence of (divs ['0,1']) st
for n being Element of NAT holds b₁ . n = EqDiv (['0,1'],(n + 1))

proof end;

uniqueness
for b₁, b₂ being sequence of (divs ['0,1']) st ( for n being Element of NAT holds b₁ . n = EqDiv (['0,1'],(n + 1)) ) & ( for n being Element of NAT holds b₂ . n = EqDiv (['0,1'],(n + 1)) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines D[01] STIRLIN1:def 1 :
for b₁ being sequence of (divs ['0,1']) holds
( b₁ = D[01] iff for n being Element of NAT holds b₁ . n = EqDiv (['0,1'],(n + 1)) );

theorem Th2: :: STIRLIN1:2

for n being Nat holds delta (EqDiv (['0,1'],(n + 1))) = 1 / (n + 1)

proof end;

theorem Th3: :: STIRLIN1:3

delta D[01] is non-zero 0 -convergent Real_Sequence

proof end;

definition

let a, b be Real;

func ax_+_b (a,b) -> PartFunc of REAL,REAL equals :: STIRLIN1:def 2
AffineMap (a,b);

coherence
AffineMap (a,b) is PartFunc of REAL,REAL ;

end;

:: deftheorem defines ax_+_b STIRLIN1:def 2 :
for a, b being Real holds ax_+_b (a,b) = AffineMap (a,b);

definition

let r be Real;

func const r -> PartFunc of REAL,REAL equals :: STIRLIN1:def 3
AffineMap (0,r);

coherence
AffineMap (0,r) is PartFunc of REAL,REAL ;

end;

:: deftheorem defines const STIRLIN1:def 3 :
for r being Real holds const r = AffineMap (0,r);

Lm2: for r being Real holds const r is constant Function of REAL,REAL

proof end;

registration

let r be Real;

cluster const r -> constant ;

coherence
const r is constant by Lm2;

end;

Lm3: for r being Real holds
( const r is total & rng (const r) = {r} )

proof end;

Lm4: for n, k being Nat
for m being non zero Nat
for x0, r being Real st k in Seg (n + 1) & x0 in ['((k -' 1) / (n + 1)),(k / (n + 1))'] holds
( ['x0,(k / (n + 1))'] c= dom (const r) & (const r) | ['x0,(k / (n + 1))'] is continuous & const r is_integrable_on ['x0,(k / (n + 1))'] & (const r) | ['x0,(k / (n + 1))'] is bounded )

proof end;

definition

func rohl -> Subset of REAL equals :: STIRLIN1:def 4
right_open_halfline (- 1);

coherence
right_open_halfline (- 1) is Subset of REAL ;

end;

:: deftheorem defines rohl STIRLIN1:def 4 :
rohl = right_open_halfline (- 1);

definition

let f be PartFunc of REAL,REAL;
let A be non empty closed_interval Subset of REAL;

pred f is_C^1-Class_on A means :: STIRLIN1:def 5
( f is_differentiable_on right_open_halfline (- 1) & f `| (right_open_halfline (- 1)) is continuous & A c= right_open_halfline (- 1) & right_open_halfline (- 1) c= dom f );

end;

:: deftheorem defines is_C^1-Class_on STIRLIN1:def 5 :
for f being PartFunc of REAL,REAL
for A being non empty closed_interval Subset of REAL holds
( f is_C^1-Class_on A iff ( f is_differentiable_on right_open_halfline (- 1) & f `| (right_open_halfline (- 1)) is continuous & A c= right_open_halfline (- 1) & right_open_halfline (- 1) c= dom f ) );

definition

let A be non empty closed_interval Subset of REAL;
let f be PartFunc of REAL,REAL;
assume A1: f is_C^1-Class_on A ;

func @' (f,A) -> Function of A,REAL equals :Def6: :: STIRLIN1:def 6
(f `| (right_open_halfline (- 1))) | A;

coherence
(f `| (right_open_halfline (- 1))) | A is Function of A,REAL

proof end;

end;

:: deftheorem Def6 defines @' STIRLIN1:def 6 :
for A being non empty closed_interval Subset of REAL
for f being PartFunc of REAL,REAL st f is_C^1-Class_on A holds
@' (f,A) = (f `| (right_open_halfline (- 1))) | A;

definition

let A be non empty closed_interval Subset of REAL;
let f be PartFunc of REAL,REAL;
assume A1: A c= dom f ;

func @ (f,A) -> Function of A,REAL equals :: STIRLIN1:def 7
f | A;

coherence
f | A is Function of A,REAL

proof end;

end;

:: deftheorem defines @ STIRLIN1:def 7 :
for A being non empty closed_interval Subset of REAL
for f being PartFunc of REAL,REAL st A c= dom f holds
@ (f,A) = f | A;

Lm5: for n, k being Nat
for x0 being Real
for f being PartFunc of REAL,REAL st k in Seg (n + 1) & x0 in ['((k -' 1) / (n + 1)),(k / (n + 1))'] & f is_C^1-Class_on ['0,1'] holds
( (f `| rohl) | ['x0,(k / (n + 1))'] is continuous & f `| rohl is_integrable_on ['x0,(k / (n + 1))'] & (f `| rohl) | ['x0,(k / (n + 1))'] is bounded )

proof end;

Lm6: for f being PartFunc of REAL,REAL st f is_C^1-Class_on ['0,1'] holds
( (f `| rohl) | ['0,1'] is continuous & f `| rohl is_integrable_on ['0,1'] & (f `| rohl) | ['0,1'] is bounded )

proof end;

Lm7: for n, k being Nat
for f being PartFunc of REAL,REAL st k in Seg (n + 1) & f is_C^1-Class_on ['0,1'] holds
( (f `| rohl) | ['((k -' 1) / (n + 1)),(k / (n + 1))'] is continuous & f `| rohl is_integrable_on ['((k -' 1) / (n + 1)),(k / (n + 1))'] & (f `| rohl) | ['((k -' 1) / (n + 1)),(k / (n + 1))'] is bounded )

proof end;

theorem Th4: :: STIRLIN1:4

for n, k being Nat
for x0 being Real
for f being PartFunc of REAL,REAL st k in Seg (n + 1) & x0 in ['((k -' 1) / (n + 1)),(k / (n + 1))'] & f is_C^1-Class_on ['0,1'] holds
integral ((f `| rohl),['x0,(k / (n + 1))']) = (f . (upper_bound ['x0,(k / (n + 1))'])) - (f . (lower_bound ['x0,(k / (n + 1))']))

proof end;

Lm8: for n, k being Nat
for f being PartFunc of REAL,REAL st k in Seg (n + 1) & f is_C^1-Class_on ['0,1'] holds
for x being Real st x in ['((k -' 1) / (n + 1)),(k / (n + 1))'] holds
(f `| rohl) . x <= upper_bound (rng ((f `| rohl) | ['((k -' 1) / (n + 1)),(k / (n + 1))']))

proof end;

Lm9: for n, k being Nat
for f being PartFunc of REAL,REAL st k in Seg (n + 1) & f is_C^1-Class_on ['0,1'] holds
for x being Real st x in ['((k -' 1) / (n + 1)),(k / (n + 1))'] holds
lower_bound (rng ((f `| rohl) | ['((k -' 1) / (n + 1)),(k / (n + 1))'])) <= (f `| rohl) . x

proof end;

definition

let n be Nat;
let f be PartFunc of REAL,REAL;

func UPBND_rng_d (f,n) -> FinSequence of F_Real means :Def8: :: STIRLIN1:def 8
( len it = n + 1 & ( for i being Nat st i in dom it holds
it . i = upper_bound (rng ((f `| rohl) | ['((i -' 1) / (n + 1)),(i / (n + 1))'])) ) );

existence
ex b₁ being FinSequence of F_Real st
( len b₁ = n + 1 & ( for i being Nat st i in dom b₁ holds
b₁ . i = upper_bound (rng ((f `| rohl) | ['((i -' 1) / (n + 1)),(i / (n + 1))'])) ) )

proof end;

uniqueness
for b₁, b₂ being FinSequence of F_Real st len b₁ = n + 1 & ( for i being Nat st i in dom b₁ holds
b₁ . i = upper_bound (rng ((f `| rohl) | ['((i -' 1) / (n + 1)),(i / (n + 1))'])) ) & len b<sub>2</sub> = n + 1 & ( for i being Nat st i in dom b<sub>2</sub> holds
b<sub>2</sub> . i = upper_bound (rng ((f `| rohl) | ['((i -' 1) / (n + 1)),(i / (n + 1))'])) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def8 defines UPBND_rng_d STIRLIN1:def 8 :
for n being Nat
for f being PartFunc of REAL,REAL
for b₃ being FinSequence of F_Real holds
( b₃ = UPBND_rng_d (f,n) iff ( len b₃ = n + 1 & ( for i being Nat st i in dom b₃ holds
b₃ . i = upper_bound (rng ((f `| rohl) | ['((i -' 1) / (n + 1)),(i / (n + 1))'])) ) ) );

definition

let n be Nat;
let f be PartFunc of REAL,REAL;

func LWBND_rng_d (f,n) -> FinSequence of F_Real means :Def9: :: STIRLIN1:def 9
( len it = n + 1 & ( for i being Nat st i in dom it holds
it . i = lower_bound (rng ((f `| rohl) | ['((i -' 1) / (n + 1)),(i / (n + 1))'])) ) );

existence
ex b₁ being FinSequence of F_Real st
( len b₁ = n + 1 & ( for i being Nat st i in dom b₁ holds
b₁ . i = lower_bound (rng ((f `| rohl) | ['((i -' 1) / (n + 1)),(i / (n + 1))'])) ) )

proof end;

uniqueness
for b₁, b₂ being FinSequence of F_Real st len b₁ = n + 1 & ( for i being Nat st i in dom b₁ holds
b₁ . i = lower_bound (rng ((f `| rohl) | ['((i -' 1) / (n + 1)),(i / (n + 1))'])) ) & len b<sub>2</sub> = n + 1 & ( for i being Nat st i in dom b<sub>2</sub> holds
b<sub>2</sub> . i = lower_bound (rng ((f `| rohl) | ['((i -' 1) / (n + 1)),(i / (n + 1))'])) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def9 defines LWBND_rng_d STIRLIN1:def 9 :
for n being Nat
for f being PartFunc of REAL,REAL
for b₃ being FinSequence of F_Real holds
( b₃ = LWBND_rng_d (f,n) iff ( len b₃ = n + 1 & ( for i being Nat st i in dom b₃ holds
b₃ . i = lower_bound (rng ((f `| rohl) | ['((i -' 1) / (n + 1)),(i / (n + 1))'])) ) ) );

definition

let f be PartFunc of REAL,REAL;

func Sum_UPBND_rng_d f -> sequence of REAL means :Def10: :: STIRLIN1:def 10
for i being Nat holds it . i = (Sum (UPBND_rng_d (f,i))) / (i + 1);

existence
ex b₁ being sequence of REAL st
for i being Nat holds b₁ . i = (Sum (UPBND_rng_d (f,i))) / (i + 1)

proof end;

uniqueness
for b₁, b₂ being sequence of REAL st ( for i being Nat holds b₁ . i = (Sum (UPBND_rng_d (f,i))) / (i + 1) ) & ( for i being Nat holds b₂ . i = (Sum (UPBND_rng_d (f,i))) / (i + 1) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def10 defines Sum_UPBND_rng_d STIRLIN1:def 10 :
for f being PartFunc of REAL,REAL
for b₂ being sequence of REAL holds
( b₂ = Sum_UPBND_rng_d f iff for i being Nat holds b₂ . i = (Sum (UPBND_rng_d (f,i))) / (i + 1) );

definition

let f be PartFunc of REAL,REAL;

func Sum_LWBND_rng_d f -> sequence of REAL means :Def11: :: STIRLIN1:def 11
for i being Nat holds it . i = (Sum (LWBND_rng_d (f,i))) / (i + 1);

existence
ex b₁ being sequence of REAL st
for i being Nat holds b₁ . i = (Sum (LWBND_rng_d (f,i))) / (i + 1)

proof end;

uniqueness
for b₁, b₂ being sequence of REAL st ( for i being Nat holds b₁ . i = (Sum (LWBND_rng_d (f,i))) / (i + 1) ) & ( for i being Nat holds b₂ . i = (Sum (LWBND_rng_d (f,i))) / (i + 1) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def11 defines Sum_LWBND_rng_d STIRLIN1:def 11 :
for f being PartFunc of REAL,REAL
for b₂ being sequence of REAL holds
( b₂ = Sum_LWBND_rng_d f iff for i being Nat holds b₂ . i = (Sum (LWBND_rng_d (f,i))) / (i + 1) );

theorem Th5: :: STIRLIN1:5

for n, k being Nat
for x0 being Real
for f being PartFunc of REAL,REAL st k in Seg (n + 1) & x0 in ['((k -' 1) / (n + 1)),(k / (n + 1))'] & f is_C^1-Class_on ['0,1'] holds
( integral ((const ((UPBND_rng_d (f,n)) . k)),x0,(k / (n + 1))) = ((UPBND_rng_d (f,n)) . k) * ((k / (n + 1)) - x0) & integral ((const ((LWBND_rng_d (f,n)) . k)),x0,(k / (n + 1))) = ((LWBND_rng_d (f,n)) . k) * ((k / (n + 1)) - x0) )

proof end;

theorem Th6: :: STIRLIN1:6

for n, k being Nat
for x0 being Real
for f being PartFunc of REAL,REAL st k in Seg (n + 1) & x0 in ['((k -' 1) / (n + 1)),(k / (n + 1))'] & f is_C^1-Class_on ['0,1'] holds
integral ((f `| rohl),x0,(k / (n + 1))) <= integral ((const ((UPBND_rng_d (f,n)) . k)),x0,(k / (n + 1)))

proof end;

theorem Th7: :: STIRLIN1:7

for n, k being Nat
for x0 being Real
for f being PartFunc of REAL,REAL st k in Seg (n + 1) & x0 in ['((k -' 1) / (n + 1)),(k / (n + 1))'] & f is_C^1-Class_on ['0,1'] holds
integral ((const ((LWBND_rng_d (f,n)) . k)),x0,(k / (n + 1))) <= integral ((f `| rohl),x0,(k / (n + 1)))

proof end;

theorem Th8: :: STIRLIN1:8

for n, k being Nat
for x0 being Real
for f being PartFunc of REAL,REAL st k in Seg (n + 1) & x0 in ['((k -' 1) / (n + 1)),(k / (n + 1))'] & f is_C^1-Class_on ['0,1'] holds
( (f . (k / (n + 1))) - (f . x0) <= ((UPBND_rng_d (f,n)) . k) * ((k / (n + 1)) - x0) & ((LWBND_rng_d (f,n)) . k) * ((k / (n + 1)) - x0) <= (f . (k / (n + 1))) - (f . x0) )

proof end;

Lm10: for n, k being Nat
for f being PartFunc of REAL,REAL st k in Seg (n + 1) & f is_C^1-Class_on ['0,1'] holds
for x being Real st x in ['((k -' 1) / (n + 1)),(k / (n + 1))'] holds
( ((const (f . (k / (n + 1)))) + (- f)) . x <= (((UPBND_rng_d (f,n)) . k) (#) (ax_+_b ((- 1),(k / (n + 1))))) . x & (((LWBND_rng_d (f,n)) . k) (#) (ax_+_b ((- 1),(k / (n + 1))))) . x <= ((const (f . (k / (n + 1)))) + (- f)) . x & ((f . (k / (n + 1))) + (- f)) . x = ((const (f . (k / (n + 1)))) + (- f)) . x )

proof end;

Lm11A: for n, k being Nat st k in Seg (n + 1) holds
( (k -' 1) / (n + 1) <= k / (n + 1) & ['((k -' 1) / (n + 1)),(k / (n + 1))'] c= dom (ax_+_b ((- 1),(k / (n + 1)))) )

proof end;

Lm11: for n, k being Nat
for f being PartFunc of REAL,REAL st k in Seg (n + 1) & f is_C^1-Class_on ['0,1'] holds
( ax_+_b ((- 1),(k / (n + 1))) is_integrable_on ['((k -' 1) / (n + 1)),(k / (n + 1))'] & (ax_+_b ((- 1),(k / (n + 1)))) | ['((k -' 1) / (n + 1)),(k / (n + 1))'] is bounded & integral ((((LWBND_rng_d (f,n)) . k) (#) (ax_+_b ((- 1),(k / (n + 1))))),((k -' 1) / (n + 1)),(k / (n + 1))) = (((LWBND_rng_d (f,n)) . k) * ((1 / (n + 1)) ^2)) / 2 & integral ((((UPBND_rng_d (f,n)) . k) (#) (ax_+_b ((- 1),(k / (n + 1))))),((k -' 1) / (n + 1)),(k / (n + 1))) = (((UPBND_rng_d (f,n)) . k) * ((1 / (n + 1)) ^2)) / 2 )

proof end;

Lm12: for n, k being Nat
for f being PartFunc of REAL,REAL st k in Seg (n + 1) & f is_C^1-Class_on ['0,1'] holds
( ['((k -' 1) / (n + 1)),(k / (n + 1))'] c= dom (- f) & ['((k -' 1) / (n + 1)),(k / (n + 1))'] c= dom (const (f . (k / (n + 1)))) & - f is_integrable_on ['((k -' 1) / (n + 1)),(k / (n + 1))'] & (- f) | ['((k -' 1) / (n + 1)),(k / (n + 1))'] is bounded & const (f . (k / (n + 1))) is_integrable_on ['((k -' 1) / (n + 1)),(k / (n + 1))'] & (const (f . (k / (n + 1)))) | ['((k -' 1) / (n + 1)),(k / (n + 1))'] is bounded & integral (((const (f . (k / (n + 1)))) + (- f)),((k -' 1) / (n + 1)),(k / (n + 1))) = (integral ((const (f . (k / (n + 1)))),((k -' 1) / (n + 1)),(k / (n + 1)))) + (integral ((- f),((k -' 1) / (n + 1)),(k / (n + 1)))) )

proof end;

Lm13: for n being non zero Nat
for k being Nat
for f being PartFunc of REAL,REAL st k in Seg n & f is_C^1-Class_on ['0,1'] holds
( - f is_integrable_on ['0,(k / n)'] & (- f) | ['0,(k / n)'] is bounded & ['0,(k / n)'] c= dom (- f) )

proof end;

Lm14: for n being Nat
for f being PartFunc of REAL,REAL st f is_C^1-Class_on ['0,1'] holds
(n + 1) * (upper_volume ((@' (f,['0,1'])),(EqDiv (['0,1'],(n + 1))))) = UPBND_rng_d (f,n)

proof end;

Lm15: for f being PartFunc of REAL,REAL st f is_C^1-Class_on ['0,1'] holds
Sum_UPBND_rng_d f = upper_sum ((@' (f,['0,1'])),D[01])

proof end;

Lm16: for f being PartFunc of REAL,REAL st f is_C^1-Class_on ['0,1'] holds
( upper_sum ((@' (f,['0,1'])),D[01]) is convergent & lim (upper_sum ((@' (f,['0,1'])),D[01])) = upper_integral (@' (f,['0,1'])) & Sum_UPBND_rng_d f is convergent & lim (Sum_UPBND_rng_d f) = upper_integral (@' (f,['0,1'])) )

proof end;

Lm17: for n being Nat
for f being PartFunc of REAL,REAL st f is_C^1-Class_on ['0,1'] holds
(n + 1) * (lower_volume ((@' (f,['0,1'])),(EqDiv (['0,1'],(n + 1))))) = LWBND_rng_d (f,n)

proof end;

Lm18: for f being PartFunc of REAL,REAL st f is_C^1-Class_on ['0,1'] holds
Sum_LWBND_rng_d f = lower_sum ((@' (f,['0,1'])),D[01])

proof end;

Lm19: for f being PartFunc of REAL,REAL st f is_C^1-Class_on ['0,1'] holds
( lower_sum ((@' (f,['0,1'])),D[01]) is convergent & lim (lower_sum ((@' (f,['0,1'])),D[01])) = lower_integral (@' (f,['0,1'])) & Sum_LWBND_rng_d f is convergent & lim (Sum_LWBND_rng_d f) = lower_integral (@' (f,['0,1'])) )

proof end;

definition

let n be Nat;
let f be PartFunc of REAL,REAL;

func 'F' (f,n) -> FinSequence of F_Real means :: STIRLIN1:def 12
( dom it = Seg (n + 1) & ( for i being Nat st i in dom it holds
it . i = integral ((const (f . (i / (n + 1)))),((i -' 1) / (n + 1)),(i / (n + 1))) ) );

existence
ex b₁ being FinSequence of F_Real st
( dom b₁ = Seg (n + 1) & ( for i being Nat st i in dom b₁ holds
b₁ . i = integral ((const (f . (i / (n + 1)))),((i -' 1) / (n + 1)),(i / (n + 1))) ) )

proof end;

uniqueness
for b₁, b₂ being FinSequence of F_Real st dom b₁ = Seg (n + 1) & ( for i being Nat st i in dom b₁ holds
b₁ . i = integral ((const (f . (i / (n + 1)))),((i -' 1) / (n + 1)),(i / (n + 1))) ) & dom b₂ = Seg (n + 1) & ( for i being Nat st i in dom b₂ holds
b₂ . i = integral ((const (f . (i / (n + 1)))),((i -' 1) / (n + 1)),(i / (n + 1))) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem defines 'F' STIRLIN1:def 12 :
for n being Nat
for f being PartFunc of REAL,REAL
for b₃ being FinSequence of F_Real holds
( b₃ = 'F' (f,n) iff ( dom b₃ = Seg (n + 1) & ( for i being Nat st i in dom b₃ holds
b₃ . i = integral ((const (f . (i / (n + 1)))),((i -' 1) / (n + 1)),(i / (n + 1))) ) ) );

definition

let n be Nat;
let f be PartFunc of REAL,REAL;

func 'G' (f,n) -> FinSequence of F_Real means :Def13: :: STIRLIN1:def 13
( dom it = Seg (n + 1) & ( for i being Nat st i in dom it holds
it . i = integral ((- f),((i -' 1) / (n + 1)),(i / (n + 1))) ) );

existence
ex b₁ being FinSequence of F_Real st
( dom b₁ = Seg (n + 1) & ( for i being Nat st i in dom b₁ holds
b₁ . i = integral ((- f),((i -' 1) / (n + 1)),(i / (n + 1))) ) )

proof end;

uniqueness
for b₁, b₂ being FinSequence of F_Real st dom b₁ = Seg (n + 1) & ( for i being Nat st i in dom b₁ holds
b₁ . i = integral ((- f),((i -' 1) / (n + 1)),(i / (n + 1))) ) & dom b₂ = Seg (n + 1) & ( for i being Nat st i in dom b₂ holds
b₂ . i = integral ((- f),((i -' 1) / (n + 1)),(i / (n + 1))) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def13 defines 'G' STIRLIN1:def 13 :
for n being Nat
for f being PartFunc of REAL,REAL
for b₃ being FinSequence of F_Real holds
( b₃ = 'G' (f,n) iff ( dom b₃ = Seg (n + 1) & ( for i being Nat st i in dom b₃ holds
b₃ . i = integral ((- f),((i -' 1) / (n + 1)),(i / (n + 1))) ) ) );

definition

let n be Nat;
let f be PartFunc of REAL,REAL;

func step_ (f,n) -> FinSequence of F_Real means :Def14: :: STIRLIN1:def 14
( dom it = Seg (n + 1) & ( for i being Nat st i in dom it holds
it . i = f . (i / (n + 1)) ) );

existence
ex b₁ being FinSequence of F_Real st
( dom b₁ = Seg (n + 1) & ( for i being Nat st i in dom b₁ holds
b₁ . i = f . (i / (n + 1)) ) )

proof end;

uniqueness
for b₁, b₂ being FinSequence of F_Real st dom b₁ = Seg (n + 1) & ( for i being Nat st i in dom b₁ holds
b₁ . i = f . (i / (n + 1)) ) & dom b₂ = Seg (n + 1) & ( for i being Nat st i in dom b₂ holds
b₂ . i = f . (i / (n + 1)) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def14 defines step_ STIRLIN1:def 14 :
for n being Nat
for f being PartFunc of REAL,REAL
for b₃ being FinSequence of F_Real holds
( b₃ = step_ (f,n) iff ( dom b₃ = Seg (n + 1) & ( for i being Nat st i in dom b₃ holds
b₃ . i = f . (i / (n + 1)) ) ) );

Lm20: for f being PartFunc of REAL,REAL
for n being Nat st f is_C^1-Class_on ['0,1'] holds
for k being Nat st k in Seg (n + 1) holds
integral ((const (f . (k / (n + 1)))),((k -' 1) / (n + 1)),(k / (n + 1))) = ((In ((1 / (n + 1)),F_Real)) * (step_ (f,n))) . k

proof end;

theorem Th9: :: STIRLIN1:9

for n being Nat
for f being PartFunc of REAL,REAL holds integral ((- f),0,0) = 0

proof end;

Lm21: for n being Nat
for f being PartFunc of REAL,REAL st f is_C^1-Class_on ['0,1'] holds
(integral ((- f),0,(n / (n + 1)))) + (integral ((- f),(n / (n + 1)),1)) = integral ((- f),0,1)

proof end;

Lm22: for n being Nat
for f being PartFunc of REAL,REAL st f is_C^1-Class_on ['0,1'] holds
Sum ('G' (f,n)) = integral ((- f),0,1)

proof end;

Lm23: for n, k being Nat
for f being PartFunc of REAL,REAL st k in Seg (n + 1) & f is_C^1-Class_on ['0,1'] holds
( (((LWBND_rng_d (f,n)) . k) * ((1 / (n + 1)) ^2)) / 2 <= integral (((const (f . (k / (n + 1)))) + (- f)),((k -' 1) / (n + 1)),(k / (n + 1))) & integral (((const (f . (k / (n + 1)))) + (- f)),((k -' 1) / (n + 1)),(k / (n + 1))) <= (((UPBND_rng_d (f,n)) . k) * ((1 / (n + 1)) ^2)) / 2 )

proof end;

Lm24: for n being Nat
for f being PartFunc of REAL,REAL st f is_C^1-Class_on ['0,1'] holds
for k being Nat st k in Seg (n + 1) holds
(((In ((1 / (n + 1)),F_Real)) * (step_ (f,n))) + ('G' (f,n))) . k = integral (((const (f . (k / (n + 1)))) + (- f)),((k -' 1) / (n + 1)),(k / (n + 1)))

proof end;

Lm25: for a, b being Element of F_Real
for p being FinSequence of the carrier of F_Real holds (a * b) * p = a * (b * p)

proof end;

Lm26: for p being FinSequence of the carrier of F_Real holds (1. F_Real) * p = p

proof end;

Lm27: for n being Nat
for f being PartFunc of REAL,REAL st f is_C^1-Class_on ['0,1'] holds
(Sum (step_ (f,n))) + ((n + 1) * (integral ((- f),0,1))) <= (1 / 2) * ((upper_sum ((@' (f,['0,1'])),D[01])) . n)

proof end;

Lm28: for n being Nat
for f being PartFunc of REAL,REAL st f is_C^1-Class_on ['0,1'] holds
(1 / 2) * ((lower_sum ((@' (f,['0,1'])),D[01])) . n) <= (Sum (step_ (f,n))) + ((n + 1) * (integral ((- f),0,1)))

proof end;

definition

let f be PartFunc of REAL,REAL;

func Sum_step f -> Real_Sequence means :Def15: :: STIRLIN1:def 15
for n being Nat holds it . n = Sum (step_ (f,n));

correctness
existence
ex b₁ being Real_Sequence st
for n being Nat holds b₁ . n = Sum (step_ (f,n));
uniqueness
for b₁, b₂ being Real_Sequence st ( for n being Nat holds b₁ . n = Sum (step_ (f,n)) ) & ( for n being Nat holds b₂ . n = Sum (step_ (f,n)) ) holds
b₁ = b₂;

proof end;

end;

:: deftheorem Def15 defines Sum_step STIRLIN1:def 15 :
for f being PartFunc of REAL,REAL
for b₂ being Real_Sequence holds
( b₂ = Sum_step f iff for n being Nat holds b₂ . n = Sum (step_ (f,n)) );

definition

let f be PartFunc of REAL,REAL;

func n_Integral f -> Real_Sequence means :Def16: :: STIRLIN1:def 16
for n being Nat holds it . n = (n + 1) * (integral ((- f),0,1));

correctness
existence
ex b₁ being Real_Sequence st
for n being Nat holds b₁ . n = (n + 1) * (integral ((- f),0,1));
uniqueness
for b₁, b₂ being Real_Sequence st ( for n being Nat holds b₁ . n = (n + 1) * (integral ((- f),0,1)) ) & ( for n being Nat holds b₂ . n = (n + 1) * (integral ((- f),0,1)) ) holds
b₁ = b₂;

proof end;

end;

:: deftheorem Def16 defines n_Integral STIRLIN1:def 16 :
for f being PartFunc of REAL,REAL
for b₂ being Real_Sequence holds
( b₂ = n_Integral f iff for n being Nat holds b₂ . n = (n + 1) * (integral ((- f),0,1)) );

definition

let f be PartFunc of REAL,REAL;

func w_seq f -> Real_Sequence equals :: STIRLIN1:def 17
(Sum_step f) + (n_Integral f);

coherence
(Sum_step f) + (n_Integral f) is Real_Sequence

proof end;

end;

:: deftheorem defines w_seq STIRLIN1:def 17 :
for f being PartFunc of REAL,REAL holds w_seq f = (Sum_step f) + (n_Integral f);

Lm30: for f being PartFunc of REAL,REAL st f is_C^1-Class_on ['0,1'] holds
( w_seq f is convergent & ( for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.(((w_seq f) . m) - ((1 / 2) * (integral ((f `| rohl) || ['0,1'])))).| < p ) )

proof end;

:: Main Lemma

theorem Th11: :: STIRLIN1:10

for f being PartFunc of REAL,REAL st f is_C^1-Class_on ['0,1'] holds
lim (w_seq f) = (1 / 2) * (integral ((f `| rohl) || ['0,1']))

proof end;

definition

let c be Real;

func x_+_ c -> PartFunc of REAL,REAL equals :: STIRLIN1:def 18
AffineMap (1,c);

coherence
AffineMap (1,c) is PartFunc of REAL,REAL ;

end;

:: deftheorem defines x_+_ STIRLIN1:def 18 :
for c being Real holds x_+_ c = AffineMap (1,c);

Lm31: for c being Real holds x_+_ c = (id REAL) + (const c)

proof end;

Lm32: for c being Real holds x_+_ c is differentiable

proof end;

Lm33: for c being Real
for Z being open Subset of REAL holds x_+_ c is_differentiable_on Z

proof end;

Lm34: for c being Real holds (x_+_ c) `| REAL = REAL --> 1

proof end;

Lm35: for c being Real holds (x_+_ c) `| rohl = rohl --> 1

proof end;

Lm36: for x1 being Real st x1 in right_open_halfline (- 1) holds
( x1 in support (x_+_ 1) & x_+_ 1 <> 0 & (x_+_ 1) . x1 <> 0 )

proof end;

Lm37: for x0 being Real st x0 in right_open_halfline (- 1) holds
(x_+_ 1) ^ is_continuous_in x0

proof end;

Lm38: for f being Function holds f " {0} = ZeroPointSet f

proof end;

Lm39: for f being Function holds support f = (dom f) \ (ZeroPointSet f)

proof end;

Lm40: for f being real-valued Function holds dom (f ^) = support f

proof end;

Lm41: for x being Real st x in right_open_halfline (- 1) holds
x + 1 in right_open_halfline 0

proof end;

Lm42: ( ((x_+_ 1) ^) | (right_open_halfline (- 1)) is continuous & right_open_halfline (- 1) c= dom ((x_+_ 1) ^) & dom (((x_+_ 1) ^) | (right_open_halfline (- 1))) = right_open_halfline (- 1) )

proof end;

Lm43: for x being Real st x in right_open_halfline (- 1) holds
( ((x_+_ 1) | rohl) . x = 1 + x & ((x_+_ 1) | rohl) . x > 0 )

proof end;

Lm44: for x being Real st x in rohl holds
(((x_+_ 1) ^) | rohl) . x = 1 / (1 + x)

proof end;

Lm45: for x0 being Real st x0 in right_open_halfline (- 1) holds
(x_+_ 1) | rohl is_differentiable_in x0

proof end;

Lm46: rng ((x_+_ 1) | rohl) = right_open_halfline 0

proof end;

Lm47: ( dom ((x_+_ 1) | rohl) = right_open_halfline (- 1) & dom (ln * ((x_+_ 1) | rohl)) = right_open_halfline (- 1) )

proof end;

Lm48: for n being Nat holds n in right_open_halfline (- 1)

proof end;

Lm49: for r being Real st r >= 0 holds
r in right_open_halfline (- 1)

proof end;

Lm50: ( dom ((x_+_ 1) | rohl) = rohl & 1 in dom ((x_+_ 1) | rohl) & 0 in dom ((x_+_ 1) | rohl) & ((x_+_ 1) | rohl) . 0 = 1 & ((x_+_ 1) | rohl) . 1 = 2 & (ln * ((x_+_ 1) | rohl)) . 1 = ln . 2 & (ln * ((x_+_ 1) | rohl)) . 0 = 0 & (ln * ((x_+_ 1) | rohl)) . 0 = ln . 1 )

proof end;

theorem Th13: :: STIRLIN1:11

ln * ((x_+_ 1) | rohl) is_differentiable_on right_open_halfline (- 1)

proof end;

theorem Th14: :: STIRLIN1:12

for Z being open Subset of REAL st Z c= dom (ln * ((x_+_ 1) | rohl)) holds
( ln * ((x_+_ 1) | rohl) is_differentiable_on Z & ( for x being Real st x in Z holds
((ln * ((x_+_ 1) | rohl)) `| Z) . x = 1 / (1 + x) ) )

proof end;

theorem Th15: :: STIRLIN1:13

(ln * ((x_+_ 1) | rohl)) `| rohl = ((x_+_ 1) ^) | rohl

proof end;

Lm51: ln * ((x_+_ 1) | rohl) is_C^1-Class_on ['0,1']

proof end;

theorem Th16: :: STIRLIN1:14

(((x_+_ 1) (#) (ln * ((x_+_ 1) | rohl))) + (- (1 (#) (x_+_ 0)))) `| rohl = ln * ((x_+_ 1) | rohl)

proof end;

theorem Lm52: :: STIRLIN1:15

integral ((ln * ((x_+_ 1) | rohl)),0,1) = log (number_e,(4 / number_e))

proof end;

theorem Th17: :: STIRLIN1:16

integral (((ln * ((x_+_ 1) | rohl)) `| rohl),['0,1']) = ln . 2

proof end;

theorem Th18: :: STIRLIN1:17

lim (w_seq (ln * ((x_+_ 1) | rohl))) = (1 / 2) * (ln . 2)

proof end;

definition

let m be non zero Nat;
let f be PartFunc of REAL,REAL;

func Step_ (f,m) -> Real_Sequence means :Def19: :: STIRLIN1:def 19
for i being Nat holds it . i = f . (i / m);

correctness
existence
ex b₁ being Real_Sequence st
for i being Nat holds b₁ . i = f . (i / m);
uniqueness
for b₁, b₂ being Real_Sequence st ( for i being Nat holds b₁ . i = f . (i / m) ) & ( for i being Nat holds b₂ . i = f . (i / m) ) holds
b₁ = b₂;

proof end;

end;

:: deftheorem Def19 defines Step_ STIRLIN1:def 19 :
for m being non zero Nat
for f being PartFunc of REAL,REAL
for b₃ being Real_Sequence holds
( b₃ = Step_ (f,m) iff for i being Nat holds b₃ . i = f . (i / m) );

theorem Th19: :: STIRLIN1:18

for m being non zero Nat
for f being PartFunc of REAL,REAL holds XFS2FS ((Step_ (f,m)) | (Segm (m + 1))) = <*(f . 0)*> ^ (step_ (f,(m -' 1)))

proof end;

theorem Th20: :: STIRLIN1:19

for m being non zero Nat
for f being PartFunc of REAL,REAL st f is_C^1-Class_on ['0,1'] holds
Sum (XFS2FS ((Step_ (f,m)) | (Segm (m + 1)))) = (f . 0) + (Sum (step_ (f,(m -' 1))))

proof end;

theorem Th21: :: STIRLIN1:20

for m being non zero Nat holds Sum (XFS2FS ((Step_ ((ln * ((x_+_ 1) | rohl)),m)) | (Segm (m + 1)))) = Sum (step_ ((ln * ((x_+_ 1) | rohl)),(m -' 1)))

proof end;

Lm53: for m being non zero Nat
for k being Nat holds (Partial_Sums (Step_ ((ln * ((x_+_ 1) | rohl)),m))) . k = ln . (((k + m) !) / ((m ^ k) * (m !)))

proof end;

Lm54: for m being non zero Nat holds Sum (step_ ((ln * ((x_+_ 1) | rohl)),(m -' 1))) = ln . (((m + m) !) / ((m ^ m) * (m !)))

proof end;

theorem :: STIRLIN1:21

for m being non zero Nat holds (w_seq (ln * ((x_+_ 1) | rohl))) . (m -' 1) = ln . ((((2 * m) !) / (m !)) * ((number_e / (4 * m)) ^ m))

proof end;

Lm56: (1 / 2) * (ln . 2) = ln . (2 #R (1 / 2))

proof end;

definition

func W_STIRL -> Real_Sequence means :Def20: :: STIRLIN1:def 20
for n being Nat holds it . n = (((2 * (n + 1)) !) / ((n + 1) !)) * ((number_e / (4 * (n + 1))) ^ (n + 1));

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

proof end;

end;

:: deftheorem Def20 defines W_STIRL STIRLIN1:def 20 :
for b₁ being Real_Sequence holds
( b₁ = W_STIRL iff for n being Nat holds b₁ . n = (((2 * (n + 1)) !) / ((n + 1) !)) * ((number_e / (4 * (n + 1))) ^ (n + 1)) );

theorem Lm57: :: STIRLIN1:22

for n being Nat holds (w_seq (ln * ((x_+_ 1) | rohl))) . n = ln . (W_STIRL . n)

proof end;

Lm58: for n being Nat holds W_STIRL . n > 0

proof end;

Lm59: exp_R /* (w_seq (ln * ((x_+_ 1) | rohl))) = W_STIRL

proof end;

theorem Th22: :: STIRLIN1:23

( lim W_STIRL = sqrt 2 & W_STIRL is convergent )

proof end;

definition

func Stirl_Seq -> Real_Sequence means :Def21X: :: STIRLIN1:def 21
for n being Nat holds it . n = (n !) / ((n ^ (n + (1 / 2))) * (number_e ^ (- n)));

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

proof end;

end;

:: deftheorem Def21X defines Stirl_Seq STIRLIN1:def 21 :
for b₁ being Real_Sequence holds
( b₁ = Stirl_Seq iff for n being Nat holds b₁ . n = (n !) / ((n ^ (n + (1 / 2))) * (number_e ^ (- n))) );

Lm60: for n being Nat holds (Stirl_Seq ^\ 1) . n = (W_STIRL /" (sqrt Wallis_Seq)) . n

proof end;

theorem :: STIRLIN1:24

lim Stirl_Seq = sqrt (2 * PI)

proof end;