| products/sources/formale sprachen/PVS/measure_integration/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: sigma_algebra.prf Sprache: PVSOriginal von: PVS© |
|
||||||
|
%-------------------------------------------------------------------------
% Measure Space % % Author: David Lester, Manchester University % % Version 1.0 04/05/09 Initial (DRL) % % Most of Chapter 4, section 1 of Berberian % %------------------------------------------------------------------------- measure_space[T:TYPE, (IMPORTING subset_algebra_def[T]) S:sigma_algebra]: THEORY BEGIN IMPORTING measure_space_def[T,S], reals@real_fun_ops_aux[T], power@real_fun_power[T], real_borel, borel_functions[real,metric_induced_topology, real,metric_induced_topology], topology@constant_continuity[real,metric_induced_topology, real,metric_induced_topology], metric_space@metric_continuity[real,(lambda (x,y:real): abs(x-y)), real,(lambda (x,y:real): abs(x-y))], metric_space@real_continuity[real,(lambda (x,y:real): abs(x-y))], pointwise_convergence[T], reals@bounded_reals[real], finite_sets@finite_cross, finite_sets@finite_sets_minmax_props[real,<=] % proof only f: VAR [T->real] g,g1,g2: VAR measurable_function[T,S] phi: VAR borel_function i,j,n,m: VAR nat s: VAR sequence[[T->real]] u: VAR sequence[measurable_function[T,S]] x: VAR T c,c1,c2,y: VAR real X: VAR set[T] Y: VAR set[real] a: VAR posreal borel_comp_measurable_is_measurable: JUDGEMENT o(phi,g) HAS_TYPE measurable_function[T,S] % SKB 4.1.12 const_measurable: LEMMA measurable_function?(lambda x: c) nn_measurable?(f):bool = measurable_function?(f) AND FORALL x: 0 <= f(x) nn_measurable: TYPE+ = (nn_measurable?) CONTAINING (lambda x: 0) nn_measurable_is_measurable: JUDGEMENT nn_measurable SUBTYPE_OF measurable_function abs_measurable: JUDGEMENT abs(g) HAS_TYPE measurable_function[T,S] expt_nat_measurable: JUDGEMENT expt(g,n) HAS_TYPE measurable_function[T,S] sq_measurable: JUDGEMENT sq(g) HAS_TYPE measurable_function[T,S] min_measurable: JUDGEMENT min(g1,g2) HAS_TYPE measurable_function[T,S] max_measurable: JUDGEMENT max(g1,g2) HAS_TYPE measurable_function[T,S] minimum_measurable: JUDGEMENT minimum(u,n) HAS_TYPE measurable_function[T,S] maximum_measurable: JUDGEMENT maximum(u,n) HAS_TYPE measurable_function[T,S] plus_measurable: JUDGEMENT plus(g) HAS_TYPE measurable_function[T,S] minus_measurable: JUDGEMENT minus(g) HAS_TYPE measurable_function[T,S] prod_measurable: JUDGEMENT *(g1,g2) HAS_TYPE measurable_function[T,S] expt_measurable: JUDGEMENT ^(g:nn_measurable,a) HAS_TYPE measurable_function[T,S] % SKB 4.1.13 measurable_plus_minus: LEMMA measurable_function?[T,S](f) <=> (measurable_function?[T,S](plus(f)) AND measurable_function?[T,S](minus(f))) % SKB 4.1.15 measurable_bounded_above?(u):bool = pointwise_bounded_above?(u) measurable_bounded_below?(u):bool = pointwise_bounded_below?(u) measurable_bounded?(u):bool = measurable_bounded_above?(u) AND measurable_bounded_below?(u) measurable_bounded_above: TYPE+ = (measurable_bounded_above?) CONTAINING (lambda n: lambda x: 0) measurable_bounded_below: TYPE+ = (measurable_bounded_below?) CONTAINING (lambda n: lambda x: 0) measurable_bounded: TYPE+ = (measurable_bounded?) CONTAINING (lambda n: lambda x: 0) measurable_bounded_above_is_bounded_above: JUDGEMENT measurable_bounded_above SUBTYPE_OF pointwise_bounded_above measurable_bounded_below_is_bounded_below: JUDGEMENT measurable_bounded_below SUBTYPE_OF pointwise_bounded_below measurable_bounded_is_measurable_bounded_above: JUDGEMENT measurable_bounded SUBTYPE_OF measurable_bounded_above measurable_bounded_is_measurable_bounded_below: JUDGEMENT measurable_bounded SUBTYPE_OF measurable_bounded_below measurable_bounded_is_bounded: JUDGEMENT measurable_bounded SUBTYPE_OF pointwise_bounded inf_measurable: LEMMA FORALL (u:measurable_bounded_below): measurable_function?[T,S](inf(u)(n)) sup_measurable: LEMMA FORALL (u:measurable_bounded_above): measurable_function?[T,S](sup(u)(n)) % SKB 4.1.19 pointwise_measurable: LEMMA pointwise_convergence?(u,f) => % SKB 4.1.20 measurable_function?[T,S](f) simple?(f):bool = measurable_function?[T,S](f) AND is_finite(image(f,fullset[T])) % SKB 4.1.21 simple: TYPE+ = (simple?) CONTAINING (lambda x: 0) simple_is_measurable: JUDGEMENT simple SUBTYPE_OF measurable_function simple_const: LEMMA simple?(lambda x: c) nn_simple?(f):bool = (FORALL x: 0 <= f(x)) AND simple?(f) nn_simple: TYPE+ = (nn_simple?) CONTAINING (lambda x: 0) nn_simple_is_simple: JUDGEMENT nn_simple SUBTYPE_OF simple h,h1,h2: VAR simple v: VAR sequence[simple] simple_sq: JUDGEMENT sq(h) HAS_TYPE simple simple_add: JUDGEMENT +(h1,h2) HAS_TYPE simple simple_scal: JUDGEMENT *(c,h) HAS_TYPE simple simple_neg: JUDGEMENT -(h) HAS_TYPE simple simple_diff: JUDGEMENT -(h1,h2) HAS_TYPE simple simple_abs: JUDGEMENT abs(h) HAS_TYPE simple simple_min: JUDGEMENT min(h1,h2) HAS_TYPE simple simple_max: JUDGEMENT max(h1,h2) HAS_TYPE simple simple_maximum: JUDGEMENT maximum(v,n) HAS_TYPE simple simple_minimum: JUDGEMENT minimum(v,n) HAS_TYPE simple simple_plus: JUDGEMENT plus(h) HAS_TYPE simple simple_minus: JUDGEMENT minus(h) HAS_TYPE simple simple_times: JUDGEMENT *(h1,h2) HAS_TYPE simple simple_expt_nat: JUDGEMENT expt(h,n) HAS_TYPE simple simple_expt: JUDGEMENT ^(h:nn_simple,a) HAS_TYPE simple % SKB 4.1.22 phi(X)(x):nat = IF member(x,X) THEN 1 ELSE 0 ENDIF phi_is_simple: JUDGEMENT phi(X:(S)) HAS_TYPE simple IMPORTING hausdorff_borel[real,metric_induced_topology], partitions[T] P: VAR finite_partition[T] simple_def1: LEMMA simple?(f) <=> % SKB 4.1.23 (is_finite(image(f,fullset[T])) AND (FORALL (y:(image(f,fullset[T]))): measurable_set?({x | y = f(x)}))) constant_over?(f)(X):bool = EXISTS y: FORALL (x:(X)): y = f(x) simple_def2: LEMMA simple?(f) <=> EXISTS P: every(S,P) AND every(constant_over?(f),P) simple_def3: LEMMA simple?(f) <=> EXISTS c1,c2,h1,h2: c1*h1+c2*h2 = f IMPORTING sup_norm[T] bounded_measurable?(f):bool = bounded?(f) AND measurable_function?(f) bounded_measurable: TYPE+ = (bounded_measurable?) CONTAINING (lambda x: 0) bounded_measurable_is_bounded: JUDGEMENT bounded_measurable SUBTYPE_OF bounded bounded_measurable_is_measurable: JUDGEMENT bounded_measurable SUBTYPE_OF measurable_function simple_is_bounded_measurable: JUDGEMENT simple SUBTYPE_OF bounded_measurable nn_bounded_measurable?(f):bool = bounded_measurable?(f) AND FORALL x: 0<=f(x) nn_bounded_measurable: TYPE+ = (nn_bounded_measurable?) CONTAINING (lambda x: 0) nn_bounded_measurable_is_bounded_measurable: JUDGEMENT nn_bounded_measurable SUBTYPE_OF bounded_measurable increasing_nn_simple?(u):bool = (FORALL n: nn_simple?(u(n))) AND pointwise_increasing?(u) increasing_nn_simple: TYPE+ = (increasing_nn_simple?) CONTAINING (lambda n: lambda x: 0) p: VAR nn_bounded_measurable w: VAR increasing_nn_simple sup_norm_simple: LEMMA EXISTS h: (forall x: 0 <= h(x) & h(x) <= p(x)) AND sup_norm(p-h) <= sup_norm(p)/2 % SKB 4.1.24 nn_simple_approx(p):nn_simple = choose({h | (forall x: 0 <= h(x) & h(x) <= p(x)) AND sup_norm(p-h) <= sup_norm(p)/2}) % The following IMPORT and recursive definition for proof only. IMPORTING reals@sigma_nat nn_simple_sequence(p)(n): RECURSIVE {h | forall x: 0 <= h(x) & h(x) <= p(x)} = IF n = 0 THEN nn_simple_approx(p) ELSE nn_simple_sequence(p-nn_simple_approx(p))(n-1) ENDIF MEASURE (lambda p: lambda n: n) nn_bounded_measurable_as_increasing_simple_sequence: % SKB 4.1.25 LEMMA EXISTS w: sup_norm_converges_to?(w,p) nn_bounded_measurable_as_sequence_prop: LEMMA sup_norm_converges_to?(w,p) => (FORALL n,x: w(n)(x) <= p(x)) bounded_measurable_as_increasing_sequence: LEMMA % SKB 4.1.25 bounded_measurable?(f) => EXISTS v: sup_norm_converges_to?(v,f) nn_measurable_def: LEMMA (FORALL x: 0 <= f(x)) => % SKB 4.1.26 (measurable_function?(f) <=> EXISTS w: pointwise_converges_upto?(w,f)) measurable_as_limit_simple_def: LEMMA % SKB 4.1.26 measurable_function?(f) <=> EXISTS v: pointwise_convergence?(v,f) END measure_space ¤ Dauer der Verarbeitung: 0.8 Sekunden (vorverarbeitet) ¤ |
Haftungshinweis
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.
Bemerkung:Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
