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