| 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_bounded_functionals.pvs Sprache: PVS |
|||||||||
|
riesz_bounded_functionals[a:real,b: {bb:real | a < bb},
(importing riesz_function_sets[a,b])Funs:TYPE FROM [INTab->real]]: THEORY %------------------------------------------------------------------------------ % Bounded linear functionals on a subtype of [real->real]. This is in direct % support of the Riesz representation theorem. %------------------------------------------------------------------------------ BEGIN ASSUMING IMPORTING riesz_function_sets[a,b] funs_subspace: ASSUMPTION bounded_linear_subspace?(fullset[Funs]) ENDASSUMING IMPORTING riesz_linear_functionals[a,b,Funs], riesz_function_sets[a,b] h,f,g: VAR Funs c,y: VAR real M: VAR nnreal L: VAR Operator bounded_op?(L) : bool = (EXISTS (M:nnreal): FORALL (f): abs(L(f)) <= M*fun_norm(f)) op_norm(L: (bounded_op?)): {M:nnreal | (FORALL (f:Funs): abs(L(f))<=M*fun_norm(f)) AND (F EXISTS (f:Funs): abs(L(f)) > M1*fun_norm(f))} op_norm_bound: LEMMA FORALL (L:(bounded_op?),f): abs(L(f)) <= op_norm(L)*fun_norm(f) bounded_linear_operator?(L): bool = bounded_op?(L) AND linear_op?(L) END riesz_bounded_functionals ¤ Dauer der Verarbeitung: 0.11 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28