From: Enrico Zoli Date: Fri, 10 Nov 2006 18:06:13 +0000 (+0000) Subject: Dama: up to L-spaces and the proof (completed up to properties of the X-Git-Tag: make_still_working~6675 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=00f8600ea6678e2e2e343df1edc4877c3abcfef8;p=helm.git Dama: up to L-spaces and the proof (completed up to properties of the absolute value) that every complete integration riesz space is an L-space. Now the plan is to prove the Lebesgue dominated convergence theorem for L-spaces as Fremlin does and to build a model of them later on as suggested by Spitters. Note: the proof of the theorem by Spitters is almost trivial because it really exploits the fact the L0 is the (Cauchy) completion of L1. The proof by Fremlin is much more general since it does not assume anything more on L-spaces. Note: we could also prove that every L-space is archimedean. --- diff --git a/helm/software/matita/dama/integration_algebras.ma b/helm/software/matita/dama/integration_algebras.ma index 534882ff2..46bebc0e9 100644 --- a/helm/software/matita/dama/integration_algebras.ma +++ b/helm/software/matita/dama/integration_algebras.ma @@ -14,92 +14,7 @@ set "baseuri" "cic:/matita/integration_algebras/". -include "reals.ma". - -record is_vector_space (K: field) (G:abelian_group) (emult:K→G→G) : Prop -≝ - { vs_nilpotent: ∀v. emult 0 v = 0; - vs_neutral: ∀v. emult 1 v = v; - vs_distributive: ∀a,b,v. emult (a + b) v = (emult a v) + (emult b v); - vs_associative: ∀a,b,v. emult (a * b) v = emult a (emult b v) - }. - -record vector_space (K:field): Type \def -{ vs_abelian_group :> abelian_group; - emult: K → vs_abelian_group → vs_abelian_group; - vs_vector_space_properties :> is_vector_space ? vs_abelian_group emult -}. - -interpretation "Vector space external product" 'times a b = - (cic:/matita/integration_algebras/emult.con _ _ a b). - -record is_semi_norm (R:real) (V: vector_space R) (semi_norm:V→R) : Prop \def - { sn_positive: ∀x:V. 0 ≤ semi_norm x; - sn_omogeneous: ∀a:R.∀x:V. semi_norm (a*x) = (abs ? a) * semi_norm x; - sn_triangle_inequality: ∀x,y:V. semi_norm (x + y) ≤ semi_norm x + semi_norm y - }. - -theorem eq_semi_norm_zero_zero: - ∀R:real.∀V:vector_space R.∀semi_norm:V→R. - is_semi_norm ? ? semi_norm → - semi_norm 0 = 0. - intros; - (* facile *) - elim daemon. -qed. - -record is_norm (R:real) (V:vector_space R) (norm:V → R) : Prop \def - { n_semi_norm:> is_semi_norm ? ? norm; - n_properness: ∀x:V. norm x = 0 → x = 0 - }. - -record is_semi_distance (R:real) (C:Type) (semi_d: C→C→R) : Prop \def - { sd_positive: ∀x,y:C. 0 ≤ semi_d x y; - sd_properness: \forall x:C. semi_d x x = 0; - sd_triangle_inequality: ∀x,y,z:C. semi_d x z ≤ semi_d x y + semi_d z y - }. - -record is_distance (R:real) (C:Type) (d:C→C→R) : Prop \def - { d_semi_distance:> is_semi_distance ? ? d; - d_properness: ∀x,y:C. d x y = 0 → x=y - }. - -definition induced_distance ≝ - λR:real.λV:vector_space R.λnorm:V→R. - λf,g:V.norm (f - g). - -theorem induced_distance_is_distance: - ∀R:real.∀V:vector_space R.∀norm:V→R. - is_norm ? ? norm → is_distance ? ? (induced_distance ? ? norm). - intros; - apply mk_is_distance; - [ apply mk_is_semi_distance; - [ unfold induced_distance; - intros; - apply sn_positive; - apply n_semi_norm; - assumption - | unfold induced_distance; - intros; - unfold minus; - rewrite < plus_comm; - rewrite > opp_inverse; - apply eq_semi_norm_zero_zero; - apply n_semi_norm; - assumption - | unfold induced_distance; - intros; - (* ??? *) - elim daemon - ] - | unfold induced_distance; - intros; - generalize in match (n_properness ? ? ? H ? H1); - intro; - (* facile *) - elim daemon - ]. -qed. +include "vector_spaces.ma". record is_lattice (C:Type) (join,meet:C→C→C) : Prop \def { (* abelian semigroup properties *) @@ -147,6 +62,33 @@ record riesz_space (K:ordered_field_ch0) : Type \def definition absolute_value \def λK.λS:riesz_space K.λf.join ? S f (-f). +(*CSC: qui la notazione non fa capire!!! *) +definition is_riesz_norm ≝ + λR:real.λV:riesz_space R.λnorm:norm ? V. + ∀f,g:V. le ? V (absolute_value ? V f) (absolute_value ? V g) → + of_le R (norm f) (norm g). + +record riesz_norm (R:real) (V:riesz_space R) : Type ≝ + { rn_norm:> norm ? V; + rn_riesz_norm_property: is_riesz_norm ? ? rn_norm + }. + +(*CSC: non fa la chiusura delle coercion verso funclass *) +definition rn_function ≝ + λR:real.λV:riesz_space R.λnorm:riesz_norm ? V. + n_function ? ? (rn_norm ? ? norm). + +coercion cic:/matita/integration_algebras/rn_function.con 1. + +(************************** L-SPACES *************************************) + +record is_l_space (R:real) (V:riesz_space R) (norm:riesz_norm ? V) : Prop ≝ + { ls_banach: is_complete ? V (induced_distance ? ? norm); + ls_linear: ∀f,g:V. le ? V 0 f → le ? V 0 g → norm (f+g) = norm f + norm g + }. + +(******************** ARCHIMEDEAN RIESZ SPACES ***************************) + record is_archimedean_riesz_space (K) (S:riesz_space K) : Prop \def { ars_archimedean: ∃u.∀n.∀a.∀p:n > O. @@ -207,16 +149,16 @@ record integration_riesz_space (R:real) : Type \def integral (absolute_value ? irs_archimedean_riesz_space (f - g)) = 0 → f=g }. -definition induced_norm ≝ +definition induced_norm_fun ≝ λR:real.λV:integration_riesz_space R.λf:V. integral ? ? (absolute_value ? ? f). lemma induced_norm_is_norm: - ∀R:real.∀V:integration_riesz_space R.is_norm ? V (induced_norm ? V). + ∀R:real.∀V:integration_riesz_space R.is_norm ? V (induced_norm_fun ? V). intros; apply mk_is_norm; [ apply mk_is_semi_norm; - [ unfold induced_norm; + [ unfold induced_norm_fun; intros; apply i_positive; [ apply (irs_integral_properties ? V) @@ -224,16 +166,16 @@ lemma induced_norm_is_norm: elim daemon ] | intros; - unfold induced_norm; + unfold induced_norm_fun; (* facile *) elim daemon | intros; - unfold induced_norm; + unfold induced_norm_fun; (* difficile *) elim daemon ] | intros; - unfold induced_norm in H; + unfold induced_norm_fun in H; apply irs_quotient_space1; unfold minus; rewrite < plus_comm; @@ -243,19 +185,62 @@ lemma induced_norm_is_norm: ]. qed. +definition induced_norm ≝ + λR:real.λV:integration_riesz_space R. + mk_norm ? ? (induced_norm_fun ? V) (induced_norm_is_norm ? V). + +lemma is_riesz_norm_induced_norm: + ∀R:real.∀V:integration_riesz_space R. + is_riesz_norm ? ? (induced_norm ? V). + intros; + unfold is_riesz_norm; + intros; + unfold induced_norm; + simplify; + unfold induced_norm_fun; + (* difficile *) + elim daemon. +qed. + +definition induced_riesz_norm ≝ + λR:real.λV:integration_riesz_space R. + mk_riesz_norm ? ? (induced_norm ? V) (is_riesz_norm_induced_norm ? V). + definition distance_induced_by_integral ≝ λR:real.λV:integration_riesz_space R. induced_distance ? ? (induced_norm R V). -theorem distance_induced_by_integral_is_distance: - ∀R:real.∀V:integration_riesz_space R. - is_distance ? ? (distance_induced_by_integral ? V). +definition is_complete_integration_riesz_space ≝ + λR:real.λV:integration_riesz_space R. + is_complete ? ? (distance_induced_by_integral ? V). + +record complete_integration_riesz_space (R:real) : Type ≝ + { cirz_integration_riesz_space:> integration_riesz_space R; + cirz_complete_integration_riesz_space_property: + is_complete_integration_riesz_space ? cirz_integration_riesz_space + }. + +(* now we prove that any complete integration riesz space is an L-space *) + +theorem is_l_space_l_space_induced_by_integral: + ∀R:real.∀V:complete_integration_riesz_space R. + is_l_space ? ? (induced_riesz_norm ? V). intros; - unfold distance_induced_by_integral; - apply induced_distance_is_distance; - apply induced_norm_is_norm. + constructor 1; + [ apply cirz_complete_integration_riesz_space_property + | intros; + unfold induced_riesz_norm; + simplify; + unfold induced_norm; + simplify; + unfold induced_norm_fun; + (* difficile *) + elim daemon + ]. qed. +(**************************** f-ALGEBRAS ********************************) + record is_algebra (K: field) (V:vector_space K) (mult:V→V→V) (one:V) : Prop ≝ { (* ring properties *) @@ -306,4 +291,4 @@ record integration_f_algebra (R:real) : Type \def ifa_f_algebra:> f_algebra ? ifa_integration_riesz_space (irs_unit ? ifa_integration_riesz_space) - }. \ No newline at end of file + }. diff --git a/helm/software/matita/dama/vector_spaces.ma b/helm/software/matita/dama/vector_spaces.ma new file mode 100644 index 000000000..c20b3ca8b --- /dev/null +++ b/helm/software/matita/dama/vector_spaces.ma @@ -0,0 +1,152 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +set "baseuri" "cic:/matita/vector_spaces/". + +include "reals.ma". + +record is_vector_space (K: field) (G:abelian_group) (emult:K→G→G) : Prop +≝ + { vs_nilpotent: ∀v. emult 0 v = 0; + vs_neutral: ∀v. emult 1 v = v; + vs_distributive: ∀a,b,v. emult (a + b) v = (emult a v) + (emult b v); + vs_associative: ∀a,b,v. emult (a * b) v = emult a (emult b v) + }. + +record vector_space (K:field): Type \def +{ vs_abelian_group :> abelian_group; + emult: K → vs_abelian_group → vs_abelian_group; + vs_vector_space_properties :> is_vector_space ? vs_abelian_group emult +}. + +interpretation "Vector space external product" 'times a b = + (cic:/matita/vector_spaces/emult.con _ _ a b). + +record is_semi_norm (R:real) (V: vector_space R) (semi_norm:V→R) : Prop \def + { sn_positive: ∀x:V. 0 ≤ semi_norm x; + sn_omogeneous: ∀a:R.∀x:V. semi_norm (a*x) = (abs ? a) * semi_norm x; + sn_triangle_inequality: ∀x,y:V. semi_norm (x + y) ≤ semi_norm x + semi_norm y + }. + +theorem eq_semi_norm_zero_zero: + ∀R:real.∀V:vector_space R.∀semi_norm:V→R. + is_semi_norm ? ? semi_norm → + semi_norm 0 = 0. + intros; + (* facile *) + elim daemon. +qed. + +record is_norm (R:real) (V:vector_space R) (norm:V → R) : Prop ≝ + { n_semi_norm:> is_semi_norm ? ? norm; + n_properness: ∀x:V. norm x = 0 → x = 0 + }. + +record norm (R:real) (V:vector_space R) : Type ≝ + { n_function:1> V→R; + n_norm_properties: is_norm ? ? n_function + }. + +record is_semi_distance (R:real) (C:Type) (semi_d: C→C→R) : Prop ≝ + { sd_positive: ∀x,y:C. 0 ≤ semi_d x y; + sd_properness: ∀x:C. semi_d x x = 0; + sd_triangle_inequality: ∀x,y,z:C. semi_d x z ≤ semi_d x y + semi_d z y + }. + +record is_distance (R:real) (C:Type) (d:C→C→R) : Prop ≝ + { d_semi_distance:> is_semi_distance ? ? d; + d_properness: ∀x,y:C. d x y = 0 → x=y + }. + +record distance (R:real) (V:vector_space R) : Type ≝ + { d_function:2> V→V→R; + d_distance_properties: is_distance ? ? d_function + }. + +definition induced_distance_fun ≝ + λR:real.λV:vector_space R.λnorm:norm ? V. + λf,g:V.norm (f - g). + +theorem induced_distance_is_distance: + ∀R:real.∀V:vector_space R.∀norm:norm ? V. + is_distance ? ? (induced_distance_fun ? ? norm). + intros; + apply mk_is_distance; + [ apply mk_is_semi_distance; + [ unfold induced_distance_fun; + intros; + apply sn_positive; + apply n_semi_norm; + apply (n_norm_properties ? ? norm) + | unfold induced_distance_fun; + intros; + unfold minus; + rewrite < plus_comm; + rewrite > opp_inverse; + apply eq_semi_norm_zero_zero; + apply n_semi_norm; + apply (n_norm_properties ? ? norm) + | unfold induced_distance_fun; + intros; + (* ??? *) + elim daemon + ] + | unfold induced_distance_fun; + intros; + generalize in match (n_properness ? ? norm ? ? H); + [ intro; + (* facile *) + elim daemon + | apply (n_norm_properties ? ? norm) + ] + ]. +qed. + +definition induced_distance ≝ + λR:real.λV:vector_space R.λnorm:norm ? V. + mk_distance ? ? (induced_distance_fun ? ? norm) + (induced_distance_is_distance ? ? norm). + +definition tends_to : + ∀R:real.∀V:vector_space R.∀d:distance ? V.∀f:nat→V.∀l:V.Prop. + alias symbol "leq" = "Ordered field le". + alias id "le" = "cic:/matita/nat/orders/le.ind#xpointer(1/1)". +apply + (λR:real.λV:vector_space R.λd:distance ? V.λf:nat→V.λl:V. + ∀n:nat.∃m:nat.∀j:nat. le m j → + d (f j) l ≤ inv R (sum_field ? (S n)) ?); + apply not_eq_sum_field_zero; + unfold; + auto new. +qed. + +definition is_cauchy_seq : ∀R:real.\forall V:vector_space R. +\forall d:distance ? V.∀f:nat→V.Prop. + apply + (λR:real.λV: vector_space R. \lambda d:distance ? V. + \lambda f:nat→V. + ∀m:nat. + ∃n:nat.∀N. le n N → + -(inv R (sum_field ? (S m)) ?) ≤ d (f N) (f n) ∧ + d (f N) (f n)≤ inv R (sum_field R (S m)) ?); + apply not_eq_sum_field_zero; + unfold; + auto. +qed. + +definition is_complete ≝ + λR:real.λV:vector_space R. + λd:distance ? V. + ∀f:nat→V. is_cauchy_seq ? ? d f→ + ex V (λl:V. tends_to ? ? d f l).