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