proposition: Lemma continuous_RInt_0 : forall (f : R -> V) (a : R) If, locally a (fun x => is_RInt f a x (If x)) -> continuous If a.
proof: Proof. move => f a If [d1 /= CIf]. assert (forall eps : posreal, norm (If a) < eps). move => eps. generalize (fun Hy => proj1 (filterlim_locally_ball_norm _ _) (CIf a Hy) eps) => /= {} CIf. assert (Rabs (a + - a) < d1). rewrite -/(Rminus _ _) Rminus_eq_0 Rabs_R0. by apply d1. destruct (CIf H) as [d CIf']. assert (exists y : SF_seq, seq_step (SF_lx y) < d /\ pointed_subdiv y /\ SF_h y = Rmin a a /\ seq.last (SF_h y) (SF_lx y) = Rmax a a). apply filter_ex. exists d => y Hy Hy'. now split. case: H0 => {CIf H} ptd [Hstep Hptd]. specialize (CIf' ptd Hstep Hptd). rewrite Rminus_eq_0 sign_0 in CIf'. rewrite -norm_opp. replace (opp (If a)) with (minus (scal 0 (Riemann_sum f ptd)) (If a)). by apply CIf'. replace (scal 0 (Riemann_sum f ptd) : V) with (zero : V). by rewrite /minus plus_zero_l. apply sym_eq ; apply: scal_zero_l. apply filterlim_locally_ball_norm. cut (forall eps : posreal, locally a (fun x : R => norm (If x) < eps)). move => H0 eps. specialize (H (pos_div_2 eps)). specialize (H0 (pos_div_2 eps)). destruct H0 as [d Hd]. exists d => /= y Hy. apply Rle_lt_trans with (norm (If y) + norm (If a))%R. rewrite -(norm_opp (If a)). apply @norm_triangle. rewrite (double_var eps). apply Rplus_lt_compat. now apply Hd. by apply H. clear H. move => eps. destruct (ex_RInt_ub f (a - d1 / 2) (a + d1 / 2)) as [Mf HMf]. apply ex_RInt_Chasles with a. apply ex_RInt_swap ; eexists ; apply CIf. rewrite /ball /= /AbsRing_ball /= /abs /minus /plus /opp /=. field_simplify (a - d1 / 2 + - a)%R. rewrite Rabs_left. apply Rminus_lt_0 ; field_simplify ; rewrite ?Rdiv_1. by apply is_pos_div_2. apply Ropp_lt_cancel ; field_simplify ; rewrite ?Rdiv_1. by apply is_pos_div_2. eexists ; apply CIf. rewrite /ball /= /AbsRing_ball /= /abs /minus /plus /opp /=. field_simplify (a + d1 / 2 + - a)%R. rewrite Rabs_pos_eq. apply Rminus_lt_0 ; field_simplify ; rewrite ?Rdiv_1. by apply is_pos_div_2. apply Rlt_le ; field_simplify ; rewrite ?Rdiv_1. by apply is_pos_div_2. assert ((a - d1 / 2) <= (a + d1 / 2)). apply Rminus_le_0. replace (a + d1 / 2 - (a - d1 / 2))%R with (d1 : R) by field. by apply Rlt_le, d1. move: HMf ; rewrite /Rmin /Rmax ; case: Rle_dec => // _ HMf. assert (0 <= Mf). eapply Rle_trans. 2: apply (HMf (a - d1 / 2)%R) ; split => // ; by apply Rle_refl. by apply norm_ge_0. generalize (fun y Hy => proj1 (filterlim_locally_ball_norm _ _) (CIf y Hy) (pos_div_2 eps)) => /= {} CIf. assert (0 < Rmin (d1 / 2) (eps / (2 * (Mf + 1)))). apply Rmin_case. by apply is_pos_div_2. apply Rdiv_lt_0_compat. by apply eps. apply Rmult_lt_0_compat. by apply Rlt_0_2. apply Rplus_le_lt_0_compat. by []. by apply Rlt_0_1. set (d2 := mkposreal _ H1). exists d2 => x /= Hx. specialize (CIf x). destruct CIf as [d' CIf]. apply Rlt_trans with (1 := Hx). apply Rle_lt_trans with (1 := Rmin_l _ _). apply Rminus_lt_0 ; field_simplify ; rewrite ?Rdiv_1 ; by apply is_pos_div_2. assert (exists y0, seq_step (SF_lx y0) < d' /\ pointed_subdiv y0 /\ SF_h y0 = Rmin a x /\ seq.last (SF_h y0) (SF_lx y0) = Rmax a x). apply filter_ex. exists d' => y Hy Hy'. now split. case: H2 => ptd [Hstep Hptd]. specialize (CIf ptd Hstep Hptd). rewrite -norm_opp. replace (opp (If x)) with (minus (minus (scal (sign (x - a)) (Riemann_sum f ptd)) (If x)) (scal (sign (x - a)) (Riemann_sum f ptd))). 2: rewrite /minus plus_comm plus_assoc plus_opp_l. 2: by apply plus_zero_l. apply Rle_lt_trans with (norm (minus (scal (sign (x - a)) (Riemann_sum f ptd)) (If x)) + norm (opp (scal (sign (x - a)) (Riemann_sum f ptd))))%R. rewrite /minus ; by apply @norm_triangle. rewrite norm_opp (double_var eps). apply Rplus_lt_le_compat. by []. apply Rle_trans with (1 := norm_scal (sign (x - a)) _). apply Rle_trans with (1 * norm (Riemann_sum f ptd)). apply Rmult_le_compat_r. apply norm_ge_0. rewrite /abs /= /sign ; case: total_order_T => [[H2|H2]|H2]. rewrite Rabs_R1. apply Rle_refl. rewrite Rabs_R0. apply Rle_0_1. rewrite Rabs_Ropp Rabs_R1. apply Rle_refl. rewrite Rmult_1_l. apply Rle_trans with (Riemann_sum (fun _ => Mf) ptd). apply Riemann_sum_norm. apply Hptd. move => t. rewrite (proj2 (proj2 Hptd)) (proj1 (proj2 Hptd)) => Ht. apply HMf ; split ; eapply Rle_trans ; try apply Ht. apply Rmin_case. apply Rlt_le, Rminus_lt_0 ; field_simplify ; rewrite ?Rdiv_1 ; by apply is_pos_div_2. apply Rlt_le, Rabs_lt_between'. apply Rlt_le_trans with (1 := Hx). by apply Rmin_l. apply Rmax_case. apply Rlt_le, Rminus_lt_0 ; field_simplify ; rewrite ?Rdiv_1 ; by apply is_pos_div_2. apply Rlt_le, Rabs_lt_between'. apply Rlt_le_trans with (1 := Hx). by apply Rmin_l. rewrite Riemann_sum_const. rewrite (proj2 (proj2 Hptd)) (proj1 (proj2 Hptd)) /=. apply Rle_trans with (Rabs (x + - a) * Mf)%R. apply Rmult_le_compat_r. by []. rewrite /Rmin /Rmax ; case: Rle_dec => _. apply Rle_abs. rewrite -Ropp_minus_distr. apply Rabs_maj2. apply Rle_trans with (Rabs (x + - a) * (Mf + 1))%R. apply Rmult_le_compat_l. by apply Rabs_pos. apply Rminus_le_0 ; ring_simplify ; by apply Rle_0_1. apply Rle_div_r. apply Rlt_le_trans with (1 := Rlt_0_1). apply Rminus_le_0 ; by ring_simplify. apply Rlt_le, Rlt_le_trans with (1 := Hx). apply Rle_trans with (1 := Rmin_r _ _). apply Req_le ; field. apply Rgt_not_eq, Rlt_le_trans with (1 := Rlt_0_1). apply Rminus_le_0 ; by ring_simplify. Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(eqtype seq) Markov Rcomplements Rbar Lub Lim_seq Derive SF_seq Continuity Hierarchy Seq_fct RInt PSeries