Quelle riesz_interval_funs.pvs Sprache: 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

quality99%

¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet) ¤

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.