proposition: Lemma ex_RInt_ub (f : R -> V) (a b : R) : ex_RInt f a b -> exists M : R, forall t : R, Rmin a b <= t <= Rmax a b -> norm (f t) <= M.
proof: Proof. wlog: a b / (a < b) => [ Hw | Hab ] Hex. case: (Rle_lt_dec a b) => Hab. case: Hab => Hab. by apply Hw. rewrite /Rmin /Rmax ; case: Rle_dec (Req_le _ _ Hab) => // _ _ ; rewrite -Hab. exists (norm (f a)) => t Ht ; replace t with a. exact: Rle_refl. apply Rle_antisym ; by case: Ht. rewrite Rmin_comm Rmax_comm ; apply ex_RInt_swap in Hex ; by apply Hw. rewrite /Rmin /Rmax ; case: Rle_dec (Rlt_le _ _ Hab) => // _ _. case: Hex => If Hex. generalize (proj1 (filterlim_locally_ball_norm _ If) Hex) => {Hex} /= Hex. case: (Hex (mkposreal _ Rlt_0_1)) => {Hex} alpha Hex. have Hn : 0 <= ((b-a)/alpha). apply Rdiv_le_0_compat. apply -> Rminus_le_0 ; apply Rlt_le, Hab. by apply alpha. set n := (nfloor _ Hn). set ptd := fun (g : R -> R -> R) => SF_seq_f2 g (unif_part a b n). assert (forall g, pointed_subdiv (ptd g) -> norm (minus (Riemann_sum f (ptd g)) If) < 1). move => g Hg ; replace (Riemann_sum f (ptd g)) with (scal (sign (b - a)) (Riemann_sum f (ptd g))). apply Hex. apply Rle_lt_trans with ((b-a)/(INR n + 1)). clearbody n ; rewrite SF_lx_f2. replace (head 0 (unif_part a b n) :: behead (unif_part a b n)) with (unif_part a b n) by auto. 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) => [ /= _ | x0]. apply Rdiv_le_0_compat ; [ by apply Rlt_le, Rgt_minus | by intuition ]. case => /= [ | x1 s] IH Hnth. apply Rdiv_le_0_compat ; [ by apply Rlt_le, Rgt_minus | by intuition ]. replace (seq_step _) with (Rmax (Rabs (x1 - x0)) (seq_step (x1 :: s))) by auto. apply Rmax_case_strong => _. rewrite (Hnth O (proj1 (Nat.succ_lt_mono _ _) (Nat.lt_0_succ _))) Rabs_right. exact: Rle_refl. apply Rle_ge, Rdiv_le_0_compat ; [ by apply Rlt_le, Rgt_minus | by intuition ]. apply IH => i Hi ; exact: (Hnth (S i) ((proj1 (Nat.succ_lt_mono _ _)) Hi)). rewrite size_mkseq => i Hi. rewrite ?nth_mkseq ?S_INR ; try apply SSR_leq. field ; apply Rgt_not_eq ; by intuition. exact: Nat.lt_le_incl. exact: Hi. by apply Nat.lt_0_succ. apply Rlt_div_l. by apply INRp1_pos. rewrite Rmult_comm ; apply Rlt_div_l. by apply alpha. rewrite /n /nfloor ; case: nfloor_ex => /= n' Hn'. by apply Hn'. split. apply Hg. rewrite -> Rmin_left, Rmax_right by now apply Rlt_le. split. apply head_unif_part. clearbody n ; rewrite /Rmax -nth_last SF_lx_f2. rewrite size_mkseq nth_mkseq ?S_INR //. field ; apply Rgt_not_eq ; by intuition. by apply Nat.lt_0_succ. rewrite -> sign_eq_1 by exact: Rlt_Rminus. exact: scal_one. move: H => {} Hex. assert (exists M, forall g : R -> R -> R, pointed_subdiv (ptd g) -> norm (Riemann_sum f (ptd g)) <= M). exists (norm If + 1) ; move => g Hg. replace (Riemann_sum f (ptd g)) with (plus (minus (Riemann_sum f (ptd g)) If) If). apply Rle_trans with (norm (minus (Riemann_sum f (ptd g)) If) + norm If). by generalize (norm_triangle (minus (Riemann_sum f (ptd g)) If) If). rewrite Rplus_comm. apply Rplus_le_compat_l. apply Rlt_le. by apply Hex. by rewrite /minus -plus_assoc plus_opp_l plus_zero_r. clearbody n ; move: H => {} Hex. assert (forall i, (S i < size (unif_part a b n))%nat -> exists M, forall t, nth 0 (unif_part a b n) i <= t <= nth 0 (unif_part a b n) (S i) -> norm (f t) <= M). move => i ; revert ptd Hex. have : sorted Rlt (unif_part a b n). apply sorted_nth => j Hj x0. rewrite size_mkseq /= in Hj. rewrite ?nth_mkseq ?S_INR /= ; try apply SSR_leq. apply Rminus_gt ; field_simplify. rewrite Rplus_comm ?Rdiv_1 ; apply Rdiv_lt_0_compat. exact: Rgt_minus. by intuition. apply Rgt_not_eq ; by intuition. by intuition. by intuition. elim: (unif_part a b n) i => [ /= i _ _ Hi | x0]. by apply Nat.nlt_0_r in Hi. case => [ /= _ i _ _ Hi | x1 s IH]. by apply Nat.succ_lt_mono, Nat.nlt_0_r in Hi. case => [ | i] Hlt /= Hex Hi. assert (exists M, forall t g, x0 <= t <= x1 -> pointed_subdiv (SF_seq_f2 g [:: x1 & s]) -> norm (plus (scal (x1 - x0) (f t)) (Riemann_sum f (SF_seq_f2 g [:: x1 & s]))) <= M). case: (Hex) => M Hex'. exists M ; move => t g Ht Hg. set g0 := fun x y => match Req_EM_T x x0 with | left _ => t | right _ => g x y end. replace (plus (scal (x1 - x0) (f t)) (Riemann_sum f (SF_seq_f2 g (x1 :: s)))) with (Riemann_sum f (SF_seq_f2 g0 [:: x0, x1 & s])). apply Hex'. case => [ | j] Hj ; rewrite SF_size_f2 /= in Hj ; rewrite SF_ly_f2 SF_lx_f2 /=. 2: apply Nat.lt_0_succ. rewrite /g0. by case: Req_EM_T (refl_equal x0). rewrite (nth_pairmap 0). rewrite /g0. suff : (nth 0 (x1 :: s) j) <> x0. case: Req_EM_T => // _ _. move: (Hg j). rewrite SF_size_f2 ; rewrite SF_ly_f2 SF_lx_f2 /=. 2: apply Nat.lt_0_succ. rewrite (nth_pairmap 0). move => Hg' ; by apply Hg', Nat.succ_lt_mono. apply SSR_leq ; by intuition. apply Rgt_not_eq. apply Nat.succ_lt_mono in Hj. elim: j Hj => {IH} [ | j IH] Hj. by apply Hlt. apply Rlt_trans with (nth 0 (x1 :: s) j). apply IH ; by intuition. apply (sorted_nth Rlt). by apply Hlt. by intuition. apply SSR_leq ; by intuition. by apply Nat.lt_0_succ. rewrite SF_cons_f2 /=. rewrite Riemann_sum_cons /=. apply f_equal2. apply f_equal. rewrite /g0. by case: Req_EM_T (refl_equal x0). case: s Hlt {IH Hex Hex' Hi Hg} => [ | x2 s] Hlt. reflexivity. rewrite !(SF_cons_f2 _ x1) /=. rewrite !Riemann_sum_cons /=. apply f_equal2. apply f_equal. rewrite /g0. by case: Req_EM_T (Rgt_not_eq _ _ (proj1 Hlt)). elim: s x2 Hlt => [ | x3 s IH] x2 Hlt. reflexivity. rewrite !(SF_cons_f2 _ x2) /=. rewrite !Riemann_sum_cons /=. apply f_equal2. apply f_equal. rewrite /g0. by case: Req_EM_T (Rgt_not_eq _ _ (Rlt_trans _ _ _ (proj1 Hlt) (proj1 (proj2 Hlt)))). apply IH. split. by apply Hlt. split. apply Rlt_trans with x2 ; by apply Hlt. by apply Hlt. by apply Nat.lt_0_succ. by apply Nat.lt_0_succ. by apply Nat.lt_0_succ. by apply Nat.lt_0_succ. by apply Nat.lt_0_succ. move: H => {} Hex. case: (Hex) => M Hex'. exists ((M + norm (Riemann_sum f (SF_seq_f2 (fun x y => x) (x1 :: s)))) / abs (x1 - x0)). move => t Ht. have Hg : pointed_subdiv (SF_seq_f2 (fun x y : R => x) (x1 :: s)). move => j ; rewrite SF_size_f2 SF_lx_f2. rewrite SF_ly_f2 /= => Hj. rewrite (nth_pairmap 0). split. apply Rle_refl. apply Rlt_le, (sorted_nth Rlt (x1::s)). by apply Hlt. by []. apply SSR_leq ; by intuition. apply Nat.lt_0_succ. specialize (Hex' _ _ Ht Hg). rewrite -(scal_one (f t)). rewrite /one /= -(Rinv_l (x1 - x0)). 2: by apply Rgt_not_eq, Rgt_minus, Hlt. rewrite -scal_assoc. eapply Rle_trans ; try apply @norm_scal. rewrite Rmult_comm. rewrite /abs /= Rabs_Rinv. 2: by apply Rgt_not_eq, Rgt_minus, Hlt. apply Rmult_le_compat_r. apply Rlt_le, Rinv_0_lt_compat. apply Rabs_pos_lt, Rgt_not_eq. by apply Rgt_minus, Hlt. set v:= scal _ _. replace v with (minus (plus (scal (x1 - x0) (f t)) (Riemann_sum f (SF_seq_f2 (fun x _ : R => x) (x1 :: s)))) (Riemann_sum f (SF_seq_f2 (fun x _ : R => x) (x1 :: s)))). rewrite /minus. apply Rle_trans with (norm (plus (scal (x1 - x0) (f t)) (Riemann_sum f (SF_seq_f2 (fun x _ : R => x) (x1 :: s)))) + norm (opp (Riemann_sum f (SF_seq_f2 (fun x _ : R => x) (x1 :: s))))). by generalize (norm_triangle (plus (scal (x1 - x0) (f t)) (Riemann_sum f (SF_seq_f2 (fun x _ : R => x) (x1 :: s)))) (opp (Riemann_sum f (SF_seq_f2 (fun x _ : R => x) (x1 :: s))))). rewrite norm_opp. apply Rplus_le_compat_r. apply Hex'. rewrite /minus -plus_assoc plus_opp_r. by apply plus_zero_r. apply IH. by apply Hlt. case: Hex => M Hex. exists ((M + norm (scal (x1 - x0) (f x0)))) => g Hg. set g0 := fun x y => match Req_EM_T x x0 with | left _ => x0 | right _ => g x y end. have Hg0 : pointed_subdiv (SF_seq_f2 g0 (x0::x1 :: s)). move => j ; rewrite SF_size_f2 SF_lx_f2. 2: apply Nat.lt_0_succ. rewrite SF_ly_f2 => Hj. rewrite nth_behead (nth_pairmap 0) /=. case: j Hj => /= [ | j ] Hj. rewrite /g0. case: Req_EM_T (refl_equal x0) => // _ _. split. exact: Rle_refl. by apply Rlt_le, Hlt. suff : (nth 0 (x1 :: s) j) <> x0. rewrite /g0 ; case: Req_EM_T => // _ _. move: (Hg j). rewrite SF_size_f2 SF_lx_f2. 2: apply Nat.lt_0_succ. rewrite SF_ly_f2 /= => {} Hg. move: (Hg (proj2 (Nat.succ_lt_mono _ _) Hj)) ; rewrite (nth_pairmap 0). by []. apply SSR_leq ; by intuition. apply Rgt_not_eq. elim: j Hj => {IH} /= [ | j IH] Hj. by apply Hlt. apply Rlt_trans with (nth 0 (x1 :: s) j). apply IH ; by intuition. apply (sorted_nth Rlt (x1::s)). by apply Hlt. by intuition. apply SSR_leq ; by intuition. replace (Riemann_sum f (SF_seq_f2 g (x1 :: s))) with (minus (Riemann_sum f (SF_seq_f2 g0 (x0::x1::s))) (scal (x1 - x0) (f x0))). apply Rle_trans with (norm (Riemann_sum f (SF_seq_f2 g0 [:: x0, x1 & s])) + norm (opp (scal (x1 - x0) (f x0)))). by generalize (norm_triangle (Riemann_sum f (SF_seq_f2 g0 [:: x0, x1 & s])) (opp (scal (x1 - x0) (f x0)))). rewrite norm_opp. apply Rplus_le_compat_r, (Hex _ Hg0). rewrite /minus plus_comm SF_cons_f2 /=. rewrite Riemann_sum_cons /= plus_assoc. replace (Riemann_sum f (SF_seq_f2 g0 (x1 :: s))) with (Riemann_sum f (SF_seq_f2 g (x1 :: s))). replace (g0 x0 x1) with x0. by rewrite plus_opp_l plus_zero_l. rewrite /g0 ; case: Req_EM_T (refl_equal x0) => //. elim: s x1 Hlt {IH Hex Hg Hg0 Hi} => [ | x2 s IH] x1 Hlt. reflexivity. rewrite !(SF_cons_f2 _ x1) /=. rewrite !Riemann_sum_cons /=. apply f_equal2. rewrite /g0 ; by case: Req_EM_T (Rgt_not_eq _ _ (proj1 Hlt)). apply IH. split. apply Rlt_trans with x1 ; by apply Hlt. by apply Hlt. exact: Nat.lt_0_succ. exact: Nat.lt_0_succ. exact: Nat.lt_0_succ. exact: (proj2 (Nat.succ_lt_mono _ _)). move:H => {} Hex. replace b with (last 0 (unif_part a b n)). pattern a at 1 ; replace a with (head 0 (unif_part a b n)). elim: (unif_part a b n) Hex => /= [ | x0]. exists (norm (f 0)) => t Ht ; rewrite (Rle_antisym t 0) ; by intuition. case => /= [ | x1 s] IH Hex. exists (norm (f x0)) => t Ht ; rewrite (Rle_antisym t x0) ; by intuition. case: (Hex _ (proj1 (Nat.succ_lt_mono _ _) (Nat.lt_0_succ _))) => /= M0 H0. case: IH => [ | M IH]. move => i Hi ; case: (Hex _ (proj1 (Nat.succ_lt_mono _ _) Hi)) => {Hex} /= M Hex. by exists M. exists (Rmax M0 M) => t Ht ; case: (Rlt_le_dec t x1) => Ht0. apply Rle_trans with (2 := RmaxLess1 _ _) ; apply H0 ; by intuition. apply Rle_trans with (2 := RmaxLess2 _ _) ; apply IH ; by intuition. apply head_unif_part. apply last_unif_part. Qed.
imports: Coq(Reals Psatz) mathcomp(ssreflect ssrbool ssrfun eqtype seq) Markov Rcomplements Rbar Lub Lim_seq SF_seq Continuity Hierarchy