proposition: Theorem Heine : forall (f:R -> R) (X:R -> Prop), compact X -> (forall x:R, X x -> continuity_pt f x) -> uniform_continuity f X.
proof: Proof. intros f0 X H0 H; elim (domain_P1 X); intro Hyp. - unfold uniform_continuity; intros; exists (mkposreal _ Rlt_0_1); intros; elim Hyp; exists x; assumption. - elim Hyp; clear Hyp; intro Hyp. + unfold uniform_continuity; intros; exists (mkposreal _ Rlt_0_1); intros; elim Hyp; clear Hyp; intros; elim H4; clear H4; intros; assert (H6 := H5 _ H1); assert (H7 := H5 _ H2); rewrite H6; rewrite H7; unfold Rminus; rewrite Rplus_opp_r; rewrite Rabs_R0; apply (cond_pos eps). + assert (X_enc : exists m : R, (exists M : R, (forall x:R, X x -> m <= x <= M) /\ m < M)). * assert (H1 := compact_P1 X H0); unfold bounded in H1; elim H1; intros; elim H2; intros; exists x; exists x0; split. -- apply H3. -- elim Hyp; intros; elim H4; intros; decompose [and] H5; assert (H10 := H3 _ H6); assert (H11 := H3 _ H8); elim H10; intros; elim H11; intros; destruct (total_order_T x x0) as [[|H15]|H15]. ++ assumption. ++ rewrite H15 in H13, H7; elim H9; apply Rle_antisym; apply Rle_trans with x0; assumption. ++ elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ (Rle_trans _ _ _ H13 H14) H15)). * elim X_enc; clear X_enc; intros m X_enc; elim X_enc; clear X_enc; intros M X_enc; elim X_enc; clear X_enc Hyp; intros X_enc Hyp; unfold uniform_continuity; intro; assert (H1 : forall t:posreal, 0 < t / 2). -- intro; unfold Rdiv; apply Rmult_lt_0_compat; [ apply (cond_pos t) | apply Rinv_0_lt_compat; prove_sup0 ]. -- set (g := fun x y:R => X x /\ (exists del : posreal, (forall z:R, Rabs (z - x) < del -> Rabs (f0 z - f0 x) < eps / 2) /\ is_lub (fun zeta:R => 0 < zeta <= M - m /\ (forall z:R, Rabs (z - x) < zeta -> Rabs (f0 z - f0 x) < eps / 2)) del /\ disc x (mkposreal (del / 2) (H1 del)) y)). assert (H2 : forall x:R, (exists y : R, g x y) -> X x). { intros; elim H2; intros; unfold g in H3; elim H3; clear H3; intros H3 _; apply H3. } set (f' := mkfamily X g H2); unfold compact in H0; assert (H3 : covering_open_set X f'). ++ unfold covering_open_set; split. ** unfold covering; intros; exists x; simpl; unfold g; split. { assumption. } assert (H4 := H _ H3); unfold continuity_pt in H4; unfold continue_in in H4; unfold limit1_in in H4; unfold limit_in in H4; simpl in H4; unfold Rdist in H4; elim (H4 (eps / 2) (H1 eps)); intros; set (E := fun zeta:R => 0 < zeta <= M - m /\ (forall z:R, Rabs (z - x) < zeta -> Rabs (f0 z - f0 x) < eps / 2)); assert (H6 : bound E). { unfold bound; exists (M - m); unfold is_upper_bound; unfold E; intros; elim H6; clear H6; intros H6 _; elim H6; clear H6; intros _ H6; apply H6. } assert (H7 : exists x : R, E x). { elim H5; clear H5; intros; exists (Rmin x0 (M - m)); unfold E; intros; split;[ split|]. - unfold Rmin; case (Rle_dec x0 (M - m)); intro. + apply H5. + apply Rlt_0_minus; apply Hyp. - apply Rmin_r. - intros; case (Req_dec x z); intro. + rewrite H9; unfold Rminus; rewrite Rplus_opp_r; rewrite Rabs_R0; apply (H1 eps). + apply H7; split. * unfold D_x, no_cond; split; [ trivial | assumption ]. * apply Rlt_le_trans with (Rmin x0 (M - m)); [ apply H8 | apply Rmin_l ]. } destruct (completeness _ H6 H7) as (x1,p). { cut (0 < x1 <= M - m). - intros (H8,H9); exists (mkposreal _ H8); split. + intros; cut (exists alp : R, Rabs (z - x) < alp <= x1 /\ E alp). * intros; elim H11; intros; elim H12; clear H12; intros; unfold E in H13; elim H13; intros; apply H15. elim H12; intros; assumption. * elim (classic (exists alp : R, Rabs (z - x) < alp <= x1 /\ E alp)); intro. -- assumption. -- assert (H12 := not_ex_all_not _ (fun alp:R => Rabs (z - x) < alp <= x1 /\ E alp) H11); unfold is_lub in p; elim p; intros; cut (is_upper_bound E (Rabs (z - x))). ++ intro; assert (H16 := H14 _ H15); elim (Rlt_irrefl _ (Rlt_le_trans _ _ _ H10 H16)). ++ unfold is_upper_bound; intros; unfold is_upper_bound in H13; assert (H16 := H13 _ H15); case (Rle_dec x2 (Rabs (z - x))); intro. ** assumption. ** elim (H12 x2); split; [ split; [ auto with real | assumption ] | assumption ]. + split. * apply p. * unfold disc; unfold Rminus; rewrite Rplus_opp_r; rewrite Rabs_R0; simpl; unfold Rdiv; apply Rmult_lt_0_compat; [ apply H8 | apply Rinv_0_lt_compat; prove_sup0 ]. - elim H7; intros; unfold E in H8; elim H8; intros H9 _; elim H9; intros H10 _; unfold is_lub in p; elim p; intros; unfold is_upper_bound in H12; unfold is_upper_bound in H11; split. + apply Rlt_le_trans with x2; [ assumption | apply (H11 _ H8) ]. + apply H12; intros; unfold E in H13; elim H13; intros; elim H14; intros; assumption. } ** { unfold family_open_set; intro; simpl; elim (classic (X x)); intro. - unfold g; unfold open_set; intros; elim H4; clear H4; intros _ H4; elim H4; clear H4; intros; elim H4; clear H4; intros; unfold neighbourhood; case (Req_dec x x0); intro. + exists (mkposreal _ (H1 x1)); rewrite <- H6; unfold included; intros; split. * assumption. * exists x1; split. -- apply H4. -- split. ++ elim H5; intros; apply H8. ++ apply H7. + set (d := x1 / 2 - Rabs (x0 - x)); assert (H7 : 0 < d). * unfold d; apply Rlt_0_minus; elim H5; clear H5; intros; unfold disc in H7; apply H7. * exists (mkposreal _ H7); unfold included; intros; split. { assumption. } exists x1; split. { apply H4. } elim H5; intros; split. { assumption. } unfold disc in H8; simpl in H8; unfold disc; simpl; unfold disc in H10; simpl in H10; apply Rle_lt_trans with (Rabs (x2 - x0) + Rabs (x0 - x)). { replace (x2 - x) with (x2 - x0 + (x0 - x)); [ apply Rabs_triang | ring ]. } replace (x1 / 2) with (d + Rabs (x0 - x)); [ idtac | unfold d; ring ]. do 2 rewrite <- (Rplus_comm (Rabs (x0 - x))); apply Rplus_lt_compat_l; apply H8. - apply open_set_P6 with (fun _:R => False). + apply open_set_P4. + unfold eq_Dom; unfold included; intros; split. * intros; elim H4. * intros; unfold g in H4; elim H4; clear H4; intros H4 _; elim H3; apply H4. } ++ elim (H0 _ H3); intros DF H4; unfold covering_finite in H4; elim H4; clear H4; intros; unfold family_finite in H5; unfold domain_finite in H5; unfold covering in H4; simpl in H4; simpl in H5; elim H5; clear H5; intros l H5; unfold intersection_domain in H5; cut (forall x:R, In x l -> exists del : R, 0 < del /\ (forall z:R, Rabs (z - x) < del -> Rabs (f0 z - f0 x) < eps / 2) /\ included (g x) (fun z:R => Rabs (z - x) < del / 2)). ** { intros; assert (H7 := Rlist_P1 l (fun x del:R => 0 < del /\ (forall z:R, Rabs (z - x) < del -> Rabs (f0 z - f0 x) < eps / 2) /\ included (g x) (fun z:R => Rabs (z - x) < del / 2)) H6); elim H7; clear H7; intros l' H7; elim H7; clear H7; intros; set (D := MinRlist l'); cut (0 < D / 2). - intro; exists (mkposreal _ H9); intros; assert (H13 := H4 _ H10); elim H13; clear H13; intros xi H13; assert (H14 : In xi l). + unfold g in H13; decompose [and] H13; elim (H5 xi); intros; apply H14; split; assumption. + elim (pos_Rl_P2 l xi); intros H15 _; elim (H15 H14); intros i H16; elim H16; intros; apply Rle_lt_trans with (Rabs (f0 x - f0 xi) + Rabs (f0 xi - f0 y)). * replace (f0 x - f0 y) with (f0 x - f0 xi + (f0 xi - f0 y)); [ apply Rabs_triang | ring ]. * rewrite <-(Rplus_half_diag eps); apply Rplus_lt_compat. -- assert (H19 := H8 i H17); elim H19; clear H19; intros; rewrite <- H18 in H20; elim H20; clear H20; intros; apply H20; unfold included in H21; apply Rlt_trans with (pos_Rl l' i / 2). ++ apply H21. elim H13; clear H13; intros; assumption. ++ unfold Rdiv; apply Rmult_lt_reg_l with 2. { prove_sup0. } rewrite Rmult_comm; rewrite Rmult_assoc; rewrite Rinv_l. { rewrite Rmult_1_r; pattern (pos_Rl l' i) at 1; rewrite <- Rplus_0_r; rewrite <-Rplus_diag; apply Rplus_lt_compat_l; apply H19. } discrR. -- assert (H19 := H8 i H17); elim H19; clear H19; intros; rewrite <- H18 in H20; elim H20; clear H20; intros; rewrite <- Rabs_Ropp; rewrite Ropp_minus_distr; apply H20; unfold included in H21; elim H13; intros; assert (H24 := H21 x H22); apply Rle_lt_trans with (Rabs (y - x) + Rabs (x - xi)). ++ replace (y - xi) with (y - x + (x - xi)); [ apply Rabs_triang | ring ]. ++ rewrite <-(Rplus_half_diag (pos_Rl l' i)); apply Rplus_lt_compat. ** apply Rlt_le_trans with (D / 2). { rewrite <- Rabs_Ropp; rewrite Ropp_minus_distr; apply H12. } unfold Rdiv; do 2 rewrite <- (Rmult_comm (/ 2)); apply Rmult_le_compat_l. { left; apply Rinv_0_lt_compat; prove_sup0. } unfold D; apply MinRlist_P1; elim (pos_Rl_P2 l' (pos_Rl l' i)); intros; apply H26; exists i; split; [ rewrite <- H7; assumption | reflexivity ]. ** assumption. - unfold Rdiv; apply Rmult_lt_0_compat; [ unfold D; apply MinRlist_P2; intros; elim (pos_Rl_P2 l' y); intros; elim (H10 H9); intros; elim H12; intros; rewrite H14; rewrite <- H7 in H13; elim (H8 x H13); intros; apply H15 | apply Rinv_0_lt_compat; prove_sup0 ]. } ** { intros; elim (H5 x); intros; elim (H8 H6); intros; set (E := fun zeta:R => 0 < zeta <= M - m /\ (forall z:R, Rabs (z - x) < zeta -> Rabs (f0 z - f0 x) < eps / 2)); assert (H11 : bound E). - unfold bound; exists (M - m); unfold is_upper_bound; unfold E; intros; elim H11; clear H11; intros H11 _; elim H11; clear H11; intros _ H11; apply H11. - assert (H12 : exists x : R, E x). { assert (H13 := H _ H9); unfold continuity_pt in H13; unfold continue_in in H13; unfold limit1_in in H13; unfold limit_in in H13; simpl in H13; unfold Rdist in H13; elim (H13 _ (H1 eps)); intros; elim H12; clear H12; intros; exists (Rmin x0 (M - m)); unfold E; intros; split. - split; [ unfold Rmin; case (Rle_dec x0 (M - m)); intro; [ apply H12 | apply Rlt_0_minus; apply Hyp ] | apply Rmin_r ]. - intros; case (Req_dec x z); intro. + rewrite H16; unfold Rminus; rewrite Rplus_opp_r; rewrite Rabs_R0; apply (H1 eps). + apply H14; split; [ unfold D_x, no_cond; split; [ trivial | assumption ] | apply Rlt_le_trans with (Rmin x0 (M - m)); [ apply H15 | apply Rmin_l ] ]. } destruct (completeness _ H11 H12) as (x0,p). cut (0 < x0 <= M - m). + intro; elim H13; clear H13; intros; exists x0; split. * assumption. * split. -- intros; cut (exists alp : R, Rabs (z - x) < alp <= x0 /\ E alp). ++ intros; elim H16; intros; elim H17; clear H17; intros; unfold E in H18; elim H18; intros; apply H20; elim H17; intros; assumption. ++ elim (classic (exists alp : R, Rabs (z - x) < alp <= x0 /\ E alp)); intro. { assumption. } assert (H17 := not_ex_all_not _ (fun alp:R => Rabs (z - x) < alp <= x0 /\ E alp) H16); unfold is_lub in p; elim p; intros; cut (is_upper_bound E (Rabs (z - x))). ** intro; assert (H21 := H19 _ H20); elim (Rlt_irrefl _ (Rlt_le_trans _ _ _ H15 H21)). ** unfold is_upper_bound; intros; unfold is_upper_bound in H18; assert (H21 := H18 _ H20); case (Rle_dec x1 (Rabs (z - x))); intro. { assumption. } elim (H17 x1); split. { split; [ auto with real | assumption ]. } assumption. -- unfold included, g; intros; elim H15; intros; elim H17; intros; decompose [and] H18; cut (x0 = x2). ++ intro; rewrite H20; apply H22. ++ unfold E in p; eapply is_lub_u. ** apply p. ** apply H21. + elim H12; intros; unfold E in H13; elim H13; intros H14 _; elim H14; intros H15 _; unfold is_lub in p; elim p; intros; unfold is_upper_bound in H16; unfold is_upper_bound in H17; split. * apply Rlt_le_trans with x1; [ assumption | apply (H16 _ H13) ]. * apply H17; intros; unfold E in H18; elim H18; intros; elim H19; intros; assumption. } Qed.
imports: Rbase Rfunctions Ranalysis1 RList List Classical_Prop Classical_Pred_Type