| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/PVS/analysis/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 kB |
|
Quelle riesz_linear_functionals.pvs Sprache: PVS |
|||||||||
|
riesz_linear_functionals[a:real,b: {bb:real | a < bb},
(importing riesz_function_sets[a,b]) Funs:TYPE FROM [INTab->real]]: THEORY %------------------------------------------------------------------------------ % Linear functionals on a subtype of [[a,b]->real]. This is in direct support % of the Riesz representation theorem. %------------------------------------------------------------------------------ BEGIN ASSUMING IMPORTING real_metric_space funs_sum_closed : ASSUMPTION FORALL (f,g:Funs): Funs_pred(f+g) funs_const_closed: ASSUMPTION FORALL (f:Funs,c:real): Funs_pred(c*f) funs_contain_zero: ASSUMPTION Funs_pred(LAMBDA (y:INTab): 0) ENDASSUMING h,f,g: VAR Funs c,y: VAR real M: VAR nnreal Operator: TYPE = [Funs->real] L : VAR Operator additive_op?(L) : bool = (FORALL (f,g): L(f+g) = L(f)+L(g)) const_inv_op?(L) : bool = (FORALL (f:Funs,c:real): L(c*f) = c*L(f)) linear_op?(L) : bool = additive_op?(L) AND const_inv_op?(L) linear_op_zero: LEMMA linear_op?(L) IMPLIES L(LAMBDA (y:INTab): 0) = 0 END riesz_linear_functionals ¤ Dauer der Verarbeitung: 0.14 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28