helm/software/matita/dama/integration_algebras.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 set "baseuri" "cic:/matita/integration_algebras/".
  16
  17 include "vector_spaces.ma".
  18 include "lattices.ma".
  19
  20 (**************** Riesz Spaces ********************)
  21
  22 record pre_riesz_space (K:ordered_field_ch0) : Type \def
  23  { rs_vector_space:> vector_space K;
  24    rs_lattice_: lattice;
  25    rs_with: os_carrier rs_lattice_ = rs_vector_space
  26  }.
  27
  28 lemma rs_lattice: ∀K:ordered_field_ch0.pre_riesz_space K → lattice.
  29  intros (K V);
  30  apply mk_lattice;
  31   [ apply (carrier V)
  32   | apply (eq_rect ? ? (λC:Type.C→C→C) ? ? (rs_with ? V));
  33     apply l_join
  34   | apply (eq_rect ? ? (λC:Type.C→C→C) ? ? (rs_with ? V));
  35     apply l_meet
  36   | apply
  37      (eq_rect' ? ?
  38       (λa:Type.λH:os_carrier (rs_lattice_ ? V)=a.
  39        is_lattice a
  40         (eq_rect Type (rs_lattice_ K V) (λC:Type.C→C→C)
  41           (l_join (rs_lattice_ K V)) a H)
  42         (eq_rect Type (rs_lattice_ K V) (λC:Type.C→C→C)
  43           (l_meet (rs_lattice_ K V)) a H))
  44       ? ? (rs_with ? V));
  45     simplify;
  46     apply l_lattice_properties
  47   ].
  48 qed.
  49
  50 coercion cic:/matita/integration_algebras/rs_lattice.con.
  51
  52 record is_riesz_space (K:ordered_field_ch0) (V:pre_riesz_space K) : Prop ≝
  53  { rs_compat_le_plus: ∀f,g,h:V. f≤g → f+h≤g+h;
  54    rs_compat_le_times: ∀a:K.∀f:V. zero K≤a → zero V≤f → zero V≤a*f
  55  }.
  56
  57 record riesz_space (K:ordered_field_ch0) : Type \def
  58  { rs_pre_riesz_space:> pre_riesz_space K;
  59    rs_riesz_space_properties: is_riesz_space ? rs_pre_riesz_space
  60  }.
  61
  62 record is_positive_linear (K) (V:riesz_space K) (T:V→K) : Prop ≝
  63  { positive: ∀u:V. os_le V 0 u → os_le K 0 (T u);
  64    linear1: ∀u,v:V. T (u+v) = T u + T v;
  65    linear2: ∀u:V.∀k:K. T (k*u) = k*(T u)
  66  }.
  67
  68 record sequentially_order_continuous (K) (V:riesz_space K) (T:V→K) : Prop ≝
  69  { soc_incr:
  70     ∀a:nat→V.∀l:V.is_increasing ? a → is_sup V a l →
  71      is_increasing K (λn.T (a n)) ∧ tends_to ? (λn.T (a n)) (T l)
  72  }.
  73
  74 definition absolute_value \def λK.λS:riesz_space K.λf.l_join S f (-f).
  75
  76 (**************** Normed Riesz spaces ****************************)
  77
  78 definition is_riesz_norm ≝
  79  λR:real.λV:riesz_space R.λnorm:norm R V.
  80   ∀f,g:V. os_le V (absolute_value ? V f) (absolute_value ? V g) →
  81    os_le R (n_function R V norm f) (n_function R V norm g).
  82
  83 record riesz_norm (R:real) (V:riesz_space R) : Type ≝
  84  { rn_norm:> norm R V;
  85    rn_riesz_norm_property: is_riesz_norm ? ? rn_norm
  86  }.
  87
  88 (*CSC: non fa la chiusura delle coercion verso funclass *)
  89 definition rn_function ≝
  90  λR:real.λV:riesz_space R.λnorm:riesz_norm ? V.
  91   n_function R V (rn_norm ? ? norm).
  92
  93 coercion cic:/matita/integration_algebras/rn_function.con 1.
  94
  95 (************************** L-SPACES *************************************)
  96 (*
  97 record is_l_space (R:real) (V:riesz_space R) (norm:riesz_norm ? V) : Prop ≝
  98  { ls_banach: is_complete ? V (induced_distance ? ? norm);
  99    ls_linear: ∀f,g:V. le ? V 0 f → le ? V 0 g → norm (f+g) = norm f + norm g
 100  }.
 101 *)
 102 (******************** ARCHIMEDEAN RIESZ SPACES ***************************)
 103
 104 record is_archimedean_riesz_space (K) (S:riesz_space K) : Prop
 105 \def
 106   { ars_archimedean: ∃u:S.∀n.∀a.∀p:n > O.
 107      os_le S
 108       (absolute_value ? S a)
 109       ((inv K (sum_field K n) (not_eq_sum_field_zero K n p))* u) →
 110      a = 0
 111   }.
 112
 113 record archimedean_riesz_space (K:ordered_field_ch0) : Type \def
 114  { ars_riesz_space:> riesz_space K;
 115    ars_archimedean_property: is_archimedean_riesz_space ? ars_riesz_space
 116  }.
 117
 118 definition is_weak_unit ≝
 119 (* This definition is by Spitters. He cites Fremlin 353P, but:
 120    1. that theorem holds only in f-algebras (as in Spitters, but we are
 121       defining it on Riesz spaces)
 122    2. Fremlin proves |x|/\u=0 \to u=0. How do we remove the absolute value?
 123  λR:real.λV:archimedean_riesz_space R.λunit: V.
 124   ∀x:V. meet x unit = 0 → u = 0.
 125   3. Fremlin proves u > 0 implies x /\ u > 0  > 0 for Archimedean spaces
 126    only. We pick this definition for now.
 127 *) λR:real.λV:archimedean_riesz_space R.λe:V.
 128     ∀v:V. lt V 0 v → lt V 0 (l_meet V v e).
 129
 130 (* Here we are avoiding a construction (the quotient space to define
 131    f=g iff I(|f-g|)=0 *)
 132 record integration_riesz_space (R:real) : Type \def
 133  { irs_archimedean_riesz_space:> archimedean_riesz_space R;
 134    irs_unit: irs_archimedean_riesz_space;
 135    irs_weak_unit: is_weak_unit ? ? irs_unit;
 136    integral: irs_archimedean_riesz_space → R;
 137    irs_positive_linear: is_positive_linear ? ? integral;
 138    irs_limit1:
 139     ∀f:irs_archimedean_riesz_space.
 140      tends_to ?
 141       (λn.integral (l_meet irs_archimedean_riesz_space f
 142        ((sum_field R n)*irs_unit)))
 143        (integral f);
 144    irs_limit2:
 145     ∀f:irs_archimedean_riesz_space.
 146      tends_to ?
 147       (λn.
 148         integral (l_meet irs_archimedean_riesz_space f
 149          ((inv ? (sum_field R (S n))
 150            (not_eq_sum_field_zero R (S n) (le_S_S O n (le_O_n n)))
 151          ) * irs_unit))) 0;
 152    irs_quotient_space1:
 153     ∀f,g:irs_archimedean_riesz_space.
 154      integral (absolute_value ? irs_archimedean_riesz_space (f - g)) = 0 → f=g
 155  }.
 156
 157 definition induced_norm_fun ≝
 158  λR:real.λV:integration_riesz_space R.λf:V.
 159   integral ? V (absolute_value ? ? f).
 160
 161 lemma induced_norm_is_norm:
 162  ∀R:real.∀V:integration_riesz_space R.is_norm R V (induced_norm_fun ? V).
 163  elim daemon.(*
 164  intros;
 165  apply mk_is_norm;
 166   [ apply mk_is_semi_norm;
 167      [ unfold induced_norm_fun;
 168        intros;
 169        apply positive;
 170        [ apply (irs_positive_linear ? V)
 171        | (* difficile *)
 172          elim daemon
 173        ]
 174      | intros;
 175        unfold induced_norm_fun;
 176        (* facile *)
 177        elim daemon
 178      | intros;
 179        unfold induced_norm_fun;
 180        (* difficile *)
 181        elim daemon
 182      ]
 183   | intros;
 184     unfold induced_norm_fun in H;
 185     apply irs_quotient_space1;
 186     unfold minus;
 187     rewrite < plus_comm;
 188     rewrite < eq_zero_opp_zero;
 189     rewrite > zero_neutral;
 190     assumption
 191   ].*)
 192 qed.
 193
 194 definition induced_norm ≝
 195  λR:real.λV:integration_riesz_space R.
 196   mk_norm ? ? (induced_norm_fun ? V) (induced_norm_is_norm ? V).
 197
 198 lemma is_riesz_norm_induced_norm:
 199  ∀R:real.∀V:integration_riesz_space R.
 200   is_riesz_norm ? ? (induced_norm ? V).
 201  intros;
 202  unfold is_riesz_norm;
 203  intros;
 204  unfold induced_norm;
 205  simplify;
 206  unfold induced_norm_fun;
 207  (* difficile *)
 208  elim daemon.
 209 qed.
 210
 211 definition induced_riesz_norm ≝
 212  λR:real.λV:integration_riesz_space R.
 213   mk_riesz_norm ? ? (induced_norm ? V) (is_riesz_norm_induced_norm ? V).
 214
 215 definition distance_induced_by_integral ≝
 216  λR:real.λV:integration_riesz_space R.
 217   induced_distance ? ? (induced_norm R V).
 218
 219 definition is_complete_integration_riesz_space ≝
 220  λR:real.λV:integration_riesz_space R.
 221   is_complete ? ? (distance_induced_by_integral ? V).
 222
 223 record complete_integration_riesz_space (R:real) : Type ≝
 224  { cirz_integration_riesz_space:> integration_riesz_space R;
 225    cirz_complete_integration_riesz_space_property:
 226     is_complete_integration_riesz_space ? cirz_integration_riesz_space
 227  }.
 228
 229 (* now we prove that any complete integration riesz space is an L-space *)
 230
 231 (*theorem is_l_space_l_space_induced_by_integral:
 232  ∀R:real.∀V:complete_integration_riesz_space R.
 233   is_l_space ? ? (induced_riesz_norm ? V).
 234  intros;
 235  constructor 1;
 236   [ apply cirz_complete_integration_riesz_space_property
 237   | intros;
 238     unfold induced_riesz_norm;
 239     simplify;
 240     unfold induced_norm;
 241     simplify;
 242     unfold induced_norm_fun;
 243     (* difficile *)
 244     elim daemon
 245   ].
 246 qed.*)
 247
 248 (**************************** f-ALGEBRAS ********************************)
 249
 250 record is_algebra (K: field) (V:vector_space K) (mult:V→V→V) (one:V) : Prop
 251 ≝
 252  { (* ring properties *)
 253    a_ring: is_ring V mult one;
 254    (* algebra properties *)
 255    a_associative_left: ∀a,f,g. a * (mult f g) = mult (a * f) g;
 256    a_associative_right: ∀a,f,g. a * (mult f g) = mult f (a * g)
 257  }.
 258
 259 record algebra (K: field) : Type \def
 260  { a_vector_space:> vector_space K;
 261    a_one: a_vector_space;
 262    a_mult: a_vector_space → a_vector_space → a_vector_space;
 263    a_algebra_properties: is_algebra ? ? a_mult a_one
 264  }.
 265
 266 interpretation "Algebra product" 'times a b =
 267  (cic:/matita/integration_algebras/a_mult.con _ a b).
 268
 269 definition ring_of_algebra ≝
 270  λK.λA:algebra K.
 271   mk_ring A (a_mult ? A) (a_one ? A)
 272    (a_ring ? ? ? ? (a_algebra_properties ? A)).
 273
 274 coercion cic:/matita/integration_algebras/ring_of_algebra.con.
 275
 276 record pre_f_algebra (K:ordered_field_ch0) : Type ≝
 277  { fa_archimedean_riesz_space:> archimedean_riesz_space K;
 278    fa_algebra_:> algebra K;
 279    fa_with: a_vector_space ? fa_algebra_ = rs_vector_space ? fa_archimedean_riesz_space
 280  }.
 281
 282 lemma fa_algebra: ∀K:ordered_field_ch0.pre_f_algebra K → algebra K.
 283  intros (K A);
 284  apply mk_algebra;
 285   [ apply (rs_vector_space ? A)
 286   | elim daemon
 287   | elim daemon
 288   | elim daemon
 289   ]
 290  qed.
 291
 292 coercion cic:/matita/integration_algebras/fa_algebra.con.
 293
 294 record is_f_algebra (K) (A:pre_f_algebra K) : Prop ≝
 295 { compat_mult_le:
 296    ∀f,g:A.
 297     os_le A (zero A) f → os_le A (zero A) g → os_le A (zero A) (a_mult ? A f g);
 298   compat_mult_meet:
 299    ∀f,g,h:A.
 300     l_meet A f g = (zero A) → l_meet A (a_mult ? A h f) g = (zero A)
 301 }.
 302
 303 record f_algebra (K:ordered_field_ch0) : Type ≝
 304 { fa_pre_f_algebra:> pre_f_algebra K;
 305   fa_f_algebra_properties: is_f_algebra ? fa_pre_f_algebra
 306 }.
 307
 308 (* to be proved; see footnote 2 in the paper by Spitters *)
 309 axiom symmetric_a_mult:
 310  ∀K.∀A:f_algebra K. symmetric ? (a_mult ? A).
 311
 312 record integration_f_algebra (R:real) : Type \def
 313  { ifa_integration_riesz_space:> integration_riesz_space R;
 314    ifa_f_algebra_: f_algebra R;
 315    ifa_with:
 316     fa_archimedean_riesz_space ? ifa_f_algebra_ =
 317     irs_archimedean_riesz_space ? ifa_integration_riesz_space
 318  }.
 319
 320 axiom ifa_f_algebra: ∀R:real.integration_f_algebra R → f_algebra R.
 321
 322 coercion cic:/matita/integration_algebras/ifa_f_algebra.con.