proposition: Lemma riemann_sum_bounds (a w : Q) (m : CR) (e : Q) (n : positive) : 0 ≤ w -> (forall (x : Q), (a ≤ x ≤ a + w) -> ball e (f x) m) -> ball (w * e) (riemann_sum f a w n) ('w * m).
proof: Proof. intros w_nn A. pose proof (riemann_sum_const a w m n). rewrite <- H. clear H. unfold riemann_sum. rewrite <- (step_mult w n), <- (Qmult_assoc (inject_Z n) _ e), <- (positive_nat_Z n). apply CRΣ_gball. intros k A1. apply CRball.gball_CRmult_Q_nonneg; [now apply step_nonneg |]. apply A. split; [apply index_inside_l | apply index_inside_r]; trivial. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.reals.CRreal Coq.Unicode.Utf8 Coq.Program.Program CoRN.reals.fast.CRArith CoRN.reals.fast.CRabs CoRN.tactics.Qauto Coq.QArith.Qround CoRN.model.metric2.Qmetric CoRN.stdlib_omissions.P CoRN.stdlib_omissions.Z CoRN.stdlib_omissions.Q CoRN.stdlib_omissions.N CoRN.ode.metric CoRN.ode.FromMetric2 CoRN.ode.SimpleIntegration