proposition: Lemma Riemann_plus (r: Range Q) (f g: sig (In r) → CR) n: Riemann r (λ x, f x + g x) n == Riemann r f n + Riemann r g n.
proof: Proof. Proof with auto. unfold Riemann. unfold cmΣ'. Admitted. Lemma Riemann_scale (r: Range Q) (f: sig (In r) → CR) (c: CR) n: Riemann r (CRmult c ∘ f)%prg n == c * Riemann r f n. Proof with auto. unfold Riemann. unfold cmΣ'. unfold Basics.compose. Admitted. Class Integral (r: Range Q) (f: sig (∈ r) → CR): Type := integral: sig (λ x: CR, ∀ e: Qpos, ∃ n: positive, ∀ m: positive, (n <= m)%positive → ball e (Riemann r f m) x). Implicit Arguments Integral [[r]]. Implicit Arguments integral [[r] [Integral]]. Notation "∫" := integral. Lemma integral_unique (r: Range Q) (f: sig (In r) → CR) {i0: Integral f} {i1: Integral f}: ` i0 == ` i1. Proof with auto. destruct i0, i1. simpl @proj1_sig. apply ball_eq. intros. set (h := (e1 * (1#2))%Qpos). setoid_replace e1 with (h+h)%Qpos. 2: subst h; unfold QposEq; simpl; ring. specialize (e h). specialize (e0 h). destruct e, e0. apply ball_triangle with (Riemann r f (Pmax x1 x2))... apply ball_sym... Qed.
imports: Unicode.Utf8 Program CRArith CRabs Qminmax Qauto Qround Qmetric stdlib_omissions.P stdlib_omissions.Z stdlib_omissions.Q stdlib_omissions.N metric2.Classified util.Container Ranges decision