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. (0:carrier V)≤u → (0:carrier K)≤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. absolute_value ? V f ≤ absolute_value ? V g →
  81    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      absolute_value ? S a ≤
 108       (inv K (sum_field K n) (not_eq_sum_field_zero K n p))* u →
 109      a = 0
 110   }.
 111
 112 record archimedean_riesz_space (K:ordered_field_ch0) : Type \def
 113  { ars_riesz_space:> riesz_space K;
 114    ars_archimedean_property: is_archimedean_riesz_space ? ars_riesz_space
 115  }.
 116
 117 definition is_weak_unit ≝
 118 (* This definition is by Spitters. He cites Fremlin 353P, but:
 119    1. that theorem holds only in f-algebras (as in Spitters, but we are
 120       defining it on Riesz spaces)
 121    2. Fremlin proves |x|/\u=0 \to u=0. How do we remove the absolute value?
 122  λR:real.λV:archimedean_riesz_space R.λunit: V.
 123   ∀x:V. meet x unit = 0 → u = 0.
 124   3. Fremlin proves u > 0 implies x /\ u > 0  > 0 for Archimedean spaces
 125    only. We pick this definition for now.
 126 *) λR:real.λV:archimedean_riesz_space R.λe:V.
 127     ∀v:V. lt V 0 v → lt V 0 (l_meet V v e).
 128
 129 (* Here we are avoiding a construction (the quotient space to define
 130    f=g iff I(|f-g|)=0 *)
 131 record integration_riesz_space (R:real) : Type \def
 132  { irs_archimedean_riesz_space:> archimedean_riesz_space R;
 133    irs_unit: irs_archimedean_riesz_space;
 134    irs_weak_unit: is_weak_unit ? ? irs_unit;
 135    integral: irs_archimedean_riesz_space → R;
 136    irs_positive_linear: is_positive_linear ? ? integral;
 137    irs_limit1:
 138     ∀f:irs_archimedean_riesz_space.
 139      tends_to ?
 140       (λn.integral (l_meet irs_archimedean_riesz_space f
 141        ((sum_field R n)*irs_unit)))
 142        (integral f);
 143    irs_limit2:
 144     ∀f:irs_archimedean_riesz_space.
 145      tends_to ?
 146       (λn.
 147         integral (l_meet irs_archimedean_riesz_space f
 148          ((inv ? (sum_field R (S n))
 149            (not_eq_sum_field_zero R (S n) (le_S_S O n (le_O_n n)))
 150          ) * irs_unit))) 0;
 151    irs_quotient_space1:
 152     ∀f,g:irs_archimedean_riesz_space.
 153      integral (absolute_value ? irs_archimedean_riesz_space (f - g)) = 0 → f=g
 154  }.
 155
 156 definition induced_norm_fun ≝
 157  λR:real.λV:integration_riesz_space R.λf:V.
 158   integral ? V (absolute_value ? ? f).
 159
 160 lemma induced_norm_is_norm:
 161  ∀R:real.∀V:integration_riesz_space R.is_norm R V (induced_norm_fun ? V).
 162  elim daemon.(*
 163  intros;
 164  apply mk_is_norm;
 165   [ apply mk_is_semi_norm;
 166      [ unfold induced_norm_fun;
 167        intros;
 168        apply positive;
 169        [ apply (irs_positive_linear ? V)
 170        | (* difficile *)
 171          elim daemon
 172        ]
 173      | intros;
 174        unfold induced_norm_fun;
 175        (* facile *)
 176        elim daemon
 177      | intros;
 178        unfold induced_norm_fun;
 179        (* difficile *)
 180        elim daemon
 181      ]
 182   | intros;
 183     unfold induced_norm_fun in H;
 184     apply irs_quotient_space1;
 185     unfold minus;
 186     rewrite < plus_comm;
 187     rewrite < eq_zero_opp_zero;
 188     rewrite > zero_neutral;
 189     assumption
 190   ].*)
 191 qed.
 192
 193 definition induced_norm ≝
 194  λR:real.λV:integration_riesz_space R.
 195   mk_norm ? ? (induced_norm_fun ? V) (induced_norm_is_norm ? V).
 196
 197 lemma is_riesz_norm_induced_norm:
 198  ∀R:real.∀V:integration_riesz_space R.
 199   is_riesz_norm ? ? (induced_norm ? V).
 200  intros;
 201  unfold is_riesz_norm;
 202  intros;
 203  unfold induced_norm;
 204  simplify;
 205  unfold induced_norm_fun;
 206  (* difficile *)
 207  elim daemon.
 208 qed.
 209
 210 definition induced_riesz_norm ≝
 211  λR:real.λV:integration_riesz_space R.
 212   mk_riesz_norm ? ? (induced_norm ? V) (is_riesz_norm_induced_norm ? V).
 213
 214 definition distance_induced_by_integral ≝
 215  λR:real.λV:integration_riesz_space R.
 216   induced_distance ? ? (induced_norm R V).
 217
 218 definition is_complete_integration_riesz_space ≝
 219  λR:real.λV:integration_riesz_space R.
 220   is_complete ? ? (distance_induced_by_integral ? V).
 221
 222 record complete_integration_riesz_space (R:real) : Type ≝
 223  { cirz_integration_riesz_space:> integration_riesz_space R;
 224    cirz_complete_integration_riesz_space_property:
 225     is_complete_integration_riesz_space ? cirz_integration_riesz_space
 226  }.
 227
 228 (* now we prove that any complete integration riesz space is an L-space *)
 229
 230 (*theorem is_l_space_l_space_induced_by_integral:
 231  ∀R:real.∀V:complete_integration_riesz_space R.
 232   is_l_space ? ? (induced_riesz_norm ? V).
 233  intros;
 234  constructor 1;
 235   [ apply cirz_complete_integration_riesz_space_property
 236   | intros;
 237     unfold induced_riesz_norm;
 238     simplify;
 239     unfold induced_norm;
 240     simplify;
 241     unfold induced_norm_fun;
 242     (* difficile *)
 243     elim daemon
 244   ].
 245 qed.*)
 246
 247 (**************************** f-ALGEBRAS ********************************)
 248
 249 record is_algebra (K: field) (V:vector_space K) (mult:V→V→V) (one:V) : Prop
 250 ≝
 251  { (* ring properties *)
 252    a_ring: is_ring V mult one;
 253    (* algebra properties *)
 254    a_associative_left: ∀a,f,g. a * (mult f g) = mult (a * f) g;
 255    a_associative_right: ∀a,f,g. a * (mult f g) = mult f (a * g)
 256  }.
 257
 258 record algebra (K: field) : Type \def
 259  { a_vector_space:> vector_space K;
 260    a_one: a_vector_space;
 261    a_mult: a_vector_space → a_vector_space → a_vector_space;
 262    a_algebra_properties: is_algebra ? ? a_mult a_one
 263  }.
 264
 265 interpretation "Algebra product" 'times a b =
 266  (cic:/matita/integration_algebras/a_mult.con _ a b).
 267
 268 definition ring_of_algebra ≝
 269  λK.λA:algebra K.
 270   mk_ring A (a_mult ? A) (a_one ? A)
 271    (a_ring ? ? ? ? (a_algebra_properties ? A)).
 272
 273 coercion cic:/matita/integration_algebras/ring_of_algebra.con.
 274
 275 record pre_f_algebra (K:ordered_field_ch0) : Type ≝
 276  { fa_archimedean_riesz_space:> archimedean_riesz_space K;
 277    fa_algebra_:> algebra K;
 278    fa_with: a_vector_space ? fa_algebra_ = rs_vector_space ? fa_archimedean_riesz_space
 279  }.
 280
 281 lemma fa_algebra: ∀K:ordered_field_ch0.pre_f_algebra K → algebra K.
 282  intros (K A);
 283  apply mk_algebra;
 284   [ apply (rs_vector_space ? A)
 285   | elim daemon
 286   | elim daemon
 287   | elim daemon
 288   ]
 289  qed.
 290
 291 coercion cic:/matita/integration_algebras/fa_algebra.con.
 292
 293 record is_f_algebra (K) (A:pre_f_algebra K) : Prop ≝
 294 { compat_mult_le:
 295    ∀f,g:A.
 296     zero A ≤ f → zero A ≤ g → zero A ≤ a_mult ? A f g;
 297   compat_mult_meet:
 298    ∀f,g,h:A.
 299     l_meet A f g = (zero A) → l_meet A (a_mult ? A h f) g = (zero A)
 300 }.
 301
 302 record f_algebra (K:ordered_field_ch0) : Type ≝
 303 { fa_pre_f_algebra:> pre_f_algebra K;
 304   fa_f_algebra_properties: is_f_algebra ? fa_pre_f_algebra
 305 }.
 306
 307 (* to be proved; see footnote 2 in the paper by Spitters *)
 308 axiom symmetric_a_mult:
 309  ∀K.∀A:f_algebra K. symmetric ? (a_mult ? A).
 310
 311 record integration_f_algebra (R:real) : Type \def
 312  { ifa_integration_riesz_space:> integration_riesz_space R;
 313    ifa_f_algebra_: f_algebra R;
 314    ifa_with:
 315     fa_archimedean_riesz_space ? ifa_f_algebra_ =
 316     irs_archimedean_riesz_space ? ifa_integration_riesz_space
 317  }.
 318
 319 axiom ifa_f_algebra: ∀R:real.integration_f_algebra R → f_algebra R.
 320
 321 coercion cic:/matita/integration_algebras/ifa_f_algebra.con.