proposition: Lemma ex_RInt_Reals_0 (f : R -> R) (a b : R) : ex_RInt f a b -> Riemann_integrable f a b.
proof: Proof. wlog: a b /(a < b) => [Hw | Hab ] Hex. case: (Rle_lt_dec a b) => Hab. case: (Rle_lt_or_eq_dec _ _ Hab) => {} Hab. by apply Hw. rewrite -Hab. by apply RiemannInt_P7. apply ex_RInt_swap in Hex ; apply RiemannInt_P1 ; by apply Hw. assert ({If : R | is_RInt f a b If}). exists (RInt f a b). exact: RInt_correct. case: H => If HIf. generalize (proj1 (filterlim_locally _ If) HIf). clear HIf. intros HIf. set (E := fun eps : posreal => (fun alpha => 0 < alpha <= b-a + 1 /\ forall ptd : SF_seq, pointed_subdiv ptd -> seq_step (SF_lx ptd) < alpha -> SF_h ptd = Rmin a b -> last (SF_h ptd) (SF_lx ptd) = Rmax a b -> Rabs (If - sign (b - a) * Riemann_sum f ptd) < eps)). have E_bnd : forall eps : posreal, bound (E eps). move => eps ; exists (b-a+1) => x [Hx _] ; by apply Hx. have E_ex : forall eps : posreal, exists x, (E eps x). move => eps ; case: (HIf eps) => {HIf} alpha HIf. exists (Rmin alpha (b-a + 1)) ; split. apply Rmin_case_strong => H. split. by apply alpha. exact: H. split. apply Rplus_le_lt_0_compat. by apply (Rminus_le_0 a b), Rlt_le. exact: Rlt_0_1. exact: Rle_refl. intros. rewrite Rabs_minus_sym. apply: HIf. move: H0 ; apply Rmin_case_strong. by []. move => Halp Hstep ; by apply Rlt_le_trans with (b-a+1). split. exact: H. split. exact: H1. exact: H2. set alpha := fun eps : posreal => proj1_sig (completeness (E eps) (E_bnd eps) (E_ex eps)). have Ealpha : forall eps : posreal, (E eps (alpha eps)). revert alpha ; move => /= eps. case: (E_ex eps) => alp H. case: completeness => alpha [ub lub] /= ; split. split. apply Rlt_le_trans with alp. by apply H. by apply ub. apply: lub => x [Hx _] ; by apply Hx. intros. apply Rnot_le_lt ; contradict H1. apply Rle_not_lt. apply: lub => x [Hx1 Hx2]. apply Rnot_lt_le ; contradict H1. by apply Rlt_not_le, Hx2. have Hn : forall eps : posreal, {n : nat | (b-a)/(INR n + 1) < alpha eps}. move => eps. have Hn : 0 <= (b-a)/(alpha eps). apply Rdiv_le_0_compat. by apply Rlt_le, Rgt_minus. by apply Ealpha. set n := (nfloor _ Hn). exists n. apply Rlt_div_l. by apply INRp1_pos. rewrite Rmult_comm ; apply Rlt_div_l. by apply Ealpha. rewrite /n /nfloor ; case: nfloor_ex => /= n' Hn'. by apply Hn'. rewrite /Riemann_integrable. suff H : forall eps : posreal, {phi : StepFun a b & {psi : StepFun a b | (forall t : R, Rmin a b <= t <= Rmax a b -> Rabs (f t - phi t) <= psi t) /\ Rabs (RiemannInt_SF psi) <= eps}}. move => eps ; set eps2 := pos_div_2 eps. case: (H eps2) => {H} phi [psi [H H0]]. exists phi ; exists psi ; split. exact: H. apply Rle_lt_trans with (1 := H0). apply Rminus_gt ; simpl ; field_simplify ; rewrite ?Rdiv_1 ; by apply eps2. move => eps ; set eps2 := pos_div_2 eps. case: (Hn eps2) => {Hn} n Hn. case: (Ealpha eps2) => {HIf} Halpha HIf. set phi := sf_SF_val_fun f a b n. exists phi. set psi1 := SF_sup_r (fun t => Rabs (f t - phi t)) a b n. have Haux : forall x, {i : nat | x = nth 0 (unif_part a b n) i /\ (i < size (unif_part a b n))%nat} + {(forall i, (i < size (unif_part a b n))%nat -> x <> nth 0 (unif_part a b n) i)}. move => x. have : {n0 : nat | x = nth 0 (unif_part a b n) n0 /\ (n0 < size (unif_part a b n))%nat} + {(forall n0 : nat, ~ (x = nth 0 (unif_part a b n) n0 /\ (n0 < size (unif_part a b n))%nat))}. apply (LPO (fun i => x = nth 0 (unif_part a b n) i /\ (i < size (unif_part a b n))%nat)). move => i. case: (Req_EM_T x (nth 0 (unif_part a b n) i)) => Hx. case: (lt_dec i (size (unif_part a b n))) => Hi. left ; split ; by []. right ; contradict Hi ; by apply Hi. right ; contradict Hx ; by apply Hx. case => [[i Hi] | Hx]. left ; by exists i. right => i Hi ; move: (Hx i) => {} Hx ; contradict Hx ; by split. set psi2_aux := fun x => match Haux x with | inleft Hi => Rabs (f x - phi x) - psi1 x | inright _ => 0 end. set psi2_ly := (SF_ly (SF_seq_f1 (fun _ => 0) (unif_part a b n))). have psi2_ad : adapted_couple psi2_aux a b (unif_part a b n) psi2_ly. split. by apply sorted_compat, unif_part_sort, Rlt_le. split. rewrite /Rmin ; case: Rle_dec (Rlt_le _ _ Hab) => //= _ _ ; field ; apply Rgt_not_eq ; by intuition. split. rewrite size_compat size_mkseq nth_compat nth_mkseq ?S_INR /=. rewrite /Rmax ; case: Rle_dec (Rlt_le _ _ Hab) => // _ _ ; field ; apply Rgt_not_eq ; by intuition. by []. split. rewrite !size_compat /psi2_ly. by rewrite (SF_ly_f1 (fun _ => 0)) size_belast' size_map. rewrite size_compat => i Hi. rewrite !nth_compat /psi2_ly (SF_ly_f1 (fun _ => 0)) => x Hx. rewrite /psi2_aux => {psi2_aux} ; case: Haux => [ [j [Hx' Hj]] | Hx' ]. rewrite Hx' in Hx |- * ; case: Hx => Hxi Hxj. case: (lt_dec i j) => Hij. contradict Hxj ; apply Rle_not_lt. apply sorted_incr. by apply unif_part_sort, Rlt_le. by []. by []. contradict Hxi ; apply Rle_not_lt. apply sorted_incr. by apply unif_part_sort, Rlt_le. by apply not_lt. by intuition. move: i Hi {Hx} ; elim: (unif_part a b n) => /= [ i Hi | x0]. by apply Nat.nlt_0_r in Hi. case => /= [ | x1 s] IH i Hi. by apply Nat.nlt_0_r in Hi. case: i Hi => /= [ | i] Hi. by []. by apply IH, Nat.succ_lt_mono. have psi2_is : IsStepFun psi2_aux a b. exists (unif_part a b n). exists psi2_ly. by []. set psi2 := mkStepFun psi2_is. set psi := mkStepFun (StepFun_P28 1 psi1 psi2). exists psi. have Hfin : forall i, (S i < size (unif_part a b n))%nat -> is_finite (Sup_fct (fun t0 : R => Rabs (f t0 - phi t0)) (nth 0 (unif_part a b n) i) (nth 0 (unif_part a b n) (S i))). case: (ex_RInt_ub f a b Hex) => M HM. case: (StepFun_bound phi) => M' HM'. have : exists m, forall x : R, Rmin a b <= x <= Rmax a b -> m <= phi x. case: (StepFun_bound (mkStepFun (StepFun_P28 (-1) (mkStepFun (StepFun_P4 a b 0)) phi))) => /= m' Hm'. exists (-m') => x Hx. replace (phi x) with (- (fct_cte 0 x + -1 * phi x)) by (rewrite /fct_cte /= ; ring). by apply Ropp_le_contravar, Hm'. case => m' Hm' i ; rewrite size_mkseq => Hi ; rewrite !nth_mkseq. rewrite /Sup_fct. have H : (a + INR i * (b - a) / (INR n + 1)) < (a + (INR (S i)) * (b - a) / (INR n + 1)). rewrite S_INR ; apply Rminus_gt ; field_simplify. rewrite ?Rdiv_1 Rplus_comm ; apply Rdiv_lt_0_compat. by apply Rgt_minus. by apply INRp1_pos. by apply Rgt_not_eq, INRp1_pos. move: (Rlt_not_eq _ _ H) ; case: Req_EM_T => // H0 _. rewrite /Rmin /Rmax ; case: Rle_dec (Rlt_le _ _ H) => // _ _. rewrite /Lub_Rbar ; case: ex_lub_Rbar ; case => [l | | ] [ub lub] /=. by []. case: (lub (Finite (Rmax (M - m') (-(-M - M'))))) => //. move => _ [x [-> Hx]]. apply Rabs_le_between_Rmax. suff H2 : Rmin a b <= x <= Rmax a b. split ; apply Rplus_le_compat, Ropp_le_contravar. apply Ropp_le_cancel, Rle_trans with (Rabs (f x)). by apply Rabs_maj2. rewrite Ropp_involutive ; by apply HM. by apply HM'. apply Rle_trans with (Rabs (f x)). by apply Rle_abs. by apply HM. by apply Hm'. rewrite /Rmin /Rmax ; case: Rle_dec (Rlt_le _ _ Hab) => // _ _ ; split ; apply Rlt_le. replace a with (a + INR O * (b - a) / (INR n + 1)) by (simpl ; field ; apply Rgt_not_eq, INRp1_pos). apply Rle_lt_trans with (2 := proj1 Hx). apply Rplus_le_compat_l, Rmult_le_compat_r. apply Rlt_le, Rinv_0_lt_compat ; by intuition. apply Rmult_le_compat_r. by apply Rlt_le, Rgt_minus. apply le_INR ; by intuition. replace b with (a + INR (S n) * (b - a) / (INR n + 1)) by (rewrite S_INR ; field ; apply Rgt_not_eq, INRp1_pos). apply Rlt_le_trans with (1 := proj2 Hx). apply Rplus_le_compat_l, Rmult_le_compat_r. apply Rlt_le, Rinv_0_lt_compat ; by intuition. apply Rmult_le_compat_r. by apply Rlt_le, Rgt_minus. apply le_INR ; by intuition. move: (a + INR i * (b - a) / (INR n + 1)) (a + INR (S i) * (b - a) / (INR n + 1)) ub H. clear => a0 b0 ub H. specialize (ub (Rabs (f ((a0 + b0) / 2) - phi ((a0 + b0) / 2)))) ; simpl in ub. assert (exists x : R, Rabs (f ((a0 + b0) / 2) - phi ((a0 + b0) / 2)) = Rabs (f x - phi x) /\ a0 < x < b0). eexists ; split => //. lra. by []. apply SSR_leq ; by intuition. apply SSR_leq ; by intuition. have Hfin' : forall t, is_finite (SF_sup_fun (fun t : R => Rabs (f t - phi t)) a b n t). rewrite /SF_sup_fun ; case: Rle_dec (Rlt_le _ _ Hab) => // _ _. rewrite /SF_fun /SF_sup_seq. case: (unif_part a b n) Hfin => [ | x0 sx] /=. move => _ t ; by case: Rle_dec. case: sx => [ | x1 sx] /=. move => _ t ; by case: Rle_dec. move => H t. case: Rlt_dec => Hx0. by []. elim: sx x0 x1 H Hx0 => [ | x2 sx IH] x0 x1 /= H Hx0. case: Rle_dec => Hx1. apply (H O) ; by intuition. by []. case: Rlt_dec => Hx1. apply (H O) ; by intuition. apply IH. move => i Hi ; apply (H (S i) (proj1 (Nat.succ_lt_mono _ _) Hi)). exact: Hx1. split. move => t Ht_ab. move: Ht_ab ; rewrite /Rmin /Rmax ; case: Rle_dec (Rlt_le _ _ Hab) => // _ _ Ht_ab. rewrite /= /psi2_aux /= ; case: (Haux t) => [ [i Hi] | Hi ] ; ring_simplify. exact: Rle_refl. change (Rbar_le (Rabs (f t - phi t)) (real (SF_sup_fun (fun t0 : R => Rabs (f t0 - phi t0)) a b n t))). rewrite Hfin'. rewrite /SF_sup_fun ; case: Rle_dec (Rlt_le _ _ Hab) => // _ _. rewrite /SF_fun /SF_sup_seq. move: (unif_part_sort a b n (Rlt_le _ _ Hab)). move: Ht_ab. pattern b at 1 ; replace b with (last 0 (unif_part a b n)). pattern a at 1 ; replace a with (head 0 (unif_part a b n)). have : (0 < size (unif_part a b n))%nat. rewrite size_mkseq ; exact: Nat.lt_0_succ. case: (unif_part a b n) Hi => [ | x0 sx] Hi Hsx Ht_ab Hsort /=. by apply Nat.lt_irrefl in Hsx. clear Hsx. case: sx Hsort Hi Ht_ab => [ | x1 sx] Hsort /= Hi [Ht_a Ht_b]. move: (Rle_antisym _ _ Ht_b Ht_a) => Ht. contradict Ht ; apply (Hi O (Nat.lt_succ_diag_r _)). apply Rle_not_lt in Ht_a. case: Rlt_dec => // _. elim: sx x0 x1 Hsort Ht_a Ht_b Hi => [ | x2 sx IH] x0 x1 Hsort /= Ht_a Ht_b Hi. case: Rle_dec => // _. rewrite /Sup_fct /Lub_Rbar. have H : x0 < x1. apply Rlt_trans with t. apply Rnot_lt_le in Ht_a ; case: Ht_a => Ht_a. by []. contradict Ht_a ; apply sym_not_eq, (Hi O). by apply Nat.lt_0_succ. case: Ht_b => Ht_b. by []. contradict Ht_b ; apply (Hi 1%nat). by apply Nat.lt_succ_diag_r. move: (Rlt_not_eq _ _ H) ; case: Req_EM_T => // H0 _. case: ex_lub_Rbar => l lub /=. apply lub ; exists t ; split. by []. rewrite /Rmin /Rmax ; case: Rle_dec (proj1 Hsort) => // _ _ ; split. apply Rnot_lt_le in Ht_a ; case: Ht_a => Ht_a. by []. contradict Ht_a ; apply sym_not_eq, (Hi O). by apply Nat.lt_0_succ. case: Ht_b => Ht_b. by []. contradict Ht_b ; apply (Hi 1%nat). by apply Nat.lt_succ_diag_r. case: Rlt_dec => Hx1. rewrite /Sup_fct /Lub_Rbar. have H : x0 < x1. apply Rlt_trans with t. apply Rnot_lt_le in Ht_a ; case: Ht_a => Ht_a. by []. contradict Ht_a ; apply sym_not_eq, (Hi O). by apply Nat.lt_0_succ. by apply Hx1. move: (Rlt_not_eq _ _ H) ; case: Req_EM_T => // H0 _. case: ex_lub_Rbar => l lub /=. apply lub ; exists t ; split. by []. rewrite /Rmin /Rmax ; case: Rle_dec (proj1 Hsort) => // _ _ ; split. apply Rnot_lt_le in Ht_a ; case: Ht_a => Ht_a. by []. contradict Ht_a ; apply sym_not_eq, (Hi O). by apply Nat.lt_0_succ. by []. apply IH. exact: (proj2 Hsort). exact: Hx1. exact: Ht_b. move => j Hj ; apply (Hi (S j) (proj1 (Nat.succ_lt_mono _ _) Hj)). apply head_unif_part. apply last_unif_part. assert (forall g : R -> R -> R, let ptd := SF_seq_f2 g (unif_part a b n) in pointed_subdiv ptd -> Rabs (If - sign (b-a) * Riemann_sum f ptd) < eps2). move => g ptd Hptd. apply HIf. exact: Hptd. rewrite SF_lx_f2. suff : forall i, (S i < size (unif_part a b n))%nat -> nth 0 (unif_part a b n) (S i) - nth 0 (unif_part a b n) i = (b-a)/(INR n + 1). elim: (unif_part a b n) => /= [ | h0 t IH]. move => _ ; by apply Ealpha. case: t IH => /= [ | h1 t] IH Hnth. by apply Ealpha. replace (seq_step _) with (Rmax (Rabs (h1 - h0)) (seq_step (h1::t))) by auto. apply (Rmax_case_strong (Rabs (h1 - h0))) => /= _. rewrite (Hnth O (proj1 (Nat.succ_lt_mono _ _) (Nat.lt_0_succ _))). rewrite Rabs_right. exact: Hn. apply Rle_ge, Rdiv_le_0_compat. by apply Rlt_le, Rgt_minus. by intuition. apply IH => i Hi. by apply (Hnth (S i)); apply ->Nat.succ_lt_mono. move => i ; rewrite size_mkseq => Hi ; rewrite !nth_mkseq. rewrite S_INR ; field ; apply Rgt_not_eq ; by intuition. apply SSR_leq ; by intuition. apply SSR_leq ; by intuition. by apply Nat.lt_0_succ. rewrite -> Rmin_left by now apply Rlt_le. apply head_unif_part. rewrite -nth_last SF_lx_f2. change (head 0 (unif_part a b n) :: behead (unif_part a b n)) with (unif_part a b n). rewrite -> Rmax_right by now apply Rlt_le. rewrite size_mkseq nth_mkseq. simpl ssrnat.predn ; rewrite S_INR ; field ; apply Rgt_not_eq ; by intuition. simpl ; apply SSR_leq, Nat.le_refl. by apply Nat.lt_0_succ. move: H => {} HIf. assert (forall g1 g2 : R -> R -> R, let ptd1 := SF_seq_f2 g1 (unif_part a b n) in let ptd2 := SF_seq_f2 g2 (unif_part a b n) in pointed_subdiv ptd1 -> pointed_subdiv ptd2 -> Rabs (Riemann_sum f ptd1 - Riemann_sum f ptd2) < eps). move => g1 g2 ptd1 ptd2 H1 H2. replace (Riemann_sum f ptd1 - Riemann_sum f ptd2) with ((If - sign (b - a) * Riemann_sum f ptd2) - (If - sign (b - a) * Riemann_sum f ptd1)). apply Rle_lt_trans with (1 := Rabs_triang _ _). rewrite Rabs_Ropp (double_var eps) ; apply Rplus_lt_compat ; by apply HIf. rewrite -> sign_eq_1 by exact: Rlt_Rminus. ring. move: H => {} HIf. rewrite /Riemann_sum in HIf. assert (forall g1 g2 : R -> R -> R, let ptd1 := SF_seq_f2 g1 (unif_part a b n) in let ptd2 := SF_seq_f2 g2 (unif_part a b n) in pointed_subdiv ptd1 -> pointed_subdiv ptd2 -> Rabs (Riemann_sum (fun x => x) (SF_seq_f2 (fun x y => f (g1 x y) - f (g2 x y)) (unif_part a b n))) < eps). move => g1 g2 ptd1 pdt2 H1 H2. replace (Riemann_sum _ _ : R) with (Riemann_sum f (SF_seq_f2 g1 (unif_part a b n)) - Riemann_sum f (SF_seq_f2 g2 (unif_part a b n))). apply HIf. exact: H1. exact: H2. elim: (unif_part a b n) => /= [ | h0]. rewrite /Riemann_sum /= /plus /zero /= ; ring. case => /= [ | h1 t] IH. rewrite /Riemann_sum /= /plus /zero /= ; ring. rewrite !(SF_cons_f2 _ h0) /= ; try by intuition. rewrite !Riemann_sum_cons /= -IH /plus /scal /= /mult /= ; ring. move:H => {} HIf. assert (forall g1 g2 : R -> R -> R, let ptd1 := SF_seq_f2 g1 (unif_part a b n) in let ptd2 := SF_seq_f2 g2 (unif_part a b n) in pointed_subdiv ptd1 -> pointed_subdiv ptd2 -> Riemann_sum id (SF_seq_f2 (fun x y : R => Rabs (f (g1 x y) - f (g2 x y))) (unif_part a b n)) < eps). move => g1 g2 ptd1 ptd2 H1 H2. set h1 := fun x y => match Rle_dec (f (g1 x y)) (f (g2 x y)) with | left _ => g2 x y | right _ => g1 x y end. set h2 := fun x y => match Rle_dec (f (g1 x y)) (f (g2 x y)) with | left _ => g1 x y | right _ => g2 x y end. replace (Riemann_sum id (SF_seq_f2 (fun x y : R => Rabs (f (g1 x y) - f (g2 x y))) (unif_part a b n))) with (Riemann_sum id (SF_seq_f2 (fun x y : R => (f (h1 x y) - f (h2 x y))) (unif_part a b n))). apply Rle_lt_trans with (1 := Rle_abs _). apply HIf. revert ptd1 ptd2 H1 H2. elim: (unif_part a b n) (0) => [z /= _ _ | x0]. move => i ; rewrite /SF_size /= => Hi ; by apply Nat.nlt_0_r in Hi. case => [ | x1 t] /= IH z H1 H2. move => i ; rewrite /SF_size /= => Hi ; by apply Nat.nlt_0_r in Hi. move: H1 H2 ; rewrite !(SF_cons_f2 _ x0) /= ; try by intuition. move => H1 H2 ; case => [ | i] /= Hi. rewrite /h1 ; case: Rle_dec => //= _. apply (H2 O (Nat.lt_0_succ _)). apply (H1 O (Nat.lt_0_succ _)). apply (IH x0 (ptd_cons _ _ H1) (ptd_cons _ _ H2)). apply Nat.succ_lt_mono, Hi. revert ptd1 ptd2 H1 H2. elim: (unif_part a b n) (0) => [z /= _ _ | x0]. move => i ; rewrite /SF_size /= => Hi ; by apply Nat.nlt_0_r in Hi. case => [ | x1 t] /= IH z H1 H2. move => i ; rewrite /SF_size /= => Hi ; by apply Nat.nlt_0_r in Hi. move: H1 H2 ; rewrite !(SF_cons_f2 _ x0) /= ; try by intuition. move => H1 H2 ; case => [ | i] /= Hi. rewrite /h2 ; case: Rle_dec => //= _. apply (H1 O (Nat.lt_0_succ _)). apply (H2 O (Nat.lt_0_succ _)). apply (IH x0 (ptd_cons _ _ H1) (ptd_cons _ _ H2)). apply Nat.succ_lt_mono, Hi. elim: (unif_part a b n) (0) => [x0 | x0]. by rewrite /Riemann_sum /= . case => [ | x1 t] IH z. by rewrite /Riemann_sum /= . rewrite !(SF_cons_f2 _ x0) /= ; try by intuition. rewrite !Riemann_sum_cons /=. apply f_equal2. rewrite /h1 /h2 /id ; case: Rle_dec => H0. rewrite Rabs_left1. apply f_equal. simpl ; ring. by apply Rle_minus. rewrite Rabs_right. apply f_equal. simpl ; ring. by apply Rgt_ge, Rgt_minus, Rnot_le_lt. by apply IH. move: H => {} HIf. assert (forall g : R -> R -> R, (forall i j, (S i < size (unif_part a b n))%nat -> (j < size (unif_part a b n))%nat -> g (nth 0 (unif_part a b n) i) (nth 0 (unif_part a b n) (S i)) <> nth 0 (unif_part a b n) j) -> let ptd := SF_seq_f2 g (unif_part a b n) in pointed_subdiv ptd -> Riemann_sum id (SF_seq_f2 (fun x y : R => Rabs (f (g x y) - phi (g x y))) (unif_part a b n)) < eps). move => g1 Hg1 ptd1 H1. rewrite /phi /sf_SF_val_fun ; case: Rle_dec (Rlt_le _ _ Hab) => //= _ _. move: (unif_part_nat a b n) => Hp. set h := fun t => match Rle_dec a t with | right _ => t | left Ha => match Rle_dec t b with | right _ => t | left Hb => match Hp t (conj Ha Hb) with | inleft H => (a + (INR (proj1_sig H) + /2) * (b - a) / (INR n + 1)) | inright _ => (a + (INR n + /2) * (b - a) / (INR n + 1)) end end end. set g2 := fun x y => h (g1 x y). set ptd2 := SF_seq_f2 g2 (unif_part a b n). have H2 : pointed_subdiv ptd2. move => i ; move: (H1 i) => {H1}. rewrite !SF_lx_f2 ; (try by apply Nat.lt_0_succ) ; rewrite !SF_ly_f2 !SF_size_f2 size_mkseq. move => H1 Hi ; move: (H1 Hi) => {H1}. simpl in Hi. rewrite !nth_behead !(nth_pairmap 0). replace (nth 0 (0 :: unif_part a b n) (S i)) with (nth 0 (unif_part a b n) i) by auto. rewrite /g2 /h => {h g2 ptd2 ptd1} H1. case: Rle_dec => Ha. case: Rle_dec => Hb. case: Hp => [ [j [Ht Hj]] | Ht] ; simpl proj1_sig. suff Hij : j = i. rewrite Hij in Ht, Hj |- * => {j Hij}. rewrite !nth_mkseq. rewrite S_INR. split ; simpl ; apply Rminus_le_0 ; field_simplify. rewrite ?Rdiv_1 ; apply Rdiv_le_0_compat. rewrite Rplus_comm -Rminus_le_0 ; exact: (Rlt_le _ _ Hab). generalize (pos_INR n) ; lra. apply Rgt_not_eq ; by intuition. rewrite ?Rdiv_1 ; apply Rdiv_le_0_compat. rewrite Rplus_comm -Rminus_le_0 ; exact: (Rlt_le _ _ Hab). generalize (pos_INR n) ; lra. apply Rgt_not_eq ; by intuition. apply SSR_leq ; rewrite size_mkseq in Hi, Hj ; by intuition. apply SSR_leq ; rewrite size_mkseq in Hi, Hj ; by intuition. apply Nat.le_antisymm ; apply not_lt. have Hij : nth 0 (unif_part a b n) j < nth 0 (unif_part a b n) (S i). apply Rle_lt_trans with (g1 (nth 0 (unif_part a b n) i) (nth 0 (unif_part a b n) (S i))). by apply Ht. case: (proj2 H1) => {} H1. exact: H1. contradict H1 ; apply (Hg1 i (S i)). rewrite size_mkseq ; by apply ->Nat.succ_lt_mono. rewrite size_mkseq ; by apply ->Nat.succ_lt_mono. contradict Hij. apply Rle_not_lt, sorted_incr. apply unif_part_sort, Rlt_le, Hab. by []. by intuition. move: (Rle_lt_trans _ _ _ (proj1 H1) (proj2 Ht)) => Hij. contradict Hij. apply Rle_not_lt, sorted_incr. apply unif_part_sort, Rlt_le, Hab. by []. rewrite size_mkseq ; by intuition. suff : i = n. move => ->. rewrite !nth_mkseq ?S_INR. split ; simpl ; apply Rminus_le_0 ; field_simplify. rewrite ?Rdiv_1 ; apply Rdiv_le_0_compat. rewrite Rplus_comm -Rminus_le_0 ; exact: (Rlt_le _ _ Hab). generalize (pos_INR n) ; lra. apply Rgt_not_eq ; by intuition. rewrite ?Rdiv_1 ; apply Rdiv_le_0_compat. rewrite Rplus_comm -Rminus_le_0 ; exact: (Rlt_le _ _ Hab). generalize (pos_INR n) ; lra. apply Rgt_not_eq ; by intuition. apply SSR_leq ; by intuition. apply SSR_leq ; by intuition. apply Nat.le_antisymm ; apply not_lt. have Hij : nth 0 (unif_part a b n) i < nth 0 (unif_part a b n) (S n). apply Rle_lt_trans with (g1 (nth 0 (unif_part a b n) i) (nth 0 (unif_part a b n) (S i))). by apply H1. case: (proj2 Ht) => {} Ht. exact: Ht. contradict Ht ; apply Hg1. rewrite size_mkseq ; by apply ->Nat.succ_lt_mono. rewrite size_mkseq ; by apply Nat.lt_succ_diag_r. contradict Hij. apply Rle_not_lt, sorted_incr. apply unif_part_sort, Rlt_le , Hab. by intuition. rewrite size_mkseq ; by intuition. have Hij : nth 0 (unif_part a b n) (n) < nth 0 (unif_part a b n) (S i). apply Rle_lt_trans with (g1 (nth 0 (unif_part a b n) i) (nth 0 (unif_part a b n) (S i))). by apply Ht. case: (proj2 H1) => {} H1. exact: H1. contradict H1 ; apply Hg1. rewrite size_mkseq ; by intuition. rewrite size_mkseq ; by intuition. contradict Hij. apply Rle_not_lt, sorted_incr. apply unif_part_sort, Rlt_le, Hab. by []. rewrite size_mkseq ; by intuition. exact: H1. exact: H1. apply SSR_leq ; rewrite size_mkseq ; by intuition. apply SSR_leq ; rewrite size_mkseq ; by intuition. move: (HIf g1 g2 H1 H2). replace (SF_seq_f2 (fun x y : R => Rabs (f (g1 x y) - SF_val_fun f a b n (g1 x y))) (unif_part a b n)) with (SF_seq_f2 (fun x y : R => Rabs (f (g1 x y) - f (g2 x y))) (unif_part a b n)). by []. have H0 : forall t, a <= t <= b -> SF_val_fun f a b n t = f (h t). move => t Ht. rewrite /h SF_val_fun_rw. case: Ht => Ha Hb. case: Rle_dec => // Ha'. case: Rle_dec => // Hb'. case: unif_part_nat => [ [i [Ht Hi]] | Ht] ; case: Hp {h g2 ptd2 H2} => [ [j [Ht' Hj]] | Ht'] ; simpl proj1_sig. apply (f_equal (fun i => f (a + (INR i + /2) * (b - a) / (INR n + 1)))). apply Nat.le_antisymm ; apply not_lt. move: (Rle_lt_trans _ _ _ (proj1 Ht) (proj2 Ht')) => Hij ; contradict Hij. apply Rle_not_lt, sorted_incr. apply unif_part_sort, Rlt_le, Hab. by []. by intuition. move: (Rle_lt_trans _ _ _ (proj1 Ht') (proj2 Ht)) => Hij ; contradict Hij. apply Rle_not_lt, sorted_incr. by apply unif_part_sort, Rlt_le. by []. by intuition. absurd (i < n)%nat. move: (Rle_lt_trans _ _ _ (proj1 Ht') (proj2 Ht)) => Hij ; contradict Hij. apply Rle_not_lt, sorted_incr. by apply unif_part_sort, Rlt_le. by []. rewrite size_mkseq ; by intuition. rewrite size_mkseq in Hi ; by intuition. absurd (j < n)%nat. move: (Rle_lt_trans _ _ _ (proj1 Ht) (proj2 Ht')) => Hij ; contradict Hij. apply Rle_not_lt, sorted_incr. by apply unif_part_sort, Rlt_le. by []. rewrite size_mkseq ; by intuition. rewrite size_mkseq in Hj ; by intuition. by []. rewrite /g2. have : forall i, (i < size (unif_part a b n))%nat -> a <= nth 0 (unif_part a b n) i <= b. move => i ; rewrite size_mkseq => Hi ; rewrite nth_mkseq. pattern b at 3 ; replace b with (a + (INR n + 1) * (b - a) / (INR n + 1)) by (field ; apply Rgt_not_eq ; intuition). pattern a at 1 ; replace a with (a + 0 * (b - a) / (INR n + 1)) by (field ; apply Rgt_not_eq ; intuition). apply Rgt_minus in Hab. split ; apply Rplus_le_compat_l ; repeat apply Rmult_le_compat_r ; try by intuition. rewrite -S_INR ; apply le_INR ; by intuition. by apply SSR_leq. revert ptd1 H1 ; elim: (unif_part a b n) => [ ptd1 H1 Hnth | x0 ]. by []. case => [ | x1 s] IH ptd1 H1 Hnth. by []. revert ptd1 H1 ; rewrite !(SF_cons_f2 _ x0) /= ; try by intuition. intro ; apply (f_equal2 (fun x y => SF_cons (x0, Rabs (f (g1 x0 x1) - x)) y)). apply sym_equal, H0. move: (H1 O (Nat.lt_0_succ _)) (Hnth O (Nat.lt_0_succ _)) (Hnth 1%nat (proj1 (Nat.succ_lt_mono _ _) (Nat.lt_0_succ _))) => /= ; intuition. by apply Rle_trans with x0. by apply Rle_trans with x1. apply (IH (ptd_cons _ _ H1)). move => i Hi ; apply (Hnth (S i)) ; simpl in Hi |- * ; by apply ->Nat.succ_lt_mono. move: H => {} HIf. rewrite Rabs_right. replace (RiemannInt_SF psi) with (Riemann_sum id (SF_seq_f2 (fun x y : R => real (Sup_fct (fun t => Rabs (f t - phi t)) x y)) (unif_part a b n))). set (F := fun s val => exists g : R -> R -> R, (forall (i j : nat), (S i < size s)%nat -> (j < size s)%nat -> g (nth 0 s i) (nth 0 s (S i)) <> nth 0 s j) /\ (let ptd := SF_seq_f2 g s in pointed_subdiv ptd) /\ Riemann_sum id (SF_seq_f2 (fun x y : R => Rabs (f (g x y) - phi (g x y))) s) = val). cut (is_lub (F (unif_part a b n)) (Riemann_sum id (SF_seq_f2 (fun x y : R => real (Sup_fct (fun t : R => Rabs (f t - phi t)) x y)) (unif_part a b n)))) => [ Hlub | ]. apply Hlub => val [g [Hnth [H0 Hval]]]. apply Rlt_le ; rewrite -Hval. apply HIf. exact: Hnth. exact: H0. 2: { rewrite StepFun_P30. replace (RiemannInt_SF psi2) with 0. rewrite Rmult_0_r Rplus_0_r /RiemannInt_SF SF_sup_subdiv SF_sup_subdiv_val ; case: Rle_dec (Rlt_le _ _ Hab) => // _ _. elim: (unif_part a b n) (unif_part_sort a b n (Rlt_le _ _ Hab)) => [ Hsort | x0 ]. by []. case => [ | x1 s] IH Hsort. by []. rewrite SF_cons_f2 /=. rewrite Riemann_sum_cons /=. rewrite Rmult_comm. by apply f_equal, IH, Hsort. exact: Nat.lt_0_succ. rewrite /RiemannInt_SF ; case: Rle_dec (Rlt_le _ _ Hab) => // _ _. rewrite (StepFun_P17 (StepFun_P1 psi2) psi2_ad). clear psi2_ad. revert psi2_ly ; elim: (unif_part a b n) => /= [ | x0]. by []. case => /= [ | x1 s] IH. by []. rewrite -IH ; ring. } 2: { rewrite StepFun_P30. replace (RiemannInt_SF psi2) with 0. rewrite Rmult_0_r Rplus_0_r ; rewrite /RiemannInt_SF SF_sup_subdiv SF_sup_subdiv_val ; case: Rle_dec (Rlt_le _ _ Hab) => // _ _. elim: (unif_part a b n) (unif_part_sort a b n (Rlt_le _ _ Hab)) => [ Hsort /= | x0]. by apply Rge_refl. case => [ | x1 s] IH Hsort /=. by apply Rge_refl. apply Rle_ge, Rplus_le_le_0_compat. apply Rmult_le_pos. rewrite /Sup_fct /Lub_Rbar. case: Req_EM_T => Hx0. by apply Rle_refl. case: ex_lub_Rbar ; case => [l | | ] [ub lub] /=. apply Rle_trans with (Rabs (f ((x0+x1)/2) - phi ((x0+x1)/2))). apply Rabs_pos. apply ub. exists ((x0+x1)/2) ; split. by []. rewrite /Rmin /Rmax ; case: Rle_dec (proj1 Hsort) => // _ _. pattern x1 at 3 ; replace x1 with ((x1 + x1)/2) by field. pattern x0 at 1 ; replace x0 with ((x0 + x0)/2) by field. split ; apply Rmult_lt_compat_r. by apply Rinv_0_lt_compat, Rlt_R0_R2. apply Rplus_lt_compat_l ; by case: (proj1 Hsort). by apply Rinv_0_lt_compat, Rlt_R0_R2. apply Rplus_lt_compat_r ; by case: (proj1 Hsort). apply Rle_refl. apply Rle_refl. apply -> Rminus_le_0 ; apply Hsort. apply Rge_le, IH, Hsort. rewrite /RiemannInt_SF ; case: Rle_dec (Rlt_le _ _ Hab) => // _ _. rewrite (StepFun_P17 (StepFun_P1 psi2) psi2_ad). clear psi2_ad. revert psi2_ly ; elim: (unif_part a b n) => /= [ | x0]. by []. case => /= [ | x1 s] IH. by []. rewrite -IH ; ring. } move: Hfin. have : sorted Rlt (unif_part a b n). apply sorted_nth => i. rewrite size_mkseq => Hi x0 ; rewrite !nth_mkseq. apply Rminus_gt ; rewrite S_INR ; field_simplify. rewrite ?Rdiv_1. apply Rdiv_lt_0_compat. rewrite Rplus_comm ; by apply Rgt_minus. by intuition. apply Rgt_not_eq ; by intuition. apply SSR_leq ; by intuition. apply SSR_leq ; by intuition. elim: (unif_part a b n) (unif_part_sort a b n (Rlt_le _ _ Hab)) => [ Hle Hlt Hfin | x1]. split ; rewrite /Riemann_sum /=. move => val [g [Hnth [Hptd Hval]]]. rewrite -Hval ; by apply Rle_refl. move => ub Hub ; apply: Hub. exists (fun _ _ => 0). split. move => i j Hi Hj ; by apply Nat.nlt_0_r in Hi. split. move => ptd i Hi ; by apply Nat.nlt_0_r in Hi. split. case => [ | x2 s] IH Hle Hlt Hfin. split ; rewrite /Riemann_sum /=. move => val [g [Hnth [Hptd Hval]]]. rewrite -Hval ; by apply Rle_refl. move => ub Hub ; apply: Hub. exists (fun _ _ => 0). split. move => i j Hi Hj. simpl in Hi ; by apply Nat.succ_lt_mono, Nat.nlt_0_r in Hi. split. move => ptd i Hi ; by apply Nat.nlt_0_r in Hi. split. rewrite SF_cons_f2 /= ; last by apply Nat.lt_0_succ. rewrite Riemann_sum_cons /=. set F0 := fun x => exists t, x1 < t < x2 /\ x = Rabs (f t - phi t) * (x2 - x1). set set_plus := fun (F : R -> Prop) (G : R -> Prop) (x : R) => exists y, exists z, x = y + z /\ F y /\ G z. suff H0 : forall (x : R), F [:: x1, x2 & s] x <-> (set_plus (F0) (F (x2::s))) x. cut (is_lub (set_plus (F0) (F (x2::s))) (real (Sup_fct (fun t : R => Rabs (f t - phi t)) x1 x2) * (x2 - x1) + Riemann_sum id (SF_seq_f2 (fun x y : R => real (Sup_fct (fun t : R => Rabs (f t - phi t)) x y)) (x2 :: s)))) => [H1 | ]. split. move => x Hx. rewrite /plus /scal /= /mult /= Rmult_comm. by apply H1, H0. move => ub Hub. rewrite /plus /scal /= /mult /= Rmult_comm. apply H1 => x Hx ; by apply Hub, H0. suff H_F0 : is_lub (F0) (real (Sup_fct (fun t : R => Rabs (f t - phi t)) x1 x2) * (x2 - x1)). have Hfin0 : (forall i : nat, (S i < size (x2 :: s))%nat -> is_finite (Sup_fct (fun t0 : R => Rabs (f t0 - phi t0)) (nth 0 (x2 :: s) i) (nth 0 (x2 :: s) (S i)))). move => i /= Hi ; move: (Hfin (S i) (proj1 (Nat.succ_lt_mono _ _) Hi)) => /= {Hfin}. by []. move: H_F0 (IH (proj2 Hle) (proj2 Hlt) Hfin0). move: (F0 (pos_div_2 eps)) (F (x2::s) (pos_div_2 eps)) (real (Sup_fct (fun t : R => Rabs (f t - phi t)) x1 x2) * (x2 - x1)) (Riemann_sum id (SF_seq_f2 (fun x4 y : R => real (Sup_fct (fun t : R => Rabs (f t - phi t)) x4 y)) (x2 :: s))). move => F1 F2 l1 l2 Hl1 Hl2. split. move => _ [y [z [-> Hx]]]. apply Rplus_le_compat. by apply Hl1, Hx. by apply Hl2, Hx. move => ub Hub. replace ub with ((ub-l2) + l2) by ring. apply Rplus_le_compat_r. apply Hl1 => y Hy. replace y with (l2 + (y - l2)) by ring. replace (ub-l2) with ((ub - y) + (y - l2)) by ring. apply Rplus_le_compat_r. apply Hl2 => z Hz. replace z with ((y+z) - y) by ring. apply Rplus_le_compat_r. apply Hub. exists y ; exists z ; by intuition. move: (Hfin O (proj1 (Nat.succ_lt_mono _ _) (Nat.lt_0_succ _))). rewrite /Sup_fct /=. move: (Rlt_not_eq _ _ (proj1 Hlt)). case: Req_EM_T => // Hx1 _. rewrite /Lub_Rbar ; case: ex_lub_Rbar ; case => [l | | ] [ub lub] ; simpl. split. move => _ [t [Ht ->]]. apply Rmult_le_compat_r. apply -> Rminus_le_0 ; apply Hle. apply ub ; exists t ; split. by []. rewrite /Rmin /Rmax ; case: Rle_dec (proj1 Hle) => // _ _ ; by intuition. move => b0 Hb0. move: (Rgt_minus _ _ (proj1 Hlt)) => H1. replace b0 with ((b0 / (x2 - x1)) * (x2 - x1)) by (field ; by apply Rgt_not_eq). apply Rmult_le_compat_r. by apply Rlt_le. change (Rbar_le l (b0 / (x2 - x1))). apply lub => _ [t [-> Ht]]. replace (Rabs (f t - phi t)) with ((Rabs (f t - phi t) * (x2 - x1)) / (x2 - x1)) by (field ; by apply Rgt_not_eq). apply Rmult_le_compat_r. by apply Rlt_le, Rinv_0_lt_compat. apply Hb0 ; exists t. split. move: Ht ; rewrite /Rmin /Rmax ; case: Rle_dec (proj1 Hle) => //. by []. by []. by []. move => val ; split => Hval. case: Hval => g [Hnth [Hptd <-]] {val}. rewrite SF_cons_f2 /=. rewrite Riemann_sum_cons /=. exists (Rabs (f (g x1 x2) - phi (g x1 x2)) * (x2 - x1)). exists (Riemann_sum id (SF_seq_f2 (fun x y : R => Rabs (f (g x y) - phi (g x y))) (x2 :: s))). split. rewrite Rmult_comm. by []. split. exists (g x1 x2) ; split. case: (Hptd O) => /=. rewrite SF_size_f2 /= ; exact: Nat.lt_0_succ. case => Hx1. case => Hx2. by split. contradict Hx2 ; apply (Hnth O 1%nat). simpl ; by intuition. simpl ; by intuition. contradict Hx1 ; apply sym_not_eq, (Hnth O O). simpl ; by intuition. simpl ; by intuition. by []. exists g. split. move => i j Hi Hj. apply (Hnth (S i) (S j)). simpl ; apply ->Nat.succ_lt_mono; apply Hi. simpl ; apply ->Nat.succ_lt_mono; apply Hj. split. move: Hptd => /=. rewrite SF_cons_f2 /=. apply ptd_cons. apply Nat.lt_0_succ. split. exact: Nat.lt_0_succ. case: Hval => /= y Hy. case: Hy => /= z [-> [F0y Fz]]. case: F0y => t [Ht ->]. case: Fz => g [Hnth [Hpdt <-]]. set g0 := fun x y => match Req_EM_T x x1 with | left _ => match Req_EM_T y x2 with | left _ => t | right _ => g x y end | right _ => g x y end. exists g0. split. move => {val y z} i j Hi Hj. rewrite /g0. case: Req_EM_T => Hx1'. case: Req_EM_T => Hx2'. case: j Hj => /= [ | j] Hj. by apply Rgt_not_eq, Ht. apply Nat.succ_lt_mono in Hj ; case: j Hj => /= [ | j] Hj. by apply Rlt_not_eq, Ht. move: (proj2 Hle : sorted Rle (x2 :: s)). apply Nat.succ_lt_mono in Hj ; move: (proj2 Ht) ; elim: j x2 s Hj {IH Hle Hlt Hfin Hnth Hpdt F0 Ht g0 Hx2' Hx1' i Hi} => [ | i IH] x0 ; case => {x1} [ | x1 s] Hi Ht Hle ; simpl. by apply Nat.lt_irrefl in Hi. apply Rlt_not_eq, Rlt_le_trans with (1 := Ht). by apply Hle. by apply Nat.nlt_0_r in Hi. apply (IH x1). by apply Nat.succ_lt_mono, Hi. apply Rlt_le_trans with (1 := Ht). by apply Hle. by apply Hle. case: i j Hi Hj Hx1' Hx2' => /= [ | i] j Hi Hj Hx1' Hx2'. by []. case: j Hj => /= [ | j] Hj. apply Rgt_not_eq, Rlt_le_trans with x2. apply Rlt_trans with t ; by intuition. apply Rle_trans with (nth 0 (x2 :: s) i). apply (sorted_incr (x2 :: s) O i). move: (ptd_sort _ Hpdt). rewrite /SF_sorted SF_lx_f2 // ; by apply Nat.lt_0_succ. by intuition. simpl ; by intuition. move: (Hpdt i). rewrite SF_size_f2 SF_lx_f2 ; (try by apply Nat.lt_0_succ) ; rewrite SF_ly_f2 (nth_pairmap 0) /=. move => H ; apply H. by intuition. apply SSR_leq ; by intuition. apply Hnth. by intuition. by intuition. simpl in Hi ; apply Nat.succ_lt_mono in Hi ; case: i Hi Hx1' => /= [ | i] Hi Hx1'. by []. case: j Hj => /= [ | j] Hj. apply Rgt_not_eq, Rlt_le_trans with x2. apply Rlt_trans with t ; by intuition. apply Rle_trans with (nth 0 (x2 :: s) i). apply (sorted_incr (x2 :: s) O i). move: (ptd_sort _ Hpdt). by rewrite /SF_sorted SF_lx_f2 // ; apply Nat.lt_0_succ. by intuition. simpl ; by intuition. move: (Hpdt i). rewrite SF_size_f2 SF_lx_f2 ; (try by apply Nat.lt_0_succ) ; rewrite SF_ly_f2 (nth_pairmap 0) /=. move => H ; apply H. by intuition. apply SSR_leq ; by intuition. apply Hnth. by intuition. by intuition. split. move => ptd i Hi. rewrite SF_size_f2 /= in Hi. rewrite SF_lx_f2 ; (try by apply Nat.lt_0_succ) ; rewrite SF_ly_f2 nth_behead (nth_pairmap 0) /=. case: i Hi => /= [ | i] Hi ; rewrite /g0. move: (refl_equal x1) ; case: Req_EM_T => // _ _. move: (refl_equal x2) ; case: Req_EM_T => // _ _. split ; apply Rlt_le ; by intuition. suff : (nth 0 (x2 :: s) i) <> x1. case: Req_EM_T => // _ _. move: (Hpdt i). rewrite SF_size_f2 SF_lx_f2 ; (try by apply Nat.lt_0_succ) ; rewrite SF_ly_f2 nth_behead (nth_pairmap 0) /=. move => H ; apply H ; by intuition. apply SSR_leq ; by intuition. apply Rgt_not_eq, Rlt_le_trans with x2. apply Rlt_trans with t ; by intuition. apply (sorted_incr (x2 :: s) O i). move: (ptd_sort _ Hpdt). by rewrite /SF_sorted SF_lx_f2 // ; apply Nat.lt_0_succ. by intuition. simpl ; by intuition. apply SSR_leq ; by intuition. rewrite SF_cons_f2 /=. rewrite Riemann_sum_cons /=. apply f_equal2. rewrite /g0 ; move: (refl_equal x1) ; case: Req_EM_T => // _ _. move: (refl_equal x2) ; case: Req_EM_T => // _ _. apply Rmult_comm. case: s Hlt {Hpdt IH Hle Hfin F0 Ht Hnth} => [ | x3 s] Hlt /=. apply refl_equal. rewrite !(SF_cons_f2 _ _ (x3 :: _)) /=. rewrite !Riemann_sum_cons /=. apply f_equal2. rewrite /g0 /id ; move: (Rgt_not_eq _ _ (proj1 Hlt)) ; by case: Req_EM_T. elim: s (x2) x3 Hlt => [ | x4 s IH] x2' x3 Hlt. exact: refl_equal. rewrite !(SF_cons_f2 _ _ (x4 :: _)) /=. rewrite !Riemann_sum_cons /=. apply f_equal2. rewrite /g0 ; move: (Rgt_not_eq _ _ (Rlt_trans _ _ _ (proj1 Hlt) (proj1 (proj2 Hlt)))) ; by case: Req_EM_T. apply (IH x3). split. apply Rlt_trans with x2' ; apply Hlt. apply Hlt. exact: Nat.lt_0_succ. exact: Nat.lt_0_succ. exact: Nat.lt_0_succ. exact: Nat.lt_0_succ. exact: Nat.lt_0_succ. Qed.
imports: Coq(Reals Psatz) mathcomp(ssreflect ssrbool ssrfun eqtype seq) Markov Rcomplements Rbar Lub Lim_seq SF_seq Continuity Hierarchy