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
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
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.
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);
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 *)
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;
qed.
include "tend.ma".
+include "metric_lattice.ma".
alias symbol "leq" = "ordered sets less or equal than".
alias symbol "and" = "constructive and".
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))));
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.
(**************************************************************************)
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 =
projects / helm.git / commitdiff