proposition: Lemma Riemann_sum_Chasles_0 (f : R -> V) (M : R) (x : R) ptd : forall (eps : posreal), (forall x, SF_h ptd <= x <= last (SF_h ptd) (SF_lx ptd) -> norm (f x) < M) -> SF_h ptd <= x <= last (SF_h ptd) (SF_lx ptd) -> pointed_subdiv ptd -> seq_step (SF_lx ptd) < eps -> norm (minus (plus (Riemann_sum f (SF_cut_down ptd x)) (Riemann_sum f (SF_cut_up ptd x))) (Riemann_sum f ptd)) < 2 * eps * M.
proof: Proof. intros eps. apply (SF_cons_ind (T := R)) with (s := ptd) => {ptd} /= [ x0 | [x0 y1] ptd IH] /= Hfx [ Hx0 Hl] Hptd Hstep. + rewrite (Rle_antisym _ _ Hx0 Hl) ; clear -Hfx. rewrite /Riemann_sum /=. case: Rle_dec (Rle_refl x) => //= _ _. rewrite ?plus_zero_r Rminus_eq_0. rewrite scal_zero_l. rewrite /minus plus_zero_l norm_opp norm_zero. apply Rmult_lt_0_compat. apply Rmult_lt_0_compat. by apply Rlt_0_2. by apply eps. by apply Rle_lt_trans with (2:= (Hfx x0 (conj (Rle_refl _) (Rle_refl _)))), norm_ge_0. + case: (Rle_dec (SF_h ptd) x) => Hx1. - replace (minus (plus (Riemann_sum f (SF_cut_down (SF_cons (x0, y1) ptd) x)) (Riemann_sum f (SF_cut_up (SF_cons (x0, y1) ptd) x))) (Riemann_sum f (SF_cons (x0, y1) ptd))) with (minus (plus (Riemann_sum f (SF_cut_down ptd x)) (Riemann_sum f (SF_cut_up ptd x))) (Riemann_sum f ptd)). apply IH. intros y Hy. apply Hfx. split. apply Rle_trans with y1. by apply (Hptd O (Nat.lt_0_succ _)). apply Rle_trans with (SF_h ptd). by apply (Hptd O (Nat.lt_0_succ _)). by apply Hy. by apply Hy. by split. by apply ptd_cons in Hptd. apply Rle_lt_trans with (2 := Hstep). by apply Rmax_r. rewrite SF_cut_down_cons_2. rewrite SF_cut_up_cons_2. rewrite /minus 2?(Riemann_sum_cons _ (x0, y1)) SF_cut_down_h. rewrite opp_plus plus_assoc /=. apply (f_equal (fun x => plus x _)). rewrite (plus_comm (scal (SF_h ptd - x0) (f y1))) -3!plus_assoc. apply f_equal. by rewrite plus_comm -plus_assoc plus_opp_l plus_zero_r. by []. split ; [ | apply Hx1]. apply Rle_trans with y1 ; by apply (Hptd O (Nat.lt_0_succ _)). split ; [ | apply Hx1]. apply Rle_trans with y1 ; by apply (Hptd O (Nat.lt_0_succ _)). - apply Rnot_le_lt in Hx1. rewrite SF_cut_down_cons_1 /=. rewrite SF_cut_up_cons_1 /=. rewrite 3!Riemann_sum_cons /= => {IH}. replace (Riemann_sum f (SF_nil x) : V) with (zero : V) by auto. rewrite plus_zero_r /minus opp_plus. rewrite (plus_comm (opp (scal (SF_h ptd - x0) (f y1)))). rewrite ?plus_assoc -(plus_assoc _ _ (opp (Riemann_sum f ptd))). rewrite plus_opp_r plus_zero_r. rewrite -scal_opp_l. rewrite /opp /= Ropp_minus_distr. rewrite /Rmin /Rmax ; case: Rle_dec => _. rewrite (plus_comm (scal (x - x0) (f y1))) -plus_assoc. rewrite -scal_distr_r /plus /= -/plus. ring_simplify (x - x0 + (x0 - SF_h ptd)). eapply Rle_lt_trans. apply @norm_triangle. replace (2 * eps * M) with (eps * M + eps * M) by ring. apply Rplus_lt_compat ; eapply Rle_lt_trans ; try (apply @norm_scal) ; apply Rmult_le_0_lt_compat. by apply Rabs_pos. by apply norm_ge_0. apply Rle_lt_trans with (2 := Hstep). apply Rle_trans with (2 := Rmax_l _ _). simpl. apply Rlt_le in Hx1. move: (Rle_trans _ _ _ Hx0 Hx1) => Hx0'. apply Rminus_le_0 in Hx1. apply Rminus_le_0 in Hx0'. rewrite /abs /= ?Rabs_pos_eq //. by apply Rplus_le_compat_l, Ropp_le_contravar. apply Hfx. by split. by apply Rabs_pos. by apply norm_ge_0. apply Rle_lt_trans with (2 := Hstep). apply Rle_trans with (2 := Rmax_l _ _). rewrite /abs /plus /= -Ropp_minus_distr Rabs_Ropp. apply Rlt_le in Hx1. move: (Rle_trans _ _ _ Hx0 Hx1) => Hx0'. apply Rminus_le_0 in Hx1. apply Rminus_le_0 in Hx0'. rewrite ?Rabs_pos_eq //. by apply Rplus_le_compat_l, Ropp_le_contravar. apply Hfx. split. apply (Hptd O (Nat.lt_0_succ _)). apply Rle_trans with (SF_h ptd). apply (Hptd O (Nat.lt_0_succ _)). apply (fun H => sorted_last ((SF_h ptd) :: (unzip1 (SF_t ptd))) O H (Nat.lt_0_succ _) (SF_h ptd)). apply ptd_sort in Hptd. by apply Hptd. rewrite -plus_assoc -scal_distr_r /plus /= -/plus. replace (SF_h ptd - x + (x0 - SF_h ptd)) with (opp (x - x0)) by (rewrite /opp /= ; ring). rewrite scal_opp_l -scal_opp_r. rewrite -scal_distr_l. eapply Rle_lt_trans. apply @norm_scal. replace (2 * eps * M) with (eps * (M + M)) by ring. apply Rmult_le_0_lt_compat. by apply Rabs_pos. by apply norm_ge_0. apply Rle_lt_trans with (2 := Hstep). apply Rle_trans with (2 := Rmax_l _ _). simpl. apply Rlt_le in Hx1. move: (Rle_trans _ _ _ Hx0 Hx1) => Hx0'. apply Rminus_le_0 in Hx0. apply Rminus_le_0 in Hx0'. rewrite /abs /= ?Rabs_pos_eq //. by apply Rplus_le_compat_r. apply Rle_lt_trans with (norm (f x) + norm (opp (f y1))). apply @norm_triangle. apply Rplus_lt_compat. apply Hfx. by split. rewrite norm_opp. apply Hfx. split. apply (Hptd O (Nat.lt_0_succ _)). apply Rle_trans with (SF_h ptd). apply (Hptd O (Nat.lt_0_succ _)). apply (fun H => sorted_last ((SF_h ptd) :: (unzip1 (SF_t ptd))) O H (Nat.lt_0_succ _) (SF_h ptd)). apply ptd_sort in Hptd. by apply Hptd. by split. by split. Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(seq) Rcomplements Rbar Lub Hierarchy