proposition: Lemma integral_lower_upper_bounded (from: Q) (width: QnonNeg) (lo hi: CR): (forall (x: Q), (from <= x <= from+` width)%Q -> lo <= f x /\ f x <= hi) -> scale (` width) lo <= ∫ f from width /\ ∫ f from width <= scale (` width) hi.
proof: Proof. Proof with auto with *. intro A. assert (from <= from <= from + `width) as B. split... rewrite <- (Qplus_0_r from) at 1. apply Qplus_le_compat... assert (lo <= hi) as lohi by (destruct (A _ B); now apply CRle_trans with (f from)). set (r := ' (1#2) * (hi - lo)). set (mid := ' (1#2) * (lo + hi)). assert (mid - r == lo) as loE by (subst mid r; ring). assert (mid + r == hi) as hiE by (subst mid r; ring). rewrite <- loE, <- hiE. rewrite scale_CRplus, scale_CRplus, scale_CRopp, CRdistance_CRle, CRdistance_comm. apply CRball.as_distance_bound. apply integral_bounded. subst r. apply CRnonNeg_le_0. apply mult_resp_nonneg. simpl. apply CRle_Qle... rewrite <- (CRplus_opp lo). apply (CRplus_le_r lo hi (-lo))... intros. apply CRball.as_distance_bound. apply -> CRdistance_CRle. rewrite loE, hiE... 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