X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fdama%2Finfsup.ma;h=b3babd1b5f43f3e0b5162855ac47fd3f400b4e7f;hb=196d60526aaf4a10d0eaaf79cf8919c108b27a10;hp=7ba29dd1bab9162554a44bad8758326b6b694a57;hpb=b3dd479a0a36aeea948dcea09336fe8dfec1462d;p=helm.git diff --git a/helm/software/matita/dama/infsup.ma b/helm/software/matita/dama/infsup.ma index 7ba29dd1b..b3babd1b5 100644 --- a/helm/software/matita/dama/infsup.ma +++ b/helm/software/matita/dama/infsup.ma @@ -62,6 +62,18 @@ definition bnk ≝ [ O ⇒ (shift ?? xn k) O | S n1 ⇒ (shift ?? xn k) (S n1) ∨ bnk_aux n1] in bnk_aux. + +notation < "'b'\sup k" non associative with precedence 50 for + @{ 'bnk $x $k }. + +interpretation "bnk" 'bnk x k = + (cic:/matita/infsup/bnk.con _ _ x k). + +notation < "('b' \sup k) \sub n" non associative with precedence 50 for + @{ 'bnk2 $x $k $n }. + +interpretation "bnk2" 'bnk2 x k n = + (cic:/matita/infsup/bnk.con _ _ x k n). lemma ank_decreasing: ∀R.∀ml:mlattice R.∀xn:sequence ml.∀k.decreasing ? (ank ?? xn k). @@ -81,36 +93,109 @@ simplify; rewrite > sym_plus in ⊢ (? ? ? (? ? ? (? (? %)))); apply meet_comm; qed. +lemma bnkS: + ∀R.∀ml:mlattice R.∀xn:sequence ml.∀k,n:nat. + ((bnk ?? xn k) (S n)) ≈ (xn k ∨ bnk ?? xn (S k) n). +intros (R ml xn k n); elim n; simplify; [apply join_comm] +simplify in H; apply (Eq≈ ? (feq_jl ???? (H))); clear H; +apply (Eq≈ ? (join_assoc ????)); +apply (Eq≈ ?? (eq_sym ??? (join_assoc ????))); +apply feq_jr; rewrite > sym_plus in ⊢ (? ? ? (? ? ? (? (? %)))); +simplify; rewrite > sym_plus in ⊢ (? ? ? (? ? ? (? (? %)))); +apply join_comm; +qed. + +lemma le_asnk_ansk: + ∀R.∀ml:mlattice R.∀xn:sequence ml.∀k,n. + (ank ?? xn k (S n)) ≤ (ank ?? xn (S k) n). +intros (R ml xn k n); +apply (Le≪ (xn k ∧ ank ?? xn (S k) n) (ankS ?????)); apply lem; +qed. + +lemma le_bnsk_bsnk: + ∀R.∀ml:mlattice R.∀xn:sequence ml.∀k,n. + (bnk ?? xn (S k) n) ≤ (bnk ?? xn k (S n)). +intros (R ml xn k n); +apply (Le≫ (xn k ∨ bnk ?? xn (S k) n) (bnkS ?????)); +apply (Le≫ ? (join_comm ???)); +apply lej; +qed. + + (* 3.27 *) -lemma foo: +lemma inf_increasing: ∀R.∀ml:mlattice R.∀xn:sequence ml. ∀alpha:sequence ml. (∀k.strong_inf ml (ank ?? xn k) (alpha k)) → increasing ml alpha. intros (R ml xn alpha H); unfold strong_inf in H; unfold lower_bound in H; unfold; -intro n; -letin H2 ≝ (λk.ankS ?? xn k n); clearbody H2; -cut (∀k.((xn k) ∧ (ank ?? xn (S k) n)) ≤ (ank ?? xn (S k) n)) as H3; [2:intro k; apply lem;] -cut (∀k.(ank ?? xn k (S n)) ≤ (ank ?? xn (S k) n)) as H4; [2: - intro k; apply (le_transitive ml ???? (H3 ?)); - apply (Le≪ ? (H2 k)); - -elim (H (S n)) (H4 H5); intro H6; elim (H5 ? H6) (m Hm); -lapply (H4 m) as H7; - - clear H5 H6; - - - -lapply (H n) as H1; clear H; elim H1 (LB H); clear H1; -lapply (LB (S n)) as H1; clear LB; -lapply (ankS ?? xn n n) as H2; +intro r; +elim (H r) (H1r H2r); +elim (H (S r)) (H1sr H2sr); clear H H2r H1sr; +intro e; cases (H2sr ? e) (w Hw); clear e H2sr; +lapply (H1r (S w)) as Hsw; clear H1r; +lapply (le_transitive ???? Hsw (le_asnk_ansk ?????)) as H; +cases (H Hw); +qed. -lapply (Le≪ (xn n∧ank R ml xn (S n) n) H2); +lemma sup_decreasing: + ∀R.∀ml:mlattice R.∀xn:sequence ml. + ∀alpha:sequence ml. (∀k.strong_sup ml (bnk ?? xn k) (alpha k)) → + decreasing ml alpha. +intros (R ml xn alpha H); unfold strong_sup in H; unfold upper_bound in H; unfold; +intro r; +elim (H r) (H1r H2r); +elim (H (S r)) (H1sr H2sr); clear H H2r H1sr; +intro e; cases (H2sr ? e) (w Hw); clear e H2sr; +lapply (H1r (S w)) as Hsw; clear H1r; +lapply (le_transitive ???? (le_bnsk_bsnk ?????) Hsw) as H; +cases (H Hw); +qed. -cases H (LB H1); clear H; +(* 3.28 *) +definition liminf ≝ + λR.λml:mlattice R.λxn:sequence ml.λx:ml. + ∃alpha:sequence ml. + (∀k.strong_inf ml (ank ?? xn k) (alpha k)) ∧ strong_sup ml alpha x. + +definition limsup ≝ + λR.λml:mlattice R.λxn:sequence ml.λx:ml. + ∃alpha:sequence ml. + (∀k.strong_sup ml (bnk ?? xn k) (alpha k)) ∧ strong_inf ml alpha x. + +(* 3.29 *) +alias symbol "and" = "constructive and". +definition lim ≝ + λR.λml:mlattice R.λxn:sequence ml.λx:ml. + (*∃y,z.*)limsup ?? xn x ∧ liminf ?? xn x(* ∧ y ≈ x ∧ z ≈ x*). + +(* 3.30 *) +lemma lim_uniq: ∀R.∀ml:mlattice R.∀xn:sequence ml.∀x:ml. + lim ?? xn x → xn ⇝ x. +intros (R ml xn x Hl); +unfold in Hl; unfold limsup in Hl; unfold liminf in Hl; +(* decompose; *) +elim Hl (low Hl_); clear Hl; +elim Hl_ (up Hl); clear Hl_; +elim Hl (Hl_ E1); clear Hl; +elim Hl_ (Hl E2); clear Hl_; +elim Hl (H1 H2); clear Hl; +elim H1 (alpha Halpha); clear H1; +elim H2 (beta Hbeta); clear H2; +apply (sandwich ?? alpha beta); +[1: intro m; elim Halpha (Ha5 Ha6); clear Halpha; + lapply (sup_increasing ????? Ha6) as Ha7; - + unfold strong_sup in Halpha Hbeta; + unfold strong_inf in Halpha Hbeta; + unfold lower_bound in Halpha Hbeta; + unfold upper_bound in Halpha Hbeta; + elim (Halpha m) (Ha5 Ha6); clear Halpha; + elim Ha5 (Ha1 Ha2); clear Ha5; + elim Ha6 (Ha3 Ha4); clear Ha6; + split; + [1: intro H; elim (Ha2 ? H) (w H1); + elim (Ha4 ? H1); + + - - - \ No newline at end of file + \ No newline at end of file