| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Delphi/Bille 0.71/ (Columbo Version 0.7©) Datei vom 17.0.2013 mit Größe 8 kB |
|
Quellcode-Bibliothek fubini_tonelli.pvs Sprache: PVS |
|||||||||
|
%------------------------------------------------------------------------------
% Fubini-Tonelli Theorems % % Author: David Lester, Manchester University, NIA, Universite Perpignan % % All references are to SK Berberian "Fundamentals of Real Analysis", % Springer, 1991 % % Version 1.0 5/06/09 Initial Version %------------------------------------------------------------------------------ fubini_tonelli[(IMPORTING subset_algebra_def, measure_def) T1,T2: TYPE, S1:sigma_algebra[T1],S2:sigma_algebra[T2], mu:sigma_finite_measure[T1,S1], nu:sigma_finite_measure[T2,S2]]: THEORY BEGIN IMPORTING product_measure[T1,T2,S1,S2], integral[[T1,T2],sigma_times(S1,S2),m_times(mu,nu)] g: VAR nn_integrable h: VAR nn_measurable[[T1,T2],sigma_times(S1,S2)] x: VAR T1 y: VAR T2 IMPORTING product_integral_def[T1,T2,S1,S2,mu,nu], fubini_tonelli_scaf[T1,T2,S1,S2,mu,nu] fubini_tonelli_1: THEOREM integrable?(h) <=> integrable1?(h) % 7.4.7 fubini_tonelli_2: THEOREM integrable?(h) <=> integrable2?(h) % 7.4.7 fubini_tonelli_3: THEOREM % 7.4.7 integral(g) = integral(integral1[T1,T2,S1,S2,mu,nu](g)) fubini_tonelli_4: THEOREM % 7.4.7 integral(g) = integral(integral2[T1,T2,S1,S2,mu,nu](g)) END fubini_tonelli ¤ 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.0.2Bemerkung: (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28