Anforderungen  |   Konzepte  |   Entwurf  |   Entwicklung  |   Qualitätssicherung  |   Lebenszyklus  |   Steuerung
 
 
 
 


Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: partial_function_props.prf   Sprache: Lisp

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.18 Sekunden  (vorverarbeitet)  ]

                                                                                                                                                                                                                                                                                                                                                                                                     


Neuigkeiten

     Aktuelles
     Motto des Tages

Software

     Produkte
     Quellcodebibliothek

Aktivitäten

     Artikel über Sicherheit
     Anleitung zur Aktivierung von SSL

Muße

     Gedichte
     Musik
     Bilder

Jenseits des Üblichen ....
    

Besucherstatistik

Besucherstatistik