| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/analysis/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 kB |
|
Quelle weierstrass_approximation.pvs Sprache: PVS |
|||||||||
|
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.11 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28