| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/PVS/complex_integration/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 2 kB |
|
Quelle essentially_bounded.pvs Sprache: PVS |
|||||||||
|
%------------------------------------------------------------------------------
% Essentially Bounded functions [T->complex] % % Author: David Lester, Manchester University % % All references are to SK Berberian "Fundamentals of Real Analysis", % Springer, 1991 % % Definition and basic properties of integrals for functions f: [T->complex] % % Version 1.0 11/3/10 Initial Version %------------------------------------------------------------------------------ essentially_bounded[(IMPORTING measure_integration@subset_algebra_def, measure_integration@measure_def) T:TYPE, S:sigma_algebra[T], mu:measure_type[T,S]]: THEORY BEGIN IMPORTING complex_measure_theory[T,S,mu] h: VAR [T->complex] x: VAR T K: VAR nnreal c: VAR complex essentially_bounded?(h):bool = complex_measurable?(h) AND ae_bounded?(h) essentially_bounded: TYPE+ = (essentially_bounded?) CONTAINING (lambda x: complex_(0,0)) f,f0,f1: VAR essentially_bounded essential_bound(f): nnreal = inf({K | ae_le?(abs(f),lambda x: K)}) essential_bound_def1: LEMMA ae_le?(abs(f),lambda x: K) => essential_bound(f) <= K essential_bound_def2: LEMMA ae_le?(abs(f),lambda x: essential_bound(f)) scal_essentially_bounded: JUDGEMENT *(c,f) HAS_TYPE essentially_bounded add_essentially_bounded: JUDGEMENT +(f0,f1) HAS_TYPE essentially_bounded opp_essentially_bounded: JUDGEMENT -(f) HAS_TYPE essentially_bounded diff_essentially_bounded: JUDGEMENT -(f0,f1) HAS_TYPE essentially_bounded prod_essentially_bounded: JUDGEMENT *(f0,f1) HAS_TYPE essentially_bounded essential_bound_scal: LEMMA % 6.6.5(2) essential_bound(c*f) = abs(c)*essential_bound(f) essential_bound_add: LEMMA % 6.6.5(3) essential_bound(f0+f1) <= essential_bound(f0)+essential_bound(f1) essential_bound_opp: LEMMA essential_bound(-f) = essential_bound(f) essential_bound_diff: LEMMA essential_bound(f0-f1) <= essential_bound(f0)+essential_bound(f1) essential_bound_eq_0: LEMMA essential_bound(f) = 0 <=> cal_N?(f) % 6.6.5(4) essential_bound_prod: LEMMA % 6.6.5(5) essential_bound(f0*f1) <= essential_bound(f0)*essential_bound(f1) IMPORTING p_integrable_def[T,S,mu,1] g: VAR p_integrable holder_judge_infty_1: JUDGEMENT *(f,g) HAS_TYPE p_integrable holder_judge_infty_2: JUDGEMENT *(g,f) HAS_TYPE p_integrable holder_infty_1: LEMMA norm(f*g) <= essential_bound(f) * norm(g) holder_infty_2: LEMMA norm(g*f) <= norm(g) * essential_bound(f) END essentially_bounded ¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28