From 2b422d5f721aacb242951118188f376bf1dc7ce2 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 24 Jan 2008 10:37:11 +0000 Subject: [PATCH] ... --- helm/software/matita/dama/depends | 3 +- helm/software/matita/dama/infsup.ma | 56 +++++++++++---------- helm/software/matita/dama/limit.ma | 41 +++++++++------ helm/software/matita/dama/metric_lattice.ma | 5 ++ helm/software/matita/dama/sandwich.ma | 21 +++++--- helm/software/matita/dama/sequence.ma | 4 +- helm/software/matita/dama/tend.ma | 4 +- 7 files changed, 80 insertions(+), 54 deletions(-) diff --git a/helm/software/matita/dama/depends b/helm/software/matita/dama/depends index 8334fa1a3..541721dbe 100644 --- a/helm/software/matita/dama/depends +++ b/helm/software/matita/dama/depends @@ -7,7 +7,6 @@ divisible_group.ma group.ma nat/orders.ma ordered_divisible_group.ma divisible_group.ma nat/orders.ma nat/times.ma ordered_group.ma sequence.ma excess.ma constructive_connectives.ma logic/connectives.ma -lattice.TF.ma excess.ma lattice.ma nat/nat.ma group.ma excess.ma prevalued_lattice.ma ordered_group.ma excess.ma constructive_connectives.ma constructive_higher_order_relations.ma higher_order_defs/relations.ma nat/plus.ma @@ -15,7 +14,7 @@ sandwich_corollary.ma sandwich.ma Q_is_orded_divisble_group.ma Q/q.ma ordered_divisible_group.ma limit.ma excess.ma infsup.ma tend.ma lattice.ma excess.ma -tend.ma metric_lattice.ma nat/orders.ma sequence.ma +tend.ma metric_space.ma nat/orders.ma sequence.ma constructive_higher_order_relations.ma constructive_connectives.ma higher_order_defs/relations.ma infsup.ma excess.ma sequence.ma constructive_pointfree/lebesgue.ma constructive_connectives.ma metric_lattice.ma sequence.ma diff --git a/helm/software/matita/dama/infsup.ma b/helm/software/matita/dama/infsup.ma index 60c4d2f81..cc3292fd0 100644 --- a/helm/software/matita/dama/infsup.ma +++ b/helm/software/matita/dama/infsup.ma @@ -16,34 +16,38 @@ include "sequence.ma". definition upper_bound ≝ λO:excess.λa:sequence O.λu:O.∀n:nat.a n ≤ u. +definition weak_sup ≝ + λO:excess.λs:sequence O.λx. + upper_bound ? s x ∧ (∀y:O.upper_bound ? s y → x ≤ y). + definition strong_sup ≝ λO:excess.λs:sequence O.λx.upper_bound ? s x ∧ (∀y:O.x ≰ y → ∃n.s n ≰ y). definition increasing ≝ λO:excess.λa:sequence O.∀n:nat.a n ≤ a (S n). -notation < "x \nbsp 'is_upper_bound' \nbsp s" non associative with precedence 50 for @{'upper_bound $s $x}. -notation < "x \nbsp 'is_lower_bound' \nbsp s" non associative with precedence 50 for @{'lower_bound $s $x}. -notation < "s \nbsp 'is_increasing'" non associative with precedence 50 for @{'increasing $s}. -notation < "s \nbsp 'is_decreasing'" non associative with precedence 50 for @{'decreasing $s}. -notation < "x \nbsp 'is_strong_sup' \nbsp s" non associative with precedence 50 for @{'strong_sup $s $x}. -notation < "x \nbsp 'is_strong_inf' \nbsp s" non associative with precedence 50 for @{'strong_inf $s $x}. - -notation > "x 'is_upper_bound' s" non associative with precedence 50 for @{'upper_bound $s $x}. -notation > "x 'is_lower_bound' s" non associative with precedence 50 for @{'lower_bound $s $x}. -notation > "s 'is_increasing'" non associative with precedence 50 for @{'increasing $s}. -notation > "s 'is_decreasing'" non associative with precedence 50 for @{'decreasing $s}. -notation > "x 'is_strong_sup' s" non associative with precedence 50 for @{'strong_sup $s $x}. -notation > "x 'is_strong_inf' s" non associative with precedence 50 for @{'strong_inf $s $x}. - -interpretation "Excess upper bound" 'upper_bound s x = (cic:/matita/infsup/upper_bound.con _ s x). -interpretation "Excess lower bound" 'lower_bound s x = (cic:/matita/infsup/upper_bound.con (cic:/matita/excess/dual_exc.con _) s x). -interpretation "Excess increasing" 'increasing s = (cic:/matita/infsup/increasing.con _ s). -interpretation "Excess decreasing" 'decreasing s = (cic:/matita/infsup/increasing.con (cic:/matita/excess/dual_exc.con _) s). -interpretation "Excess strong sup" 'strong_sup s x = (cic:/matita/infsup/strong_sup.con _ s x). -interpretation "Excess strong inf" 'strong_inf s x = (cic:/matita/infsup/strong_sup.con (cic:/matita/excess/dual_exc.con _) s x). - -definition seq_dual_exc_hint: ∀E.sequence E → sequence (dual_exc E) ≝ λE.λx:sequence E.x. -definition seq_dual_exc_hint1: ∀E.sequence (dual_exc E) → sequence E ≝ λE.λx:sequence (dual_exc E).x. - -coercion cic:/matita/infsup/seq_dual_exc_hint.con nocomposites. -coercion cic:/matita/infsup/seq_dual_exc_hint1.con nocomposites. +notation < "x \nbsp 'is_upper_bound' \nbsp s" non associative with precedence 50 for @{'upper_bound $_ $s $x}. +notation < "x \nbsp 'is_lower_bound' \nbsp s" non associative with precedence 50 for @{'lower_bound $_ $s $x}. +notation < "s \nbsp 'is_increasing'" non associative with precedence 50 for @{'increasing $_ $s}. +notation < "s \nbsp 'is_decreasing'" non associative with precedence 50 for @{'decreasing $_ $s}. +notation < "x \nbsp 'is_strong_sup' \nbsp s" non associative with precedence 50 for @{'strong_sup $_ $s $x}. +notation < "x \nbsp 'is_strong_inf' \nbsp s" non associative with precedence 50 for @{'strong_inf $_ $s $x}. + +notation > "x 'is_upper_bound' s 'in' e" non associative with precedence 50 for @{'upper_bound $e $s $x}. +notation > "x 'is_lower_bound' s 'in' e" non associative with precedence 50 for @{'lower_bound $e $s $x}. +notation > "s 'is_increasing' 'in' e" non associative with precedence 50 for @{'increasing $e $s}. +notation > "s 'is_decreasing' 'in' e" non associative with precedence 50 for @{'decreasing $e $s}. +notation > "x 'is_strong_sup' s 'in' e" non associative with precedence 50 for @{'strong_sup $e $s $x}. +notation > "x 'is_strong_inf' s 'in' e" non associative with precedence 50 for @{'strong_inf $e $s $x}. + +interpretation "Excess upper bound" 'upper_bound e s x = (cic:/matita/infsup/upper_bound.con e s x). +interpretation "Excess lower bound" 'lower_bound e s x = (cic:/matita/infsup/upper_bound.con (cic:/matita/excess/dual_exc.con e) s x). +interpretation "Excess increasing" 'increasing e s = (cic:/matita/infsup/increasing.con e s). +interpretation "Excess decreasing" 'decreasing e s = (cic:/matita/infsup/increasing.con (cic:/matita/excess/dual_exc.con e) s). +interpretation "Excess strong sup" 'strong_sup e s x = (cic:/matita/infsup/strong_sup.con e s x). +interpretation "Excess strong inf" 'strong_inf e s x = (cic:/matita/infsup/strong_sup.con (cic:/matita/excess/dual_exc.con e) s x). + +lemma strong_sup_is_weak: + ∀O:excess.∀s:sequence O.∀x:O.strong_sup ? s x → weak_sup ? s x. +intros (O s x Ssup); elim Ssup (Ubx M); clear Ssup; split; [assumption] +intros 3 (y Uby E); cases (M ? E) (n En); unfold in Uby; cases (Uby ? En); +qed. diff --git a/helm/software/matita/dama/limit.ma b/helm/software/matita/dama/limit.ma index 14a0637b3..1250511e8 100644 --- a/helm/software/matita/dama/limit.ma +++ b/helm/software/matita/dama/limit.ma @@ -14,30 +14,34 @@ include "infsup.ma". +definition shift ≝ λT:Type.λs:sequence T.λk:nat.λn.s (n+k). + (* 3.28 *) definition limsup ≝ λE:excess.λxn:sequence E.λx:E.∃alpha:sequence E. - (∀k.(alpha k) is_strong_sup xn) ∧ x is_strong_inf alpha. + (∀k.(alpha k) is_strong_sup (shift ? xn k) in E) ∧ + x is_strong_inf alpha in E. -notation < "x \nbsp 'is_limsup' \nbsp s" non associative with precedence 50 for @{'limsup $s $x}. -notation < "x \nbsp 'is_liminf' \nbsp s" non associative with precedence 50 for @{'liminf $s $x}. -notation > "x 'is_limsup' s" non associative with precedence 50 for @{'limsup $s $x}. -notation > "x 'is_liminf' s" non associative with precedence 50 for @{'liminf $s $x}. +notation < "x \nbsp 'is_limsup' \nbsp s" non associative with precedence 50 for @{'limsup $_ $s $x}. +notation < "x \nbsp 'is_liminf' \nbsp s" non associative with precedence 50 for @{'liminf $_ $s $x}. +notation > "x 'is_limsup' s 'in' e" non associative with precedence 50 for @{'limsup $e $s $x}. +notation > "x 'is_liminf' s 'in' e" non associative with precedence 50 for @{'liminf $e $s $x}. -interpretation "Excess limsup" 'limsup s x = (cic:/matita/limit/limsup.con _ s x). -interpretation "Excess liminf" 'liminf s x = (cic:/matita/limit/limsup.con (cic:/matita/excess/dual_exc.con _) s x). +interpretation "Excess limsup" 'limsup e s x = (cic:/matita/limit/limsup.con e s x). +interpretation "Excess liminf" 'liminf e s x = (cic:/matita/limit/limsup.con (cic:/matita/excess/dual_exc.con e) s x). (* 3.29 *) -definition lim ≝ λE:excess.λxn:sequence E.λx:E. x is_limsup xn ∧ x is_liminf xn. +definition lim ≝ + λE:excess.λxn:sequence E.λx:E. x is_limsup xn in E ∧ x is_liminf xn in E. -notation < "x \nbsp 'is_lim' \nbsp s" non associative with precedence 50 for @{'lim $s $x}. -notation > "x 'is_lim' s" non associative with precedence 50 for @{'lim $s $x}. -interpretation "Excess lim" 'lim s x = (cic:/matita/limit/lim.con _ s x). +notation < "x \nbsp 'is_lim' \nbsp s" non associative with precedence 50 for @{'lim $_ $s $x}. +notation > "x 'is_lim' s 'in' e" non associative with precedence 50 for @{'lim $e $s $x}. +interpretation "Excess lim" 'lim e s x = (cic:/matita/limit/lim.con e s x). lemma sup_decreasing: ∀E:excess.∀xn:sequence E. - ∀alpha:sequence E. (∀k.(alpha k) is_strong_sup xn) → - alpha is_decreasing. + ∀alpha:sequence E. (∀k.(alpha k) is_strong_sup xn in E) → + alpha is_decreasing in E. intros (E xn alpha H); unfold strong_sup in H; unfold upper_bound in H; unfold; intro r; elim (H r) (H1r H2r); @@ -47,10 +51,17 @@ cases (H1r w Hw); qed. include "tend.ma". +include "metric_lattice.ma". (* 3.30 *) lemma lim_tends: ∀R.∀ml:mlattice R.∀xn:sequence ml.∀x:ml. - x is_lim xn → xn ⇝ x. + x is_lim xn in ml → xn ⇝ x. intros (R ml xn x Hl); unfold lim in Hl; unfold limsup in Hl; - +cases Hl (e1 e2); cases e1 (an Han); cases e2 (bn Hbn); clear Hl e1 e2; +cases Han (SSan SIxan); cases Hbn (SSbn SIxbn); clear Han Hbn; +cases SIxan (LBxan Hxg); cases SIxbn (UPxbn Hxl); clear SIxbn SIxan; +change in UPxbn:(%) with (x is_lower_bound bn in ml); +unfold upper_bound in UPxbn LBxan; change +intros (e He); +(* 2.6 OC *) diff --git a/helm/software/matita/dama/metric_lattice.ma b/helm/software/matita/dama/metric_lattice.ma index 9f5811b6d..fdd49fe57 100644 --- a/helm/software/matita/dama/metric_lattice.ma +++ b/helm/software/matita/dama/metric_lattice.ma @@ -39,6 +39,11 @@ record mlattice (R : todgroup) : Type ≝ { ml_prop2: ∀a,b,c:ml_carr. δ (a∨b) (a∨c) + δ (a∧b) (a∧c) ≤ (δ b c) }. +interpretation "Metric lattice leq" 'leq a b = + (cic:/matita/excess/le.con (cic:/matita/metric_lattice/excess_OF_mlattice1.con _ _) a b). +interpretation "Metric lattice geq" 'geq a b = + (cic:/matita/excess/le.con (cic:/matita/metric_lattice/excess_OF_mlattice.con _ _) a b). + lemma eq_to_ndlt0: ∀R.∀ml:mlattice R.∀a,b:ml. a ≈ b → ¬ 0 < δ a b. intros (R ml a b E); intro H; apply E; apply ml_prop1; assumption; diff --git a/helm/software/matita/dama/sandwich.ma b/helm/software/matita/dama/sandwich.ma index 0ab83082e..aaea369f5 100644 --- a/helm/software/matita/dama/sandwich.ma +++ b/helm/software/matita/dama/sandwich.ma @@ -27,6 +27,7 @@ intros 3 (x y z); rewrite > sym_plus; apply ltwl; qed. include "tend.ma". +include "metric_lattice.ma". alias symbol "leq" = "ordered sets less or equal than". alias symbol "and" = "constructive and". @@ -48,13 +49,19 @@ cases (H n3) (H7 H8); clear Lt_n1n3 Lt_n2n3 Lt_n1n2_n3 c H1 H2 H n1 n2; cut (δ (xn n3) x ≤ δ (bn n3) x + δ (an n3) x + δ (an n3) x) as main_ineq; [2: apply (le_transitive ???? (mtineq ???? (an n3))); cut ( δ(an n3) (bn n3)+- δ(xn n3) (bn n3)≈( δ(an n3) (xn n3))) as H11; [2: - lapply (le_mtri ?? ??? (ge_to_le ??? H7) (ge_to_le ??? H8)) as H9; clear H7 H8; - lapply (feq_plusr ? (- δ(xn n3) (bn n3)) ?? H9) as H10; clear H9; - apply (Eq≈ (0 + δ(an n3) (xn n3)) ? (zero_neutral ??)); - apply (Eq≈ (δ(an n3) (xn n3) + 0) ? (plus_comm ???)); - apply (Eq≈ (δ(an n3) (xn n3) + (-δ(xn n3) (bn n3) +  δ(xn n3) (bn n3))) ? (opp_inverse ??)); - apply (Eq≈ (δ(an n3) (xn n3) + (δ(xn n3) (bn n3) + -δ(xn n3) (bn n3))) ? (plus_comm ?? (δ(xn n3) (bn n3)))); - apply (Eq≈ ?? (eq_sym ??? (plus_assoc ????))); assumption;] + lapply (le_mtri ?? ??? H8 H7) as H9; clear H7 H8; + lapply (Eq≈ ? (msymmetric ????) H9) as H10; clear H9; + lapply (feq_plusr ? (- δ(xn n3) (bn n3)) ?? H10) as H9; clear H10; + apply (Eq≈ ? H9); clear H9; + apply (Eq≈ (δ(xn n3) (an n3)+ δ(bn n3) (xn n3)+- δ(xn n3) (bn n3)) (plus_comm ??( δ(xn n3) (an n3)))); + apply (Eq≈ (δ(xn n3) (an n3)+ δ(bn n3) (xn n3)+- δ(bn n3) (xn n3)) (feq_opp ??? (msymmetric ????))); + apply (Eq≈ ( δ(xn n3) (an n3)+ (δ(bn n3) (xn n3)+- δ(bn n3) (xn n3))) (plus_assoc ????)); + apply (Eq≈ (δ(xn n3) (an n3) + (- δ(bn n3) (xn n3) + δ(bn n3) (xn n3))) (plus_comm ??(δ(bn n3) (xn n3)))); + apply (Eq≈ (δ(xn n3) (an n3) + 0) (opp_inverse ??)); + apply (Eq≈ ? (plus_comm ???)); + apply (Eq≈ ? (zero_neutral ??)); + apply (Eq≈ ? (msymmetric ????)); + apply eq_reflexive;] apply (Le≪ (δ(an n3) (xn n3)+ δ(an n3) x) (msymmetric ??(an n3)(xn n3))); apply (Le≪ (δ(an n3) (bn n3)+- δ(xn n3) (bn n3)+ δ(an n3) x) H11); apply (Le≪ (- δ(xn n3) (bn n3)+ δ(an n3) (bn n3)+δ(an n3) x) (plus_comm ??(δ(an n3) (bn n3)))); diff --git a/helm/software/matita/dama/sequence.ma b/helm/software/matita/dama/sequence.ma index 5a3e0ea1c..44620ba39 100644 --- a/helm/software/matita/dama/sequence.ma +++ b/helm/software/matita/dama/sequence.ma @@ -14,8 +14,8 @@ include "excess.ma". -definition sequence := λO:excess.nat → O. +definition sequence := λO:Type.nat → O. -definition fun_of_sequence: ∀O:excess.sequence O → nat → O ≝ λO.λx:sequence O.x. +definition fun_of_sequence: ∀O:Type.sequence O → nat → O ≝ λO.λx:sequence O.x. coercion cic:/matita/sequence/fun_of_sequence.con 1. diff --git a/helm/software/matita/dama/tend.ma b/helm/software/matita/dama/tend.ma index d2decf0dc..a5bf7501a 100644 --- a/helm/software/matita/dama/tend.ma +++ b/helm/software/matita/dama/tend.ma @@ -13,14 +13,14 @@ (**************************************************************************) include "sequence.ma". -include "metric_lattice.ma". (* we should probably use something weaker *) +include "metric_space.ma". include "nat/orders.ma". definition tends0 ≝ λO:pogroup.λs:sequence O.∀e:O.0 < e → ∃N.∀n.N < n → -e < s n ∧ s n < e. definition d2s ≝ - λR.λml:mlattice R.λs:sequence ml.λk.λn. δ (s n) k. + λR.λms:metric_space R.λs:sequence ms.λk.λn. δ (s n) k. notation "s ⇝ x" non associative with precedence 50 for @{'tends $s $x}. interpretation "tends to" 'tends s x = -- 2.39.2