Anforderungen  |   Konzepte  |   Entwurf  |   Entwicklung  |   Qualitätssicherung  |   Lebenszyklus  |   Steuerung
 
 
 
 


Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: harmonic_polynomials.prf   Sprache: PVS

Original von: PVS©

piecewise_continuous[T: TYPEFROM real]: THEORY
%------------------------------------------------------------------------------
%
%  Piecewise Continuity
%
%------------------------------------------------------------------------------

BEGIN

   ASSUMING
      IMPORTING deriv_domain_def[T]

      connected_domain : ASSUMPTION connected?[T]


      not_one_element : ASSUMPTION not_one_element?[T]

   ENDASSUMING

   IMPORTING fundamental_theorem[T],%continuity_interval,
         indefinite_integral[T]

   a,b,c,x: VAR T
   f,F,G: VAR [T -> real]
   N: VAR posnat

   % continuous on a closed interval

   piecewise_continuous?(N,(P:[upto(N)->T]),H:[below(N)->[T->real]]): bool =
     strict_increasing?(P) AND
     FORALL (i:below(N)): continuous_on?(H(i),closed_intv(P(i),P(i+1)))

   piecewise_continuous?(f,a,b,N,(P:[upto(N)->T]),
                               H:[below(N)->[T->real]]): bool =
       piecewise_continuous?(N,P,H) AND
       P(0)=a AND P(N)=b AND
       FORALL (i:below(N)): FORALL (x):
         P(i)<x AND x<P(i+1) IMPLIES f(x)=H(i)(x)

   piecewise_continuous?(f,a,b): bool =
     EXISTS (N,(P:[upto(N)->T]),H:[below(N)->[T->real]]):
       piecewise_continuous?(f,a,b,N,P,H)

   % Integration

   continuous_on_integrable: LEMMA a < b AND 
     continuous_on?(f,closed_intv(a,b))
     IMPLIES integrable?(a,b,f)

   piecewise_continuous_integrable: LEMMA
     a<b AND
     piecewise_continuous?(f,a,b) IMPLIES
     Integrable?(a,b,f)

   piecewise_continuous_integral: LEMMA
     FORALL (N,(P:[upto(N)->T]),H:[below(N)->[T->real]],i:nat):
       i<N AND
       a<b AND piecewise_continuous?(f,a,b,N,P,H) AND
       P(i)<=x AND x<=P(i+1)
       IMPLIES
       Integrable?(a,x,f) AND
       Integral(a,x,f) = sigma(0,i-1,LAMBDA (k:nat): IF k<N THEN Integral(P(k),P(k+1),H(k)) ELSE ENDIF) +
                Integral(P(i),x,H(i))
       


   % fundamental3_piecewise: THEOREM 
   %   FORALL (N,(P:[upto(N)->T]),H:[below(N)->[T->real]]):
   %     a<b AND piecewise_continuous?(F,a,b,N,H) AND
   %     (FORALL (i:upto(N),x:closed_interval(P(i),P(i+1))): 
   %     derivable?(H(i),x) AND (P(i)<x AND x<P(i+1) 
   %       IMPLIES deriv(H(i),x)=f(x)))
      

END piecewise_continuous



¤ Dauer der Verarbeitung: 0.19 Sekunden  (vorverarbeitet)  ¤





Druckansicht
unsichere Verbindung
Druckansicht
sprechenden Kalenders

Eigene Datei ansehen




schauen Sie vor die Tür

Fenster


Die Firma ist wie angegeben erreichbar.

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff



                                                                                                                                                                                                                                                                                                                                                                                                     


Neuigkeiten

     Aktuelles
     Motto des Tages

Software

     Produkte
     Quellcodebibliothek

Aktivitäten

     Artikel über Sicherheit
     Anleitung zur Aktivierung von SSL

Muße

     Gedichte
     Musik
     Bilder

Jenseits des Üblichen ....
    

Besucherstatistik

Besucherstatistik