(* *)
(**************************************************************************)
-include "sandwich_corollary.ma".
+include "sequence.ma".
-(* 3.19 *)
-definition supremum ≝
- λR.λml:mlattice R.λxn:sequence ml.λx:ml.
- increasing ? xn → upper_bound ? xn x ∧ xn ⇝ x.
+definition upper_bound ≝ λO:excess.λa:sequence O.λu:O.∀n:nat.a n ≤ u.
-definition infimum ≝
- λR.λml:mlattice R.λxn:sequence ml.λx:ml.
- decreasing ? xn → lower_bound ? xn x ∧ xn ⇝ x.
-
-(* 3.20 *)
-lemma supremum_uniq:
- ∀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);
-qed.
+definition strong_sup ≝
+ λO:excess.λs:sequence O.λx.upper_bound ? s x ∧ (∀y:O.x ≰ y → ∃n.s n ≰ y).
-definition shift : ∀R.∀ml:mlattice R.∀xn:sequence ml.nat → sequence ml ≝
- λR.λml:mlattice R.λxn:sequence ml.λm:nat.λn.xn (n+m).
-
-definition ank ≝
- λR.λml:mlattice R.λxn:sequence ml.λk:nat.
- let rec ank_aux (i : nat) ≝
- match i with
- [ 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).
+definition increasing ≝ λO:excess.λa:sequence O.∀n:nat.a n ≤ a (S n).
-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.
- let rec bnk_aux (i : nat) ≝
- match i with
- [ O ⇒ (shift ?? xn k) O
- | S n1 ⇒ (shift ?? xn k) (S n1) ∨ bnk_aux n1]
- in bnk_aux.
+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 < "'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 > "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}.
-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).
-intros (R ml xn k); unfold; intro n; simplify; apply lem;
-qed.
+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).
-(* 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).
-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 ????));
-apply (Eq≈ ?? (eq_sym ??? (meet_assoc ????)));
-apply feq_mr; rewrite > sym_plus in ⊢ (? ? ? (? ? ? (? (? %))));
-simplify; rewrite > sym_plus in ⊢ (? ? ? (? ? ? (? (? %))));
-apply meet_comm;
-qed.
+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.
-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
+coercion cic:/matita/infsup/seq_dual_exc_hint.con nocomposites.
+coercion cic:/matita/infsup/seq_dual_exc_hint1.con nocomposites.
projects / helm.git / blobdiff