|
step_fun_props[T: TYPE+ FROM real]: THEORY
%------------------------------------------------------------------------------
%
% Theory and proofs taken from Introduction to Analysis (Maxwell Rosenlicht)
%
% Author: Rick Butler NASA Langley
%------------------------------------------------------------------------------
BEGIN
ASSUMING
IMPORTING deriv_domain_def[T]
connected_domain : ASSUMPTION connected?[T]
not_one_element : ASSUMPTION not_one_element?[T]
ENDASSUMING
% AUTO_REWRITE+ not_one_element
% <=(x,y:T): bool = x <= y %% hide ugly restrictions
% AUTO_REWRITE+ <=
IMPORTING step_fun_def[T], % integral_step,
reals@sigma_below,
structures@sort_seq_lems[T,<=],
step_fun_scaf[T]
a,b,c,d,x,y,z,xl,xh: VAR T
f,f1,f2,g: VAR [T -> real]
eps, delta: VAR posreal
xv,yv,cc: VAR real
is_step: LEMMA a < b AND
(EXISTS (P: partition[T](a,b)): %% PROVED %%
Let N = length(P), xx = seq(P) IN
(FORALL (ii: below(N-1)): (EXISTS (fv: real):
(FORALL x: xx(ii) < x AND x < xx(ii+1) IMPLIES
f(x) = fv))))
IMPLIES
step_function?(a,b,f)
UUPart(a:T, b:{x:T|a<x}, c: {x:T|b<x}, P1: partition[T](a,b),
P2: partition[T](b, c)): partition[T](a,c) =
LET N1 = length(P1),
NUU = length(P1) + length(P2) - 1 IN
(# length := NUU,
seq := (LAMBDA (kk: below(NUU)):
IF kk < N1 THEN P1`seq(kk)
ELSE P2`seq(kk-N1+1)
ENDIF)
#)
split_step_is_step: LEMMA a < b AND b < c AND %% PROVED %%
step_function?(a, b, f) AND
step_function?(b, c, g)
IMPLIES
step_function?(a, c,
(LAMBDA (x: T):
IF x < a OR x > c THEN 0
ELSIF x <= b THEN f(x)
ELSE g(x)
ENDIF))
% UnionPart(a:T,b:{x:T|a<x},P1,P2: partition[T](a,b)): partition[T](a,b) =
% set2part(union(part2set(a, b, P1), part2set(a, b, P2)))
ssis_prep: LEMMA FORALL (a:T, b: {x:T|a<x}, P1,P2: partition[T](a, b),
nn: below(length(UnionPart(a,b,P1,P2))-1), x,y: T):
(in_sect?(a,b,UnionPart(a,b,P1,P2),nn,x) AND
in_sect?(a,b,UnionPart(a,b,P1,P2),nn,y) )
IMPLIES
(EXISTS (ii: below(length(P1)-1)): in_sect?(a,b,P1,ii,x) AND
in_sect?(a,b,P1,ii,y))
AND (EXISTS (jj: below(length(P2)-1)): in_sect?(a,b,P2,jj,x) AND
in_sect?(a,b,P2,jj,y))
sum_step_is_step: LEMMA a < b AND %% PROVED %%
step_function?(a, b, f) AND
step_function?(a, b, g)
IMPLIES
step_function?(a, b, f + g)
diff_step_is_step: LEMMA a < b AND
step_function?(a, b, f) AND %% PROVED %%
step_function?(a, b, g)
IMPLIES
step_function?(a, b, f - g)
step_function_subrng: LEMMA a <= b AND b < c AND c <= d AND
step_function?(a, d, f)
IMPLIES step_function?(b, c, f)
END step_fun_props
[ Dauer der Verarbeitung: 0.25 Sekunden
(vorverarbeitet)
]
|
