proposition: Lemma bounded_with_real_mid (from: Q) (width: Qpos) (mid: CR) (r: Qpos): (forall x, from <= x <= from+proj1_sig width -> ball (proj1_sig r) (f x) mid) -> ball (proj1_sig (width * r)%Qpos) (∫ f from (from_Qpos width)) (scale (proj1_sig width) mid).
proof: Proof. Proof with auto. intros H d1 d2. simpl approximate. destruct (Qscale_modulus_pos width d2) as [P E]. rewrite E. simpl. set (v := (exist (Qlt 0) (/ (proj1_sig width) * proj1_sig d2)%Q P)). assert (QposEq (d1 + width * r + d2)%Qpos (d1 + width * (r + v))%Qpos). { unfold QposEq; simpl; field. apply Qpos_nonzero. } unfold QposEq in H0. rewrite H0. clear H0. apply regFunBall_Cunit. apply integral_bounded_prim. intros. apply ball_triangle with mid... apply ball_approx_r. 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