|
bounded_variation[T:TYPE+ from real]: THEORY
%------------------------------------------------------------------------------
% Functions of Bounded Variation on an interval [a,b]
%------------------------------------------------------------------------------
BEGIN
ASSUMING
IMPORTING deriv_domain_def[T]
connected_domain : ASSUMPTION connected?[T]
not_one_element : ASSUMPTION not_one_element?[T]
ENDASSUMING
IMPORTING rs_partition[T], reals@real_fun_preds
a,b,c,d,x,y,z: VAR T
D,m,M,v1,v2,cc,RS1,RS2,K: VAR real
delta : VAR posreal
f,g,h,G: VAR [T -> real]
% The variation of a function on a partition = Sum( |f(x_{k+1}) - f(x_k)| )
variation_on(a,(b | a<b),P:partition(a,b))(f) : nnreal =
sigma[below(P`length-1)](0,P`length-2,LAMBDA (n:below(P`length-1)):
abs(f(P`seq(n+1))-f(P`seq(n))))
variation_on_strictly_sort: LEMMA a<b IMPLIES FORALL (P:partition(a,b)):
variation_on(a,b,P) = variation_on(a,b,strictly_sort(P))
bounded_variation?(a,(b | a<b))(f): bool = (EXISTS (M: nnreal):
(FORALL (P:partition(a,b)): variation_on(a,b,P)(f) <= M))
monotonic_BV: LEMMA FORALL (bb:T | a<bb): monotonic?[(closed_intv(a,bb))](f) IMPLIES bounded_variation?(a,bb)(f)
BV_bounded: LEMMA a<b AND bounded_variation?(a,b)(f) IMPLIES bounded_on?(a,b,f)
BV_bound: LEMMA a<b AND (FORALL (P:partition(a,b)): variation_on(a,b,P)(f) <= M) IMPLIES
(FORALL (x:(closed_intv(a,b))): abs(f(x)) <= abs(f(a))+M)
BV_add: LEMMA a<b AND bounded_variation?(a,b)(f) AND bounded_variation?(a,b)(g)
IMPLIES bounded_variation?(a,b)((LAMBDA (x:T): f(x)+g(x)))
BV_scal: LEMMA a<b and bounded_variation?(a,b)(f) IMPLIES bounded_variation?(a,b)(LAMBDA (x:T): D*f(x))
BV_sub: LEMMA a<b AND bounded_variation?(a,b)(f) AND bounded_variation?(a,b)(g)
IMPLIES bounded_variation?(a,b)((LAMBDA (x:T): f(x)-g(x)))
BV_mult: LEMMA a<b AND bounded_variation?(a,b)(f) AND bounded_variation?(a,b)(g)
IMPLIES bounded_variation?(a,b)(LAMBDA (x:T): f(x)*g(x))
%----------------%
variation_on_subset: LEMMA a<=c AND c<d AND d<=b IMPLIES FORALL (Pcd:partition(c,d)):
EXISTS (Pab:partition(a,b)):
variation_on(c,d,Pcd)(f) <= variation_on(a,b,Pab)(f)
BV_subset: LEMMA a<=c AND c<d AND d<=b AND bounded_variation?(a,b)(f) IMPLIES bounded_variation?(c,d)(f)
% ----- The total variation of a function over a subinterval [a,x] of [a,b] ------ %
total_variation(a,(b|a<b),f:(bounded_variation?(a,b)))(x : (closed_intv(a,b))) : {M : nnreal |
(x = a IMPLIES M = 0) AND
(x>a IMPLIES FORALL (P:partition(a,x)): variation_on(a,x,P)(f)<=M) AND
(FORALL (M1: nnreal): M1 < M IMPLIES EXISTS (P:partition(a,x)):
variation_on(a,x,P)(f) > M1)}
% The total variation can be approximated
total_variation_approx: LEMMA a<b AND bounded_variation?(a,b)(f) IMPLIES FORALL (x:(closed_intv(a,b))):
a /= x IMPLIES FORALL (epsi:posreal): EXISTS (P:partition(a,x)):
variation_on(a,x,P)(f) > total_variation(a,b,f)(x)-epsi
BV_decomposition: LEMMA a<b IMPLIES (bounded_variation?(a,b)(f) IFF
LET CI = closed_intv(a,b) IN
EXISTS (g,h): f = (LAMBDA (x:T): g(x)-h(x)) AND
increasing?[(CI)](g) AND increasing?[(CI)](h))
END bounded_variation
¤ Dauer der Verarbeitung: 0.0 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
