Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: riesz_interval_funs.pvs Sprache: PVS

Original von: PVS^©

riesz_interval_funs[a:real,b: {bb:real | a < bb}]: THEORY
%------------------------------------------------------------------------------
%  Real valued functions on a closed interval
%------------------------------------------------------------------------------

BEGIN

   IMPORTING real_metric_space,real_fun_on_compact_sets,
         metric_space_real_fun

   c: VAR real
   M: VAR nnreal

   Intab : set[real] = closed_intv(a,b)
   INTab : TYPE = (closed_intv(a,b))

   h,f,g: VAR [INTab -> real]

   x :VAR INTab

   IMPORTING metric_space_real_fun[INTab,real_dist]

   bounded_on_int?(h): bool = EXISTS (M:nnreal): FORALL (x): abs(h(x))<=M

   bounded_on_int_sum_closed: LEMMA bounded_on_int?(f) AND bounded_on_int?(h) IMPLIES bounded_on_int?(f+h)

   bounded_on_int_const_closed: LEMMA bounded_on_int?(f) IMPLIES bounded_on_int?(c*f)

   fun_norm(f: (bounded_on_int?)): {M:nnreal | (FORALL (x): abs(f(x))<=M) AND (FORALL (M1:real): M1 < M IMPLIES
           EXISTS (x): abs(f(x)) > M1)}

   fun_norm_dist(f,g:(bounded_on_int?)): {k:nnreal|k=0 IFF f=g} = fun_norm(f-g)

   fun_norm_bound: LEMMA FORALL (f:(bounded_on_int?),x): abs(f(x)) <= fun_norm(f)

   fun_norm_zero: LEMMA bounded_on_int?(f) IMPLIES (fun_norm(f) = 0 IFF f = (LAMBDA (y:INTab): 0))

   fun_norm_scal: LEMMA FORALL (f:(bounded_on_int?),c): fun_norm(c*f) = abs(c)*fun_norm(f)

   fun_norm_triangle: LEMMA FORALL (f,g:(bounded_on_int?)): fun_norm(f+g) <= fun_norm(f)+fun_norm(g)

   bounded_funs_metric_space: LEMMA metric_space?[(bounded_on_int?),fun_norm_dist](bounded_on_int?)

   int_compact: LEMMA compact?(Intab)

   Bounded_Function : TYPE = (bounded_on_int?)

   continuous_on_int?(h): bool = continuous?(h,Intab)

   Continuous_Function: TYPE = (continuous_on_int?)

   fc,gc : VAR Continuous_Function
   fb,gb: VAR Bounded_Function

   continuous_implies_bounded: LEMMA FORALL (h:Continuous_Function): bounded_on_int?(h)

   continuous_function_bounded: JUDGEMENT Continuous_Function Subtype_of Bounded_Function

END riesz_interval_funs

¤ Dauer der Verarbeitung: 0.15 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.