:: A Formal Proof of {S}tirling's Formula
:: by Yasushige Watase
::
:: Received September 17, 2025
:: Copyright (c) 2025-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 4.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/4.0/.
environ
vocabularies NUMBERS, SUBSET_1, REAL_1, INTEGRA1, FINSEQ_1, ORDINAL4, CARD_3,
ARYTM_1, ARYTM_3, RELAT_1, FUNCT_1, XXREAL_0, NAT_1, XBOOLE_0, VALUED_1,
TARSKI, XXREAL_2, ORDINAL2, CARD_1, FDIFF_1, XXREAL_1, RCOMP_1, INTEGRA5,
MEASURE5, XCMPLX_0, VECTSP_1, LTLAXIO1, VALUED_0, SQUARE_1, REALSET1,
PARTFUN1, TAYLOR_1, LIMFUNC1, PRALG_3, PRE_POLY, DIOPHAN2, JGRAPH_2,
FCONT_1, SEQ_4, FUNCT_7, STRUCT_0, NEWTON, SEQ_1, QC_LANG1, POWER, SEQ_2,
PREPOWER, MEASURE7, INTEGRA4, MESFUN14, FUNCT_3, INTEGRA2, FUNCT_2,
SUPINF_2, FUNCOP_1, COMPLEX1, GR_CY_1, MESFUNC1, INTEGRA7, SERIES_1,
PRGCOR_2, AFINSQ_1, SIN_COS, STIRLIN1, WALLIS01;
notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, RELSET_1,
PARTFUN1, FUNCT_2, FUNCOP_1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0,
SQUARE_1, NAT_1, VALUED_0, COMPLEX1, NAT_D, XXREAL_2, FINSEQ_1, VALUED_1,
SEQ_1, SEQ_2, RFUNCT_1, RVSUM_1, NEWTON, SEQ_4, RCOMP_1, FCONT_1,
FDIFF_1, PREPOWER, POWER, SERIES_1, LIMFUNC1, MEASURE5, SIN_COS,
AFINSQ_1, IRRAT_1, TAYLOR_1, PRE_POLY, INTEGRA1, INTEGRA2, INTEGRA3,
INTEGRA4, INTEGRA5, PARTFUN3, STRUCT_0, ALGSTR_0, RLVECT_1, VECTSP_1,
POLYNOM1, BINOM, INTEGRA7, MATRTOP1, DIOPHAN2, MESFUN14, WALLIS01;
constructors RELSET_1, SQUARE_1, NAT_D, BINOP_2, COMSEQ_2, RVSUM_1, SEQ_4,
FCONT_1, FDIFF_1, PREPOWER, LIMFUNC1, MEASURE6, SIN_COS, TAYLOR_1,
INTEGRA2, INTEGRA3, INTEGRA4, INTEGRA5, PARTFUN3, FVSUM_1, BINOM,
INTEGRA7, MATRTOP1, DIOPHAN2, RVSUM_4, MESFUN14, E_TRANS1, WALLIS01;
registrations RELAT_1, NUMBERS, XXREAL_0, XREAL_0, MEMBERED, FINSEQ_1,
RCOMP_1, INTEGRA1, VALUED_0, VALUED_1, FUNCT_2, FINSET_1, XXREAL_2,
CARD_1, RELSET_1, MEASURE5, ORDINAL1, FUNCT_1, NAT_1, POLYDIFF, FUNCOP_1,
NEWTON04, XCMPLX_0, NEWTON, SIN_COS, RVSUM_4, STRUCT_0, SUBSET_1,
VECTSP_1, FCONT_1, SQUARE_1, NAT_6, PARTFUN3, POWER, FINSEQ_9, FCONT_3,
FDIFF_1, AFINSQ_1, FOMODEL0, WALLIS01;
requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM;
definitions PBOOLE;
equalities VALUED_1, STRUCT_0, SQUARE_1, XCMPLX_0, ORDINAL1, FINSEQ_1,
XBOOLE_0, INTEGRA1, SUBSET_1;
expansions FUNCT_2, TARSKI, XBOOLE_0, FUNCT_1, SEQ_2, INTEGRA1, FDIFF_1;
theorems SEQ_4, PARTFUN1, INTEGRA1, RFUNCT_1, FUNCT_1, FINSEQ_1, RVSUM_1,
SEQ_1, SEQ_2, FDIFF_1, ABSVALUE, NAT_1, TARSKI, INTEGRA2, INTEGRA4,
FCONT_1, FDIFF_2, RELAT_1, XREAL_0, FUNCT_2, XBOOLE_1, XCMPLX_1, XREAL_1,
XXREAL_0, ORDINAL1, VALUED_1, XXREAL_2, XXREAL_1, INTEGRA3, BINOM,
FUNCOP_1, VECTSP_1, INTEGRA5, COMPTRIG, INTEGRA6, NAT_D, INTEGRA7,
ZFMISC_1, NUMBERS, PDLAX, TAYLOR_1, PREPOWER, NEWTON, RLVECT_1, FINSEQ_3,
FDIFF_4, POWER, ORDEQ_01, FINSEQ_5, LIMFUNC1, PRE_POLY, DIOPHAN2,
TARSKI_0, JORDAN5A, FUZZY_6, FUZZY_8, POLYNOM1, FVSUM_1, MOEBIUS3, NIVEN,
COUSIN, DIFF_4, FDIFF_7, MESFUN14, NEWTON02, MATRPROB, INTEGR24,
MATRTOP1, FUZIMPL2, RVSUM_4, DBLSEQ_2, SQUARE_1, SERIES_1, E_TRANS1,
WALLIS01;
schemes FINSEQ_1, NAT_1, FUNCT_2, NUMPOLY1;
begin :: Section 1. Lemma on the Riemann sum over an equal partition
Lm1:
for n be Nat holds
divset(EqDiv(['0,1'],n+1),1) = [.0,1/(n+1).]
proof
let n be Nat;
set A = ['0,1'];
set D = EqDiv(A,n+1);
A1: vol A = 1 -0 by INTEGRA6:5; then
A2: EqDiv(A,n+1) divide_into_equal n+1 by MESFUN14:def 1; then
A3: len D = n+1 by INTEGRA4:def 1; then
A4: dom D = Seg (n+1) by FINSEQ_1:def 3;
A5: divset(D,1) = [. lower_bound A,D.1 .] by COUSIN:50
.= [. 0,D.1 .] by FUZZY_6:7;
1 <= n+1 by NAT_1:14; then
1 in Seg (n+1); then
D.1 = lower_bound A + vol(A)/(len D)*1
by A2,A4,INTEGRA4:def 1
.= 0 + (1/(n+1))*1 by FUZZY_6:7,A1,A3
.= 1/(n+1);
hence thesis by A5;
end;
theorem Th1:
for n be Nat,k be Nat st k in Seg (n+1) holds
divset(EqDiv(['0,1'],(n+1)),k) = [.(k-'1)/(n+1), k/(n+1).]
proof
let n be Nat,k be Nat;
set A = ['0,1'];
set D = EqDiv(A,n+1);
assume
A1: k in Seg (n+1);
A2: vol A = 1 -0 by INTEGRA6:5; then
A3: EqDiv(A,n+1) divide_into_equal (n+1) by MESFUN14:def 1; then
A4: len D = n+1 by INTEGRA4:def 1; then
A5: dom D = Seg (n+1) by FINSEQ_1:def 3;
A7: k in dom D by A1,A4,FINSEQ_1:def 3;
A6: 1 <= k & k <= n+1 by A1,FINSEQ_1:1; then
per cases by XXREAL_0:1;
suppose
A8: k = 1; then
[.(k-'1)/(n+1), k/(n+1).] = [.0/(n+1), 1/(n+1).] by XREAL_1:232
.= [.0,1/(n+1).];
hence thesis by A8,Lm1;
end;
suppose
A9: k > 1; then
A10: k-'1 = k-1 by XREAL_1:233;
1 < (k-1)+1 by A9; then
A12: 1 <= k-'1 by A10,NAT_1:13;
k-'1 < k by A9,XREAL_1:237; then
k-'1 < n+1 by A6,XXREAL_0:2; then
A14: k-'1 in dom D by A12,A5;
k in dom D by A1,A4,FINSEQ_1:def 3; then
A16: D.k = lower_bound A + vol(A)/(len D)*k
by A3,INTEGRA4:def 1 .= 0 + (1/(n+1))*k by FUZZY_6:7,A2,A4
.= k/(n+1);
A17: D.(k-'1) = lower_bound A + vol(A)/(len D)*(k-'1)
by A3,A14,INTEGRA4:def 1 .= 0 + (1/(n+1))*(k-'1) by FUZZY_6:7,A2,A4
.= (k-'1)/(n+1);
divset(D,k) = [.D.(k-1),D.k.] by A9,A7,COUSIN:50
.= [.(k-'1)/(n+1),k/(n+1).] by A9,XREAL_1:233,A16,A17;
hence thesis;
end;
end;
definition
func D[01] -> sequence of divs ['0,1'] means :Def1:
for n be Element of NAT holds it.n = EqDiv(['0,1'],n+1);
existence
proof
defpred P[Element of NAT,set] means
$2 = EqDiv(['0,1'],$1+1);
A1:now let m be Element of NAT;
reconsider r = EqDiv(['0,1'],m+1) as Element of divs ['0,1']
by INTEGRA1:def 3;
take r;
thus P[m,r];
end;
consider IT be Function of NAT, divs ['0,1'] such that
A2: for m be Element of NAT holds P[m,IT.m] from FUNCT_2:sch 3(A1);
take IT;
thus thesis by A2;
end;
uniqueness
proof
let s1,s2 be sequence of (divs ['0,1']) such that
A3: for n be Element of NAT holds s1.n
= EqDiv(['0,1'],n+1) and
A4: for n be Element of NAT holds s2.n
= EqDiv(['0,1'],n+1);
for n be Element of NAT holds s1.n = s2.n
proof
let n be Element of NAT;
thus s1.n = EqDiv(['0,1'],n+1) by A3
.= s2.n by A4;
end;
hence thesis;
end;
end;
theorem Th2:
for n be Nat holds delta(EqDiv(['0,1'],n+1)) = 1/(n+1)
proof
let n be Nat;
set A = ['0,1'];
set D = EqDiv(['0,1'],n+1);
A1: vol A = 1 -0 by INTEGRA6:5; then
A2: D divide_into_equal (n+1) by MESFUN14:def 1;
A3: len D = n+1 by A2,INTEGRA4:def 1;
A4: for i being Nat st i in dom D holds upper_volume(chi(A,A),D).i = 1/(n+1)
proof
let i be Nat;
assume
A5: i in dom D; then
upper_volume(chi(A,A),D).i
= vol(divset(D,i)) by INTEGRA1:20
.= 1/(n+1) by A1,A2,A5,MESFUN14:15;
hence thesis;
end;
A6: len (upper_volume(chi(A,A),D)) = len D by INTEGRA1:def 6;
rng (upper_volume(chi(A,A),D)) = {1/(n+1)}
proof
for o be object st o in rng (upper_volume(chi(A,A),D)) holds
o in {1/(n+1)}
proof
let o be object;
assume o in rng upper_volume(chi(A,A),D); then
consider x being object such that
A8: x in dom upper_volume(chi(A,A),D) &
o = (upper_volume(chi(A,A),D)).x by FUNCT_1:def 3;
x in dom D by A6,FINSEQ_3:29,A8; then
(upper_volume(chi(A,A),D)).x = 1/(n+1) by A4;
hence thesis by A8,TARSKI:def 1;
end; then
A9: rng upper_volume(chi(A,A),D) c= {1/(n+1)};
A10: 0+1 in Seg (n+1) by NEWTON02:104; then
A11: 1 in dom D by A3,FINSEQ_1:def 3;
1 in dom upper_volume(chi(A,A),D)
by A10,A3,FINSEQ_1:def 3,A6; then
(upper_volume(chi(A,A),D)).1 in rng upper_volume(chi(A,A),D)
by FUNCT_1:3; then
1/(n+1) in rng (upper_volume(chi(A,A),D)) by A11,A4;
hence thesis by A9,ZFMISC_1:31;
end; then
max rng upper_volume(chi(A,A),D) = 1/(n+1) by XXREAL_2:11;
hence thesis by INTEGRA3:def 1;
end;
theorem Th3:
delta(D[01]) is 0-convergent non-zero Real_Sequence
proof
set A = ['0,1'];
A1: vol A = 1 - 0 by INTEGRA6:5;
consider T being DivSequence of A such that
A2: delta T is convergent & lim delta T = 0 &
for n be Element of NAT holds
ex Tn being Division of A st Tn divide_into_equal n+1 & T.n =Tn
by A1,INTEGRA6:16;
A3: for n be Nat holds (D[01]).n = T.n
proof
let n be Nat;
defpred P[Nat] means (D[01]).$1 = T.$1;
A4: for n be Nat holds P[n] implies P[n+1]
proof
let n be Nat;
assume
P[n];
reconsider m = n+1 as Nat;
consider Tm be Division of A such that
A5: Tm divide_into_equal m+1 & T.m =Tm by A2;
T.m = EqDiv(['0,1'],m+1) by A1,MESFUN14:def 1,A5
.= (D[01]).m by Def1;
hence thesis;
end;
A6: P[0]
proof
consider T0 be Division of A such that
A7: T0 divide_into_equal 0+1 & T.0 = T0 by A2;
T.0 = EqDiv(['0,1'],0+1) by A1,MESFUN14:def 1,A7
.= (D[01]).0 by Def1;
hence thesis;
end;
for n be Nat holds P[n] from NAT_1:sch 2(A6,A4);
hence thesis;
end;
A8: T = D[01] by A3;
for j be Nat holds (delta T).j<>0
proof
let j be Nat;
reconsider jj = j as Element of NAT by ORDINAL1:def 12;
(delta T).j = delta(T.jj) by INTEGRA3:def 2
.= delta((D[01]).jj) by A3
.= delta(EqDiv(['0,1'],jj+1)) by Def1
.= 1/(j+1) by Th2;
hence thesis;
end;
hence thesis by A8,A2,FDIFF_1:def 1,SEQ_1:5;
end;
definition
let a,b be Real;
func ax_+_b(a,b) -> PartFunc of REAL,REAL equals
AffineMap(a,b);
coherence;
end;
definition
let r be Real;
func const(r) -> PartFunc of REAL,REAL equals
AffineMap(0,r);
coherence;
end;
Lm2:
for r be Real holds
const(r) is constant Function of REAL,REAL
proof
let r be Real;
set f = const(r);
for x, y being object st x in dom f & y in dom f holds f.x = f.y
proof
let x, y be object;
assume x in dom f & y in dom f; then
reconsider x1 = x, y1 = y as Real;
f.x1 = 0*x1 + r by FCONT_1:def 4 .= 0*y1 +r
.= f.y1 by FCONT_1:def 4;
hence thesis;
end;
hence thesis by FUNCT_1:def 10;
end;
registration
let r be Real;
cluster const(r) -> constant;
coherence by Lm2;
end;
Lm3:
for r be Real holds
const(r) is total & rng const(r) = {r}
proof
let r be Real;
consider y be Element of REAL such that
A1: rng const(r) = {y} by FUNCT_2:111;
reconsider r1 = r as Element of REAL by XREAL_0:def 1;
r1 in REAL; then
A2: r1 in dom const(r) by FUNCT_2:def 1;
(const r).r1 = 0*r1 + r by FCONT_1:def 4 .= r1; then
r1 in rng const(r) by A2,FUNCT_1:3;
hence thesis by A1,TARSKI:def 1;
end;
Lm4:
for n,k be Nat,m be non zero Nat, x0, r be 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
let n,k be Nat,m be non zero Nat, x0, r be Real;
set f = const(r);
set a = x0, b = k/(n+1);
set X = REAL;
assume
A1: k in Seg (n+1) & x0 in ['(k-'1)/(n+1),k/(n+1)']; then
1 <= k by FINSEQ_1:1; then
k-'1 <= k by XREAL_1:237; then
['(k-'1)/(n+1),k/(n+1)'] = [.(k-'1)/(n+1),k/(n+1).]
by XREAL_1:72,INTEGRA5:def 3; then
A4: a <= b by A1,XXREAL_1:1;
A5: [.a,b.] c= X;
X c= dom f & ['(k-'1)/m,k/m'] c= X & f|X is continuous by FUNCT_2:def 1;
hence thesis by A4,A5,INTEGRA7:19;
end;
definition
func rohl -> Subset of REAL equals
right_open_halfline(-1);
coherence;
end;
definition
let f be PartFunc of REAL,REAL,
A be non empty closed_interval Subset of REAL;
pred f is_C^1-Class_on A means
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;
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:
(f`|right_open_halfline(-1))|A;
coherence
proof
reconsider df = (f`|right_open_halfline(-1)) as PartFunc of REAL,REAL;
A2: dom (f`|right_open_halfline(-1)) = right_open_halfline(-1)
by A1,FDIFF_1:def 7;
A3: dom ((f`|right_open_halfline(-1))|A) = A by A2,A1,RELAT_1:62;
rng (df|A) c= REAL;
hence thesis by A3,FUNCT_2:2;
end;
end;
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
f|A;
coherence
proof
A2: dom (f|A) = A by A1,RELAT_1:62;
rng (f|A) c= REAL;
hence thesis by A2,FUNCT_2:2;
end;
end;
reserve Z for open Subset of REAL;
Lm5:
for n be Nat,k be Nat, x0 be Real, f be 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
let n be Nat,k be Nat, x0 be Real, f be PartFunc of REAL,REAL;
set a = x0, b = k/(n+1);
set Z = ['0,1'];
set X = ['a,b'];
assume
A1: k in Seg (n+1) & x0 in ['(k-'1)/(n+1),k/(n+1)'] &
f is_C^1-Class_on ['0,1'];
A2: ['0,1'] = [. 0,1 .] by INTEGRA5:def 3;
1 <= k by A1,FINSEQ_1:1; then
k-'1 <= k by XREAL_1:237; then
A5: ['(k-'1)/(n+1),k/(n+1)'] = [.(k-'1)/(n+1),k/(n+1).]
by XREAL_1:72,INTEGRA5:def 3; then
A6: a <= b by A1,XXREAL_1:1;
A7: 0 <= x0 by A5,A1,XXREAL_1:1;
k <= n+1 by A1,FINSEQ_1:1; then
k/(n+1) <= (n+1)/(n+1) by XREAL_1:72; then
k/(n+1) <= 1 by XCMPLX_1:60; then
[. a,b .] c= Z by A2,A7,XXREAL_1:34; then
A8: [' a,b '] c= Z by A6,INTEGRA5:def 3;
reconsider g = (f`|rohl) as PartFunc of REAL,REAL;
dom g = rohl by A1,FDIFF_1:def 7; then
a <= b & [. a,b .] c= X & X c= dom g & g|X is continuous by
A6,A8,INTEGRA5:def 3,A1,XBOOLE_1:1;
hence thesis by INTEGRA7:19;
end;
Lm6:
for f be 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
set a = 0, b = 1;
set X = right_open_halfline(-1);
let f be PartFunc of REAL,REAL;
assume
A1: f is_C^1-Class_on ['0,1'];
reconsider g = (f`|X) as PartFunc of REAL,REAL;
a <= b & [. a,b .] c= X & X c= dom g & g|X is continuous
by A1,FDIFF_1:def 7,INTEGRA5:def 3;
hence thesis by INTEGRA7:19;
end;
Lm7:
for n be Nat,k be Nat,f be 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
let n be Nat,k be Nat, f be PartFunc of REAL,REAL;
assume
A1: k in Seg (n+1) & f is_C^1-Class_on ['0,1'];
reconsider x0 = (k-'1)/(n+1) as Real;
1 <= k by A1,FINSEQ_1:1; then
A2: k-'1 <= k by XREAL_1:237; then
A3: ['(k-'1)/(n+1),k/(n+1)'] = [.(k-'1)/(n+1),k/(n+1).]
by XREAL_1:72,INTEGRA5:def 3;
(k-'1)/(n+1) <= x0 & x0 <= k/(n+1) by A2,XREAL_1:72; then
x0 in ['(k-'1)/(n+1),k/(n+1)'] by A3,XXREAL_1:1;
hence thesis by A1,Lm5;
end;
theorem Th4:
for n be Nat,k be Nat, x0 be Real, f be 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
let n be Nat,k be Nat, x0 be Real, f be PartFunc of REAL,REAL;
set a = x0, b = k/(n+1);
set X = rohl;
assume
A1: k in Seg (n+1) & x0 in ['(k-'1)/(n+1),k/(n+1)'] &
f is_C^1-Class_on ['0,1']; then
A2: f is_differentiable_on rohl & f`|rohl is continuous &
['0,1'] c= rohl & rohl c= dom f;
A3: ['0,1'] = [. 0,1 .] by INTEGRA5:def 3;
1 <= k by A1,FINSEQ_1:1; then
k-'1 <= k by XREAL_1:237; then
A5: ['(k-'1)/(n+1),k/(n+1)'] = [.(k-'1)/(n+1),k/(n+1).]
by INTEGRA5:def 3,XREAL_1:72; then
A6: a <= b by A1,XXREAL_1:1;
A7: 0 <= x0 by A5,A1,XXREAL_1:1;
k <= n+1 by A1,FINSEQ_1:1; then
k/(n+1) <= (n+1)/(n+1) by XREAL_1:72; then
k/(n+1) <= 1 by XCMPLX_1:60; then
[. a,b .] c= [' 0,1 '] by A3,A7,XXREAL_1:34; then
[' a,b '] c= ['0,1'] by A6,INTEGRA5:def 3; then
A8: ['a,b'] c= X by A2;
(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 by A1,Lm5;
hence thesis by A8,A1,INTEGRA5:13;
end;
Lm8:
for n be Nat,k be Nat, f be PartFunc of REAL,REAL
st k in Seg (n+1) & f is_C^1-Class_on ['0,1'] holds
for x be 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
let n be Nat,k be Nat, f be PartFunc of REAL,REAL;
set X = ['0,1'];
set g = f`|rohl;
A2: ['0,1'] = [. 0,1 .] by INTEGRA5:def 3;
assume
A1: k in Seg (n+1) & f is_C^1-Class_on ['0,1']; then
1 <= k by FINSEQ_1:1; then
A4: k-'1 <= k by XREAL_1:237;
for x be 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
let x be Real;
assume
A5: x in ['(k-'1)/(n+1),k/(n+1)'];
k <= n+1 by A1,FINSEQ_1:1; then
k/(n+1) <= (n+1)/(n+1) by XREAL_1:72; then
A6: k/(n+1) <= 1 by XCMPLX_1:60;
A7: ['(k-'1)/(n+1),k/(n+1)'] = [.(k-'1)/(n+1),k/(n+1).]
by A4,XREAL_1:72,INTEGRA5:def 3;
A8: [.(k-'1)/(n+1),k/(n+1).] c= [. 0,1 .] by A6,XXREAL_1:34;
dom (f`|rohl) = rohl by A1,FDIFF_1:def 7; then
A10: x in dom ((f`|rohl)|['(k-'1)/(n+1), k/(n+1)'])
by A5,RELAT_1:62,A8, A7,A2,A1,XBOOLE_1:1;
((f`|rohl)|[.(k-'1)/(n+1), k/(n+1).]).x = (f`|rohl).x
by A7,A5,FUNCT_1:49; then
A11: (f`|rohl).x in rng ((f`|rohl)|[.(k-'1)/(n+1), k/(n+1).])
by A7,A10,FUNCT_1:3;
(f`|rohl)|['(k-'1)/(n+1),k/(n+1)'] is bounded by A1,Lm7;
then
rng((f`|rohl)|['(k-'1)/(n+1),k/(n+1)']) is bounded_above
by INTEGRA1:13;
hence thesis by A7,A11,SEQ_4:def 1;
end;
hence thesis;
end;
Lm9:
for n be Nat,k be Nat, f be PartFunc of REAL,REAL
st k in Seg (n+1) & f is_C^1-Class_on ['0,1'] holds
for x be 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
let n be Nat,k be Nat, f be PartFunc of REAL,REAL;
set X = ['0,1'];
set g = f`|rohl;
A2: ['0,1'] = [. 0,1 .] by INTEGRA5:def 3;
assume
A1: k in Seg (n+1) & f is_C^1-Class_on ['0,1']; then
1 <= k by FINSEQ_1:1; then
A3: k-'1 <= k by XREAL_1:237;
for x be 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
let x be Real;
assume
A4: x in ['(k-'1)/(n+1),k/(n+1)'];
k <= n+1 by A1,FINSEQ_1:1; then
k/(n+1) <= (n+1)/(n+1) by XREAL_1:72; then
A5: k/(n+1) <= 1 by XCMPLX_1:60;
A6: ['(k-'1)/(n+1),k/(n+1)'] = [.(k-'1)/(n+1),k/(n+1).]
by A3,XREAL_1:72,INTEGRA5:def 3;
A7: dom (f`|rohl) = rohl by A1,FDIFF_1:def 7;
[.(k-'1)/(n+1),k/(n+1).] c= [. 0,1 .] by A5,XXREAL_1:34; then
A9: x in dom ((f`|rohl)|['(k-'1)/(n+1), k/(n+1)'])
by A4,A7,RELAT_1:62,A6,A2,A1,XBOOLE_1:1;
((f`|rohl)|[.(k-'1)/(n+1), k/(n+1).]).x = (f`|rohl).x
by A6,A4,FUNCT_1:49; then
A10: (f`|rohl).x in rng ((f`|rohl)|[.(k-'1)/(n+1), k/(n+1).])
by A6,A9,FUNCT_1:3;
(f`|rohl)|['(k-'1)/(n+1),k/(n+1)'] is bounded by A1,Lm7;
then
rng((f`|rohl)|['(k-'1)/(n+1),k/(n+1)']) is bounded_below
by INTEGRA1:11;
hence thesis by A6,A10,SEQ_4:def 2;
end;
hence thesis;
end;
definition
let n be Nat,f be PartFunc of REAL,REAL;
func UPBND_rng_d(f,n) -> FinSequence of F_Real means :Def8:
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
proof
defpred P[Nat,object] means
$2 = upper_bound rng ((f`|rohl)|['($1-'1)/(n+1),$1/(n+1)']);
A1: for k be Nat st k in Seg (n+1) ex x being Element of F_Real st P[k,x]
proof
let k be Nat;
assume k in Seg (n+1);
set r = upper_bound rng ((f`|rohl)|['(k-'1)/(n+1),k/(n+1)']);
reconsider r as Element of [#]F_Real by VECTSP_1:def 5,XREAL_0:def 1;
take r;
thus thesis;
end;
consider f being FinSequence of F_Real such that
A2: dom f = Seg (n+1) & for k being Nat st k in Seg (n+1) holds P[k,f.k]
from FINSEQ_1:sch 5(A1);
take f;
thus len f = n+1 by FINSEQ_1:def 3,A2;
thus thesis by A2;
end;
uniqueness
proof
let z1,z2 be FinSequence of F_Real;
assume that
A3: len z1 = n+1 and
A4: for i be Nat st i in dom z1 holds
z1.i = upper_bound rng ((f`|rohl)|['(i-'1)/(n+1),i/(n+1)'])
and
A5: len z2 = n+1 and
A6: for i be Nat st i in dom z2 holds
z2.i = upper_bound rng ((f`|rohl)|['(i-'1)/(n+1),i/(n+1)']);
A7: dom z1 = Seg len z1 by FINSEQ_1:def 3 .= dom z2 by A3,A5,FINSEQ_1:def 3;
for x be Nat st x in dom z1 holds z1.x = z2.x
proof
let x be Nat;
assume
A8: x in dom z1; then
reconsider x9 = x as Element of NAT;
thus
z1.x = upper_bound rng ((f`|rohl)|['(x9-'1)/(n+1),x9/(n+1)'])
by A4,A8
.= z2.x by A6,A7,A8;
end;
hence thesis by A7;
end;
end;
definition
let n be Nat,f be PartFunc of REAL,REAL;
func LWBND_rng_d(f,n) -> FinSequence of F_Real means :Def9:
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
proof
defpred P[Nat,object] means
$2 = lower_bound rng ((f`|rohl)|['($1-'1)/(n+1),$1/(n+1)']);
A1: for k be Nat st k in Seg (n+1) ex x being Element of F_Real st P[k,x]
proof
let k be Nat;
assume k in Seg (n+1);
set r = lower_bound rng ((f`|rohl)|['(k-'1)/(n+1),k/(n+1)']);
reconsider r as Element of [#]F_Real by VECTSP_1:def 5,XREAL_0:def 1;
take r;
thus thesis;
end;
consider f being FinSequence of F_Real such that
A2: dom f = Seg (n+1) & for k being Nat st k in Seg (n+1) holds P[k,f.k]
from FINSEQ_1:sch 5(A1);
take f;
thus len f = n+1 by FINSEQ_1:def 3,A2;
thus thesis by A2;
end;
uniqueness
proof
let z1,z2 be FinSequence of F_Real;
assume that
A3: len z1 = n+1 and
A4: for i be Nat st i in dom z1 holds
z1.i = lower_bound rng ((f`|rohl)|['(i-'1)/(n+1),i/(n+1)'])
and
A5: len z2 = n+1 and
A6: for i be Nat st i in dom z2 holds
z2.i = lower_bound rng ((f`|rohl)|['(i-'1)/(n+1),i/(n+1)']);
A7: dom z1 = dom z2 by A3,A5,FINSEQ_3:29;
for x be Nat st x in dom z1 holds z1.x = z2.x
proof
let x be Nat;
assume
A8: x in dom z1; then
reconsider x9 = x as Element of NAT;
thus z1.x = lower_bound rng ((f`|rohl)|['(x9-'1)/(n+1),x9/(n+1)'])
by A4,A8
.= z2.x by A6,A7,A8;
end;
hence thesis by A7;
end;
end;
definition
let f be PartFunc of REAL,REAL;
func Sum_UPBND_rng_d(f) -> sequence of REAL means :Def10:
for i being Nat holds it.i = (Sum (UPBND_rng_d(f,i)))/(i+1);
existence
proof
defpred P[Element of NAT,Element of REAL] means
$2 = (Sum (UPBND_rng_d(f,$1)))/($1+1);
A1: for x being Element of NAT ex y being Element of REAL st P[x,y]
proof
let x be Element of NAT;
set r = (Sum (UPBND_rng_d(f,x)))/(x+1);
reconsider r as Element of REAL by XREAL_0:def 1;
take r;
thus thesis;
end;
consider f being Function of NAT, REAL such that
A2: for x being Element of NAT holds P[x,f.x] from FUNCT_2:sch 3(A1);
take f;
let i be Nat;
i in NAT by ORDINAL1:def 12;
hence thesis by A2;
end;
uniqueness
proof
let s,t be sequence of REAL such that
A3: for n being Nat holds s.n = (Sum (UPBND_rng_d(f,n)))/(n+1) and
A4: for n being Nat holds t.n = (Sum (UPBND_rng_d(f,n)))/(n+1);
let n be Element of NAT;
thus s.n = (Sum (UPBND_rng_d(f,n)))/(n+1) by A3
.= t.n by A4;
end;
end;
definition
let f be PartFunc of REAL,REAL;
func Sum_LWBND_rng_d(f) -> sequence of REAL means :Def11:
for i being Nat holds it.i = (Sum (LWBND_rng_d(f,i)))/(i+1);
existence
proof
defpred P[Element of NAT,Element of REAL] means
$2 = (Sum (LWBND_rng_d(f,$1)))/($1+1);
A1: for x being Element of NAT ex y being Element of REAL st P[x,y]
proof
let x be Element of NAT;
set r = (Sum (LWBND_rng_d(f,x)))/(x+1);
reconsider r as Element of REAL by XREAL_0:def 1;
take r;
thus thesis;
end;
consider f being Function of NAT, REAL such that
A2: for x being Element of NAT holds P[x,f.x] from FUNCT_2:sch 3(A1);
take f;
let i be Nat;
i in NAT by ORDINAL1:def 12;
hence thesis by A2;
end;
uniqueness
proof
let s,t be sequence of REAL such that
A3: for n being Nat holds s.n = (Sum (LWBND_rng_d(f,n)))/(n+1) and
A4: for n being Nat holds t.n = (Sum (LWBND_rng_d(f,n)))/(n+1);
let n be Element of NAT;
thus s.n = (Sum (LWBND_rng_d(f,n)))/(n+1) by A3
.= t.n by A4;
end;
end;
theorem Th5:
for n be Nat,k be Nat, x0 be Real, f be 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
let n be Nat,k be Nat, x0 be Real, f be PartFunc of REAL,REAL;
assume
A1: k in Seg (n+1) & x0 in ['(k-'1)/(n+1),k/(n+1)']
& f is_C^1-Class_on ['0,1']; then
1 <= k by FINSEQ_1:1; then
k-'1 <= k by XREAL_1:237; then
['(k-'1)/(n+1),k/(n+1)'] = [.(k-'1)/(n+1),k/(n+1).]
by XREAL_1:72,INTEGRA5:def 3; then
A4: (k-'1)/(n+1) <= x0 & x0 <= k/(n+1) by A1,XXREAL_1:1;
A5: dom const(UPBND_rng_d(f,n).k) = REAL by FUNCT_2:def 1;
A6: for t be Real st t in ['x0,k/(n+1)'] holds
(const(UPBND_rng_d(f,n).k)).t = UPBND_rng_d(f,n).k
proof
let t be Real;
assume t in ['x0,k/(n+1)']; then
(const(UPBND_rng_d(f,n).k)).t in rng const(UPBND_rng_d(f,n).k)
by FUNCT_1:3,A5; then
(const(UPBND_rng_d(f,n).k)).t in {UPBND_rng_d(f,n).k} by Lm3;
hence thesis by TARSKI:def 1;
end;
A10: dom const((LWBND_rng_d(f,n)).k) = REAL by FUNCT_2:def 1;
for t be Real st t in ['x0,k/(n+1)'] holds
(const((LWBND_rng_d(f,n)).k)).t = (LWBND_rng_d(f,n)).k
proof
let t be Real;
assume t in ['x0,k/(n+1)']; then
(const((LWBND_rng_d(f,n)).k)).t in rng const((LWBND_rng_d(f,n)).k)
by FUNCT_1:3,A10; then
(const((LWBND_rng_d(f,n)).k)).t in {(LWBND_rng_d(f,n)).k} by Lm3;
hence thesis by TARSKI:def 1;
end;
hence thesis by A6,A5,A4,INTEGRA6:26,A10;
end;
theorem Th6:
for n be Nat,k be Nat, x0 be Real, f be 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
let n be Nat,k be Nat, x0 be Real, f be PartFunc of REAL,REAL;
set df = f`|rohl;
set a = x0, b = k/(n+1);
set X = ['0,1'];
assume
A1: k in Seg (n+1) & x0 in ['(k-'1)/(n+1),k/(n+1)']
& f is_C^1-Class_on ['0,1'];
A2: ['0,1'] = [. 0,1 .] by INTEGRA5:def 3;
reconsider r = UPBND_rng_d(f,n).k as Real;
set g1 = const(r);
1 <= k by A1,FINSEQ_1:1; then
A4: k-'1 <= k by XREAL_1:237; then
A5: ['(k-'1)/(n+1),k/(n+1)'] = [.(k-'1)/(n+1),k/(n+1).]
by XREAL_1:72,INTEGRA5:def 3; then
A6: (k-'1)/(n+1) <= x0 & x0 <= k/(n+1) by A1,XXREAL_1:1; then
A7: [.a,b.] c= [.(k-'1)/(n+1),k/(n+1) .] by XXREAL_1:34;
A8: x0 <= k/(n+1) by A5,A1,XXREAL_1:1;
A9: a <= b by A5,A1,XXREAL_1:1;
k <= (n+1) by A1,FINSEQ_1:1; then
k/(n+1) <= (n+1)/(n+1) by XREAL_1:72; then
k/(n+1) <= 1 by XCMPLX_1:60; then
[. a,b .] c= X by A6,A2,XXREAL_1:34; then
A10: [' a,b '] c= X by A9,INTEGRA5:def 3;
A11: [' a,b '] = [.a,b.] by A6,INTEGRA5:def 3;
A12: ['(k-'1)/(n+1),k/(n+1)'] = [.(k-'1)/(n+1),k/(n+1).]
by A4,XREAL_1:72,INTEGRA5:def 3;
dom (f`|rohl) = rohl by A1,FDIFF_1:def 7; then
A14: ['a,b'] c= dom df & df is_integrable_on ['a,b'] & df|['a,b'] is bounded
by A1,Lm5,XBOOLE_1:1,A10;
A15: ['a,b'] c= dom g1 & g1 is_integrable_on ['a,b'] & g1| ['a,b'] is bounded
by A1,Lm4;
for x be Real st x in ['a,b'] holds df.x <= g1.x
proof
let x be Real;
assume
A16: x in ['a,b'];
len UPBND_rng_d(f,n) = n+1 by Def8; then
A18: k in dom (UPBND_rng_d(f,n)) by A1,FINSEQ_1:def 3;
(const r).x = 0*x + r by FCONT_1:def 4
.= upper_bound rng ((f`|rohl)|['(k-'1)/(n+1),k/(n+1)']) by A18,Def8;
hence thesis by A12,A11,A7,A16,A1,Lm8;
end;
hence thesis by A15,A14,A8,ORDEQ_01:48;
end;
theorem Th7:
for n be Nat,k be Nat, x0 be Real, f be 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
let n be Nat,k be Nat, x0 be Real, f be PartFunc of REAL,REAL;
set df = f`|rohl;
set a = x0, b = k/(n+1);
set X = ['0,1'];
assume
A1: k in Seg (n+1) & x0 in ['(k-'1)/(n+1),k/(n+1)']
& f is_C^1-Class_on ['0,1'];
A2: f is_differentiable_on rohl & f`|rohl is continuous &
['0,1'] c= rohl & rohl c= dom f by A1;
A3: ['0,1'] = [. 0,1 .] by INTEGRA5:def 3;
reconsider r = (LWBND_rng_d(f,n)).k as Real;
set g1 = const(r);
1 <= k by A1,FINSEQ_1:1; then
A5: k-'1 <= k by XREAL_1:237; then
A6: ['(k-'1)/(n+1),k/(n+1)'] = [.(k-'1)/(n+1),k/(n+1).]
by INTEGRA5:def 3,XREAL_1:72; then
A7: (k-'1)/(n+1) <= x0 & x0 <= k/(n+1) by A1,XXREAL_1:1; then
A8: [.a,b.] c= [.(k-'1)/(n+1),k/(n+1) .] by XXREAL_1:34;
A9: x0 <= k/(n+1) by A6,A1,XXREAL_1:1;
A10: a <= b by A6,A1,XXREAL_1:1;
k <= n+1 by A1,FINSEQ_1:1; then
k/(n+1) <= (n+1)/(n+1) by XREAL_1:72; then
k/(n+1) <= 1 by XCMPLX_1:60; then
[. a,b .] c= X by A7,A3,XXREAL_1:34; then
A11: [' a,b '] c= X by A10,INTEGRA5:def 3;
A12: [' a,b '] = [.a,b.] by A7,INTEGRA5:def 3;
A13: ['(k-'1)/(n+1),k/(n+1)'] = [.(k-'1)/(n+1),k/(n+1).]
by A5,XREAL_1:72,INTEGRA5:def 3;
dom (f`|rohl) = rohl by A1,FDIFF_1:def 7; then
A15: ['a,b'] c= dom df & df is_integrable_on ['a,b'] & df|['a,b'] is bounded
by A2,A11,A1,Lm5;
A16: ['a,b'] c= dom g1 & g1 is_integrable_on ['a,b'] & g1| ['a,b'] is bounded
by A1,Lm4;
for x be Real st x in ['a,b'] holds g1.x <= df.x
proof
let x be Real;
assume
A18: x in ['a,b'];
len LWBND_rng_d(f,n) = n+1 by Def9; then
A20: k in dom (LWBND_rng_d(f,n)) by A1,FINSEQ_1:def 3;
(const(r)).x = 0*x + r by FCONT_1:def 4
.= lower_bound rng ((f`|rohl)|['(k-'1)/(n+1),k/(n+1)'])
by A20,Def9;
hence thesis by A13,A12,A8,A18,A1,Lm9;
end;
hence thesis by A16,A15,A9,ORDEQ_01:48;
end;
theorem Th8:
for n be Nat,k be Nat, x0 be Real, f be 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
let n be Nat,k be Nat, x0 be Real, f be PartFunc of REAL,REAL;
assume
A1: k in Seg (n+1) & x0 in ['(k-'1)/(n+1),k/(n+1)']
& f is_C^1-Class_on ['0,1']; then
1 <= k by FINSEQ_1:1; then
k-'1 <= k by XREAL_1:237; then
['(k-'1)/(n+1),k/(n+1)'] = [.(k-'1)/(n+1),k/(n+1).]
by INTEGRA5:def 3,XREAL_1:72; then
A3: (k-'1)/(n+1) <= x0 & x0 <= k/(n+1) by A1,XXREAL_1:1; then
A4: lower_bound ['x0,k/(n+1)']
= lower_bound [.x0,k/(n+1).] by INTEGRA5:def 3
.= x0 by A3,JORDAN5A:19;
A5: upper_bound ['x0,k/(n+1)']
= upper_bound [.x0,k/(n+1).] by A3,INTEGRA5:def 3
.= k/(n+1) by A3,JORDAN5A:19;
integral(f`|rohl,['x0,k/(n+1)']) = f.(k/(n+1)) -f.x0
by A4,A5,Th4,A1; then
A6: integral(f`|rohl,x0,k/(n+1)) = f.(k/(n+1)) -f.x0 by A3,INTEGRA5:def 4;
A7: integral(const((LWBND_rng_d(f,n)).k),x0,k/(n+1))
= ((LWBND_rng_d(f,n)).k)*(k/(n+1) -x0) by A1,Th5;
integral(const(UPBND_rng_d(f,n).k),x0,k/(n+1))
= (UPBND_rng_d(f,n).k)*(k/(n+1) -x0) by A1,Th5;
hence thesis by A6,A7,Th7,Th6,A1;
end;
Lm10:
for n be Nat,k be Nat, f be PartFunc of REAL,REAL
st k in Seg (n+1) & f is_C^1-Class_on ['0,1'] holds
for x be 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
let n be Nat,k be Nat,f be PartFunc of REAL,REAL;
set n1 = n+1;
assume
A1: k in Seg n1 & f is_C^1-Class_on ['0,1']; then
A2: f is_differentiable_on rohl & f`|rohl is continuous &
['0,1'] c= rohl & rohl c= dom f & ['0,1'] c= dom f by XBOOLE_1:1;
A3: ['0,1'] = [. 0,1 .] by INTEGRA5:def 3;
1 <= k by A1,FINSEQ_1:1; then
k-'1 <= k by XREAL_1:237; then
A5: ['(k-'1)/n1,k/n1'] = [.(k-'1)/n1,k/n1.] by XREAL_1:72,INTEGRA5:def 3;
k <= n1 by A1,FINSEQ_1:1; then
k/n1 <= n1/n1 by XREAL_1:72; then
k/n1 <= 1 by XCMPLX_1:60; then
A6: ['(k-'1)/n1,k/n1'] c= ['0,1'] by A3,A5,XXREAL_1:34;
set ck = UPBND_rng_d(f,n).k;
set c1 = const(ck);
set g = (ax_+_b(-1,k/n1));
for x be Real st x in ['(k-'1)/n1,k/n1'] holds
(const(f.(k/n1)) + (-f)).x
<= ((UPBND_rng_d(f,n).k)(#)(ax_+_b(-1,k/n1))).x
&
(((LWBND_rng_d(f,n)).k)(#)(ax_+_b(-1,k/n1))).x
<= (const(f.(k/n1)) + (-f)).x
&
(f.(k/n1) + (-f)).x = (const(f.(k/n1)) + (-f)).x
proof
let x be Real;
assume
A7: x in ['(k-'1)/n1,k/n1'];
reconsider jj= -1 as Real;
A8: ((UPBND_rng_d(f,n).k)(#)(ax_+_b(-1,k/n1))).x
= (UPBND_rng_d(f,n).k)*(AffineMap(-1,k/n1)).x by VALUED_1:6
.= (UPBND_rng_d(f,n).k)*(jj*x + k/n1) by FCONT_1:def 4
.= (UPBND_rng_d(f,n).k)*((k/n1) - x);
A9: (((LWBND_rng_d(f,n)).k)(#)(ax_+_b(-1,k/n1))).x
= ((LWBND_rng_d(f,n)).k)*(AffineMap(-1,k/n1)).x by VALUED_1:6
.= ((LWBND_rng_d(f,n)).k)*(jj*x + k/n1) by FCONT_1:def 4
.= ((LWBND_rng_d(f,n)).k)*((k/n1) - x);
A10: dom (f.(k/n1) + (-f)) = dom ((-1)(#)f) by VALUED_1:def 2
.= dom f by VALUED_1:def 5; then
A11: (f.(k/n1) + (-f)).x
= f.(k/n1) + (-f).x by A7,A2,A6,VALUED_1:def 2
.= f.(k/n1) -f.x by VALUED_1:8;
A12: dom (-f) = dom f by VALUED_1:def 5;
A13: dom (const(f.(k/n1)) + (-f))
= dom (const(f.(k/n1))) /\ dom(-f) by VALUED_1:def 1
.= REAL /\ dom(-f) by FUNCT_2:def 1
.= dom f by A12,XBOOLE_1:28;
(const(f.(k/n1))).x = 0*x + f.(k/n1) by FCONT_1:def 4 .= f.(k/n1);
then (f.(k/n1) + (-f)).x
= (const(f.(k/n1))).x + (-f).x by A7,A2,A6,A10,VALUED_1:def 2
.= ((const(f.(k/n1))) + (-f)).x by A13,A7,A2,A6,VALUED_1:def 1;
hence thesis by A8,Th8,A7,A1,A11,A9;
end;
hence thesis;
end;
Lm11A:
for n be Nat,k be 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
let n be Nat,k be Nat;
assume
A1: k in Seg (n+1);
set n1 = n+1;
set f1 = AffineMap(-1,k/(n+1));
reconsider a = (k-'1)/(n+1), b = k/(n+1) as Real;
1 <= k by A1,FINSEQ_1:1; then
A3: k-'1 <= k by XREAL_1:237;
dom (ax_+_b(-1,k/(n+1))) = REAL by FUNCT_2:def 1;
hence thesis by A3,XREAL_1:72;
end;
Lm11:
for n be Nat,k be Nat, f be 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
let n be Nat,k be Nat, f be PartFunc of REAL,REAL;
assume
A1: k in Seg (n+1) & f is_C^1-Class_on ['0,1'];
set n1 = n+1;
set w1 = (LWBND_rng_d(f,n)).k;
set f1 = AffineMap(-1,k/(n+1));
reconsider a = (k-'1)/(n+1), b = k/(n+1), c = (LWBND_rng_d(f,n)).k
as Real;
A2: 1 <= k by A1,FINSEQ_1:1; then
A3: k-'1 <= k by XREAL_1:237; then
A4: a <= b by XREAL_1:72;
A5: ['a,b'] = [.a,b.] by A3,XREAL_1:72,INTEGRA5:def 3;
dom (ax_+_b(-1,k/(n+1))) = REAL by FUNCT_2:def 1; then
A7: a<=b & [' a,b '] c= dom ((ax_+_b(-1,k/n1))) &
((ax_+_b(-1,k/n1))) is_integrable_on [' a,b '] &
((ax_+_b(-1,k/n1)))|['a,b'] is bounded by A3,XREAL_1:72,FUZZY_6:41;
reconsider jj = -1 as Real;
A8: k/n1 - (k -' 1)/n1
= k/n1 - (k - 1)/n1 by A2,XREAL_1:233
.= 1/n1;
A9: integral(ax_+_b(-1,k/n1),a,b)
= integral((AffineMap(-1,k/n1)),['a,b']) by A5,INTEGRA5:19
.= (b - a)*( jj*(b + a)/2 + b) by A4,FUZZY_8:42
.= (1/n1)^2/2 by A8;
A10: integral(((LWBND_rng_d(f,n)).k)(#)(ax_+_b(-1,k/n1)),a,b)
= ((LWBND_rng_d(f,n)).k)*integral(ax_+_b(-1,k/n1),a,b) by A7,INTEGRA6:10
.= ((LWBND_rng_d(f,n)).k)*(1/n1)^2/2 by A9;
integral((UPBND_rng_d(f,n).k)(#)(ax_+_b(-1,k/n1)),a,b)
= (UPBND_rng_d(f,n).k)*integral(ax_+_b(-1,k/n1),a,b) by A7,INTEGRA6:10
.= (UPBND_rng_d(f,n).k)*(1/n1)^2/2 by A9;
hence thesis by FUZZY_6:41,A10;
end;
Lm12:
for n be Nat,k be Nat, f be 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
let n be Nat,k be Nat, f be PartFunc of REAL,REAL;
set n1 = n+1;
assume
A1: k in Seg n1 & f is_C^1-Class_on ['0,1']; then
A2: f is_differentiable_on rohl & f`|rohl is continuous &
['0,1'] c= rohl & rohl c= dom f & ['0,1'] c= dom f by XBOOLE_1:1;
set a = (k-'1)/n1, b = k/n1;
k >= 1 by A1,FINSEQ_1:1; then
A4: k-'1 <= k by XREAL_1:237; then
A5: ['a,b'] = [.a,b.] by XREAL_1:72,INTEGRA5:def 3;
A6: ['0,1'] = [.0,1 .] by INTEGRA5:def 3;
k <= n1 by A1,FINSEQ_1:1; then
k/n1 <= n1/n1 by XREAL_1:72; then
k/n1 <= 1 by XCMPLX_1:60; then
A10: ['a,b'] c= ['0,1'] by A6,A5,XXREAL_1:34; then
A11: ['a,b'] c= dom f by A2;
a <= b & [. a,b .] c= rohl & rohl c= dom f & f|rohl is continuous
by A1,XBOOLE_1:1,XREAL_1:72, FDIFF_1:25,A10,A5,A4; then
A12: f|[' a,b '] is continuous & f is_integrable_on [' a,b '] &
f|[' a,b '] is bounded by INTEGRA7:19;
dom const(f.(k/n1)) = REAL by FUNCT_2:def 1; then
(k-'1)/n1 <= k/n1 &
['(k-'1)/n1,k/n1'] c= dom (-f) &
['(k-'1)/n1,k/n1'] c= dom (const(f.(k/n1))) &
-f is_integrable_on ['(k-'1)/n1,k/n1']
& (-f)|['(k-'1)/n1,k/n1'] is bounded &
const(f.(k/n1)) is_integrable_on ['(k-'1)/n1,k/n1'] &
(const(f.(k/n1)))|['(k-'1)/n1,k/n1'] is bounded
by XREAL_1:72,VALUED_1:def 5,A4,FUZZY_6:41,A11,A12, INTEGRA6:9,
RFUNCT_1:80;
hence thesis by INTEGRA6:12;
end;
Lm13:
for n be non zero Nat,k be Nat, f be 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
let n be non zero Nat,k be Nat, f be PartFunc of REAL,REAL;
assume
A1: k in Seg n & f is_C^1-Class_on ['0,1']; then
A2: f is_differentiable_on rohl & f`|rohl is continuous &
['0,1'] c= rohl & rohl c= dom f & ['0,1'] c= dom f by XBOOLE_1:1;
set a = 0, b = k/n;
A3: ['a,b'] = [.a,b.] by INTEGRA5:def 3;
A4: ['0,1'] = [. 0,1 .] by INTEGRA5:def 3;
k <= n by A1,FINSEQ_1:1; then
k/n <= n/n by XREAL_1:72; then
k/n <= 1 by XCMPLX_1:60; then
A7: ['a,b'] c= ['0,1'] by A4,A3,XXREAL_1:34; then
A8: ['a,b'] c= dom f by A2;
a <= b & [. a,b .] c= rohl & rohl c= dom f & f|rohl is continuous
by A1,XBOOLE_1:1,FDIFF_1:25,A3,A7; then
f|[' a,b '] is continuous & f is_integrable_on [' a,b '] &
f|[' a,b '] is bounded by INTEGRA7:19;
hence thesis by VALUED_1:def 5,A8,INTEGRA6:9,RFUNCT_1:80;
end;
Lm14:
for n be Nat, f be 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
let n be Nat, f be PartFunc of REAL,REAL;
set n1 = n+1;
assume
A1: f is_C^1-Class_on ['0,1'];
set df = f`|['0,1'];
set Dn = EqDiv(['0,1'],n1);
A2: dom UPBND_rng_d(f,n) = Seg len UPBND_rng_d(f,n) by FINSEQ_1:def 3
.= Seg n1 by Def8;
A3: vol ['0,1'] = 1 -0 by INTEGRA6:5; then
A4: EqDiv(['0,1'],n1) divide_into_equal n1 by MESFUN14:def 1; then
A5: len Dn = n1 by INTEGRA4:def 1; then
A6: dom Dn = Seg n1 by FINSEQ_1:def 3;
reconsider r1 = n1 as Real;
set p = upper_volume (@'(f,['0,1']),Dn);
A7: len p = len Dn by INTEGRA1:def 6 .= n1 by A4,INTEGRA4:def 1;
dom p = Seg n1 by A7,FINSEQ_1:def 3; then
A9: dom (r1*p) = dom UPBND_rng_d(f,n) by A2,VALUED_1:def 5;
for j be Nat st j in dom UPBND_rng_d(f,n) holds
(n1*(upper_volume (@'(f,['0,1']),EqDiv(['0,1'],n1)))).j
= (UPBND_rng_d(f,n)).j
proof
let j be Nat;
A13: (j-'1)/n1 <= j/n1 by NAT_D:35,XREAL_1:72;
assume
A11: j in dom UPBND_rng_d(f,n); then
A12: j in dom Dn by A2,A5,FINSEQ_1:def 3;
[.(j-'1)/n1,j/n1.] = divset (EqDiv(['0,1'],n1),j) by A11,A2,Th1; then
A15: upper_bound (rng ((f`|rohl)|(divset (EqDiv(['0,1'],n1),j))))
= upper_bound rng ((f`|rohl)|['(j-'1)/n1,j/n1'])
by A13,INTEGRA5:def 3
.= (UPBND_rng_d(f,n)).j by A11,Def8;
(upper_volume (@'(f,['0,1']),EqDiv(['0,1'],n1))).j
= (upper_bound (rng (@'(f,['0,1'])|(divset (Dn,j)))))
* (vol (divset (Dn,j))) by A12,INTEGRA1:def 6
.= (upper_bound (rng (((f`|rohl)|['0,1'])|(divset (Dn,j)))))
* (vol (divset (Dn,j))) by A1,Def6
.= (upper_bound (rng ((f`|rohl)|(divset (Dn,j)))))
* (vol (divset (Dn,j))) by A12,INTEGRA1:8,RELAT_1:74
.= ((UPBND_rng_d(f,n)).j)*(1/n1) by A3,A11,A2,A6,A4,MESFUN14:15,A15;
then
n1*(upper_volume (@'(f,['0,1']),EqDiv(['0,1'],n1))).j
= ((UPBND_rng_d(f,n)).j)*((1/n1)*n1)
.= ((UPBND_rng_d(f,n)).j)*1 by XCMPLX_1:87
.= (UPBND_rng_d(f,n)).j;
hence thesis by RVSUM_1:44;
end;
hence thesis by A9;
end;
Lm15:
for f be 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
let f be PartFunc of REAL,REAL;
assume
A1: f is_C^1-Class_on ['0,1'];
A2: dom (Sum_UPBND_rng_d(f)) = NAT by FUNCT_2:def 1
.= dom(upper_sum(@'(f,['0,1']),D[01])) by FUNCT_2:def 1;
for x be object st x in dom (Sum_UPBND_rng_d(f)) holds
(Sum_UPBND_rng_d(f)).x = upper_sum(@'(f,['0,1']),(D[01])).x
proof
let x be object;
assume
A4: x in dom (Sum_UPBND_rng_d(f)); then
reconsider x1 = x as Nat;
(x1+1)*(upper_volume (@'(f,['0,1']),EqDiv(['0,1'],x1+1)))
= UPBND_rng_d(f,x1) by A1,Lm14; then
A5: Sum UPBND_rng_d(f,x1)
= Sum((x1+1)*(upper_volume(@'(f,['0,1']),EqDiv(['0,1'],x1+1))))
by NIVEN:6
.= (x1+1)*Sum(upper_volume (@'(f,['0,1']),EqDiv(['0,1'],x1+1)))
by RVSUM_1:87;
(Sum_UPBND_rng_d(f)).x1
= (Sum (UPBND_rng_d(f,x1)))/(x1+1) by Def10
.= ((1/(x1+1))*(x1+1))*
(Sum(upper_volume(@'(f,['0,1']),EqDiv(['0,1'],x1+1))) ) by A5
.= 1*(Sum(upper_volume (@'(f,['0,1']),EqDiv(['0,1'],x1+1))))
by XCMPLX_1:106
.= upper_sum(@'(f,['0,1']),(D[01]).x1) by Def1,A4
.= upper_sum(@'(f,['0,1']),(D[01])).x1 by INTEGRA2:def 2;
hence thesis;
end;
hence thesis by A2;
end;
Lm16:
for f be 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
let f be PartFunc of REAL,REAL;
assume
A1: f is_C^1-Class_on ['0,1'];
A2: vol ['0,1'] = 1 -0 by INTEGRA6:5;
(f`|rohl)|['0,1'] is bounded by Lm6,A1; then
@'(f,['0,1'])|['0,1'] is bounded by A1,Def6; then
upper_sum(@'(f,['0,1']),(D[01])) is convergent &
lim upper_sum(@'(f,['0,1']),(D[01])) = upper_integral(@'(f,['0,1']))
by A2,Th3,INTEGRA3:26;
hence thesis by A1,Lm15;
end;
Lm17:
for n be Nat, f be 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
let n be Nat, f be PartFunc of REAL,REAL;
set n1 = n+1;
assume
A1: f is_C^1-Class_on ['0,1'];
set df = f`|rohl;
set Dn = EqDiv(['0,1'],n1);
A2: dom LWBND_rng_d(f,n) = Seg len LWBND_rng_d(f,n) by FINSEQ_1:def 3
.= Seg n1 by Def9;
A3: vol ['0,1'] = 1 -0 by INTEGRA6:5; then
A4: EqDiv(['0,1'],n1) divide_into_equal n1 by MESFUN14:def 1; then
A5: len Dn = n1 by INTEGRA4:def 1;
reconsider r1 = n1 as Real;
set p = lower_volume (@'(f,['0,1']),Dn);
len p = len Dn by INTEGRA1:def 7 .= n1 by A4,INTEGRA4:def 1; then
dom p = Seg n1 by FINSEQ_1:def 3; then
A8: dom (r1*p) = dom LWBND_rng_d(f,n) by VALUED_1:def 5,A2;
for j be Nat st j in dom(LWBND_rng_d(f,n)) holds
(n1*(lower_volume (@'(f,['0,1']),EqDiv(['0,1'],n1)))).j
= (LWBND_rng_d(f,n)).j
proof
let j be Nat;
assume
A10: j in dom(LWBND_rng_d(f,n)); then
A11: j in dom Dn by A2,A5,FINSEQ_1:def 3;
(j-'1)/n1 <= j/n1 by NAT_D:35,XREAL_1:72; then
['(j-'1)/n1, j/n1'] = [.(j-'1)/n1, j/n1.] by INTEGRA5:def 3; then
A13: lower_bound (rng ((f`|rohl)|(divset (EqDiv(['0,1'],n1),j))))
= lower_bound rng ((f`|rohl)|['(j-'1)/n1,j/n1']) by A10,A2,Th1
.= (LWBND_rng_d(f,n)).j by A10,Def9;
(lower_volume (@'(f,['0,1']),EqDiv(['0,1'],n1))).j
= (lower_bound (rng (@'(f,['0,1'])|(divset (Dn,j)))))
* (vol (divset (Dn,j))) by A11,INTEGRA1:def 7
.= (lower_bound (rng (((f`|rohl)|['0,1'])|(divset (Dn,j)))))
* (vol (divset (Dn,j))) by A1,Def6
.= (lower_bound (rng ((f`|rohl)|(divset (Dn,j)))))
* (vol (divset (Dn,j))) by A11,INTEGRA1:8,RELAT_1:74
.= ((LWBND_rng_d(f,n)).j)*(1/n1) by A11,A3,A4,MESFUN14:15,A13; then
n1*(lower_volume (@'(f,['0,1']),EqDiv(['0,1'],n1))).j
= ((LWBND_rng_d(f,n)).j)*((1/n1)*n1)
.= ((LWBND_rng_d(f,n)).j)*1 by XCMPLX_1:87
.= (LWBND_rng_d(f,n)).j;
hence thesis by RVSUM_1:44;
end;
hence thesis by A8;
end;
Lm18:
for f be 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
let f be PartFunc of REAL,REAL;
assume
A1: f is_C^1-Class_on ['0,1'];
A2: dom (Sum_LWBND_rng_d(f)) = NAT by FUNCT_2:def 1
.= dom(lower_sum(@'(f,['0,1']),D[01])) by FUNCT_2:def 1;
for x be object st x in dom (Sum_LWBND_rng_d(f)) holds
(Sum_LWBND_rng_d(f)).x = lower_sum(@'(f,['0,1']),(D[01])).x
proof
let x be object;
assume
A4: x in dom Sum_LWBND_rng_d(f); then
reconsider x1 = x as Nat;
(x1+1)*(lower_volume (@'(f,['0,1']),EqDiv(['0,1'],x1+1)))
= LWBND_rng_d(f,x1) by A1,Lm17; then
A5: Sum (LWBND_rng_d(f,x1))
= Sum((x1+1)*(lower_volume (@'(f,['0,1']),EqDiv(['0,1'],x1+1))))
by NIVEN:6
.= (x1+1)*Sum(lower_volume (@'(f,['0,1']),EqDiv(['0,1'],x1+1)))
by RVSUM_1:87;
(Sum_LWBND_rng_d(f)).x1
= (Sum (LWBND_rng_d(f,x1)))/(x1+1) by Def11
.= ((1/(x1+1))*(x1+1))*
(Sum(lower_volume(@'(f,['0,1']),EqDiv(['0,1'],x1+1))) ) by A5
.= 1*(Sum(lower_volume (@'(f,['0,1']),EqDiv(['0,1'],x1+1))))
by XCMPLX_1:106
.= lower_sum(@'(f,['0,1']),(D[01]).x1) by A4,Def1
.= lower_sum(@'(f,['0,1']),(D[01])).x1 by INTEGRA2:def 3;
hence thesis;
end;
hence thesis by A2;
end;
Lm19:
for f be 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
let f be PartFunc of REAL,REAL;
A2: vol ['0,1'] = 1 -0 by INTEGRA6:5;
assume
A1: f is_C^1-Class_on ['0,1']; then
(f`|rohl)|['0,1'] is bounded by Lm6; then
@'(f,['0,1'])|['0,1'] is bounded by A1,Def6; then
lower_sum(@'(f,['0,1']),(D[01])) is convergent &
lim lower_sum(@'(f,['0,1']),(D[01])) = lower_integral(@'(f,['0,1']))
by A2,Th3,INTEGRA3:25;
hence thesis by A1,Lm18;
end;
definition
let n be Nat, f be PartFunc of REAL,REAL;
func 'F'(f,n) -> FinSequence of F_Real means
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
proof
defpred P[Nat,object] means
$2 = integral(const(f.($1/(n+1))),($1-'1)/(n+1),$1/(n+1));
A1: for k be Nat st k in Seg (n+1) ex x being Element of F_Real st P[k,x]
proof
let k be Nat;
assume k in Seg (n+1);
set r = integral(const(f.(k/(n+1))),(k-'1)/(n+1),k/(n+1));
reconsider r as Element of [#]F_Real by VECTSP_1:def 5, XREAL_0:def 1;
take r;
thus thesis;
end;
consider g being FinSequence of F_Real such that
A2: dom g = Seg (n+1) & for k being Nat st k in Seg (n+1) holds P[k,g.k]
from FINSEQ_1:sch 5(A1);
take g;
thus thesis by A2;
end;
uniqueness
proof
let z1,z2 be FinSequence of F_Real;
assume that
A3: dom z1 = Seg (n+1) and
A4: for i be Nat st i in dom z1 holds
z1.i = integral(const(f.(i/(n+1))),(i-'1)/(n+1),i/(n+1))
and
A5: dom z2 = Seg (n+1) and
A6: for i be Nat st i in dom z2 holds
z2.i = integral(const(f.(i/(n+1))),(i-'1)/(n+1),i/(n+1));
for x be Nat st x in dom z1 holds z1.x = z2.x
proof
let x be Nat;
assume
A7: x in dom z1; then
reconsider x9 = x as Element of NAT;
thus
z1.x = integral(const(f.(x9/(n+1))),(x9-'1)/(n+1),x9/(n+1)) by A4,A7
.= z2.x by A6,A3,A5,A7;
end;
hence thesis by A3,A5;
end;
end;
definition
let n be Nat, f be PartFunc of REAL,REAL;
func 'G'(f,n) -> FinSequence of F_Real means :Def13:
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
proof
defpred P[Nat,object] means
$2 = integral((-f),($1-'1)/(n+1),$1/(n+1));
A1: for k be Nat st k in Seg (n+1) ex x being Element of F_Real st P[k,x]
proof
let k be Nat;
assume k in Seg (n+1);
set r = integral((-f),(k-'1)/(n+1),k/(n+1));
reconsider r as Element of [#]F_Real by VECTSP_1:def 5, XREAL_0:def 1;
take r;
thus thesis;
end;
consider g being FinSequence of F_Real such that
A2: dom g = Seg (n+1) & for k being Nat st k in Seg (n+1) holds P[k,g.k]
from FINSEQ_1:sch 5(A1);
take g;
thus thesis by A2;
end;
uniqueness
proof
let z1,z2 be FinSequence of F_Real;
assume that
A3: dom z1 = Seg (n+1) and
A4: for i be Nat st i in dom z1 holds
z1.i = integral((-f),(i-'1)/(n+1),i/(n+1))
and
A5: dom z2 = Seg (n+1) and
A6: for i be Nat st i in dom z2 holds
z2.i = integral((-f),(i-'1)/(n+1),i/(n+1));
for x be Nat st x in dom z1 holds z1.x = z2.x
proof
let x be Nat;
assume
A7: x in dom z1; then
reconsider x9 = x as Element of NAT;
thus z1.x = integral((-f),(x9-'1)/(n+1),x9/(n+1)) by A4,A7
.= z2.x by A6,A3,A5,A7;
end;
hence thesis by A3,A5;
end;
end;
definition
let n be Nat,f be PartFunc of REAL,REAL;
func step_(f,n) -> FinSequence of F_Real means
:Def14:
dom it = Seg (n+1) & for i being Nat st i in dom it holds
it.i = f.(i/(n+1));
existence
proof
defpred P[Nat,object] means
$2 = f.($1/(n+1));
A1: for k be Nat st k in Seg (n+1) ex x being Element of F_Real st P[k,x]
proof
let k be Nat;
assume k in Seg (n+1);
set r = f.(k/(n+1));
reconsider r as Element of [#]F_Real by VECTSP_1:def 5,XREAL_0:def 1;
take r;
thus thesis;
end;
consider g being FinSequence of F_Real such that
A2: dom g = Seg (n+1) & for k being Nat st k in Seg (n+1) holds P[k,g.k]
from FINSEQ_1:sch 5(A1);
take g;
thus thesis by A2;
end;
uniqueness
proof
let z1,z2 be FinSequence of F_Real;
assume that
A3: dom z1 = Seg (n+1) and
A4: for i be Nat st i in dom z1 holds
z1.i = f.(i/(n+1)) and
A5: dom z2 = Seg (n+1) and
A6: for i be Nat st i in dom z2 holds
z2.i = f.(i/(n+1));
for x be Nat st x in dom z1 holds z1.x = z2.x
proof
let x be Nat;
assume
A7: x in dom z1; then
reconsider x9 = x as Element of NAT;
thus z1.x = f.(x9/(n+1)) by A4,A7
.= z2.x by A6,A3,A5,A7;
end;
hence thesis by A3,A5;
end;
end;
Lm20:
for f be PartFunc of REAL,REAL, n be Nat st f is_C^1-Class_on ['0,1'] holds
for k be 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
let f be PartFunc of REAL,REAL, n be Nat;
set n1 = n+1;
reconsider r1 = 1/n1 as Element of F_Real by XREAL_0:def 1,VECTSP_1:def 5;
assume
f is_C^1-Class_on ['0,1'];
for k be Nat st k in Seg (n+1) holds
integral(const(f.(k/(n+1))),(k-'1)/(n+1),k/(n+1))
= (r1*(step_(f,n))).k
proof
let k be Nat;
set n1 = n+1;
set c = (k-'1)/n1, d = k/n1;
set a = 0, b = f.(k/n1);
assume
A1: k in Seg (n+1); then
A2: 1 <= k by FINSEQ_1:1; then
A3: k-'1 <= k by XREAL_1:237; then
A4: c <= d by XREAL_1:72;
A5: ['c,d'] = [.c,d.] by A3,XREAL_1:72,INTEGRA5:def 3;
A6: (k/n1 - (k-'1)/n1) = k/n1 - (k-1)/n1 by A2,XREAL_1:233
.= 1/n1;
A7: k in dom(step_(f,n)) by A1,Def14; then
A8: k in dom(r1*(step_(f,n))) by POLYNOM1:def 1;
A9: r1*((step_(f,n)).k)
= r1*((step_(f,n))/.k) by A7, PARTFUN1:def 6
.= (r1*(step_(f,n)))/.k by A7,POLYNOM1:def 1
.= (r1*(step_(f,n))).k by A8, PARTFUN1:def 6;
integral(const(f.(k/(n+1))),(k-'1)/(n+1),k/(n+1))
= integral((AffineMap(a,b)),['c,d']) by INTEGRA5:19,A5
.= (k/n1 - (k-'1)/n1)*(0*(k/n1 + (k-'1)/n1)/2 + f.(k/n1))
by A4,FUZZY_8:42
.= r1*(step_(f,n)).k by A6,A7,Def14;
hence thesis by A9;
end;
hence thesis;
end;
theorem Th9:
for n be Nat,f be PartFunc of REAL,REAL holds
integral(-f,0,0) = 0
proof
let n be Nat, f be PartFunc of REAL,REAL;
A1: [. 0,0 .] = ['0,0'] by INTEGRA5:def 3;
['0,0'] = [. 0,0 .] by INTEGRA5:def 3; then
-integral(-f,['0,0']) = integral(-f,0,0) by INTEGRA5:20; then
integral(-f,0,0) = -integral(-f,0,0) by A1,INTEGRA5:19;
hence thesis;
end;
Lm21:
for n be Nat,f be 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
let n be Nat,f be PartFunc of REAL,REAL;
assume
A1: f is_C^1-Class_on ['0,1'];
set s = (n+1)-'1;
A2: s < s + 1 by XREAL_1:39;
A3: s < n+1 by XREAL_1:39;
A4: (s+1)/(n+1) = 1 by XCMPLX_1:60;
integral((-f),0,s/(n+1)) + integral((-f),s/(n+1),1) = integral((-f),0,1)
proof
per cases;
suppose
A5: s <> 0; then
s >= 1 by NAT_1:14; then
s in Seg (n+1) by A3; then
A6: -f is_integrable_on ['0, s/(n+1)'] &
(-f) | ['0, s/(n+1)'] is bounded & ['0, s/(n+1)'] c= dom (-f)
by Lm13,A1;
A7: 0 < s/(n+1) < (s+1)/(n+1) by A2,XREAL_1:74, A5;
1 <= s+1 & s+1 <= n+1 by NAT_1:14; then
A8: s+1 in Seg (n+1); then
A9: ['0,(s+1)/(n+1)'] c= dom(-f) by Lm13,A1;
-f is_integrable_on ['s/(n+1), (s+1)/(n+1)'] &
(-f) | ['s/(n+1), (s+1)/(n+1)'] is bounded &
['s/(n+1), (s+1)/(n+1)'] c= dom (-f) by A8,Lm12,A1;
hence thesis by A4,INTEGR24:1,A9,A6,A7;
end;
suppose
A10: s = 0;
integral(-f,0,0) = 0 by Th9;
hence thesis by A10;
end;
end;
hence thesis;
end;
Lm22:
for n be Nat,f be PartFunc of REAL,REAL
st f is_C^1-Class_on ['0,1'] holds Sum 'G'(f,n) = integral((-f),0,1)
proof
let n be Nat,f be PartFunc of REAL,REAL;
set n1 = n+ 1;
assume
A1: f is_C^1-Class_on ['0,1'];
A2: dom ('G'(f,n)) = Seg n1 by Def13;
Sum 'G'(f,n) = integral(-f,0,1)
proof
defpred P[Nat] means
$1 < n1 implies Sum ('G'(f,n)|$1) = integral((-f),0,$1/n1);
A3: for j be Nat st for m be Nat st m < j holds P[m] holds P[j]
proof
let j be Nat;
assume
A4: for m be Nat st m < j holds P[m];
j < n1 implies Sum ('G'(f,n)|j) = integral((-f),0,j/n1)
proof
assume
A5: j < n1;
per cases;
suppose
j > 0; then
reconsider s = j - 1 as Nat;
s + 1 = j-1 +1 = j; then
s < j by NAT_1:19; then
A9: s < n1 implies Sum ('G'(f,n)|s) = integral((-f),0,s/n1)
by A4;
A10: 1 <= s+1 by NAT_1:14;
reconsider g = ('G'(f,n)|s) as FinSequence of F_Real;
A11: rng ('G'(f,n)) c= the carrier of F_Real by FINSEQ_1:def 4;
A12: s + 1 in dom ('G'(f,n)) by A2,A5,A10; then
reconsider rs = ('G'(f,n)).(s+1) as Element of F_Real by A11,FUNCT_1:3;
A13: s < s + 1 by XREAL_1:29; then
A14: s < n1 by A5,XXREAL_0:2;
A15: ('G'(f,n)).(s+1)
= integral((-f),((s+1)-'1)/n1,(s+1)/n1) by A12,Def13
.= integral((-f),s/n1,(s+1)/n1);
A16: integral((-f),0,s/n1) + integral((-f),s/n1,(s+1)/n1)
= integral((-f),0,(s+1)/n1)
proof
per cases;
suppose
A17: s <> 0; then
s >= 1 by NAT_1:14; then
s in Seg n1 by A14; then
A18: -f is_integrable_on ['0, s/n1'] &
(-f) | ['0, s/n1'] is bounded & ['0, s/n1'] c= dom (-f)
by Lm13,A1;
A19: 0 < s/n1 < (s+1)/n1 by XREAL_1:29,74,A17;
1 <= s+1 & s+1 < n1 by A5,NAT_1:14; then
A20: s+1 in Seg n1; then
A21: ['0,(s+1)/n1'] c= dom(-f) by Lm13,A1;
-f is_integrable_on ['(s+1-'1)/n1, (s+1)/n1'] &
(-f) | ['(s+1-'1)/n1, (s+1)/n1'] is bounded &
['(s+1-'1)/n1, (s+1)/n1'] c= dom (-f) by A20,Lm12,A1;
hence thesis by INTEGR24:1,A21,A18,A19;
end;
suppose
A23: s = 0;
integral(-f,0,0) = 0 by Th9;
hence thesis by A23;
end;
end;
Sum ('G'(f,n)|(s+1)) = Sum (g^<* rs *>) by A12,FINSEQ_5:10
.= Sum g + rs by FVSUM_1:71
.= integral(-f,0,(s+1)/n1) by A16,A15,A9,A13,A5,XXREAL_0:2;
hence thesis;
end;
suppose
A25: j = 0;
Sum ('G'(f,n)|0) = Sum( <*>(the carrier of F_Real))
.= 0.F_Real by RLVECT_1:43 .= 0 by VECTSP_1:def 5;
hence thesis by Th9,A25;
end;
end;
hence thesis;
end;
A27: for j be Nat holds P[j] from NAT_1:sch 4(A3);
reconsider i = n1-'1 as Nat;
A28: rng ('G'(f,n)) c= the carrier of F_Real by FINSEQ_1:def 4;
reconsider g = ('G'(f,n)|i) as FinSequence of F_Real;
A29: ('G'(f,n)).(i+1) in rng ('G'(f,n)) by A2,FUNCT_1:3,FINSEQ_1:3;
reconsider r1 = ('G'(f,n)).(i+1) as Element of F_Real by A28,A29;
A30: ('G'(f,n)).n1 = integral((-f),(n1-'1)/n1,n1/n1)
by Def13,A2,FINSEQ_1:3
.= integral((-f),(n1-'1)/n1,1) by XCMPLX_1:60;
A31: Sum ('G'(f,n)|(n1-1)) = integral((-f),0,(n1-1)/n1) by A27,XREAL_1:44;
Sum ('G'(f,n)|(i+1)) = Sum (g^<* r1 *>) by A2,FINSEQ_1:3,FINSEQ_5:10
.= Sum g + r1 by FVSUM_1:71
.= integral((-f),0,1) by A1,Lm21,A30,A31;
hence thesis by A2;
end;
hence thesis;
end;
Lm23:
for n be Nat,k be Nat, f be 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
let n be Nat,k be Nat, f be PartFunc of REAL,REAL;
set n1 = n+1;
assume
A1: k in Seg n1 & f is_C^1-Class_on ['0,1'];
set a = (k-'1)/n1, b = k/n1;
set f1 = (ax_+_b(-1,k/n1));
set g = const(f.(k/n1)) + (-f);
reconsider w1 = (UPBND_rng_d(f,n)).k as Real;
reconsider w2 = (LWBND_rng_d(f,n)).k as Real;
A2: (k-'1)/n1 <= k/n1 &
['(k-'1)/n1,k/n1'] c= dom (-f) &
['(k-'1)/n1,k/n1'] c= dom (const(f.(k/n1))) &
-f is_integrable_on ['(k-'1)/n1,k/n1'] &
(-f)|['(k-'1)/n1,k/n1'] is bounded &
const(f.(k/n1)) is_integrable_on ['(k-'1)/n1,k/n1'] &
(const(f.(k/n1)))|['(k-'1)/n1,k/n1'] is bounded &
integral(const(f.(k/n1)) + (-f),(k-'1)/n1,k/n1)
= integral(const(f.(k/n1)),(k-'1)/n1,k/n1) + integral((-f),(k-'1)/n1,k/n1)
by Lm12,Lm11A,A1;
A3: (k-'1)/n1 <= k/n1 & [' (k-'1)/n1,k/n1 '] c= dom ((ax_+_b(-1,k/n1))) &
((ax_+_b(-1,k/n1))) is_integrable_on ['(k-'1)/n1,k/n1 '] &
((ax_+_b(-1,k/n1)))|['(k-'1)/n1,k/n1 '] is bounded &
integral(((LWBND_rng_d(f,n)).k)(#)(ax_+_b(-1,k/n1)),(k-'1)/n1,k/n1)
= ((LWBND_rng_d(f,n)).k)*(1/n1)^2/2 &
integral(((UPBND_rng_d(f,n)).k)(#)(ax_+_b(-1,k/n1)),(k-'1)/n1,k/n1)
= ((UPBND_rng_d(f,n)).k)*(1/n1)^2/2 by Lm11,Lm11A,A1;
A4: w1(#)f1 is_integrable_on ['a,b'] by A3,INTEGRA6:9;
A5: (w1(#)f1)|['a,b'] is bounded by A3,RFUNCT_1:80;
A6: w2(#)f1 is_integrable_on ['a,b'] by A3,INTEGRA6:9;
A7: (w2(#)f1)|['a,b'] is bounded by A3,RFUNCT_1:80;
A8: dom f = dom (-f) by VALUED_1:def 5;
dom (const(f.(k/n1)) + (-f))
= dom (const(f.(k/n1))) /\ dom(-f) by VALUED_1:def 1
.= REAL /\ dom(-f) by FUNCT_2:def 1
.= dom(-f) by A8,XBOOLE_1:28; then
A9: [' (k-'1)/n1,k/n1 '] c= dom g by Lm12,A1;
A10: ['a,b'] c= dom f1 & f1 is_integrable_on ['a,b'] &
f1| ['a,b'] is bounded by Lm11,Lm11A,A1; then
A11: ['a,b'] c= dom (w1(#)f1) by VALUED_1:def 5;
A12: ['a,b'] c= dom (w2(#)f1) by A10,VALUED_1:def 5;
A13: g is_integrable_on ['a,b'] &
g| ['a,b'] is bounded by A2,INTEGRA6:19;
A14: for x be Real st x in ['a,b'] holds g.x <= (w1(#)f1).x by A1,Lm10;
for x be Real st x in ['a,b'] holds (w2(#)f1).x <= g.x by A1,Lm10;
hence thesis by A3,A12,A6,A7,A13,A9,
ORDEQ_01:48,A11,A4,A5,A14;
end;
Lm24:
for n be Nat, f be PartFunc of REAL,REAL
st f is_C^1-Class_on ['0,1'] holds
for k be 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
let n be Nat, f be PartFunc of REAL,REAL;
set n1 = n+1;
assume
A1: f is_C^1-Class_on ['0,1'];
reconsider r1 = 1/n1 as Element of F_Real by VECTSP_1:def 5,XREAL_0:def 1;
A2: dom (r1*(step_(f,n))) = dom(step_(f,n)) by POLYNOM1:def 1
.= Seg n1 by Def14; then
A3: dom ((r1*(step_(f,n))) + 'G'(f,n)) = Seg n1 by BINOM:def 1; then
A4: len ((r1*(step_(f,n))) + 'G'(f,n)) = n1 by FINSEQ_1:def 3;
reconsider FG = ((r1*(step_(f,n)))+'G'(f,n)) as FinSequence of F_Real;
for i be Nat st i in Seg n1 holds
FG.i = integral(const(f.(i/n1)) + (-f),(i-'1)/n1,i/n1)
proof
let i be Nat;
assume
A5: i in Seg n1; then
A6: 1 <= i <= n1 by FINSEQ_1:1;
A7: i in dom ('G'(f,n)) by A5,Def13; then
A8: ('G'(f,n))/.i = ('G'(f,n)).i by PARTFUN1:def 6;
((r1*(step_(f,n))) + 'G'(f,n)).i
= ((r1*(step_(f,n))) + 'G'(f,n))/.i by A5,A3,PARTFUN1:def 6
.= (r1*(step_(f,n)))/.i + ('G'(f,n))/.i by A4,A6,BINOM:def 1
.= (In(1/(n1),F_Real)*(step_(f,n))).i + ('G'(f,n)).i
by A5,A2,PARTFUN1:def 6,A8
.= integral(const(f.(i/n1)),(i-'1)/n1,i/n1) + ('G'(f,n)).i
by A5,A1,Lm20
.= integral(const(f.(i/n1)),(i-'1)/n1,i/n1)
+ integral((-f),(i-'1)/n1,i/n1) by Def13,A7
.= integral(const(f.(i/n1)) + (-f),(i-'1)/n1,i/n1) by A1,A5,Lm12;
hence thesis;
end;
hence thesis;
end;
Lm25:
for a,b being Element of F_Real,
p being FinSequence of the carrier of F_Real holds (a*b)*p = a * (b*p)
proof
let a,b be Element of F_Real, p be FinSequence of the carrier of F_Real;
set bp = b*p;
set ab1p = (a*b)*p;
set a1bp = a*(b*p);
A1: dom bp = dom p by POLYNOM1:def 1;
A2: dom ab1p = dom p by POLYNOM1:def 1;
dom a1bp = dom bp by POLYNOM1:def 1 .= dom p by POLYNOM1:def 1; then
A4: dom a1bp = dom ab1p by POLYNOM1:def 1;
now
let i be Nat such that
A5: i in dom ab1p;
thus ab1p/.i = (a*b)*p/.i by A2,A5,POLYNOM1:def 1
.= a*(b*p/.i)
.= a*(bp/.i) by A2,A5,POLYNOM1:def 1
.= (a*(bp))/.i by A1,A2,A5,POLYNOM1:def 1;
end;
hence thesis by A4,FINSEQ_5:12;
end;
Lm26:
for p being FinSequence of the carrier of F_Real holds (1.F_Real)*p = p
proof
let p be FinSequence of the carrier of F_Real;
set p1 = (1.F_Real)*p;
A1: dom p1 = dom p by POLYNOM1:def 1;
now
let i be Nat;
assume i in dom p1;
hence p1/.i = (1.F_Real)*(p/.i) by A1,POLYNOM1:def 1 .= p/.i;
end;
hence thesis by A1,FINSEQ_5:12;
end;
Lm27:
for n be Nat, f be 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
let n be Nat, f be PartFunc of REAL,REAL;
set n1 = n + 1;
set F1 = (In(1/(n+1),F_Real)*(step_(f,n)));
assume
A1: f is_C^1-Class_on ['0,1'];
A2: len (UPBND_rng_d(f,n)) = n1 by Def8; then
A3: dom (UPBND_rng_d(f,n)) = Seg n1 by FINSEQ_1:def 3;
reconsider r1 = 1/n1 as Real;
reconsider r2 = 1/n1 as Element of F_Real by XREAL_0:def 1,VECTSP_1:def 5;
A4: dom (r1 * (UPBND_rng_d(f,n)))
= dom (UPBND_rng_d(f,n)) by VALUED_1:def 5;
A5: vol ['0,1'] = 1 -0 by INTEGRA6:5; then
A6: EqDiv(['0,1'],n1) divide_into_equal n1 by MESFUN14:def 1; then
A7: len EqDiv(['0,1'],n1) = n1 by INTEGRA4:def 1;
set Dn = EqDiv(['0,1'],n1);
A8: len (upper_volume(@'(f,['0,1']),EqDiv(['0,1'],n1)))
= len EqDiv(['0,1'],n1) by INTEGRA1:def 6 .= n1 by A6,INTEGRA4:def 1;
for k be Nat st k in dom (upper_volume(@'(f,['0,1']),EqDiv(['0,1'],n1)))
holds
(upper_volume(@'(f,['0,1']),EqDiv(['0,1'],n1))).k
= (r1 * UPBND_rng_d(f,n)).k
proof
let k be Nat;
assume
k in dom (upper_volume(@'(f,['0,1']),EqDiv(['0,1'],n1))); then
A10: k in Seg (n+1) by A8,FINSEQ_1:def 3; then
A11: k in dom EqDiv(['0,1'],n1) by A7,FINSEQ_1:def 3; then
A12: vol divset(EqDiv(['0,1'],n1),k) = 1/n1 by A5,A6,MESFUN14:15;
(k-'1)/n1 <= k/n1 by NAT_D:35,XREAL_1:72; then
A13: ['(k-'1)/n1, k/n1'] = [.(k-'1)/n1, k/n1.] by INTEGRA5:def 3;
A14: @'(f,['0,1']) = (f`|rohl)|['0,1'] by A1,Def6;
A15: k in dom (UPBND_rng_d(f,n)) by A2,FINSEQ_1:def 3,A10; then
(r1 * UPBND_rng_d(f,n)).k
= (1/n1)*(UPBND_rng_d(f,n)).k by A4,VALUED_1:def 5
.= upper_bound rng ((f`|rohl)|['(k-'1)/n1,k/n1']) * (1/n1) by A15,Def8
.= upper_bound rng ((f`|rohl)|divset (EqDiv(['0,1'],n1),k))
* (vol divset(Dn,k)) by A12,A10,Th1,A13
.= (upper_bound (rng (((f`|rohl)|['0,1'])|(divset (Dn,k)) )))
* (vol (divset (Dn,k))) by A11,INTEGRA1:8,RELAT_1:74
.= (upper_volume(@'(f,['0,1']),EqDiv(['0,1'],n1))).k
by A14,A11,INTEGRA1:def 6;
hence thesis;
end; then
A16: upper_volume(@'(f,['0,1']),EqDiv(['0,1'],n1))
= r1 * (UPBND_rng_d(f,n)) by A3,A4,A8,FINSEQ_1:def 3;
n in NAT by ORDINAL1:def 12; then
A18: upper_sum(@'(f,['0,1']),(D[01]).n)
= Sum(r1*(UPBND_rng_d(f,n))) by A16,Def1
.= Sum(r1*@(UPBND_rng_d(f,n))) by MATRTOP1:def 2
.= r1*Sum(@(UPBND_rng_d(f,n))) by RVSUM_1:87;
reconsider r1 = 1/n1 as Element of F_Real by XREAL_0:def 1,VECTSP_1:def 5;
A19: dom F1 = dom(step_(f,n)) by POLYNOM1:def 1
.= Seg n1 by Def14; then
A20: dom F1 = dom ('G'(f,n)) by Def13;
reconsider H = UPBND_rng_d(f,n) as FinSequence of F_Real;
reconsider FG = (F1 + 'G'(f,n)) as FinSequence of F_Real;
reconsider r3 = 2*n1 as Element of F_Real by XREAL_0:def 1,VECTSP_1:def 5;
A21: dom (F1 + 'G'(f,n)) = Seg n1 by A19,BINOM:def 1;
Seg(len(r3*FG)) = Seg(len(FG * r3)) by BINOM:6
.= dom(FG * r3) by FINSEQ_1:def 3
.= dom FG by POLYNOM1:def 2
.= Seg len FG by FINSEQ_1:def 3; then
A22: len(r3*FG) = len FG by FINSEQ_1:6 .= n1 by A21,FINSEQ_1:def 3;
len UPBND_rng_d(f,n) = n1 by Def8; then
A23: dom UPBND_rng_d(f,n) = Seg n1 by FINSEQ_1:def 3;
dom (r2 * (UPBND_rng_d(f,n)))
= dom (UPBND_rng_d(f,n)) by POLYNOM1:def 1; then
A24: len (r2*(UPBND_rng_d(f,n))) = len (UPBND_rng_d(f,n)) by FINSEQ_3:29
.= n1 by Def8;
A25: for k be Nat st k in dom (r3*(F1 + 'G'(f,n))) holds
(r3*(F1 + 'G'(f,n))).k <= (r2*(UPBND_rng_d(f,n))).k
proof
let k be Nat;
assume
A26: k in dom(r3*(F1 + 'G'(f,n))); then
A27: k in Seg n1 by A22,FINSEQ_1:def 3;
A28: k in dom FG by A21,A22,FINSEQ_1:def 3,A26; then
A29: r3*(FG.k) = r3*(FG/.k) by PARTFUN1:def 6
.= (r3*FG)/.k by A28,POLYNOM1:def 1
.= (r3*FG).k by A26,PARTFUN1:def 6;
A30: dom H = dom (r2*H) by POLYNOM1:def 1;
A31: k in dom H by A23,A22,FINSEQ_1:def 3,A26;
k in dom (r2*H) by A30,A23,A22,FINSEQ_1:def 3,A26; then
A33: (r2*H).k = (r2*H)/.k by PARTFUN1:def 6
.= r2*(H/.k) by A31,POLYNOM1:def 1
.= r2*(H.k) by A31,PARTFUN1:def 6;
((1/n1)^2/2)*(2*n1) = (1/n1)*((1/n1)*n1)
.= (1/n1)*1 by XCMPLX_1:87; then
A35: (((UPBND_rng_d(f,n)).k)*(1/(n+1))^2/2)*(2*n1)
= ((UPBND_rng_d(f,n)).k)*(1/n1);
(F1 + 'G'(f,n)).k
= integral(const(f.(k/(n+1))) + (-f),(k-'1)/(n+1),k/(n+1))
by Lm24,A1,A27;
hence thesis by A29,A33,A35,XREAL_1:64,Lm23,A1,A27;
end;
A37: Sum (r3*(F1 + 'G'(f,n)))
= r3* Sum(F1 + 'G'(f,n)) by FVSUM_1:73
.= r3*(Sum F1 + Sum('G'(f,n))) by A20,BINOM:7
.= r3*(Sum F1 + integral((-f),0,1)) by Lm22,A1;
reconsider rf = Sum F1 as Element of F_Real;
reconsider r0 = n1 as Element of F_Real by VECTSP_1:def 5,XREAL_0:def 1;
A38: r0*r1 = In(1,REAL) by XCMPLX_1:106;
A39: r0*F1 = (r0*r1)*(step_(f,n)) by Lm25
.= step_(f,n) by Lm26,A38,VECTSP_1:def 5;
A40: n1*(Sum F1 + integral((-f),0,1))
= r0*(Sum F1) + r0*integral((-f),0,1)
.= Sum (step_(f,n)) + r0*integral((-f),0,1) by A39,FVSUM_1:73;
A41: Sum (r2*(UPBND_rng_d(f,n)))
= r2*(Sum (UPBND_rng_d(f,n))) by FVSUM_1:73
.= upper_sum(@'(f,['0,1']),(D[01]).n)
by A18,MATRPROB:36,MATRTOP1:def 2;
r3*(Sum F1 + integral((-f),0,1))
<= upper_sum(@'(f,['0,1']),(D[01]).n)
by A37,A41,A25,A24,A22,E_TRANS1:2; then
(2*(n+1))*(Sum F1 + integral((-f),0,1))
<= (upper_sum(@'(f,['0,1']),(D[01]))).n by INTEGRA2:def 2; then
(1/2)*((2*(n+1))*(Sum F1 + integral((-f),0,1)))
<= (1/2)*(upper_sum(@'(f,['0,1']),(D[01]))).n by XREAL_1:64;
hence thesis by A40;
end;
Lm28:
for n be Nat, f be 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
let n be Nat, f be PartFunc of REAL,REAL;
set n1 = n + 1;
set F1 = (In(1/(n+1),F_Real)*(step_(f,n)));
assume
A1: f is_C^1-Class_on ['0,1'];
A2: len (LWBND_rng_d(f,n)) = n1 by Def9; then
A3: dom (LWBND_rng_d(f,n)) = Seg n1 by FINSEQ_1:def 3;
reconsider r1 = 1/n1 as Real;
reconsider r2 = 1/n1 as Element of F_Real by XREAL_0:def 1,VECTSP_1:def 5;
A4: dom (r1 * (LWBND_rng_d(f,n)))
= dom LWBND_rng_d(f,n) by VALUED_1:def 5;
A5: vol ['0,1'] = 1 -0 by INTEGRA6:5; then
A6: EqDiv(['0,1'],n1) divide_into_equal n1 by MESFUN14:def 1; then
A7: len EqDiv(['0,1'],n1) = n1 by INTEGRA4:def 1;
set Dn = EqDiv(['0,1'],n1);
A8: len (lower_volume(@'(f,['0,1']),EqDiv(['0,1'],n1)))
= len EqDiv(['0,1'],n1) by INTEGRA1:def 7 .= n1 by A6,INTEGRA4:def 1;
for k be Nat st k in dom (lower_volume(@'(f,['0,1']),EqDiv(['0,1'],n1)))
holds
(lower_volume(@'(f,['0,1']),EqDiv(['0,1'],n1))).k
= (r1 * LWBND_rng_d(f,n)).k
proof
let k be Nat;
assume
k in dom (lower_volume(@'(f,['0,1']),EqDiv(['0,1'],n1))); then
A10: k in Seg (n+1) by A8,FINSEQ_1:def 3; then
A11: k in dom EqDiv(['0,1'],n1) by A7,FINSEQ_1:def 3; then
A12: vol divset(EqDiv(['0,1'],n1),k)
= 1/n1 by A5,A6,MESFUN14:15;
(k-'1)/n1 <= k/n1 by NAT_D:35,XREAL_1:72; then
A13: ['(k-'1)/n1, k/n1'] = [.(k-'1)/n1, k/n1.] by INTEGRA5:def 3;
A14: @'(f,['0,1']) = (f`|rohl)|['0,1'] by A1,Def6;
A15: k in dom (LWBND_rng_d(f,n)) by A2,FINSEQ_1:def 3,A10;
(r1 * LWBND_rng_d(f,n)).k
= (1/n1)*(LWBND_rng_d(f,n)).k by A4,A15,VALUED_1:def 5
.= lower_bound rng ((f`|rohl)|['(k-'1)/n1,k/n1']) * (1/n1)
by A15,Def9
.= lower_bound rng ((f`|rohl)|divset (EqDiv(['0,1'],n1),k))
* (vol divset(Dn,k)) by A12,A10,Th1,A13
.= (lower_bound (rng (((f`|rohl)|['0,1'])|(divset (Dn,k)) )))
* (vol (divset (Dn,k))) by A11,INTEGRA1:8,RELAT_1:74
.= (lower_volume(@'(f,['0,1']),EqDiv(['0,1'],n1))).k
by A14,A11,INTEGRA1:def 7;
hence thesis;
end; then
A16: lower_volume(@'(f,['0,1']),EqDiv(['0,1'],n1))
= r1 * (LWBND_rng_d(f,n)) by A8,FINSEQ_1:def 3,A3,A4;
n in NAT by ORDINAL1:def 12; then
A18: lower_sum(@'(f,['0,1']),(D[01]).n)
= Sum(r1*(LWBND_rng_d(f,n))) by A16,Def1
.= Sum(r1*@(LWBND_rng_d(f,n))) by MATRTOP1:def 2
.= r1*Sum(@(LWBND_rng_d(f,n))) by RVSUM_1:87;
reconsider r1 = 1/n1 as Element of F_Real by XREAL_0:def 1,VECTSP_1:def 5;
A19: dom F1 = dom(step_(f,n)) by POLYNOM1:def 1 .= Seg n1 by Def14; then
A20: dom F1 = dom ('G'(f,n)) by Def13;
reconsider H = LWBND_rng_d(f,n) as FinSequence of F_Real;
reconsider FG = (F1 + 'G'(f,n)) as FinSequence of F_Real;
reconsider r3 = 2*n1 as Element of F_Real by XREAL_0:def 1,VECTSP_1:def 5;
A21: dom (F1 + 'G'(f,n)) = Seg n1 by A19,BINOM:def 1;
Seg(len(r3*FG )) = Seg(len(FG * r3)) by BINOM:6
.= dom(FG * r3) by FINSEQ_1:def 3
.= dom FG by POLYNOM1:def 2
.= Seg len FG by FINSEQ_1:def 3; then
A22: len(r3*FG) = len FG by FINSEQ_1:6 .= n1 by A21,FINSEQ_1:def 3;
len H = n1 by Def9; then
A24: dom H = Seg n1 by FINSEQ_1:def 3;
dom (r2 * H) = dom H by POLYNOM1:def 1; then
A25: len (r2*H) = len H by FINSEQ_3:29 .= n1 by Def9;
A26: for k be Nat st k in dom (r2*H) holds
(r2*H).k <= (r3*(F1 + 'G'(f,n))).k
proof
let k be Nat;
assume
A27: k in dom (r2*H); then
A28: k in Seg n1 by A25,FINSEQ_1:def 3; then
A29: k in dom(r3*FG) by A22,FINSEQ_1:def 3;
A30: k in dom FG by A21,A25,A27,FINSEQ_1:def 3; then
A31: r3*(FG.k) = r3*(FG/.k) by PARTFUN1:def 6
.= (r3*FG)/.k by A30,POLYNOM1:def 1
.= (r3*FG).k by A29,PARTFUN1:def 6;
A32: k in dom H by A24,A25,A27,FINSEQ_1:def 3;
A33: (r2*H).k = (r2*H)/.k by A27,PARTFUN1:def 6
.= r2*(H/.k) by A32,POLYNOM1:def 1
.=r2*(H.k) by A32,PARTFUN1:def 6;
((1/n1)^2/2)*(2*n1) = (1/n1)*((1/n1)*n1)
.= (1/n1)*1 by XCMPLX_1:87; then
A35: ((H.k)*(1/(n+1))^2/2)*(2*n1) = (H.k)*(1/n1);
(F1 + 'G'(f,n)).k
= integral(const(f.(k/(n+1))) + (-f),(k-'1)/(n+1),k/(n+1))
by Lm24,A1,A28;
hence thesis by A31,A33,A35,XREAL_1:64,Lm23,A1,A28;
end;
A37: Sum (r3*(F1 + 'G'(f,n))) = r3* Sum(F1 + 'G'(f,n)) by FVSUM_1:73
.= r3*(Sum F1 + Sum('G'(f,n))) by A20,BINOM:7
.= r3*(Sum F1 + integral((-f),0,1)) by Lm22,A1;
reconsider rf = Sum F1 as Element of F_Real;
reconsider r0 = n1 as Element of F_Real by XREAL_0:def 1,VECTSP_1:def 5;
A38: r0*r1 = In(1,REAL) by XCMPLX_1:106;
A39: r0*F1 = (r0*r1)*(step_(f,n)) by Lm25
.= step_(f,n) by Lm26,A38,VECTSP_1:def 5;
A40: n1*(Sum F1 + integral((-f),0,1)) = r0*(Sum F1) + r0*integral(-f,0,1)
.= Sum (step_(f,n)) + r0*integral((-f),0,1) by A39,FVSUM_1:73;
A41: Sum (r2*H) = r2*(Sum H) by FVSUM_1:73
.= lower_sum(@'(f,['0,1']),(D[01]).n) by A18,MATRPROB:36,MATRTOP1:def 2;
lower_sum(@'(f,['0,1']),(D[01]).n) <= r3*(Sum F1 + integral((-f),0,1))
by A37,A41,A26,A22,A25,E_TRANS1:2; then
(lower_sum(@'(f,['0,1']),(D[01]))).n
<= (2*(n+1))*(Sum F1 + integral((-f),0,1)) by INTEGRA2:def 3;
then
(1/2)*(lower_sum(@'(f,['0,1']),(D[01]))).n
<= (1/2)*((2*(n+1))*(Sum F1 + integral((-f),0,1))) by XREAL_1:64;
hence thesis by A40;
end;
definition
let f be PartFunc of REAL,REAL;
func Sum_step(f) -> Real_Sequence means :Def15:
for n be Nat holds it.n = Sum step_(f,n);
correctness
proof
deffunc F(Nat) = Sum step_(f,$1);
(ex seq being Real_Sequence st for n being Nat holds seq.n = F(n)) &
(for seq1, seq2 being Real_Sequence st
(for n being Nat holds seq1.n = F(n)) &
(for n being Nat holds seq2.n = F(n)) holds seq1 = seq2)
from NUMPOLY1:sch 1;
hence thesis;
end;
end;
definition
let f be PartFunc of REAL,REAL;
func n_Integral(f) -> Real_Sequence means :Def16:
for n be Nat holds it.n = (n+1)*integral((-f),0,1);
correctness
proof
deffunc F(Nat) = ($1+1)*integral((-f),0,1);
(ex seq being Real_Sequence st for n being Nat holds seq.n = F(n)) &
(for seq1, seq2 being Real_Sequence st
(for n being Nat holds seq1.n = F(n)) &
(for n being Nat holds seq2.n = F(n)) holds seq1 = seq2)
from NUMPOLY1:sch 1;
hence thesis;
end;
end;
definition
let f be PartFunc of REAL,REAL;
func w_seq(f) -> Real_Sequence equals
Sum_step(f) + n_Integral(f);
coherence
proof
dom Sum_step(f) = NAT & NAT = dom n_Integral(f) by FUNCT_2:def 1;
then
A2: dom (Sum_step(f) + n_Integral(f))
= NAT /\ NAT by VALUED_1:def 1 .= NAT;
rng (Sum_step(f) + n_Integral(f)) c= REAL;
hence thesis by A2,FUNCT_2:2;
end;
end;
Lm30:
for f be PartFunc of REAL,REAL st f is_C^1-Class_on ['0,1'] holds
w_seq(f) is convergent &
for p be Real st 0 < p ex n be Nat st for m be Nat st n<=m holds
|. (w_seq(f)).m- (1/2)*(integral((f`|rohl)||['0,1'])) .| < p
proof
let f be PartFunc of REAL,REAL;
assume
A1: f is_C^1-Class_on ['0,1']; then
A2: @'(f,['0,1']) = (f`|rohl)|['0,1'] by Def6;
(f`|rohl)||['0,1'] is integrable by A1,Lm6,INTEGRA5:def 1; then
A4: lim lower_sum(@'(f,['0,1']),D[01])
= integral(@'(f,['0,1'])) by A1,A2,Lm19;
reconsider r0 = integral((f`|rohl)||['0,1']) as Real;
A5: r0 = integral(@'(f,['0,1'])) by A1,Def6
.= lim upper_sum(@'(f,['0,1']),D[01]) by Lm16,A1;
reconsider r1 = (1/2)*r0 as Real;
set u1 = upper_sum(@'(f,['0,1']),D[01]);
set l1 = lower_sum(@'(f,['0,1']),D[01]);
A6: u1 is convergent by A1,Lm16;
A7: l1 is convergent by A1,Lm19;
for p be Real st 0 < p ex n be Nat st for m be Nat st n<=m holds
|. (w_seq(f)).m- r1 .| < p
proof
let p be Real;
assume
A8: 0 < p; then
consider n be Nat such that
A9: for m be Nat st n<=m holds |. u1.m- lim u1 .| < p
by A6,SEQ_2:def 7;
consider k be Nat such that
A10: for m be Nat st k <= m holds |. l1.m- lim l1 .| < p
by A8,A7,SEQ_2:def 7;
reconsider m0 = max(n,k) as Element of NAT by ORDINAL1:def 12;
dom Sum_step f = NAT & NAT = dom n_Integral(f) by FUNCT_2:def 1;
then
A12: dom (Sum_step(f) + n_Integral(f)) = NAT /\ NAT by VALUED_1:def 1
.= NAT;
for i be Nat st m0 <= i holds |. (w_seq(f)).i- r1 .| < p
proof
let i be Nat;
assume
A14: m0 <= i;
reconsider i0 = i as Element of NAT by ORDINAL1:def 12;
n <= m0 by XXREAL_0:25; then
n <= i by A14,XXREAL_0:2; then
A15: |. u1.i - lim u1 .| < p by A9;
A16: (1/2)*p < p by A8,XREAL_1:157;
A17: -p < (1/2)*(-p) by A8,XREAL_1:156;
A18: Sum (step_(f,i0)) + (i0+1)*integral((-f),0,1) - (1/2)*(lim u1)
<= (1/2)* (u1.i0) - (1/2)*(lim u1) by Lm27,A1,XREAL_1:9;
reconsider x = u1.i0- lim u1 as Real;
x <= p & -p <= x by A15,ABSVALUE:5; then
(1/2)*x <= (1/2)*p by XREAL_1:64; then
A19: Sum (step_(f,i0)) + (i0+1)*integral((-f),0,1) - (1/2)*(lim u1)
<= (1/2)*p by A18,XXREAL_0:2;
k <= m0 by XXREAL_0:25; then
k <= i by A14,XXREAL_0:2; then
A20: |. l1.i- lim l1 .| < p by A10;
A21: (1/2)* (l1.i0) - (1/2)*(lim l1) <=
Sum (step_(f,i0)) + (i0+1)*integral((-f),0,1) - (1/2)*(lim l1)
by Lm28,A1,XREAL_1:9;
reconsider x = l1.i0- lim l1 as Real;
x <= p & -p <= x by A20,ABSVALUE:5; then
(1/2)*(-p) <= (1/2)*x by XREAL_1:64; then
A22: (1/2)*(-p) <=
Sum (step_(f,i0)) + (i0+1)*integral((-f),0,1) - (1/2)*(lim l1)
by A21,XXREAL_0:2;
A23: (w_seq(f)).i0 = (Sum_step(f)).i0 + (n_Integral(f)).i0
by A12,VALUED_1:def 1
.= Sum (step_(f,i0)) + (n_Integral(f)).i0 by Def15
.= Sum (step_(f,i0)) + (i0+1)*integral((-f),0,1) by Def16;
A24: -p < (w_seq(f)).i0 - r1 by A22,A17,XXREAL_0:2,A23,A4,A2;
per cases by ABSVALUE:1;
suppose |. (w_seq(f)).i0 - r1 .| = (w_seq(f)).i0 - r1;
hence thesis by A5,A19,A16,XXREAL_0:2,A23;
end;
suppose
A25: |. (w_seq(f)).i0 - r1 .| = -((w_seq(f)).i0 - r1);
reconsider a = (w_seq(f)).i0 - r1, b = -1 as Real;
b*a < b*(-p) by A24,XREAL_1:69;
hence thesis by A25;
end;
end;
hence thesis;
end;
hence thesis;
end;
:: Main Lemma
theorem Th11:
for f be 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
let f be PartFunc of REAL,REAL;
assume f is_C^1-Class_on ['0,1']; then
w_seq(f) is convergent &
for p be Real st 0 < p ex n be Nat st for m be Nat st n<=m holds
|. (w_seq(f)).m- (1/2)*(integral((f`|rohl)||['0,1'])) .| < p
by Lm30;
hence thesis by SEQ_2:def 7;
end;
begin :: Section 2: Apply the Lemma to log(1+x)
definition
let c be Real;
func x_+_c -> PartFunc of REAL,REAL equals
AffineMap(1,c);
coherence;
end;
Lm31:
for c be Real holds
x_+_(c) = id REAL + const(c)
proof
let c be Real;
A1: dom(id REAL + const(c)) = REAL by FUNCT_2:def 1;
for x being object st x in dom x_+_(c) holds
(x_+_(c)).x = (id REAL + const(c)).x
proof
let x be object;
assume
A2: x in dom x_+_(c); then
reconsider x1 = x as Real;
A3: (x_+_(c)).x1 = 1*x1 +c by FCONT_1:def 4;
A4: (id REAL).x1 = x1 by A2, FUNCT_1:18;
(id REAL + const(c)).x1
= (id REAL).x1 + (const(c)).x1 by A2,A1,VALUED_1:def 1
.= x1 + (0*x1 + c) by A4,FCONT_1:def 4
.= x1 + c;
hence thesis by A3;
end;
hence thesis by FUNCT_2:def 1,A1;
end;
Lm32:
for c be Real holds x_+_(c) is differentiable
proof
let c be Real;
dom const(c) = dom id REAL by FUNCT_2:def 1; then
const(c) is_differentiable_on REAL & id REAL is_differentiable_on REAL
by FDIFF_1:def 8; then
(id REAL) + const(c) is_differentiable_on [#]REAL by FDIFF_2:17;
hence thesis by Lm31;
end;
Lm33:
for c be Real holds
for Z be open Subset of REAL holds x_+_(c) is_differentiable_on Z
proof
let c be Real;
let Z be open Subset of REAL;
A1: dom x_+_(c) = REAL by FUNCT_2:def 1;
reconsider f = x_+_(c) as differentiable PartFunc of REAL,REAL by Lm32;
f is_differentiable_on Z by A1,FDIFF_1:28;
hence thesis;
end;
Lm34:
for c be Real holds (x_+_(c))`|REAL = REAL --> 1
proof
let c be Real;
set f = x_+_(c);
A1: f is_differentiable_on REAL by FUZIMPL2:2; then
A2: dom (f`|REAL) = dom (REAL --> 1) by FDIFF_1:def 7;
for x being Real st x in REAL holds (f`|REAL).x = (REAL --> 1).x
proof
let x be Real;
assume
A3: x in REAL; then
(f`|REAL).x
= diff(AffineMap(1,c),x) by A1,FDIFF_1:def 7 .= 1 by FUZIMPL2:2;
hence thesis by FUNCOP_1:7,A3;
end;
hence thesis by A2;
end;
Lm35:
for c be Real holds (x_+_(c))`|rohl = rohl --> 1
proof
let c be Real;
set f = x_+_(c);
reconsider X = REAL as Subset of REAL by ZFMISC_1:def 1;
reconsider Z = rohl as open Subset of REAL;
f`|Z = (f`|X)|Z by FUZIMPL2:2,PDLAX:12 .= (REAL --> 1)|rohl by Lm34
.= (REAL /\ rohl) --> 1 by FUNCOP_1:12;
hence thesis by XBOOLE_1:28;
end;
Lm36:
for x1 be Real st x1 in right_open_halfline(-1) holds
x1 in support x_+_(1) & x_+_(1) <> 0 & (x_+_(1)).x1 <> 0
proof
let x1 be Real;
assume
A1: x1 in right_open_halfline(-1);
A2: right_open_halfline(-1) = ]. -1,+infty .[ by LIMFUNC1:def 3;
(x_+_(1)).x1 = 1*x1 +1 by FCONT_1:def 4 .= x1 +1; then
(x_+_(1)).x1 <> 0 by A1,A2,XXREAL_1:4;
hence thesis by PRE_POLY:def 7;
end;
Lm37:
for x0 be Real holds
x0 in right_open_halfline(-1) implies x_+_(1)^ is_continuous_in x0
proof
let x0 be Real;
assume x0 in right_open_halfline(-1); then
A2: (x_+_(1)).x0 <> 0 by Lm36;
dom x_+_(1) = REAL by FUNCT_2:def 1; then
x_+_(1) is_continuous_in x0 by FCONT_1:def 2,XREAL_0:def 1;
hence thesis by A2,FCONT_1:10;
end;
Lm38:
for f being Function holds f"{0} = ZeroPointSet f
proof
let f be Function;
A1: for o1 being object holds o1 in f"{0} implies o1 in ZeroPointSet f
proof
let o1 be object;
assume o1 in f"{0}; then
o1 in dom f & f.o1 in {0} by FUNCT_1:def 7; then
o1 in dom f & f.o1 = 0 by TARSKI:def 1;
hence thesis by DIOPHAN2:7;
end;
for o1 being object holds o1 in ZeroPointSet f implies o1 in f"{0}
proof
let o1 be object;
assume o1 in ZeroPointSet f; then
o1 in dom f & f.o1 = 0 by DIOPHAN2:7; then
o1 in dom f & f.o1 in {0} by TARSKI:def 1;
hence thesis by FUNCT_1:def 7;
end;
hence thesis by A1,TARSKI_0:2;
end;
Lm39:
for f being Function holds support f = dom f \ ZeroPointSet f
proof
let f be Function;
dom f \ ZeroPointSet f
= dom f \(dom f \ support f) by DIOPHAN2:def 1
.= dom f /\ support f by XBOOLE_1:48
.= support f by PRE_POLY:37,XBOOLE_1:28;
hence thesis;
end;
Lm40:
for f being real-valued Function holds
dom (f^) = support f
proof
let f be real-valued Function;
dom (f^) = (dom f) \ (f " {0}) by RFUNCT_1:def 2
.= (dom f) \ ZeroPointSet f by Lm38 .= support f by Lm39;
hence thesis;
end;
Lm41:
for x be Real st x in right_open_halfline(-1) holds
x+1 in right_open_halfline(0)
proof
let x be Real;
assume
A1: x in right_open_halfline(-1);
right_open_halfline(-1) = ]. -1,+infty .[ by LIMFUNC1:def 3; then
-1 < x & x < +infty by A1,XXREAL_1:4; then
A3: -1+1 < x + 1 by XREAL_1:8;
x+1 < +infty by XXREAL_0:9,XREAL_0:def 1; then
x+1 in ]. 0,+infty .[ by A3,XXREAL_1:4;
hence thesis by LIMFUNC1:def 3;
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
A1: right_open_halfline(-1) c= support x_+_(1) by Lm36;
A2: dom (x_+_(1)^) = support x_+_(1) by Lm40;
A3: dom ((x_+_(1)^)|right_open_halfline(-1))
= dom (x_+_(1)^) /\ right_open_halfline(-1) by RELAT_1:61
.= right_open_halfline(-1) by A1,A2,XBOOLE_1:28; then
for x0 be Real st x0 in dom ((x_+_(1)^)|right_open_halfline(-1))
holds (x_+_(1)^)|right_open_halfline(-1) is_continuous_in x0
by Lm37,FCONT_1:1;
hence thesis by A3,A1,Lm40,FCONT_1:def 2;
end;
Lm43:
for x be Real st x in right_open_halfline(-1) holds
((x_+_(1))|rohl).x = 1+x &
((x_+_(1))|rohl).x > 0
proof
let x be Real;
assume
A1: x in right_open_halfline(-1); then
x in ].-1,+infty.[ by LIMFUNC1:def 3; then
A2: -1 < x & x < +infty by XXREAL_1:4;
A3: ((x_+_(1))|rohl).x = (x_+_(1)).x by A1,FUNCT_1:49
.= 1*x +1 by FCONT_1:def 4 .= x +1;
-1+1 < x + 1 by A2,XREAL_1:8;
hence thesis by A3;
end;
Lm44:
for x be Real st x in rohl holds
((x_+_(1)^)|rohl).x = 1/(1+x)
proof
let x be Real;
assume
A1: x in rohl; then
((x_+_(1)^)|rohl).x = (x_+_(1)^).x by FUNCT_1:49
.= ((x_+_(1)).x)" by Lm42,A1,RFUNCT_1:def 2
.= (1*x + 1)" by FCONT_1:def 4
.= 1/(x +1);
hence thesis;
end;
Lm45:
for x0 be Real st x0 in right_open_halfline(-1) holds
(x_+_(1))|rohl is_differentiable_in x0
proof
let x0 be Real;
assume
A1: x0 in right_open_halfline(-1);
(x_+_(1))|rohl is_differentiable_on right_open_halfline(-1)
by Lm33,INTEGRA7:5;
hence thesis by A1;
end;
Lm46:
rng ((x_+_(1))|rohl) = right_open_halfline(0)
proof
A1: dom (x_+_(1)) = REAL by FUNCT_2:def 1;
A2: for o be object st o in rng ((x_+_(1))|rohl)
holds o in right_open_halfline(0)
proof
let o be object;
assume o in rng ((x_+_(1))|rohl); then
consider o1 be object such that
A4: o1 in dom((x_+_(1))|rohl) &
o = ((x_+_(1))|rohl).o1 by FUNCT_1:def 3;
reconsider x1 = o1 as Real by A4;
o = (x_+_(1)).x1 by A4,A1,FUNCT_1:49
.= 1*x1 +1 by FCONT_1:def 4 .= x1 +1;
hence thesis by A4,A1,Lm41;
end;
for o be object st o in right_open_halfline(0)
holds o in rng ((x_+_(1))|rohl)
proof
let o be object;
assume
A6: o in right_open_halfline(0); then
reconsider x1 = o as Real;
reconsider x0 = x1 - 1 as Real;
x1 in ].0,+infty.[ by A6, LIMFUNC1:def 3; then
0 < x1 & x1 < +infty by XXREAL_1:4; then
0 -1 < x1 - 1 by XREAL_1:9; then
-1 < x0 & x0 < +infty by XXREAL_0:9, XREAL_0:def 1; then
x0 in ].-1,+infty.[ by XXREAL_1:4; then
A10: x0 in dom ((x_+_(1))|rohl) by A1,LIMFUNC1:def 3; then
((x_+_(1))|rohl).x0 = (x_+_(1)).x0 by A1,FUNCT_1:49
.= 1*x0 +1 by FCONT_1:def 4 .= x1;
hence thesis by A10,FUNCT_1:3;
end;
hence thesis by A2,TARSKI_0:2;
end;
Lm47:
dom ((x_+_(1))|rohl) = right_open_halfline(-1) &
dom (ln*((x_+_(1))|rohl)) = right_open_halfline(-1)
proof
dom (x_+_(1)) = REAL by FUNCT_2:def 1; then
A2: dom ((x_+_(1))|rohl) = right_open_halfline(-1);
rng ((x_+_(1))|rohl) c= dom ln by TAYLOR_1:def 2,def 3,Lm46;
hence thesis by A2,RELAT_1:27;
end;
Lm48:
for n be Nat holds n in right_open_halfline(-1)
proof
let n be Nat;
-1 < n & n < +infty by XXREAL_0:9,XREAL_0:def 1; then
n in ].-1,+infty.[ by XXREAL_1:4;
hence thesis by LIMFUNC1:def 3;
end;
Lm49:
for r be Real st r >= 0 holds r in right_open_halfline(-1)
proof
let r be Real;
assume r >= 0; then
-1 < r & r < +infty by XXREAL_0:9,XREAL_0:def 1; then
r in ].-1,+infty.[ by XXREAL_1:4;
hence thesis by LIMFUNC1:def 3;
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
set f1 = (x_+_(1));
A1: dom f1 = REAL by FUNCT_2:def 1; then
A2: 1 in dom (f1|rohl) & 0 in dom (f1|rohl) by Lm48;
A3: ((x_+_(1))|rohl).1 = (x_+_(1)).1 by Lm48,FUNCT_1:49
.= 1*1 + 1 by FCONT_1:def 4 .= 2;
((x_+_(1))|rohl).0 = (x_+_(1)).0 by Lm48,FUNCT_1:49
.= 1*0 + 1 by FCONT_1:def 4 .= 1;
hence thesis by A1,A3,A2,FUNCT_1:13,MOEBIUS3:12;
end;
theorem Th13:
ln*((x_+_(1))|rohl) is_differentiable_on right_open_halfline(-1)
proof
set f0 = (x_+_(1))|rohl;
set Z = (right_open_halfline(-1));
for x0 be Real st x0 in Z holds
ln*((x_+_(1))|rohl) is_differentiable_in x0
proof
let x0 be Real;
assume
A1: x0 in Z; then
A2: f0.x0 > 0 by Lm43;
f0 is_differentiable_in x0 by A1,Lm45;
hence thesis by A2,TAYLOR_1:20;
end;
hence thesis by Lm47;
end;
theorem Th14:
for Z be open Subset of REAL st Z c= dom (ln*((x_+_(1))|rohl)) holds
ln*((x_+_(1))|rohl) is_differentiable_on Z &
for x be Real st x in Z holds ((ln*((x_+_(1))|rohl))`|Z).x = 1/(1+x)
proof
let Z be open Subset of REAL;
set f = (x_+_(1))|rohl;
assume
A1: Z c= dom (ln*((x_+_(1))|rohl));
for x be Real st x in Z holds f.x = 1+x & f.x > 0
proof
let x be Real;
assume
A2: x in Z; then
x in rohl by Lm47,A1; then
x in ].-1,+infty.[ by LIMFUNC1:def 3; then
-1 < x & x < +infty by XXREAL_1:4; then
A3: -1+1 < x + 1 by XREAL_1:8;
f.x = (x_+_(1)).x by A2,Lm47,A1,FUNCT_1:49
.= 1*x + 1 by FCONT_1:def 4 .= x + 1;
hence thesis by A3;
end;
hence thesis by A1,FDIFF_4:1;
end;
theorem Th15:
(ln*((x_+_(1))|rohl))`|rohl = (x_+_(1)^)|rohl
proof
set Z = rohl;
A1: ln*((x_+_(1))|Z) is_differentiable_on Z &
for x be Real st x in Z holds ((ln*((x_+_(1))|rohl))`|Z).x = 1/(1+x)
by Lm47,Th14;
for o be object st o in dom ((ln*((x_+_(1))|Z))`|Z) holds
((ln*((x_+_(1))|Z))`|Z).o = ((x_+_(1)^)|Z).o
proof
let o be object;
assume
A2: o in dom ((ln*((x_+_(1))|rohl))`|Z); then
A3: o in Z by A1,FDIFF_1:def 7;
reconsider x = o as Real by A2;
((ln*((x_+_(1))|Z))`|Z).x = 1/(1+x) by Lm47,Th14,A3
.= ((x_+_(1)^)|rohl).x by Lm44,A3;
hence thesis;
end;
hence thesis by Lm42,A1,FDIFF_1:def 7;
end;
Lm51:
ln*((x_+_(1))|rohl) is_C^1-Class_on ['0,1']
proof
A1: ['0,1'] = [. 0,1 .] by INTEGRA5:def 3;
-1 < 0 & 1 < +infty by XXREAL_0:9,XREAL_0:def 1; then
[. 0,1 .] c= ]. -1,+infty .[ by XXREAL_1:47;
hence thesis by Th13,Lm42,Th15,A1,LIMFUNC1:def 3;
end;
reserve x,x0,x1,x2 for Real;
theorem Th16:
((x_+_(1))(#)(ln*((x_+_(1))|rohl)) + (-1(#)(x_+_(0))))`|rohl
= ln*((x_+_(1))|rohl)
proof
set f0 = (x_+_(0));
set f1 = (x_+_(1));
set f2 = ln*((x_+_(1))|rohl);
A1: f0 is_differentiable_on rohl by Lm33;
A2: f1 is_differentiable_on rohl by Lm33;
A3: f2 is_differentiable_on rohl by Th14,Lm47; then
A4: f1 (#) f2 is_differentiable_on rohl &
(f1(#)f2)`|rohl = (f1`|rohl)(#)f2 + f1(#)(f2`|rohl) by A2,FDIFF_2:20;
A5: dom (f1(#)((f1^)|rohl)) = dom f1 /\ dom ((f1^)|rohl) by VALUED_1:def 4
.= REAL /\ rohl by Lm42,FUNCT_2:def 1 .= rohl by XBOOLE_1:28;
A6: f1(#)((f1^)|rohl) = rohl --> 1
proof
for x be object st x in dom (f1(#)((f1^)|rohl)) holds
(f1(#)((f1^)|rohl)).x = (rohl --> 1).x
proof
let x be object;
assume
A7: x in dom (f1(#)((f1^)|rohl)); then
A8: x in ].-1,+infty.[ by A5,LIMFUNC1:def 3;
reconsider x1 = x as Real by A7;
f1.x1 = 1*x1 +1 by FCONT_1:def 4 .= x1 + 1; then
A9: f1.x1 <> 0 by A8,XXREAL_1:4; then
x in support f1 by PRE_POLY:def 7; then
A10: x in dom (f1^) by Lm40;
(f1(#)((f1^)|rohl)).x = f1.x1 * ((f1^)|rohl).x1 by A7,VALUED_1:def 4
.= f1.x1 * (f1^).x1 by A7,A5,FUNCT_1:49
.= f1.x1 * (1/((f1).x1)) by A10,RFUNCT_1:def 2
.= 1 by A9,XCMPLX_1:106
.= (rohl --> 1).x by A7,A5,FUNCOP_1:7;
hence thesis;
end;
hence thesis by A5;
end;
A11: (f1(#)f2)`|rohl = (f1`|rohl)(#)f2 + f1(#)(f2`|rohl) by A2,A3,FDIFF_2:20
.= (rohl --> 1)(#)f2 + (rohl --> 1) by A6,Th15,Lm35;
A12: (-1(#)f0)`|rohl = -1(#)(f0`|rohl) by A1,FDIFF_2:19
.= -1(#)(rohl -->1) by Lm35;
A13: (-1(#)f0) is_differentiable_on rohl &
((-1(#)f0))`|rohl = -1(#)(f0`|rohl) by A1,FDIFF_2:19;
1 is Element of REAL by NUMBERS:19; then
reconsider h = (rohl --> 1) as Function of rohl,REAL by FUNCOP_1:46;
A14: dom ((rohl --> 1) (#) f2) = dom (rohl --> 1) /\ dom f2 by VALUED_1:def 4
.= rohl by Lm47;
A15: dom ((rohl --> 1)(#)f2 + (rohl --> 1))
= dom ((rohl --> 1)(#)f2) /\ dom (rohl --> 1) by VALUED_1:def 1
.= rohl by A14; then
A16: dom ((rohl --> 1)(#)f2 + (rohl --> 1) + (-1)(#)(rohl -->1))
= rohl /\ dom((-1)(#)(rohl -->1)) by VALUED_1:def 1
.= rohl /\ dom (rohl -->1) by VALUED_1:def 5
.= rohl;
(rohl --> 1)(#)f2 + (rohl --> 1) + (-1)(#)(rohl -->1) = f2
proof
for o be object st o in dom f2 holds
((rohl --> 1)(#)f2 + (rohl --> 1) + (-1)(#)(rohl -->1)).o = f2.o
proof
let o be object;
assume
A18: o in dom f2; then
reconsider x1 = o as Real;
((rohl --> 1)(#)f2).x1
= ((rohl --> 1).x1) * (f2.x1) by A18,Lm47,A14,VALUED_1:def 4
.= 1*(f2.x1) by A18,Lm47,FUNCOP_1:7 .= f2.x1; then
A20: ((rohl --> 1)(#)f2 + (rohl --> 1)).x1
= f2.x1 + (rohl --> 1).x1 by A18,Lm47,A15,VALUED_1:def 1
.= f2.x1 + 1 by A18,Lm47,FUNCOP_1:7;
A21: dom ((-1)(#)(rohl -->1)) = rohl by VALUED_1:def 5;
((rohl --> 1)(#)f2 + (rohl --> 1) + (-1)(#)(rohl -->1)).x1
= (f2.x1 + 1) + ((-1)(#)(rohl -->1)).x1
by A20,A16,A18,Lm47,VALUED_1:def 1
.= (f2.x1 + 1) + (-1)*((rohl -->1).x1)
by A21,A18,Lm47,VALUED_1:def 5
.= (f2.x1 + 1) + (-1)*1 by A18,Lm47,FUNCOP_1:7
.= f2.x1;
hence thesis;
end;
hence thesis by A16, Lm47;
end;
hence thesis by A12,A11,A4,A13,FDIFF_2:17;
end;
theorem Lm52:
integral(ln*((x_+_(1))|rohl),0,1) = log(number_e,4/number_e)
proof
set f0 = (x_+_(0));
set f1 = (x_+_(1));
set f2 = ln*((x_+_(1))|rohl);
set F = ((f1(#)f2) + (-1(#)f0));
A1: f0 is_differentiable_on rohl by Lm33;
A2: f1 is_differentiable_on rohl by Lm33;
f2 is_differentiable_on rohl by Lm47,Th14; then
A4: f1 (#) f2 is_differentiable_on rohl &
(f1(#)f2)`|rohl = (f1`|rohl)(#)f2 + f1(#)(f2`|rohl) by A2,FDIFF_2:20;
A5: (-1(#)f0) is_differentiable_on rohl &
((-1(#)f0))`|rohl = -1(#)(f0`|rohl) by A1,FDIFF_2:19;
dom f1 = REAL by FUNCT_2:def 1; then
A6: dom((f1(#)f2)) = REAL /\ rohl by Lm47,VALUED_1:def 4
.= rohl by XBOOLE_1:28;
A7: dom ((-1(#)f0)) = REAL by FUNCT_2:def 1; then
A8: dom F = rohl /\ REAL by A6,VALUED_1:def 1 .= rohl by XBOOLE_1:28;
A9: (f1(#)f2) + (-1(#)f0) is_differentiable_on rohl by A4,A5,FDIFF_2:17;
A10: ['0,1'] = [. 0,1 .] by INTEGRA5:def 3;
-1 < 0 & 1 < +infty by XXREAL_0:9,XREAL_0:def 1; then
[. 0,1 .] c= ]. -1,+infty .[ by XXREAL_1:47; then
A11: [. 0,1 .] c= rohl by LIMFUNC1:def 3;
set a = 0, b = 1;
f2|rohl is continuous by Lm47,Th14,FDIFF_1:25; then
A13: f2|[' a,b '] is continuous & f2 is_integrable_on [' a,b '] &
f2|[' a,b '] is bounded by A11,Lm47,INTEGRA7:19;
F`|rohl = f2|rohl by Lm47,Th16; then
F in IntegralFuncs(f2,rohl) by A9,INTEGRA7:def 1; then
A15: F.b = integral(f2,a,b) + F.a by A11,A10,A13,INTEGRA7:18,def 2;
A16: 1 in [. 0,1 .] & 0 in [. 0,1 .] by XXREAL_1:1;
A17: F.b = (f1(#)f2).1 + (-1(#)f0).1 by A8,Lm48,VALUED_1:def 1
.= f1.1 * f2.1 + (-1(#)f0).1 by A6,Lm48,VALUED_1:def 4
.= f1.1 * f2.1 + (-1)*(f0.1) by A7,A16,VALUED_1:def 5
.= (1*1 +1)*(ln.2) -f0.1 by Lm50,FCONT_1:def 4
.= 2*(ln.2) -(1*1+0) by FCONT_1:def 4 .= 2*(ln.2) -1;
A18: F.a = (f1(#)f2).0 + (-1(#)f0).0 by A8,Lm48,VALUED_1:def 1
.= f1.0 * f2.0 + (-1(#)f0).0 by A6,Lm48,VALUED_1:def 4
.= f1.0 * f2.0 + (-1)*(f0.0) by A7,A16,VALUED_1:def 5
.= 0 -f0.0 by Lm50
.= 0 -(1*0+0) by FCONT_1:def 4
.= 0;
reconsider e0 = number_e as Real;
A19: e0 > 2 & e0 <> 1 by TAYLOR_1:11;
0 < e0 < +infty by TAYLOR_1:11,XXREAL_0:9,XREAL_0:def 1; then
e0 in ].0,+infty.[ by XXREAL_1:4; then
A20: e0 in right_open_halfline(0) by LIMFUNC1:def 3; then
A22: ln.e0 = log(e0,e0) by TAYLOR_1:def 2,def 3 .= 1 by A19,POWER:52;
0 < 2 < +infty by XXREAL_0:9,XREAL_0:def 1; then
2 in ].0,+infty.[ by XXREAL_1:4; then
2 in right_open_halfline(0) by LIMFUNC1:def 3; then
2*(ln.2) = 2*log(e0,2) by TAYLOR_1:def 2,def 3
.= log(e0,4) by POWER:60,55,A19; then
integral(f2,a,b)
= log(e0,4) - log(e0,e0) by A20,TAYLOR_1:def 2,def 3,A22,A17,A18,A15
.= log(e0,4/e0) by A19,POWER:54;
hence thesis;
end;
theorem Th17:
integral((ln*((x_+_(1))|rohl))`|rohl,['0,1']) = ln.2
proof
set f = ln*((x_+_(1))|rohl);
['0,1'] = [. 0,1 .] by INTEGRA5:def 3; then
A2: f.(upper_bound ['0,1']) = ln.2 by Lm50,JORDAN5A:19;
A3: f.(lower_bound ['0,1']) = 0 by Lm50,FUZZY_6:7;
A4: (f`|rohl)|['0,1'] is continuous &
f`|rohl is_integrable_on ['0,1'] &
(f`|rohl)|['0,1'] is bounded by Lm51,Lm6;
integral(f`|rohl,['0,1'])
= ln.2 - 0 by A2,A3,Lm51,A4,INTEGRA5:13;
hence thesis;
end;
theorem Th18:
lim w_seq(ln*((x_+_(1))|rohl)) = (1/2)*(ln.2)
proof
set f = ln*((x_+_(1))|rohl);
lim w_seq(f) = (1/2)*(integral((f`|rohl)||['0,1'])) by Lm51,Th11
.= (1/2)*(ln.2) by INTEGRA5:def 2,Th17;
hence thesis;
end;
definition
let m be non zero Nat,f be PartFunc of REAL,REAL;
func Step_(f,m) -> Real_Sequence means :Def19:
for i be Nat holds it.i = f.(i/m);
correctness
proof
deffunc F(Nat) = f.($1/m);
(ex seq being Real_Sequence st for n being Nat holds seq.n = F(n)) &
(for seq1, seq2 being Real_Sequence st
(for n being Nat holds seq1.n = F(n)) &
(for n being Nat holds seq2.n = F(n)) holds seq1 = seq2)
from NUMPOLY1:sch 1;
hence thesis;
end;
end;
theorem Th19:
for m be non zero Nat, f be PartFunc of REAL,REAL holds
(XFS2FS((Step_(f,m))|Segm(m+1))) = <*f.0*>^(step_(f,m-'1))
proof
let m be non zero Nat,f be PartFunc of REAL,REAL;
reconsider m1 = m + 1 as Nat;
reconsider mm1 = m -'1 as Nat;
A1: mm1 + 1 = m by NAT_1:14,XREAL_1:235;
reconsider p = (Step_(f,m))|Segm m1 as XFinSequence of REAL;
A2: dom (step_(f,mm1)) = Seg (mm1 +1) by Def14;
dom <*f.0*> = Seg 1 by FINSEQ_1:def 8; then
A3: len <*f.0*> = 1 by FINSEQ_1:def 3;
A4: dom Shift(p,1) = Seg m1 by DBLSEQ_2:45;
A5: len (<*f.0*>^(step_(f,mm1)))
= len <*f.0*> + len (step_(f,mm1)) by FINSEQ_1:22
.= 1 + mm1+1 by A2,FINSEQ_1:def 3,A3.= m1 by NAT_1:14,XREAL_1:235; then
A6: dom (<*f.0*>^(step_(f,mm1))) = Seg m1 by FINSEQ_1:def 3;
A7: (Shift(Step_(f,m)|(Segm m1),1)) = XFS2FS p by RVSUM_4:def 12;
for x be Nat st x in dom Shift(Step_(f,m)|(Segm m1),1) holds
(Shift(Step_(f,m)|(Segm m1),1)).x = (<*f.0*>^(step_(f,mm1))).x
proof
let x be Nat;
assume
A8: x in dom (Shift(Step_(f,m)|(Segm m1),1)); then
A9: 1 <= x <= m+1 by A4,FINSEQ_1:1;
then reconsider x1 = x - 1 as Nat;
A11: m < m+1 by XREAL_1:29;
A12: x - 1 <= (m+1) -1 by A9,XREAL_1:9; then
A13: x1 < m+1 by A11,XXREAL_0:2;
A14: (Shift(Step_(f,m)|(Segm m1),1)).x
= (Shift(Step_(f,m)|(Segm m1),1)).(x1+1)
.= (Step_(f,m)|(Segm m1)).x1 by A13,NAT_1:44,VALUED_1:def 12
.= (Step_(f,m)).x1 by A13,NAT_1:44,FUNCT_1:49
.= f.(x1/m) by Def19;
(<*f.0*>^(step_(f,mm1))).x = f.(x1/m)
proof
per cases;
suppose
x = 1;
hence thesis;
end;
suppose
A16: x <> 1;
1 <= x <= m+1 by A8,A4,FINSEQ_1:1; then
1 < x by A16,XXREAL_0:1; then
1-1 < x1 by XREAL_1:8; then
1 <= x1 <= m by A12,NAT_1:14; then
x1 in Seg m; then
A19: x1 in dom step_(f,mm1) by Def14,A1;
len <*f.0*> < x & x <= len (<*f.0*>^(step_(f,mm1)))
by A16,XXREAL_0:1,A9,A3,A5; then
(<*f.0*>^(step_(f,mm1))).x
= (step_(f,mm1)).(x -1) by A3,FINSEQ_1:24
.= f.(x1/(mm1+1)) by A19,Def14;
hence thesis by NAT_1:14,XREAL_1:235;
end;
end;
hence thesis by A14;
end;
hence thesis by A7,A6,DBLSEQ_2:45;
end;
theorem Th20:
for m be non zero Nat,
f be 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
let m be non zero Nat, f be PartFunc of REAL,REAL;
assume f is_C^1-Class_on ['0,1']; then
A2: f is_differentiable_on rohl & f`|rohl is continuous &
['0,1'] c= rohl & rohl c= dom f & ['0,1'] c= dom f by XBOOLE_1:1;
['0,1'] = [. 0,1 .] by INTEGRA5:def 3; then
A4: 0 in dom f by XXREAL_1:1,A2;
reconsider f0 = f.0 as Element of F_Real by A4,PARTFUN1:4,VECTSP_1:def 5;
XFS2FS((Step_(f,m))|Segm(m+1)) = <*f0*>^(step_(f,m-'1)) by Th19; then
Sum (XFS2FS((Step_(f,m))|Segm(m+1)))
= Sum (<*f0*>^(step_(f,m-'1))) by NIVEN:6
.= f0 + Sum (step_(f,m-'1)) by FVSUM_1:72
.= f.0 + Sum (step_(f,m-'1));
hence thesis;
end;
theorem Th21:
for m be non zero Nat holds
Sum (XFS2FS((Step_(ln*((x_+_(1))|rohl),m))|Segm(m+1)))
= Sum (step_(ln*((x_+_(1))|rohl),m-'1))
proof
let m be non zero Nat;
reconsider f = ln*((x_+_(1))|rohl) as PartFunc of REAL,REAL;
Sum (XFS2FS((Step_(f,m))|Segm(m+1)))
= 0 + Sum (step_(f,m-'1)) by Lm50,Lm51,Th20
.= Sum (step_(f,m-'1));
hence thesis;
end;
Lm53:
for m be non zero Nat, k be Nat holds
(Partial_Sums (Step_(ln*((x_+_(1))|rohl),m))).k = ln.((k+m)!/((m^k)*(m!)))
proof
let m be non zero Nat, k be Nat;
defpred P[Nat] means
(Partial_Sums (Step_(ln*((x_+_(1))|rohl),m))).$1
= ln.(($1+m)!/((m^$1)*(m!)));
A1: for k be Nat holds P[k] implies P[k+1]
proof
let k be Nat;
assume
A2: P[k];
((x_+_(1))|rohl).((k+1)/m) = (x_+_(1)).((k+1)/m) by Lm49,FUNCT_1:49
.= 1*((k+1)/m) + 1 by FCONT_1:def 4
.= ((k+1)/m) + m/m by XCMPLX_1:60
.= (k+m+1)/m; then
A4: (ln*((x_+_(1))|rohl)).((k+1)/m)
= ln.((k+m+1)/m) by Lm49,Lm50,FUNCT_1:13;
set n1 = m;
set kn1 = k+m;
A5: (kn1!/((n1^k)*(n1!))) * ((kn1+1)/n1)
= ( kn1! * (kn1+1)) / (((n1!) * (n1^k)) * n1) by XCMPLX_1:76
.= ((kn1+1)!)/((n1!) * ((n1^k) *(n1^1))) by NEWTON:15
.= (k+m+1)!/((n1!)* (n1^(k+1))) by NEWTON:8;
ln.((k+n1)!/((n1^k)*(n1!))) + (Step_(ln*((x_+_(1))|rohl),n1)).(k+1)
= ln.(kn1!/((n1^k)*(n1!))) + ln.((kn1+1)/n1) by A4,Def19
.= ln.(((k+1)+n1)!/( ((n1)^(k+1))*((n1)!))) by A5,MOEBIUS3:19;
hence thesis by A2,SERIES_1:def 1;
end;
A6: P[0]
proof
A7: (Partial_Sums (Step_(ln*((x_+_(1))|rohl),m))).0
= (Step_(ln*((x_+_(1))|rohl),m)).0 by SERIES_1:def 1
.= (ln*((x_+_(1))|rohl)).(0/m) by Def19
.= ln.1 by Lm50;
ln.((0+m)!/((m^0)*(m!))) = ln.(m!/(1*(m!))) by NEWTON:4
.= ln.1 by XCMPLX_1:60;
hence thesis by A7;
end;
for n be Nat holds P[n] from NAT_1:sch 2(A6,A1);
hence thesis;
end;
Lm54:
for m be non zero Nat holds
Sum (step_(ln*((x_+_(1))|rohl),m-'1)) = ln.((m+m)!/((m^m)*(m!)))
proof
set f = ln*((x_+_(1))|rohl);
let m be non zero Nat;
(Partial_Sums Step_(f,m)).m
= Sum(Shift(Step_(f,m)|Segm(m+1),1)) by DBLSEQ_2:49
.= Sum (XFS2FS ((Step_(ln*((x_+_(1))|rohl),m))|Segm (m+1)))
by RVSUM_4:def 12
.= Sum (step_(f,m-'1)) by Th21;
hence thesis by Lm53;
end;
theorem
for m be non zero Nat holds
(w_seq(ln*((x_+_(1))|rohl))).(m-'1)
= ln.(((2*m)!/(m!))*((number_e/(4*m))^m))
proof
let m be non zero Nat;
set f = ln*((x_+_(1))|rohl);
reconsider k0 = m-'1 as Element of NAT;
A1: k0 + 1 = m by NAT_1:14,XREAL_1:235;
dom (Sum_step f) = NAT & NAT = dom n_Integral(f) by FUNCT_2:def 1; then
A3: dom (Sum_step(f) + n_Integral(f))
= NAT /\ NAT by VALUED_1:def 1
.= NAT;
set a = 0, b = 1, X = rohl;
a <= b & [. a,b .] c= X & X c= dom f & f|X is continuous
by Lm51,FDIFF_1:25,INTEGRA5:def 3; then
f|[' a,b '] is continuous & f is_integrable_on [' a,b '] &
f|[' a,b '] is bounded by INTEGRA7:19; then
A5: integral((-f),0,1)
= (-1) * integral(f,0,1) by Lm51,XBOOLE_1:1,INTEGRA6:10;
set e0 = number_e;
A6: e0 <> 1 by TAYLOR_1:11;
A7: 1/((4/e0)^m) = 1/((4^m)/(e0^m)) by TAYLOR_1:11,POWER:31
.= 1*((e0^m)/(4^m)) by XCMPLX_1:79;
A8: m*integral((-f),0,1) = -(m*(log(e0,4/e0))) by Lm52,A5
.= -log(e0,(4/e0)^m) by TAYLOR_1:11,A6,POWER:55
.= ln.1 - ln.((4/e0)^m) by DIFF_4:3,TAYLOR_1:11,MOEBIUS3:12
.= ln.((e0^m)/(4^m)) by A7,DIFF_4:4,TAYLOR_1:11;
A9: (e0/(4*m))^m = e0 to_power m/(4*m) to_power m by TAYLOR_1:11,POWER:31
.= (e0|^m)/((4*m)|^m);
A10: ((m+m)!/((m^m)*(m!))) * ((e0^m)/(4^m))
= (((m+m)!)*(e0^m))/((m^m)*(m!)*(4^m)) by XCMPLX_1:76
.= (((2*m)!)*(e0^m))/(((m^m)*(4^m))*(m!))
.= (((2*m)!)*(e0^m))/((m!)*((4*m)^m)) by POWER:30
.= ((2*m)!/(m!))*((e0/(4*m))^m) by A9,XCMPLX_1:76;
(w_seq(f)).(m-'1)
= (Sum_step(f)).k0 + (n_Integral(f)).k0 by A3,VALUED_1:def 1
.= Sum (step_(f,k0)) + (n_Integral(f)).k0 by Def15
.= Sum (step_(f,k0)) + m*integral((-f),0,1) by A1,Def16
.= ln.((m+m)!/((m^m)*(m!))) + ln.((e0^m)/(4^m)) by A8,Lm54
.= ln.(((2*m)!/(m!))*((e0/(4*m))^m)) by A10,TAYLOR_1:11,MOEBIUS3:19;
hence thesis;
end;
Lm56:
(1/2)*(ln.2) = ln.(2#R(1/2))
proof
reconsider e0 = number_e as Real;
A1: e0 > 2 & e0 <> 1 by TAYLOR_1:11;
0 < 2 < +infty by XXREAL_0:9,XREAL_0:def 1; then
2 in ].0,+infty.[ by XXREAL_1:4; then
A2: 2 in right_open_halfline(0) by LIMFUNC1:def 3;
2 to_power (1/2) > 0 by POWER:34; then
A3: 2#R(1/2) > 0 by POWER:def 2;
(1/2)*(ln.2)
= (1/2)*log(e0,2) by A2,TAYLOR_1:def 2,def 3
.= log(e0,2 to_power (1/2)) by A1,POWER:55
.= log(number_e,2#R(1/2)) by POWER:def 2
.= ln.(2#R(1/2)) by A3,DIFF_4:3;
hence thesis;
end;
definition
func W_STIRL -> Real_Sequence means :Def20:
for n be Nat holds it.n
= ((2*(n+1))!/((n+1)!))*((number_e/(4*(n+1)))^(n+1));
correctness
proof
deffunc F(Nat) =
((2*($1+1))!/(($1+1)!))*((number_e/(4*($1+1)))^($1+1));
(ex seq being Real_Sequence st for n being Nat holds seq.n = F(n)) &
(for seq1, seq2 being Real_Sequence st
(for n being Nat holds seq1.n = F(n)) &
(for n being Nat holds seq2.n = F(n)) holds seq1 = seq2)
from NUMPOLY1:sch 1;
hence thesis;
end;
end;
theorem Lm57:
for n be Nat holds
(w_seq(ln*((x_+_(1))|rohl))).n = ln.(W_STIRL.n)
proof
let n be Nat;
reconsider m = n+1 as non zero Nat;
set f = ln*((x_+_(1))|rohl);
reconsider k0 = m-'1 as Element of NAT;
dom (Sum_step(f)) = NAT & NAT = dom (n_Integral f) by FUNCT_2:def 1;
then
A2: dom (Sum_step(f) + n_Integral(f))
= NAT /\ NAT by VALUED_1:def 1
.= NAT;
set a = 0, b = 1, X = rohl;
a <= b & [. a,b .] c= X & X c= dom f & f|X is continuous
by Lm51,FDIFF_1:25,INTEGRA5:def 3; then
A3: f|[' a,b '] is continuous & f is_integrable_on [' a,b '] &
f|[' a,b '] is bounded by INTEGRA7:19;
A4: integral((-f),0,1)
= (-1) * integral(f,0,1) by Lm51,XBOOLE_1:1,A3,INTEGRA6:10;
A5: number_e <> 1 by TAYLOR_1:11;
set e0 = number_e;
A6: 1/((4/number_e)^m) = 1/((4^m)/(e0^m)) by TAYLOR_1:11,POWER:31
.= 1*((e0^m)/(4^m)) by XCMPLX_1:79;
A7: m*integral((-f),0,1)
= -(m*(log(number_e,4/number_e))) by A4,Lm52
.= -log(number_e,(4/number_e)^m) by TAYLOR_1:11,A5,POWER:55
.= ln.1 - ln.((4/number_e)^m) by DIFF_4:3,TAYLOR_1:11,MOEBIUS3:12
.= ln.((e0^m)/(4^m)) by A6,DIFF_4:4,TAYLOR_1:11;
A8: (e0/(4*m))^m = e0 to_power m/(4*m) to_power m by TAYLOR_1:11,POWER:31
.= (e0|^m)/((4*m)|^m);
A9: ((m+m)!/((m^m)*(m!))) * ((e0^m)/(4^m))
= (((m+m)!)*(e0^m))/((m^m)*(m!)*(4^m)) by XCMPLX_1:76
.= (((2*m)!)*(e0^m))/(((m^m)*(4^m))*(m!))
.= (((2*m)!)*(e0^m))/((m!)*((4*m)^m)) by POWER:30
.= ((2*m)!/(m!))*((e0/(4*m))^m) by A8,XCMPLX_1:76;
(w_seq(f)).n = (Sum_step(f)).k0 + (n_Integral(f)).k0 by A2,VALUED_1:def 1
.= Sum (step_(f,k0)) + (n_Integral(f)).k0 by Def15
.= Sum (step_(f,k0)) + m*integral((-f),0,1) by Def16
.= ln.((m+m)!/((m^m)*(m!))) + ln.((e0^m)/(4^m)) by A7,Lm54
.= ln.(((2*(n+1))!/((n+1)!))*((number_e/(4*(n+1)))^(n+1)))
by A9,TAYLOR_1:11,MOEBIUS3:19;
hence thesis by Def20;
end;
Lm58:
for n be Nat holds W_STIRL.n > 0
proof
let n be Nat;
W_STIRL.n = ((2*(n+1))!/((n+1)!))*((number_e/(4*(n+1)))^(n+1)) by Def20;
hence thesis by TAYLOR_1:11;
end;
Lm59:
exp_R/*(w_seq(ln*((x_+_(1))|rohl))) = W_STIRL
proof
set f = ln*((x_+_(1))|rohl);
set X = REAL;
dom exp_R = REAL by FUNCT_2:def 1; then
A2: rng w_seq f c= dom exp_R;
dom (exp_R/*(w_seq(f))) = NAT by FUNCT_2:def 1; then
A3: dom (exp_R/*(w_seq(f))) = dom W_STIRL by FUNCT_2:def 1;
for o be object st o in dom W_STIRL holds
(exp_R/*(w_seq(f))).o = W_STIRL.o
proof
let o be object;
assume
A4: o in dom W_STIRL; then
o in NAT; then
A5: o in dom w_seq f by FUNCT_2:def 1;
reconsider n = o as Nat by A4;
(exp_R/*(w_seq f)).o
= (exp_R*(w_seq f)).o by A2,FUNCT_2:def 11
.= exp_R.((w_seq f).o) by A5,FUNCT_1:13
.= exp_R.(ln.(W_STIRL.n)) by Lm57
.= exp_R.(log(number_e,W_STIRL.n)) by Lm58,DIFF_4:3
.= W_STIRL.n by TAYLOR_1:15,Lm58;
hence thesis;
end;
hence thesis by A3;
end;
theorem Th22:
lim W_STIRL = sqrt(2) & W_STIRL is convergent
proof
set X = REAL;
set f = ln*((x_+_(1))|rohl);
A1: exp_R|X is continuous;
A2: rng w_seq(ln*((x_+_(1))|rohl)) c= X;
A3: w_seq(f) is convergent by Lm30,Lm51;
A4: X c= dom exp_R by FUNCT_2:def 1;
A5: 2#R(1/2) >= 1 by PREPOWER:85;
0 < 2#R(1/2) & 2#R(1/2) < +infty
by PREPOWER:85,XXREAL_0:9,XREAL_0:def 1; then
2#R(1/2) in ].0,+infty.[ by XXREAL_1:4; then
2#R(1/2) in right_open_halfline(0) by LIMFUNC1:def 3; then
2#R(1/2) in dom ln by TAYLOR_1:def 3,def 2; then
A8: lim w_seq(f) in X by Lm56,Th18,PARTFUN1:4;
A9: 2#R(1/2) = sqrt(2) by FDIFF_7:2;
exp_R.(lim w_seq(f))
= exp_R.(log(number_e,(2#R(1/2)))) by Lm56,Th18,A5,DIFF_4:3
.= 2#R(1/2) by A5,TAYLOR_1:15;
hence thesis by Lm59,A1,A2,A3,A4,FCONT_1:13,A8,A9;
end;
definition
func Stirl_Seq -> Real_Sequence means :Def21X:
for n be Nat holds it.n = n!/((n^(n+1/2))*(number_e^(-n)));
correctness
proof
deffunc F(Nat) = $1!/(($1^($1+1/2))*(number_e^(-$1)));
(ex seq being Real_Sequence st for n being Nat holds seq.n = F(n)) &
(for seq1, seq2 being Real_Sequence st
(for n being Nat holds seq1.n = F(n)) &
(for n being Nat holds seq2.n = F(n)) holds seq1 = seq2)
from NUMPOLY1:sch 1;
hence thesis;
end;
end;
Lm60:
for n be Nat holds (Stirl_Seq^\1).n = (W_STIRL/"sqrt Wallis_Seq).n
proof
let n be Nat;
set e0 = number_e;
reconsider m = n+1 as non zero Nat;
A2: W_STIRL.n = ((2*m)!/(m!))*((number_e/(4*m))^m) by Def20;
A3: ((m!)|^2) = (m!) to_power 2 .= (m!)^2 by POWER:46;
A4: (sqrt Wallis_Seq).n = (sqrt Wallis_Seq).(m-'1)
.= sqrt(m)*((2*m)!)/((4^m)*((m!)^2)) by A3,WALLIS01:52;
A5: (e0/(4*m))^m = e0 to_power m/(4*m) to_power m by TAYLOR_1:11,POWER:31
.= (e0|^m)/((4*m)|^m);
A6: (4*m)^m = (4^m) * (m^m) by NEWTON:7;
set t = (2*m)!, s = m!;
set u = (s*(e0^m)*(4^m)), v = (((4*m)^m)*(sqrt m));
A7: e0^(-m) = 1/(e0^m) by TAYLOR_1:11,POWER:28;
A8: m^(1/2) = m#R(1/2) by POWER:def 2 .= sqrt m by FDIFF_7:2;
A9: u/v = ((4^m)*(s*(e0^m)))/((4^m)*((m^m)*(sqrt m))) by A6
.= (s*(e0^m))/((m^m)*(sqrt(m))) by XCMPLX_1:91
.= s/((m^m)*(sqrt(m))/(e0^m)) by XCMPLX_1:77
.= s/((m^(m+1/2))*(e0^(-m))) by A8,POWER:27,A7;
(W_STIRL/"sqrt Wallis_Seq).n
= ((t/(m!))*((e0/(4*m))^m))/(sqrt(m)*((2*m)!)/((4^m)*((m!)^2)))
by A2,A4,VALUED_1:17
.= ((t*(e0^m))/(s*((4*m)^m)))/(sqrt(m)*t/((4^m)*(s^2)))
by A5,XCMPLX_1:76
.= ((t*(e0^m))*((4^m)*(s*s)))/((s*((4*m)^m))*(sqrt(m)*t)) by XCMPLX_1:84
.= ((t*s)*u)/((t*s)*v)
.= (n+1)!/(((n+1)^((n+1)+1/2))*(number_e^(-(n+1)))) by A9,XCMPLX_1:91
.= (Stirl_Seq).(n+1) by Def21X
.= (Stirl_Seq^\1).n by NAT_1:def 3;
hence thesis;
end;
theorem
lim Stirl_Seq = sqrt(2*PI)
proof
A1: dom sqrt Wallis_Seq = NAT by FUNCT_2:def 1;
A2: for n being Nat holds (sqrt Wallis_Seq).n <> 0
proof
let n be Nat;
n in dom sqrt Wallis_Seq by A1,ORDINAL1:def 12;
hence thesis;
end;
A4: sqrt Wallis_Seq is convergent by WALLIS01:48,WALLIS01:50;
A6: Stirl_Seq^\1 = W_STIRL/"sqrt Wallis_Seq by Lm60; then
A7: Stirl_Seq^\1 is convergent
by Th22,WALLIS01:51,SEQ_2:23,A2,SEQ_1:5,A4,COMPTRIG:5;
lim (Stirl_Seq^\1) = sqrt(2)/(1/sqrt(PI))
by Th22,WALLIS01:51,SEQ_2:24,A2,SEQ_1:5,A4,COMPTRIG:5,A6
.= sqrt(2*PI) by SQUARE_1:29,COMPTRIG:5;
hence thesis by A7,SEQ_4:22;
end;