(* *)
(**************************************************************************)
+include "ordered_uniform.ma".
-
-include "nat/plus.ma".
-include "nat/orders.ma".
-
-lemma ltwl: ∀a,b,c:nat. b + a < c → a < c.
-intros 3 (x y z); elim y (H z IH H); [apply H]
-apply IH; apply lt_S_to_lt; apply H;
+lemma le_w_plus: ∀n,m,o.n+m≤o → m ≤ o.
+intro; elim n; simplify; [assumption]
+lapply (le_S ?? H1); apply H; apply le_S_S_to_le; assumption;
qed.
-lemma ltwr: ∀a,b,c:nat. a + b < c → a < c.
-intros 3 (x y z); rewrite > sym_plus; apply ltwl;
+alias symbol "leq" = "Ordered set less or equal than".
+alias symbol "and" = "logical and".
+theorem sandwich:
+ ∀O:ordered_uniform_space.∀l:O.∀a,b,x:sequence O.
+ (∀i:nat.a i ≤ x i ∧ x i ≤ b i) →
+ a uniform_converges l →
+ b uniform_converges l →
+ x uniform_converges l.
+intros 10;
+cases (us_phi3 ? ? H3) (V GV); cases GV (Gv HV); clear GV;
+cases (us_phi3 ? ? Gv) (W GW); cases GW (Gw HW); clear GW;
+cases (H1 ? Gw) (ma Hma); cases (H2 ? Gw) (mb Hmb); clear H1 H2;
+exists [apply (ma + mb)] intros; apply (HV 〈l,(x i)〉);
+unfold; simplify; exists [apply (a i)] split;
+[2: apply (ous_convex_l ?? Gv 〈a i,b i〉); cases (H i) (Lax Lxb); clear H;
+ [1: apply HW; exists [apply l]simplify; split;
+ [1: cases (us_phi4 ?? Gw 〈(a i),l〉); apply H2; clear H2 H;
+ apply (Hma i); rewrite > sym_plus in H1; apply (le_w_plus mb); assumption;
+ |2: apply Hmb; apply (le_w_plus ma); assumption]
+ |2,3: simplify; apply (le_transitive (a i) ?? Lax Lxb);
+ |4: apply (le_reflexive);
+ |5,6: assumption;]
+|1: apply HW; exists[apply l] simplify; split;
+ [1: apply (us_phi1 ?? Gw); unfold; apply eq_reflexive;
+ |2: apply Hma; rewrite > sym_plus in H1; apply (le_w_plus mb); assumption;]]
qed.
-
-include "tend.ma".
-include "metric_lattice.ma".
-
-alias symbol "leq" = "ordered sets less or equal than".
-alias symbol "and" = "constructive and".
-theorem sandwich:
-let ugo ≝ excess_OF_lattice1 in
- ∀R.∀ml:mlattice R.∀an,bn,xn:sequence ml.∀x:ml.
- (∀n. (xn n ≤ an n) ∧ (bn n ≤ xn n)) →
- an ⇝ x → bn ⇝ x → xn ⇝ x.
-intros (R ml an bn xn x H Ha Hb);
-unfold tends0 in Ha Hb ⊢ %; unfold d2s in Ha Hb ⊢ %; intros (e He);
-alias num (instance 0) = "natural number".
-cases (Ha (e/2) (divide_preserves_lt ??? He)) (n1 H1); clear Ha;
-cases (Hb (e/2) (divide_preserves_lt ??? He)) (n2 H2); clear Hb;
-apply (ex_introT ?? (n1+n2)); intros (n3 Lt_n1n2_n3);
-lapply (ltwr ??? Lt_n1n2_n3) as Lt_n1n3; lapply (ltwl ??? Lt_n1n2_n3) as Lt_n2n3;
-cases (H1 ? Lt_n1n3) (c daxe); cases (H2 ? Lt_n2n3) (c dbxe);
-cases (H n3) (H7 H8); clear Lt_n1n3 Lt_n2n3 Lt_n1n2_n3 c H1 H2 H n1 n2;
-(* the main inequality *)
-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 ?? ??? 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))));
- apply (Le≪ (- δ(xn n3) (bn n3)+ (δ(an n3) (bn n3)+δ(an n3) x)) (plus_assoc ????));
- apply (Le≪ ((δ(an n3) (bn n3)+δ(an n3) x)+- δ(xn n3) (bn n3)) (plus_comm ???));
- apply lew_opp; [apply mpositive] apply fle_plusr;
- apply (Le≫ ? (plus_comm ???));
- apply (Le≫ ( δ(an n3) x+ δx (bn n3)) (msymmetric ????));
- apply mtineq;]
-split; [ (* first the trivial case: -e< δ(xn n3) x *)
- apply (lt_le_transitive ????? (mpositive ????));
- apply lt_zero_x_to_lt_opp_x_zero; assumption;]
-(* the main goal: δ(xn n3) x<e *)
-apply (le_lt_transitive ???? main_ineq);
-apply (Lt≫ (e/2+e/2+e/2)); [apply (divpow ?e 2)]
-repeat (apply ltplus; try assumption);
-qed.
+
projects / helm.git / blobdiff