|
piecewise_continuous[T: TYPE+ FROM 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 0 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)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
