proposition: Lemma approx_maj : forall (Un:nat -> R) (pr:has_ub Un) (eps:R), 0 < eps -> exists k : nat, Rabs (lub Un pr - Un k) < eps.
proof: Proof. intros Un pr. pose (Vn := fix aux n := match n with S n' => if Rle_lt_dec (aux n') (Un n) then Un n else aux n' | O => Un O end). pose (In := fix aux n := match n with S n' => if Rle_lt_dec (Vn n) (Un n) then n else aux n' | O => O end). assert (VUI: forall n, Vn n = Un (In n)). { induction n. - easy. - simpl. destruct (Rle_lt_dec (Vn n) (Un (S n))) as [H1|H1]. + destruct (Rle_lt_dec (Un (S n)) (Un (S n))) as [H2|H2]. * easy. * elim (Rlt_irrefl _ H2). + destruct (Rle_lt_dec (Vn n) (Un (S n))) as [H2|H2]. * elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H2 H1)). * exact IHn. } assert (HubV : has_ub Vn). { destruct pr as (ub, Hub). exists ub. intros x (n, Hn). rewrite Hn, VUI. apply Hub. now exists (In n). } assert (HgrV : Un_growing Vn). { intros n. induction n. - simpl. destruct (Rle_lt_dec (Un O) (Un 1%nat)) as [H|_]. + exact H. + apply Rle_refl. - simpl. destruct (Rle_lt_dec (Vn n) (Un (S n))) as [H1|H1]. + destruct (Rle_lt_dec (Un (S n)) (Un (S (S n)))) as [H2|H2]. * exact H2. * apply Rle_refl. + destruct (Rle_lt_dec (Vn n) (Un (S (S n)))) as [H2|H2]. * exact H2. * apply Rle_refl. } destruct (ub_to_lub Vn HubV) as (l, Hl). unfold lub. destruct (ub_to_lub Un pr) as (l', Hl'). replace l' with l. - intros eps Heps. destruct (Un_cv_crit_lub Vn HgrV l Hl eps Heps) as (n, Hn). exists (In n). rewrite <- VUI. rewrite Rabs_minus_sym. apply Hn. apply Nat.le_refl. - apply Rle_antisym. + apply Hl. intros n (k, Hk). rewrite Hk, VUI. apply Hl'. now exists (In k). + apply Hl'. intros n (k, Hk). rewrite Hk. apply Rle_trans with (Vn k). * clear. induction k. -- apply Rle_refl. -- simpl. destruct (Rle_lt_dec (Vn k) (Un (S k))) as [H|H]. ++ apply Rle_refl. ++ now apply Rlt_le. * apply Hl. now exists k. Qed.
imports: Rbase Rfunctions Rseries Lia