opp: carrier → carrier;
ag_abelian_group_properties: is_abelian_group ? plus zero opp
}.
-
+
notation "0" with precedence 89
for @{ 'zero }.
interpretation "Ring opp" 'uminus a =
(cic:/matita/integration_algebras/opp.con _ a).
+
+definition minus ≝
+ λG:abelian_group.λa,b:G. a + -b.
+
+interpretation "Ring minus" 'minus a b =
+ (cic:/matita/integration_algebras/minus.con _ a b).
theorem plus_assoc: ∀G:abelian_group. associative ? (plus G).
intro;
(****************************** rings *********************************)
-record is_ring (G:abelian_group) (mult:G→G→G) : Prop
+record is_ring (G:abelian_group) (mult:G→G→G) (one:G) : Prop
≝
- { (* multiplicative semigroup properties *)
+ { (* multiplicative monoid properties *)
mult_assoc_: associative ? mult;
+ one_neutral_left_: left_neutral ? mult one;
+ one_neutral_right_: right_neutral ? mult one;
(* ring properties *)
mult_plus_distr_left_: distributive_left ? mult (plus G);
- mult_plus_distr_right_: distributive_right ? mult (plus G)
+ mult_plus_distr_right_: distributive_right ? mult (plus G);
+ not_eq_zero_one_: (0 ≠ one)
}.
record ring : Type \def
{ r_abelian_group:> abelian_group;
mult: r_abelian_group → r_abelian_group → r_abelian_group;
- r_ring_properties: is_ring r_abelian_group mult
+ one: r_abelian_group;
+ r_ring_properties: is_ring r_abelian_group mult one
}.
theorem mult_assoc: ∀R:ring.associative ? (mult R).
intros;
- apply (mult_assoc_ ? ? (r_ring_properties R)).
+ apply (mult_assoc_ ? ? ? (r_ring_properties R)).
+qed.
+
+theorem one_neutral_left: ∀R:ring.left_neutral ? (mult R) (one R).
+ intros;
+ apply (one_neutral_left_ ? ? ? (r_ring_properties R)).
+qed.
+
+theorem one_neutral_right: ∀R:ring.right_neutral ? (mult R) (one R).
+ intros;
+ apply (one_neutral_right_ ? ? ? (r_ring_properties R)).
qed.
theorem mult_plus_distr_left: ∀R:ring.distributive_left ? (mult R) (plus R).
intros;
- apply (mult_plus_distr_left_ ? ? (r_ring_properties R)).
+ apply (mult_plus_distr_left_ ? ? ? (r_ring_properties R)).
qed.
theorem mult_plus_distr_right: ∀R:ring.distributive_right ? (mult R) (plus R).
intros;
- apply (mult_plus_distr_right_ ? ? (r_ring_properties R)).
+ apply (mult_plus_distr_right_ ? ? ? (r_ring_properties R)).
+qed.
+
+theorem not_eq_zero_one: ∀R:ring.0 ≠ one R.
+ intros;
+ apply (not_eq_zero_one_ ? ? ? (r_ring_properties R)).
qed.
interpretation "Ring mult" 'times a b =
(cic:/matita/integration_algebras/mult.con _ a b).
+notation "1" with precedence 89
+for @{ 'one }.
+
+interpretation "Field one" 'one =
+ (cic:/matita/integration_algebras/one.con _).
+
lemma eq_mult_zero_x_zero: ∀R:ring.∀x:R.0*x=0.
intros;
generalize in match (zero_neutral R 0); intro;
assumption.
qed.
-record is_field (R:ring) (one:R) (inv:∀x:R.x ≠ 0 → R) : Prop
+record is_field (R:ring) (inv:∀x:R.x ≠ 0 → R) : Prop
≝
{ (* multiplicative abelian properties *)
mult_comm_: symmetric ? (mult R);
- (* multiplicative monoid properties *)
- one_neutral_: left_neutral ? (mult R) one;
(* multiplicative group properties *)
- inv_inverse_: ∀x.∀p: x ≠ 0. mult ? (inv x p) x = one;
- (* integral domain *)
- not_eq_zero_one_: (0 ≠ one)
+ inv_inverse_: ∀x.∀p: x ≠ 0. mult ? (inv x p) x = 1
}.
-
lemma opp_opp: \forall R:ring. \forall x:R. (-(-x))=x.
intros;
apply (cancellationlaw ? (-x) ? ?);
record field : Type \def
{ f_ring:> ring;
- one: f_ring;
inv: ∀x:f_ring. x ≠ 0 → f_ring;
- field_properties: is_field f_ring one inv
+ field_properties: is_field f_ring inv
}.
-notation "1" with precedence 89
-for @{ 'one }.
-
-interpretation "Field one" 'one =
- (cic:/matita/integration_algebras/one.con _).
-
theorem mult_comm: ∀F:field.symmetric ? (mult F).
intro;
- apply (mult_comm_ ? ? ? (field_properties F)).
-qed.
-
-theorem one_neutral: ∀F:field.left_neutral ? (mult F) 1.
- intro;
- apply (one_neutral_ ? ? ? (field_properties F)).
+ apply (mult_comm_ ? ? (field_properties F)).
qed.
theorem inv_inverse: ∀F:field.∀x.∀p: x ≠ 0. mult ? (inv F x p) x = 1.
intro;
- apply (inv_inverse_ ? ? ? (field_properties F)).
-qed.
-
-theorem not_eq_zero_one: ∀F:field.0 ≠ 1.
- [2:
- intro;
- apply (not_eq_zero_one_ ? ? ? (field_properties F))
- | skip
- ]
+ apply (inv_inverse_ ? ? (field_properties F)).
qed.
definition sum_field ≝
interpretation "Ordered field lt" 'lt a b =
(cic:/matita/integration_algebras/lt.con _ a b).
-(*incompleto
lemma le_zero_x_to_le_opp_x_zero: ∀F:ordered_field_ch0.∀x:F. 0 ≤ x → -x ≤ 0.
intros;
- generalize in match (of_plus_compat ? ? ? ? ? ? ? ? F ? ? (-x) H); intro;
- rewrite > (zero_neutral ? ? ? ? F) in H1;
- rewrite > (plus_comm ? ? ? ? F) in H1;
- rewrite > (opp_inverse ? ? ? ? F) in H1;
-
+ generalize in match (of_plus_compat ? ? F ? ? (-x) H); intro;
+ rewrite > zero_neutral in H1;
+ rewrite > plus_comm in H1;
+ rewrite > opp_inverse in H1;
assumption.
-qed.*)
-
-axiom le_x_zero_to_le_zero_opp_x: ∀F:ordered_field_ch0.∀x:F. x ≤ 0 → 0 ≤ -x.
-(* intros;
- generalize in match (of_plus_compat ? ? ? ? ? ? ? ? F ? ? (-x) H); intro;
- rewrite > (zero_neutral ? ? ? ? F) in H1;
- rewrite > (plus_comm ? ? ? ? F) in H1;
- rewrite > (opp_inverse ? ? ? ? F) in H1;
+qed.
+
+lemma le_x_zero_to_le_zero_opp_x: ∀F:ordered_field_ch0.∀x:F. x ≤ 0 → 0 ≤ -x.
+ intros;
+ generalize in match (of_plus_compat ? ? F ? ? (-x) H); intro;
+ rewrite > zero_neutral in H1;
+ rewrite > plus_comm in H1;
+ rewrite > opp_inverse in H1;
assumption.
-qed.*)
+qed.
(*
lemma eq_opp_x_times_opp_one_x: ∀F:ordered_field_ch0.∀x:F.-x = -1*x.
generalize in match (of_mult_compat ? ? ? ? ? ? ? ? F ? ? H2 H2); intro;
*)
-axiom not_eq_sum_field_zero: ∀F,n. n > O → sum_field F n ≠ 0.
+(* The ordering is not necessary. *)
+axiom not_eq_sum_field_zero: ∀F:ordered_field_ch0.∀n. O<n → sum_field F n ≠ 0.
record is_vector_space (K: field) (G:abelian_group) (emult:K→G→G) : Prop
≝
rs_compat_le_times: ∀a:K.∀f. of_le ? 0 a → le ? L 0 f → le ? L 0 (a*f)
}.
-record riesz_space : Type \def
- { rs_ordered_field_ch0: ordered_field_ch0;
- rs_vector_space:> vector_space rs_ordered_field_ch0;
+record riesz_space (K:ordered_field_ch0) : Type \def
+ { rs_vector_space:> vector_space K;
rs_lattice:> lattice rs_vector_space;
rs_riesz_space_properties: is_riesz_space ? rs_vector_space rs_lattice
}.
-definition absolute_value \def λS:riesz_space.λf.join ? S f (-f).
+definition absolute_value \def λK.λS:riesz_space K.λf.join ? S f (-f).
-record is_archimedean_riesz_space (S:riesz_space) : Prop
+record is_archimedean_riesz_space (K) (S:riesz_space K) : Prop
\def
{ ars_archimedean: ∃u.∀n.∀a.∀p:n > O.
le ? S
- (absolute_value S a)
+ (absolute_value ? S a)
(emult ? S
- (inv ? (sum_field (rs_ordered_field_ch0 S) n) (not_eq_sum_field_zero ? n p))
+ (inv ? (sum_field K n) (not_eq_sum_field_zero ? n p))
u) →
a = 0
}.
-record archimedean_riesz_space : Type \def
- { ars_riesz_space:> riesz_space;
- ars_archimedean_property: is_archimedean_riesz_space ars_riesz_space
+record archimedean_riesz_space (K:ordered_field_ch0) : Type \def
+ { ars_riesz_space:> riesz_space K;
+ ars_archimedean_property: is_archimedean_riesz_space ? ars_riesz_space
}.
-record is_algebra (K: field) (V:vector_space K) (mult:V→V→V) : Prop
+record is_algebra (K: field) (V:vector_space K) (mult:V→V→V) (one:V) : Prop
≝
{ (* ring properties *)
- a_ring: is_ring V mult;
+ a_ring: is_ring V mult one;
(* algebra properties *)
a_associative_left: ∀a,f,g. a * (mult f g) = mult (a * f) g;
a_associative_right: ∀a,f,g. a * (mult f g) = mult f (a * g)
record algebra (K: field) (V:vector_space K) : Type \def
{ a_mult: V → V → V;
- a_algebra_properties: is_algebra K V a_mult
+ a_one: V;
+ a_algebra_properties: is_algebra K V a_mult a_one
}.
interpretation "Algebra product" 'times a b =
(cic:/matita/integration_algebras/a_mult.con _ _ _ a b).
-record is_f_algebra (S:archimedean_riesz_space)
- (A:algebra (rs_ordered_field_ch0 (ars_riesz_space S)) S) : Prop
+interpretation "Algebra one" 'one =
+ (cic:/matita/integration_algebras/a_one.con _ _ _).
+
+definition ring_of_algebra ≝
+ λK.λV:vector_space K.λA:algebra ? V.
+ mk_ring V (a_mult ? ? A) (a_one ? ? A)
+ (a_ring ? ? ? ? (a_algebra_properties ? ? A)).
+
+coercion cic:/matita/integration_algebras/ring_of_algebra.con.
+
+record is_f_algebra (K) (S:archimedean_riesz_space K) (A:algebra ? S) : Prop
\def
{ compat_mult_le:
∀f,g:S.
meet ? S f g = 0 → meet ? S (a_mult ? ? A h f) g = 0
}.
-record f_algebra : Type \def
-{ fa_archimedean_riesz_space: archimedean_riesz_space;
- fa_algebra: algebra ? fa_archimedean_riesz_space;
- fa_f_algebra_properties: is_f_algebra fa_archimedean_riesz_space fa_algebra
+record f_algebra (K:ordered_field_ch0) : Type \def
+{ fa_archimedean_riesz_space:> archimedean_riesz_space K;
+ fa_algebra:> algebra ? fa_archimedean_riesz_space;
+ fa_f_algebra_properties: is_f_algebra ? fa_archimedean_riesz_space fa_algebra
}.
+
+(* to be proved; see footnote 2 in the paper by Spitters *)
+axiom symmetric_a_mult: ∀K.∀A:f_algebra K. symmetric ? (a_mult ? ? A).
+
+
+definition tends_to : ∀F:ordered_field_ch0.∀f:nat→F.∀l:F.Prop.
+ alias symbol "leq" = "Ordered field le".
+ alias id "le" = "cic:/matita/nat/orders/le.ind#xpointer(1/1)".
+ apply
+ (λF:ordered_field_ch0.λf:nat → F.λl:F.
+ ∀n:nat.∃m:nat.∀j:nat. le m j →
+ l - (inv F (sum_field F (S n)) ?) ≤ f j ∧
+ f j ≤ l + (inv F (sum_field F (S n)) ?));
+ apply not_eq_sum_field_zero;
+ unfold;
+ auto new.
+qed.
+
+record is_integral (K) (A:f_algebra K) (I:Type_OF_f_algebra ? A→K) : Prop
+\def
+ { i_positive: ∀f:Type_OF_f_algebra ? A. le ? (lattice_OF_f_algebra ? A) 0 f → of_le K 0 (I f);
+ i_linear1: ∀f,g:Type_OF_f_algebra ? A. I (f + g) = I f + I g;
+ i_linear2: ∀f:A.∀k:K. I (emult ? A k f) = k*(I f)
+ }.
+
+(* Here we are avoiding a construction (the quotient space to define
+ f=g iff I(|f-g|)=0 *)
+record is_integration_f_algebra (K) (A:f_algebra K) (I:Type_OF_f_algebra ? A→K) : Prop
+\def
+ { ifa_integral: is_integral ? ? I;
+ ifa_limit1:
+ ∀f:A. tends_to ? (λn.I(meet ? A f ((sum_field K n)*(a_one ? ? A)))) (I f);
+ ifa_limit2:
+ ∀f:A.
+ tends_to ?
+ (λn.
+ I (meet ? A f
+ ((inv ? (sum_field K (S n))
+ (not_eq_sum_field_zero K (S n) (le_S_S O n (le_O_n n)))
+ ) * (a_one ? ? A)))) 0;
+ ifa_quotient_space1:
+ ∀f,g:A. f=g → I(absolute_value ? A (f - g)) = 0
+ }.
\ No newline at end of file
projects / helm.git / blobdiff