Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/Isabelle/Tools/VSCode/extension/src/   (Wiener Entwicklungsmethode ©)  Datei vom 16.11.2025 mit Größe 1 kB image not shown  

Impressum weierstrass_approximation.pvs   Sprache: unbekannt

 
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

92%


[ Seitenstruktur0.27Drucken  etwas mehr zur Ethik  ]