proposition: Lemma integral_bounded (from: Q) (width: QnonNeg) (mid: CR) (r: CR) (rnn: CRnonNeg r) (A: forall (x: Q), (from <= x <= from+` width) -> CRball r mid (f x)): CRball (scale (proj1_sig width) r) (∫ f from width) (scale (proj1_sig width) mid).
proof: Proof. Proof with auto. revert A. pattern width. apply QnonNeg.Qpos_ind; intros. intros ?? E. assert (forall z, scale (`x) z == scale (`y) z) as scale_wd. { intro z. apply Cmap_wd. rewrite E. reflexivity. reflexivity. } split; intro; intros. rewrite <- scale_wd, <- scale_wd, <- E. apply H. intros. apply A. rewrite <- E... rewrite scale_wd, scale_wd, E. apply H. intros. apply A. rewrite E... rewrite zero_width_integral, scale_0, scale_0. apply CRball.reflexive, CRnonNeg_0. apply (bounded_with_real_radius from q mid r rnn)... 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