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