Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/C/     Datei vom 12.6.2008 mit Größe 1 kB image not shown  

Quellcode-Bibliothek riesz_interval_funs.pvs   Interaktion und
PortierbarkeitPVS

 
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

99%


¤ 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.0.14Bemerkung:  Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können  ¤

*Eine klare Vorstellung vom Zielzustand




Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.