| products/sources/formale Sprachen/PVS/lebesgue/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: factor_groups.prf Sprache: PVSOriginal von: PVS© |
|
||||||
|
%------------------------------------------------------------------------------
% The Lebesgue criterion for Riemann Integrability % % Author: David Lester, Manchester University % % References: AJ Weir, "Lebesgue Integration and Measure" CUP, 1973. % % Version 1.0 26/2/10 Initial Version %------------------------------------------------------------------------------ riemann_link: THEORY BEGIN IMPORTING riemann_scaf, analysis@integral_def[real], analysis@integral_bounded[real], analysis@integral_cont[real], metric_space@continuity_link[real] a,b,x: VAR real f: VAR [real->real] continuous_at?(f,x): MACRO bool = continuity_def.continuous_at?(f,x) continuous?(f): MACRO bool = continuity_def.continuous?(f) bounded_on_def: LEMMA FORALL (a:real,b:{x | a < x},f): bounded_on?(a,b,f) <=> zeroed_bounded?[a,b](phi(closed(a,b))*f) riemann_integrable_def: LEMMA a <= b => (Integrable?(a,b,f) <=> bounded_on?(a,b,f) AND ae_continuous?(a,b,f)) riemann_lebesgue_integrable: LEMMA a <= b AND Integrable?(a,b,f) => integrable?(closed(a,b))(f) riemann_lebesgue_integral: LEMMA a <= b AND Integrable?(a,b,f) => Integral(a,b,f) = integral(closed(a,b),f) bounded_ae_continuous_integrable: LEMMA a <= b AND bounded_on?(a,b,f) AND ae_continuous?(a,b,f) => integrable?(closed(a,b))(f) continuous_is_Integrable: LEMMA a <= b AND continuous?(f) => Integrable?(a,b,f) continuous_is_integrable: LEMMA a <= b AND continuous?(f) => integrable?(closed(a,b))(f) continuous_at_is_bounded: LEMMA a <= b AND (FORALL x: a <= x AND x <= b => continuous_at?(f,x)) => bounded_on?(a,b,f) END riemann_link ¤ Dauer der Verarbeitung: 0.15 Sekunden (vorverarbeitet) ¤ |
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
