proposition: Lemma integrate_plus (f g : Q -> CR) `{@IsUniformlyContinuous Q (msp_mspc_ball Q_as_MetricSpace) CR (msp_mspc_ball CR) f f_mu, @IsUniformlyContinuous Q (msp_mspc_ball Q_as_MetricSpace) CR (msp_mspc_ball CR) g g_mu} (a : Q) (w : QnonNeg) : @integrate (f + g) (@Integral_instance_0 (f+g) _ (@uc_ulc _ _ _ _ _ _ (@sum_uc Q (msp_mspc_ball Q_as_MetricSpace) (msp_mspc_ball_ext Q_as_MetricSpace) f g _ _ _ _))) a w = ∫ f a w + ∫ g a w.
proof: Proof. apply ball_closed. intros e e_pos. mc_setoid_replace (0 + e) with e by ring. assert (he_pos : 0 < e / 2) by solve_propholds. assert (qe_pos : 0 < e / 4) by solve_propholds. destruct (integral_approximation f a w (exist _ _ qe_pos)) as [Nf F]. destruct (integral_approximation g a w (exist _ _ qe_pos)) as [Ng G]. destruct (@integral_approximation (f + g) (@Integral_instance_0 (f+g) _ (@uc_ulc _ _ _ _ _ _ (@sum_uc Q (msp_mspc_ball Q_as_MetricSpace) (msp_mspc_ball_ext Q_as_MetricSpace) f g _ _ _ _))) _ _ (@uc_ulc _ _ _ _ _ _ (@sum_uc Q (msp_mspc_ball Q_as_MetricSpace) (msp_mspc_ball_ext Q_as_MetricSpace) f g _ _ _ _)) a w (exist _ _ he_pos)) as [Ns S]. set (n := Pos.max (Pos.max Nf Ng) Ns). assert (Nf <= n)%positive by (transitivity (Pos.max Nf Ng); apply Pos.le_max_l). assert (Ng <= n)%positive by (transitivity (Pos.max Nf Ng); [apply Pos.le_max_r | apply Pos.le_max_l]). assert (Ns <= n)%positive by apply Pos.le_max_r. setoid_replace e with (e/2+e/2)%Q. apply ball_triangle with (b:= riemann_sum (f + g) a (proj1_sig w) n). - apply ball_sym, S; assumption. - rewrite riemann_sum_plus. mc_setoid_replace (e / 2) with (e / 4 + e / 4) by (field; split; discriminate). now apply mspc_ball_CRplus; [apply F | apply G]. - unfold Qdiv. rewrite <- Qmult_plus_distr_r. setoid_replace (/ 2 + / 2)%Q with 1%Q by reflexivity. rewrite Qmult_1_r. reflexivity. 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