proposition: Lemma bounded_with_real_radius (from: Q) (width: Qpos) (mid: CR) (r: CR) (rnn: CRnonNeg r): (forall (x: Q), from <= x <= from+` width -> CRball r mid (f x)) -> CRball (scale (proj1_sig width) r) (∫ f from (from_Qpos width)) (scale (proj1_sig width) mid).
proof: Proof. Proof with auto. intro A. unfold CRball. intros. unfold CRball in A. setoid_replace q with (proj1_sig width * (q / proj1_sig width))%Q by (simpl; field; auto). assert (r <= ' (q / proj1_sig width)). { apply (mult_cancel_leEq CRasCOrdField) with (' (proj1_sig width)). simpl. apply CRlt_Qlt... rewrite mult_commutes. change (' (proj1_sig width) * r <= ' (q / proj1_sig width) * ' (proj1_sig width)). rewrite CRmult_Qmult. unfold Qdiv. rewrite <- Qmult_assoc. rewrite (Qmult_comm (/ proj1_sig width)). rewrite Qmult_inv_r... rewrite Qmult_1_r. rewrite CRmult_scale... } assert (0 <= (q / proj1_sig width))%Q as E. apply CRle_Qle. apply CRle_trans with r... apply -> CRnonNeg_le_0... apply (bounded_with_nonneg_radius from width mid (exist _ _ E)). intros. apply ball_sym... 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