proposition: Lemma Riemann_sums_approximate_integral (a: Q) (w: QnonNeg) (e: Qpos) (iw: Q) (n: nat): (S n * iw == proj1_sig w)%Q -> (iw <= lmu a (proj1_sig w) (proj1_sig e))%Qinf -> ball (proj1_sig e * proj1_sig w) (@cmΣ CRasCMonoid (S n) (fun i => 'iw * f (a + i * iw))%CR) (∫ f a w).
proof: Proof. intros A B. assert (ne_sn_0 : ~ S n == 0) by (change 0 with (inject_Z (Z.of_nat 0)); rewrite Q_of_nat_inj; apply S_O). assert (iw_nn : 0 <= iw) by (apply Qdiv_l in A; [| assumption]; rewrite A; apply Qmult_le_0_compat; [now auto|]; apply Qinv_le_0_compat, Qle_nat). set (iw' := exist _ iw iw_nn : QnonNeg ). change iw with (proj1_sig iw'). change (from_nat (S n) * iw' == w)%Qnn in A. rewrite <- A at 2. rewrite <- integral_repeated_additive. setoid_replace (proj1_sig e * proj1_sig w)%Q with (S n * (iw * proj1_sig e))%Q by (unfold QnonNeg.eq in A; simpl in A; rewrite Qmult_assoc; rewrite A; apply Qmult_comm). apply CRΣ_gball. intros m H. rewrite CRmult_scale. apply ball_sym. apply CRball.rational. setoid_replace (' (iw * proj1_sig e)) with (scale (proj1_sig iw') (' ` e)) by now rewrite <- scale_Qmult. apply integral_bounded; [apply CRnonNegQpos |]. intros x [A1 A2]. apply CRball.rational. apply (luc_gball a (proj1_sig w) (`iw')); trivial. + apply gball_Qabs. setoid_replace (a - (a + m * proj1_sig iw')) with (- (m * proj1_sig iw')) by ring. rewrite Qabs_opp. apply Qabs_le_nonneg; [Qauto_nonneg |]. apply Qle_trans with (y := (S n * proj1_sig iw')). apply Qmult_le_compat_r. apply Qlt_le_weak. rewrite <- Zlt_Qlt. now apply inj_lt. apply (proj2_sig iw'). change (S n * proj1_sig iw' == proj1_sig w) in A. rewrite <- A; reflexivity. + apply gball_Qabs, Qabs_Qle_condition. split. apply Qplus_le_l with (z := x), Qplus_le_l with (z := proj1_sig w). setoid_replace (- proj1_sig w + x + proj1_sig w) with x by ring. setoid_replace (a - x + x + proj1_sig w) with (a + proj1_sig w) by ring. apply Qle_trans with (y := (a + m * ` iw' + ` iw')); [easy |]. setoid_rewrite <- (Qmult_1_l (` iw')) at 2. change 1%Q with (inject_Z (Z.of_nat 1)). rewrite <- Qplus_assoc, <- Qmult_plus_distr_l, <- Zplus_Qplus, <- Nat2Z.inj_add. apply Qplus_le_r. change (S n * proj1_sig iw' == proj1_sig w) in A. rewrite <- A. apply Qmult_le_compat_r. rewrite <- Zle_Qle. apply inj_le. rewrite Nat.add_comm. now apply Nat.le_succ_l. apply (proj2_sig iw'). apply Qplus_le_l with (z := x), Qplus_le_l with (z := - proj1_sig w). setoid_replace (a - x + x + - proj1_sig w) with (a - proj1_sig w) by ring. setoid_replace (proj1_sig w + x + - proj1_sig w) with x by ring. apply Qle_trans with (y := a). rewrite <- (Qplus_0_r a) at 2. apply Qplus_le_r. change 0 with (-0). apply Qopp_le_compat, (proj2_sig w). apply Qle_trans with (y := a + m * ` iw'); [| easy]. rewrite <- (Qplus_0_r a) at 1. apply Qplus_le_r, Qmult_le_0_compat; [apply Qle_nat | apply (proj2_sig iw')]. + apply gball_Qabs, Qabs_Qle_condition; split. apply (Qplus_le_r (x + `iw')). setoid_replace (x + `iw' + - `iw') with x by ring. setoid_replace (x + (proj1_sig iw') + (a + m * proj1_sig iw' - x)) with (a + m * proj1_sig iw' + proj1_sig iw') by ring. apply A2. apply (Qplus_le_r (x - `iw')). setoid_replace (x - proj1_sig iw' + (a + m * proj1_sig iw' - x)) with (a + m * proj1_sig iw' - proj1_sig iw') by ring. setoid_replace (x - `iw' + `iw') with x by ring. apply Qle_trans with (y := a + m * proj1_sig iw'); [| easy]. apply Qminus_less. apply (proj2_sig iw'). 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