|
weierstrass_approximation: THEORY
%--------------------------------------------------------------------------
% The Weierstrass Approximation Theorem
% (Every continuous function on a closed interval can be uniformly
% approximated by polynomials)
%
% Version 1 April 2010
%
% Anthony Narkawicz NASA
%--------------------------------------------------------------------------
BEGIN
IMPORTING reals@bernstein_polynomials,
real_fun_continuity_equiv,
real_fun_on_compact_sets[real,real_dist],
uniform_continuity[real,real_dist,real,real_dist],
reals@sqrt
x,y,t,Ma : VAR real
i,j,m,p,n : VAR nat
k,r,Np : VAR posnat
delta : VAR posreal
a,b : VAR real
f: VAR [real -> real]
Weierstrass_approx_combin1: LEMMA
p<=2 AND k > p IMPLIES
sigma(0,k,LAMBDA (i:nat): IF i > k THEN 0 ELSE i^p*C(k,i)*(-1)^(k-i) ENDIF) = 0
Weierstrass_approximation_0_1: LEMMA
continuous?[real,real_dist,real,real_dist](f,closed_intv(0,1))
IMPLIES
FORALL (epsilon:posreal):
EXISTS (a: sequence[real],n:nat):
FORALL (x:(closed_intv(0,1))):
abs(polynomial(a,n)(x) - f(x)) < epsilon
END weierstrass_approximation
¤ Dauer der Verarbeitung: 0.17 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
