proposition: Lemma int_abs_bound (a b M : Q) : (forall x : Q, x ∈ (a, b) -> abs (f x) ≤ 'M) -> abs (int a b) ≤ '(abs (b - a) * M).
proof: Proof. intros A. unfold int. assert (0 <= (' M))%CR as Mpos. { apply (@CRle_trans _ (abs (f a))). apply CRabs_nonneg. apply (A a). split. apply meet_lb_l. apply join_ub_l. } destruct (decide (a ≤ b)) as [AB | AB]. - assert (∀ x : Q, a ≤ x ≤ a + ` ((b - a) ↾ int_obligation_1 a b AB) → CRabs (f x) ≤ ' M). { intros. apply A. split; simpl. apply (Qle_trans _ a). apply meet_lb_l. apply H0. simpl in H0. apply (Qle_trans _ b). destruct H0. ring_simplify in H1. exact H1. apply join_ub_r. } apply (CRle_trans (integral_abs_bound f a ((b - a) ↾ int_obligation_1 a b AB) M H0)). simpl. rewrite Qmult_comm, <- (Qmult_comm M). rewrite <- CRmult_Qmult, <- CRmult_Qmult. apply CRmult_le_compat_l. exact Mpos. apply CRle_Qle. apply Qle_Qabs. - unfold abs, abs_sig, CR_abs, proj1_sig. rewrite CRabs_opp. assert (∀ x : Q, b ≤ x ≤ b + ` ((a - b) ↾ int_obligation_2 a b AB) → CRabs (f x) ≤ ' M). { intros. apply A. split; simpl. apply (Qle_trans _ b). apply meet_lb_r. apply H0. simpl in H0. apply (Qle_trans _ a). destruct H0. ring_simplify in H1. exact H1. apply join_ub_l. } apply (CRle_trans (integral_abs_bound f b ((a - b) ↾ int_obligation_2 a b AB) M H0)). unfold proj1_sig, stdlib_rationals.Abs_instance_0. rewrite Qmult_comm, <- (Qmult_comm M). rewrite <- CRmult_Qmult, <- CRmult_Qmult. apply CRmult_le_compat_l. exact Mpos. apply CRle_Qle. rewrite (Qabs_Qminus b a). apply Qle_Qabs. 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