proposition: Lemma ex_RInt_Chasles_1 {V : CompleteNormedModule R_AbsRing} (f : R -> V) (a b c : R) : a <= b <= c -> ex_RInt f a c -> ex_RInt f a b.
proof: Proof. intros [Hab Hbc] If. case: Hab => [Hab | <- ]. 2: by apply ex_RInt_point. apply (filterlim_locally_closely (F := Riemann_fine a b) (fun ptd : SF_seq => scal (sign (b - a)) (Riemann_sum f ptd))). apply: (filterlim_filter_le_2 _ closely_norm_le_closely). apply <- (filterlim_closely_norm (F := Riemann_fine a b) (fun ptd : SF_seq => scal (sign (b - a)) (Riemann_sum f ptd))). intros eps. generalize (filterlim_locally_closely (F := Riemann_fine a c) (fun ptd : SF_seq => scal (sign (c - a)) (Riemann_sum f ptd))). move /proj2 /(_ If). move /(filterlim_filter_le_2 _ closely_le_closely_norm) => H. case: (proj1 (filterlim_closely_norm (F := Riemann_fine a c) (fun ptd : SF_seq => scal (sign (c - a)) (Riemann_sum f ptd))) H eps) => {H If} [P [[alpha HP] If]]. destruct (filter_ex (F := Riemann_fine b c) (fun y => seq_step (SF_lx y) < alpha /\ pointed_subdiv y /\ SF_h y = Rmin b c /\ seq.last (SF_h y) (SF_lx y) = Rmax b c)) as [y' Hy']. by exists alpha. exists (fun y => P (SF_cat y y') /\ last (SF_h y) (SF_lx y) = Rmax a b) ; split. exists alpha ; intros. assert (last 0 (SF_lx y) = head 0 (SF_lx y')). simpl in H0, Hy' |- *. rewrite (proj1 (proj2 (proj2 Hy'))). rewrite (proj2 (proj2 H0)). rewrite /Rmin ; case: Rle_dec => // _. rewrite /Rmax ; case: Rle_dec (Rlt_le _ _ Hab) => //. split. apply HP ; intuition. rewrite SF_lx_cat seq_step_cat. by apply Rmax_case. by apply Nat.lt_0_succ. by apply Nat.lt_0_succ. by []. apply SF_cat_pointed => //. rewrite H3 /Rmin ; case: Rle_dec (Rlt_le _ _ Hab) => // _ _. case: Rle_dec (Rlt_le _ _ (Rlt_le_trans _ _ _ Hab Hbc)) => //. rewrite SF_last_cat // H8. rewrite /Rmax ; case: Rle_dec (Rlt_le _ _ Hab) => // _ _. case: Rle_dec (Rlt_le _ _ (Rlt_le_trans _ _ _ Hab Hbc)) => //. by apply H0. intros. specialize (If _ _ (proj1 H) (proj1 H0)). rewrite -> sign_eq_1 by exact: Rlt_Rminus. rewrite -> sign_eq_1 in If by now apply Rlt_Rminus, Rlt_le_trans with b. apply Rle_lt_trans with (2 := If). apply Req_le, f_equal. rewrite !scal_one. case: H => _ ; case: H0 => _ ; clear ; intros. rewrite -b1 in b0. move: v u b0 y' {b1}. apply (SF_cons_ind (fun v => forall u : SF_seq, last (SF_h v) (SF_lx v) = last (SF_h u) (SF_lx u) -> forall y' : SF_seq, minus (Riemann_sum f v) (Riemann_sum f u) = minus (Riemann_sum f (SF_cat v y')) (Riemann_sum f (SF_cat u y')))) => [v0 | v0 v IH u Huv y]. apply (SF_cons_ind (fun u => last (SF_h (SF_nil v0)) (SF_lx (SF_nil v0)) = last (SF_h u) (SF_lx u) -> forall y' : SF_seq, minus (Riemann_sum f (SF_nil v0)) (Riemann_sum f u) = minus (Riemann_sum f (SF_cat (SF_nil v0) y')) (Riemann_sum f (SF_cat u y')))) => [u0 /= Huv | u0 u IH Huv y]. apply (SF_cons_ind (fun y' : SF_seq => minus (Riemann_sum f (SF_nil v0)) (Riemann_sum f (SF_nil u0)) = minus (Riemann_sum f (SF_cat (SF_nil v0) y')) (Riemann_sum f (SF_cat (SF_nil u0) y')))) => [y0 | y0 y IH]. by []. simpl in Huv. rewrite Huv /SF_cat /=. rewrite (Riemann_sum_cons _ (u0,snd y0)) /=. rewrite /minus opp_plus (plus_comm (scal _ _)) -plus_assoc. now rewrite (plus_assoc (scal _ _)) !plus_opp_r plus_zero_l plus_opp_r. rewrite -SF_cons_cat !Riemann_sum_cons. rewrite /minus !opp_plus !(plus_comm (opp (scal _ _))) !plus_assoc. by rewrite -!/(minus _ _) -IH. rewrite -SF_cons_cat !Riemann_sum_cons. rewrite /minus -!plus_assoc. by rewrite -!/(minus _ _) -IH. Qed.
imports: Coq(Reals Psatz) mathcomp(ssreflect ssrbool ssrfun eqtype seq) Markov Rcomplements Rbar Lub Lim_seq SF_seq Continuity Hierarchy