proposition: Lemma integral_abs_bound (from : Q) (width : QnonNeg) (M : Q) : (forall (x : Q), (from ≤ x ≤ from + proj1_sig width) -> CRabs (f x) ≤ 'M) -> CRabs (∫ f from width) ≤ '(`width * M).
proof: Proof. intro A. rewrite <- (CRplus_0_r (∫ f from width)), <- CRopp_0. apply CRball.as_distance_bound. rewrite <- (scale_0_r (proj1_sig width)). rewrite <- CRmult_Qmult, CRmult_scale. apply integral_bounded; trivial. + apply CRnonNeg_le_0. apply CRle_trans with (y := CRabs (f from)); [apply CRabs_nonneg |]. apply A. split; [reflexivity |]. apply semirings.nonneg_plus_le_compat_r; change (0 <= proj1_sig width)%Q; Qauto_nonneg. + intros x A2. apply CRball.as_distance_bound. rewrite CRdistance_comm. change (CRabs (f x - 0) ≤ 'M). rewrite rings.minus_0_r; now apply A. 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 MathClasses.misc.propholds