proposition: Lemma bounded_with_nonneg_radius (from: Q) (width: Qpos) (mid: CR) (r: QnonNeg): (forall (x: Q), (from <= x <= from+ proj1_sig width) -> ball (proj1_sig r) (f x) mid) -> ball (proj1_sig width * proj1_sig r) (∫ f from (from_Qpos width)) (scale (proj1_sig width) mid).
proof: Proof. Proof with auto. pattern r. apply QnonNeg.Qpos_ind. - intros ?? E. split. intros H ?. rewrite <- E. apply H. intros. rewrite E... intros H ?. rewrite E. apply H. intros. rewrite <- E... - rewrite Qmult_0_r. intros. apply ball_eq. intros e epos. setoid_replace e with (proj1_sig (width * (exist _ _ epos * Qpos_inv width))%Qpos) by (simpl; field; apply Qpos_nonzero). apply bounded_with_real_mid. intros q ?. setoid_replace (f q) with mid... apply ball_refl. apply Qpos_nonneg. apply H, H0. - intros. apply bounded_with_real_mid. intros. apply H, H0. 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