X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fdama%2Fdama%2Flebesgue.ma;h=46fe6e4223afa0136c19bed8423339b88308758c;hb=99f153e43f18bc682339bed41c8230af2ac6fd2f;hp=85f686da3ebed0968b3e7970ee599d3fb552b9a5;hpb=3cd093c8c3f5454514802e5d3ae5edc150dbbf72;p=helm.git diff --git a/helm/software/matita/contribs/dama/dama/lebesgue.ma b/helm/software/matita/contribs/dama/dama/lebesgue.ma index 85f686da3..46fe6e422 100644 --- a/helm/software/matita/contribs/dama/dama/lebesgue.ma +++ b/helm/software/matita/contribs/dama/dama/lebesgue.ma @@ -16,10 +16,30 @@ include "sandwich.ma". include "property_exhaustivity.ma". -le x_i e y_i stanno o no nel segmento? +lemma order_converges_bigger_lowsegment: + ∀C:ordered_set. + ∀a:sequence C.∀l,u:C.∀H:∀i:nat.a i ∈ [l,u]. + ∀x:C.∀p:a order_converges x. + ∀j.l ≤ (fst p) j. +intros; cases p; clear p; simplify; cases H1; clear H1; cases H2; clear H2; +cases (H3 j); clear H3; cases H2; cases H7; clear H2 H7; +intro H2; cases (H8 ? H2); +cases (H (w1+j)); apply (H12 H7); +qed. +lemma order_converges_smaller_upsegment: + ∀C:ordered_set. + ∀a:sequence C.∀l,u:C.∀H:∀i:nat.a i ∈ [l,u]. + ∀x:C.∀p:a order_converges x. + ∀j.(snd p) j ≤ u. +intros; cases p; clear p; simplify; cases H1; clear H1; cases H2; clear H2; +cases (H3 j); clear H3; cases H2; cases H7; clear H2 H7; +intro H2; cases (H10 ? H2); +cases (H (w1+j)); apply (H11 H7); +qed. + (* Theorem 3.10 *) -theorem lebesgue: +theorem lebesgue_oc: ∀C:ordered_uniform_space. (∀l,u:C.order_continuity {[l,u]}) → ∀a:sequence C.∀l,u:C.∀H:∀i:nat.a i ∈ [l,u]. @@ -31,14 +51,41 @@ theorem lebesgue: (segment_ordered_uniform_space C l u)) (λn.sig_in C (λx.x∈[l,u]) (a n) (H n)) (sig_in ?? x h). -intros; cases H2 (xi H4); cases H4 (yi H5); cases H5; clear H4 H5; -cases H3; cases H5; cases H4; clear H3 H4 H5 H2; +intros; +generalize in match (order_converges_bigger_lowsegment ???? H1 ? H2); +generalize in match (order_converges_smaller_upsegment ???? H1 ? H2); +cases H2 (xi yi Hx Hy Hxy); clear H2; simplify in ⊢ (% → % → ?); intros; +cut (∀i.xi i ∈ [l,u]) as Hxi; [2: + intros; split; [2:apply H3] cases (Hxy i) (H5 _); cases H5 (H7 _); + apply (le_transitive ???? (H7 0)); simplify; + cases (H1 i); assumption;] clear H3; +cut (∀i.yi i ∈ [l,u]) as Hyi; [2: + intros; split; [apply H2] cases (Hxy i) (_ H5); cases H5 (H7 _); + apply (le_transitive ????? (H7 0)); simplify; + cases (H1 i); assumption;] clear H2; split; -[2: intro h; cases (H l u (λn:nat.sig_in ?? (a n) (H1 n)) (sig_in ?? x h)); - +[1: cases Hx; cases H3; cases Hy; cases H7; split; + [1: apply (le_transitive ???? (H8 0)); cases (Hyi 0); assumption + |2: apply (le_transitive ????? (H4 0)); cases (Hxi 0); assumption] +|2: intros 3 (h); + letin X ≝ (sig_in ?? x h); + letin Xi ≝ (λn.sig_in ?? (xi n) (Hxi n)); + letin Yi ≝ (λn.sig_in ?? (yi n) (Hyi n)); + letin Ai ≝ (λn:nat.sig_in ?? (a n) (H1 n)); + apply (sandwich {[l,u]} X Xi Yi Ai); try assumption; + [1: intro j; cases (Hxy j); cases H3; cases H4; split; + [apply (H5 0);|apply (H7 0)] + |2: cases (H l u Xi X) (Ux Uy); apply Ux; cases Hx; split; [apply H3;] + cases H4; split; [apply H5] intros (y Hy);cases (H6 (fst y));[2:apply Hy]; + exists [apply w] apply H7; + |3: cases (H l u Yi X) (Ux Uy); apply Uy; cases Hy; split; [apply H3;] + cases H4; split; [apply H5] intros (y Hy);cases (H6 (fst y));[2:apply Hy]; + exists [apply w] apply H7;]] +qed. + (* Theorem 3.9 *) -theorem lebesgue: +theorem lebesgue_se: ∀C:ordered_uniform_space.property_sigma C → (∀l,u:C.exhaustive {[l,u]}) → ∀a:sequence C.∀l,u:C.∀H:∀i:nat.a i ∈ [l,u]. @@ -50,22 +97,34 @@ theorem lebesgue: (segment_ordered_uniform_space C l u)) (λn.sig_in C (λx.x∈[l,u]) (a n) (H n)) (sig_in ?? x h). -intros; cases H3 (xi H4); cases H4 (yi H5); cases H5; cases H6; cases H8; -cases H9; cases H10; cases H11; clear H3 H4 H5 H6 H8 H9 H10 H11 H15 H16; -lapply (uparrow_upperlocated ? xi x)as Ux;[2: split; assumption] -lapply (downarrow_lowerlocated ? yi x)as Uy;[2: split; assumption] -cases (restrict_uniform_convergence ? H ?? (H1 l u) (λn:nat.sig_in ?? (a n) (H2 n)) x); -[ split; assumption] -split; simplify; - [1: intro; cases (H7 n); cases H3; - - - lapply (sandwich ? x xi yi a ); - [2: intro; cases (H7 i); cases H3; cases H4; split[apply (H5 0)|apply (H8 0)] - |3: intros 2; - cases (restrict_uniform_convergence ? H ?? (H1 l u) ? x); - [1: - -lapply (restrict_uniform_convergence ? H ?? (H1 l u) - (λn:nat.sig_in ?? (a n) (H2 n)) x); - [2:split; assumption] \ No newline at end of file +intros (C S); +generalize in match (order_converges_bigger_lowsegment ???? H1 ? H2); +generalize in match (order_converges_smaller_upsegment ???? H1 ? H2); +cases H2 (xi yi Hx Hy Hxy); clear H2; simplify in ⊢ (% → % → ?); intros; +cut (∀i.xi i ∈ [l,u]) as Hxi; [2: + intros; split; [2:apply H3] cases (Hxy i) (H5 _); cases H5 (H7 _); + apply (le_transitive ???? (H7 0)); simplify; + cases (H1 i); assumption;] clear H3; +cut (∀i.yi i ∈ [l,u]) as Hyi; [2: + intros; split; [apply H2] cases (Hxy i) (_ H5); cases H5 (H7 _); + apply (le_transitive ????? (H7 0)); simplify; + cases (H1 i); assumption;] clear H2; +split; +[1: cases Hx; cases H3; cases Hy; cases H7; split; + [1: apply (le_transitive ???? (H8 0)); cases (Hyi 0); assumption + |2: apply (le_transitive ????? (H4 0)); cases (Hxi 0); assumption] +|2: intros 3; + lapply (uparrow_upperlocated ? xi x Hx)as Ux; + lapply (downarrow_lowerlocated ? yi x Hy)as Uy; + letin X ≝ (sig_in ?? x h); + letin Xi ≝ (λn.sig_in ?? (xi n) (Hxi n)); + letin Yi ≝ (λn.sig_in ?? (yi n) (Hyi n)); + letin Ai ≝ (λn:nat.sig_in ?? (a n) (H1 n)); + apply (sandwich {[l,u]} X Xi Yi Ai); try assumption; + [1: intro j; cases (Hxy j); cases H3; cases H4; split; + [apply (H5 0);|apply (H7 0)] + |2: cases (restrict_uniform_convergence_uparrow ? S ?? (H l u) Xi x Hx); + apply (H4 h); + |3: cases (restrict_uniform_convergence_downarrow ? S ?? (H l u) Yi x Hy); + apply (H4 h);]] +qed.