proposition: Lemma integral_approximation (a : Q) (w : QnonNeg) (e : Qpos) : exists N : positive, forall n : positive, (N <= n)%positive -> mspc_ball e (riemann_sum a (proj1_sig w) n) (∫ f a w).
proof: Proof. destruct (Qlt_le_dec 1 (proj1_sig w)) as [A1 | A1]. * assert (0 < proj1_sig w) by (apply (Qlt_trans _ 1); auto with qarith). set (N := Z.to_pos (Qceiling (comp_inf (λ x, proj1_sig w / x) (lmu a (proj1_sig w)) 0 (proj1_sig e / proj1_sig w)))). exists N; intros n A2. assert (Qinf.eq (proj1_sig e) (proj1_sig e / proj1_sig w * proj1_sig w)). { simpl. unfold canonical_names.equiv. unfold stdlib_rationals.Q_eq. field. intro abs. rewrite abs in H. exact (Qlt_irrefl 0 H). } rewrite H0. clear H0. assert (P : 0 < proj1_sig e / proj1_sig w). { (apply Qmult_lt_0_compat; [| apply Qinv_lt_0_compat]; auto). } change (proj1_sig e / proj1_sig w) with (proj1_sig (exist _ _ P)). apply (Riemann_sums_approximate_integral' a w ((exist (Qlt 0) (proj1_sig e / proj1_sig w) P))). change (` (exist (Qlt 0) (` e / proj1_sig w) P)) with (proj1_sig e / proj1_sig w). destruct (lmu a (proj1_sig w) (proj1_sig e / proj1_sig w)) as [mu |] eqn:A3; [| easy]. subst N; unfold comp_inf in A2; rewrite A3 in A2. change (step (proj1_sig w) n <= mu); unfold step. setoid_replace (1#n) with (/(n#1)) by reflexivity. assert (0 < mu) as A4. change (Qinf.lt 0 mu). rewrite <- A3. apply (@uc_pos _ (@sig_mspc_ball Q (msp_mspc_ball Q_as_MetricSpace) (@mspc_ball Q (msp_mspc_ball Q_as_MetricSpace) (proj1_sig w) a)) CR (msp_mspc_ball CR) (@restrict Q (msp_mspc_ball Q_as_MetricSpace) CR f a (proj1_sig w)) (lmu a (proj1_sig w))). trivial. trivial. apply Qle_div_l; auto. reflexivity. now apply Z.Ple_Zle_to_pos, Q.Zle_Qle_Qceiling in A2. * set (N := Z.to_pos (Qceiling (comp_inf (λ x, 1 / x) (lmu a (proj1_sig w)) 0 (proj1_sig e)))). exists N; intros n A2. apply (mspc_monotone (proj1_sig e * proj1_sig w)). + change (proj1_sig e * proj1_sig w <= proj1_sig e). rewrite <- (Qmult_1_r (proj1_sig e)) at 2. apply Qmult_le_compat_l; auto. apply Qpos_nonneg. + apply Riemann_sums_approximate_integral'. destruct (lmu a (proj1_sig w) (proj1_sig e)) as [mu |] eqn:A3; [| easy]. subst N; unfold comp_inf in A2; rewrite A3 in A2. change (step (proj1_sig w) n <= mu); unfold step. setoid_replace (1#n) with (/(n#1)) by reflexivity. assert (0 < mu) as A4. change (Qinf.lt 0 mu). rewrite <- A3. apply (@uc_pos _ (@sig_mspc_ball Q (msp_mspc_ball Q_as_MetricSpace) (@mspc_ball Q (msp_mspc_ball Q_as_MetricSpace) (proj1_sig w) a)) CR (msp_mspc_ball CR) (@restrict Q (msp_mspc_ball Q_as_MetricSpace) CR f a (proj1_sig w)) (lmu a (proj1_sig w))). trivial. apply (proj2_sig e). apply Qle_div_l; auto. reflexivity. apply Z.Ple_Zle_to_pos, Q.Zle_Qle_Qceiling in A2. apply (Qle_trans _ (1 / mu)); trivial. apply Qmult_le_compat_r; trivial. now apply Qinv_le_0_compat, Qlt_le_weak. 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