(* 3.20 *)
lemma supremum_uniq:
- ∀R.∀ml:mlattice R.∀xn:sequence ml.increasing ? xn → (* BUG again the wrong coercion is chosen *)
- ∀x,y:apart_of_metric_space ? ml.supremum ?? xn x → supremum ?? xn y → x ≈ y.
+ ∀R.∀ml:mlattice R.∀xn:sequence ml.increasing ? xn →
+ ∀x,y:ml.supremum ?? xn x → supremum ?? xn y → δ x y ≈ 0.
intros (R ml xn Hxn x y Sx Sy);
elim (Sx Hxn) (_ Hx); elim (Sy Hxn) (_ Hy);
apply (tends_uniq ?? xn ?? Hx Hy);
[ O ⇒ (shift ?? xn k) O
| S n1 ⇒ (shift ?? xn k) (S n1) ∧ ank_aux n1]
in ank_aux.
+
+notation < "'a'\sup k" non associative with precedence 50 for
+ @{ 'ank $x $k }.
+
+interpretation "ank" 'ank x k =
+ (cic:/matita/infsup/ank.con _ _ x k).
+
+notation < "'a'(k \atop n)" non associative with precedence 50 for
+ @{ 'ank2 $x $k $n }.
+
+interpretation "ank2" 'ank2 x k n =
+ (cic:/matita/infsup/ank.con _ _ x k n).
definition bnk ≝
λR.λml:mlattice R.λxn:sequence ml.λk:nat.
[ 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.∀m.decreasing ? (ank ?? xn m).
-intros (R ml xn m); unfold; intro n; simplify; apply lem;
+ ∀R.∀ml:mlattice R.∀xn:sequence ml.∀k.decreasing ? (ank ?? xn k).
+intros (R ml xn k); unfold; intro n; simplify; apply lem;
qed.
(* 3.26 *)
lemma ankS:
∀R.∀ml:mlattice R.∀xn:sequence ml.∀k,n:nat.
- ((ank ?? xn k) (S n)) ≈ (xn k ∧ ank ?? xn (S k) n).
+ ((ank ?? xn k) (S n)) ≈ (xn k ∧ ank ?? xn (S k) n).
intros (R ml xn k n); elim n; simplify; [apply meet_comm]
simplify in H; apply (Eq≈ ? (feq_ml ???? (H))); clear H;
apply (Eq≈ ? (meet_assoc ????));
simplify; rewrite > sym_plus in ⊢ (? ? ? (? ? ? (? (? %))));
apply meet_comm;
qed.
-
-
-
\ No newline at end of file
+
+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 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 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.
+
+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.
+
+(* 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
projects / helm.git / blobdiff