proposition: Lemma Riemann_sum_norm (f : R -> V) (g : R -> R) ptd : pointed_subdiv ptd -> (forall t, SF_h ptd <= t <= last (SF_h ptd) (SF_lx ptd) -> norm (f t) <= g t) -> norm (Riemann_sum f ptd) <= Riemann_sum g ptd.
proof: Proof. apply SF_cons_ind with (s := ptd) => {ptd} /= [x0 | [x0 y0] s IH] /= Hs H. rewrite norm_zero ; exact: Rle_refl. rewrite !Riemann_sum_cons /=. eapply Rle_trans. by apply @norm_triangle. apply Rplus_le_compat. eapply Rle_trans. apply @norm_scal. refine (_ (Hs O _)). simpl. intros [H1 H2]. rewrite /abs /= Rabs_pos_eq. apply Rmult_le_compat_l. apply -> Rminus_le_0. now apply Rle_trans with y0. apply H. apply (conj H1). apply Rle_trans with (1 := H2). apply (sorted_last (SF_lx s) O) with (x0 := 0). by apply (ptd_sort _ Hs). exact: Nat.lt_0_succ. apply -> Rminus_le_0. now apply Rle_trans with y0. exact: Nat.lt_0_succ. apply IH. by apply ptd_cons with (h := (x0,y0)). move => t Ht ; apply H ; split. by apply Rle_trans with (2 := proj1 Ht), (ptd_sort _ Hs). by apply Ht. Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(seq) Rcomplements Rbar Lub Hierarchy