proposition: Lemma Integrate01_correct_generalize : forall (a b : Q) (F : PartFunct IR) (f : Q_as_MetricSpace --> CR) (e : Qpos), (forall (o : Q) (H : Dom F (inj_Q IR o)), a <= o <= b -> msp_eq (f o) (IRasCR (F (inj_Q IR o) H))) -> forall (H01 : inj_Q IR a [<=] inj_Q IR b) (HF : Continuous_I H01 F) (c : a < b) (s : StepQ), QposInf_le (Qpos2QposInf (SupDistanceToLinear s c)) (mu f ((1 # 2) * e)) -> @AbsSmall CRasCOrdField (' ((b - a) * proj1_sig e)%Q)%CR (IRasCR (integral (inj_Q IR a) (inj_Q IR b) H01 F HF) - (' ((b - a) * IntegralQ (dist_raw (uc_stdFun f ^@> s) ((1 # 2) * e)%Qpos))%Q))%CR.
proof: Proof. intros a b F f e Hf Hab HF Hab0 s Hs. destruct (Qpos_sub _ _ Hab0) as [ba Hba]. stepl ('proj1_sig (ba*e)%Qpos)%CR. 2: simpl; rewrite Hba; rewrite Qplus_comm; unfold Qminus; rewrite <- Qplus_assoc, Qplus_opp_r, Qplus_0_r; reflexivity. revert a b Hab0 ba Hba F Hab HF Hf Hs. induction s; intros a b Hab0 ba Hba F Hab HF Hf Hs. - change (IntegralQ (dist_raw (constStepF (uc_stdFun f) <@^ x) ((1 # 2) * e)%Qpos)) with (approximate (f x) ((1 # 2) * e)%Qpos). rewrite <- (IR_inj_Q_as_CR ((b - a) * approximate (f x) ((1 # 2) * e)%Qpos)). unfold cg_minus. simpl. eapply AbsSmall_wdr;[|apply IR_minus_as_CR]. eapply AbsSmall_wdl;[|apply IR_inj_Q_as_CR]. rewrite <- IR_AbsSmall_as_CR. unfold SupDistanceToLinear in Hs. simpl in Hs. set (a0:=inj_Q IR (approximate (f x) ((1 # 2) * e)%Qpos)). set (e':=(inj_Q IR (proj1_sig e))). assert (X:forall y : IR, Compact Hab y -> forall Hy : Dom F y, AbsSmall e' ((F y Hy)[-]a0)). intros y Hy Hyf. rewrite -> IR_AbsSmall_as_CR. unfold e'. apply AbsSmall_wdr with (IRasCR (F y Hyf) - IRasCR a0)%CR;[|apply eq_symmetric; apply IR_minus_as_CR]. rewrite IR_inj_Q_as_CR. apply (CRAbsSmall_ball (IRasCR (F y Hyf))). unfold a0; rewrite -> IR_inj_Q_as_CR. assert (X0:(forall (q : Q) (Hq : Dom F (inj_Q IR q)), clcr (inj_Q IR a) (inj_Q IR b) (inj_Q IR q) -> (Cbind QPrelengthSpace f (' q) == IRasCR (F (inj_Q IR q) Hq))%CR)). intros q Hq [Hq0 H1]. pose proof (Cbind_correct QPrelengthSpace f). apply ucEq_equiv in H. rewrite -> (H (' q))%CR. clear H. rewrite -> (BindLaw1 f). apply Hf. split. apply (leEq_inj_Q IR). auto. apply (leEq_inj_Q IR). auto. assert (X:=@ContinuousCorrect (clcr (inj_Q IR a) (inj_Q IR b)) (inj_Q_less _ _ _ Hab0) F (Continuous_Int (clcr (inj_Q IR a) (inj_Q IR b)) Hab Hab F HF) (Cbind QPrelengthSpace f) X0 y Hyf Hy). set (z:=(' approximate (f x) ((1 # 2) * e)%Qpos)%CR). rewrite -> X. setoid_replace (proj1_sig e) with (proj1_sig ((1#2)*e + (1#2)*e)%Qpos) by (simpl; ring). apply ball_triangle with (f x); [|apply ball_approx_r]. rewrite <- (BindLaw1 f). pose proof (Cbind_correct QPrelengthSpace f) as H. apply ucEq_equiv in H. rewrite <- (H (Cunit_fun Q_as_MetricSpace x)). clear H. set (z0:=(Cbind QPrelengthSpace f (Cunit_fun Q_as_MetricSpace x))). apply: uc_prf. clear z X X0 Hyf. pose (mu f ((1#2)*e)%Qpos) as z. simpl. simpl in z. simpl in Hs. fold z in Hs. fold CR z. destruct z as [z|];[|constructor]. unfold ball_ex. eapply ball_weak_le. apply Hs. change (Cunit_fun Q_as_MetricSpace x) with ('x)%CR. rewrite <- IR_inj_Q_as_CR. rewrite <- CRAbsSmall_ball. autorewrite with QposElim. unfold cg_minus; simpl. eapply AbsSmall_wdr;[|apply IR_minus_as_CR]. eapply AbsSmall_wdl;[|apply IR_inj_Q_as_CR]. rewrite <- IR_AbsSmall_as_CR. apply AbsIR_imp_AbsSmall. assert(X:=leEq_or_leEq _ (inj_Q IR x) y). rewrite -> leEq_def. intros Y. apply X. clear X. intros X. revert Y. change (Not (inj_Q IR (Qmax (x - a) (b - x))[<]AbsIR (y[-]inj_Q IR x))). rewrite <- leEq_def. apply AbsSmall_imp_AbsIR. destruct X as [X|X]. apply leEq_imp_AbsSmall. apply shift_leEq_lft; assumption. apply leEq_transitive with (inj_Q IR (b - x)%Q). stepr ((inj_Q IR b)[-](inj_Q IR x)); [| now (apply eq_symmetric; apply inj_Q_minus)]. apply minus_resp_leEq. destruct Hy; assumption. apply inj_Q_leEq. apply Qmax_ub_r. apply AbsSmall_minus. apply leEq_imp_AbsSmall. apply shift_leEq_lft; assumption. apply leEq_transitive with (inj_Q IR (x - a)%Q). stepr ((inj_Q IR x)[-](inj_Q IR a)); [| now (apply eq_symmetric; apply inj_Q_minus)]. apply minus_resp_leEq_rht. destruct Hy; assumption. apply inj_Q_leEq. apply Qmax_ub_l. split. apply shift_leEq_minus. stepl (([--]e'[+]a0)[*](inj_Q IR b[-]inj_Q IR a)). apply lb_integral. intros y Hy Hyf. apply shift_plus_leEq. destruct (X y Hy Hyf); assumption. rstepl ([--]((inj_Q IR b[-]inj_Q IR a)[*]e') [+] (inj_Q IR b[-]inj_Q IR a)[*]a0). csetoid_replace (inj_Q IR b[-]inj_Q IR a) (inj_Q IR (b-a)%Q); [|apply eq_symmetric; apply inj_Q_minus]. apply bin_op_wd_unfolded. apply un_op_wd_unfolded. unfold e'. stepl (inj_Q IR ((b-a)*proj1_sig e)%Q); [| now apply inj_Q_mult]. apply: inj_Q_wd;simpl. autorewrite with QposElim. rewrite Hba. ring. apply eq_symmetric; apply inj_Q_mult. apply shift_minus_leEq. stepr ((e'[+]a0)[*](inj_Q IR b[-]inj_Q IR a)). apply ub_integral. intros y Hy Hyf. apply shift_leEq_plus. destruct (X y Hy Hyf); assumption. rstepl (((inj_Q IR b[-]inj_Q IR a)[*]e') [+] (inj_Q IR b[-]inj_Q IR a)[*]a0). csetoid_replace (inj_Q IR b[-]inj_Q IR a) (inj_Q IR (b-a)%Q); [|apply eq_symmetric; apply inj_Q_minus]. apply bin_op_wd_unfolded. unfold e'. stepl (inj_Q IR ((b-a)*proj1_sig e)%Q); [| now apply inj_Q_mult]. apply: inj_Q_wd;simpl. rewrite Hba. ring. apply eq_symmetric; apply inj_Q_mult. - set (z:=(IntegralQ (glue o (Map (fun z : RegularFunction Qball => approximate z ((1 # 2) * e)%Qpos) (Map f s1):StepQ) (Map (fun z : RegularFunction Qball => approximate z ((1 # 2) * e)%Qpos) (Map f s2))))). change (IntegralQ (dist_raw (uc_stdFun f ^@> glue o s1 s2) ((1 # 2) * e)%Qpos)) with z. apply (CRAbsSmall_ball (IRasCR (integral (inj_Q IR a) (inj_Q IR b) Hab F HF))). set (c:=(affineCombo (OpenUnitDual o) a b:Q)). assert (Hac:inj_Q IR a[<=]inj_Q IR c). unfold c. apply inj_Q_leEq. simpl; auto with *. assert (Hcb:inj_Q IR c[<=]inj_Q IR b). unfold c. apply inj_Q_leEq. simpl; auto with *. assert (HFl :Continuous_I Hac F). revert HF. apply included_imp_contin. intros x [Hxl Hxr]. split; auto. apply leEq_transitive with (inj_Q IR c); auto. assert (HFr :Continuous_I Hcb F). revert HF. apply included_imp_contin. intros x [Hxl Hxr]. split; auto. apply leEq_transitive with (inj_Q IR c); auto. setoid_replace (IRasCR (integral _ _ Hab F HF)) with (IRasCR (integral _ _ Hac F HFl)+IRasCR (integral _ _ Hcb F HFr))%CR; [| now (rewrite <- IR_plus_as_CR;apply IRasCR_wd; apply eq_symmetric; apply integral_plus_integral)]. unfold z. rewrite -> Integral_glue. clear z. set (zl:=IntegralQ (Map (fun z : RegularFunction Qball => approximate z ((1 # 2) * e)%Qpos) (Map f s1))). set (zr:=IntegralQ (Map (fun z : RegularFunction Qball => approximate z ((1 # 2) * e)%Qpos) (Map f s2))). setoid_replace ((b - a) * (o * zl + (1 - o) * zr))%Q with ((c - a)*zl + (b - c)*zr)%Q; [| now (unfold c, affineCombo, OpenUnitDual; simpl; ring)]. assert (Hac0: a < c). unfold c; auto with*. assert (Hcb0: c < b). unfold c; auto with*. destruct (Qpos_sub _ _ Hac0) as [ca Hca]. destruct (Qpos_sub _ _ Hcb0) as [bc Hbc]. assert (Z:(QposEq ba (ca + bc))%Qpos). unfold QposEq. rewrite -> Hba in Hbc. rewrite -> Hca in Hbc. replace LHS with (- a + (a + proj1_sig ba))%Q by simpl; ring. rewrite Hbc. simpl. ring. assert (QposEq (ba*e) ((ca+bc)*e)). { unfold QposEq. simpl. unfold QposEq in Z. rewrite Z. reflexivity. } clear Z. unfold QposEq in H. rewrite H. clear H. assert (QposEq ((ca + bc)*e) (ca*e + bc*e)) by (unfold QposEq; simpl; ring). unfold QposEq in H. rewrite H. clear H. rewrite <- CRAbsSmall_ball. setoid_replace (@cg_minus CRasCGroup (IRasCR (integral (inj_Q IR a) (inj_Q IR c) Hac F HFl) + IRasCR (integral (inj_Q IR c) (inj_Q IR b) Hcb F HFr))%CR (' ((c - a) * zl + (b - c) * zr)%Q)%CR) with ((IRasCR (integral (inj_Q IR a) (inj_Q IR c) Hac F HFl) - ('((c-a)*zl))%Q)+ ((IRasCR (integral (inj_Q IR c) (inj_Q IR b) Hcb F HFr) - ('((b - c) * zr)%Q))))%CR. stepl ('proj1_sig (ca * e)%Qpos + 'proj1_sig (bc * e)%Qpos)%CR. apply: AbsSmall_plus. apply (IHs1 _ _ Hac0); auto. intros o0 H [H0 H1]. apply Hf. split; eauto with qarith. destruct (mu f ((1#2)*e)) as [q|];[|constructor]. simpl in Hs|-*. eapply Qle_trans;[|apply Hs]. rewrite -> SupDistanceToLinear_glue. replace LHS with (proj1_sig (SupDistanceToLinear s1 (affineCombo_gt (OpenUnitDual o) Hab0))). apply Qmax_ub_l. apply SupDistanceToLinear_wd1; reflexivity. apply (IHs2 _ _ Hcb0); auto. intros o0 H [H0 H1]. apply Hf. clear - H0 H1 Hac0. split; eauto with qarith. destruct (mu f ((1#2)*e)) as [q|];[|constructor]. simpl in Hs|-*. eapply Qle_trans;[|apply Hs]. rewrite -> SupDistanceToLinear_glue. replace LHS with (proj1_sig (SupDistanceToLinear s2 (affineCombo_lt (OpenUnitDual o) Hab0))). apply Qmax_ub_r. apply SupDistanceToLinear_wd1; reflexivity. change (' proj1_sig (ca * e)%Qpos + ' proj1_sig (bc * e)%Qpos ==(' proj1_sig (ca * e + bc * e)%Qpos))%CR. unfold Qpos_mult, Qpos_plus, proj1_sig. ring. generalize (IRasCR (integral (inj_Q IR a) (inj_Q IR c) Hac F HFl)) (IRasCR (integral (inj_Q IR c) (inj_Q IR b) Hcb F HFr)). intros x y. clear - x y. change (@cg_minus CRasCGroup (x + y)%CR (' ((c - a) * zl + (b - c) * zr)%Q)%CR) with (x + y - ' ((c - a) * zl + (b - c) * zr)%Q)%CR. ring. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.metric2.IntegrableFunction CoRN.model.metric2.BoundedFunction CoRN.model.metric2.CRmetric CoRN.reals.fast.CRArith CoRN.reals.fast.CRIR CoRN.ftc.Integral CoRN.model.structures.StepQsec CoRN.model.structures.OpenUnit CoRN.model.totalorder.QMinMax CoRN.model.totalorder.QposMinMax Coq.QArith.Qabs CoRN.tactics.Qauto Coq.QArith.Qround CoRN.model.metric2.L1metric CoRN.model.metric2.LinfMetric CoRN.model.ordfields.Qordfield CoRN.algebra.COrdFields2 CoRN.model.metric2.Qmetric CoRN.reals.fast.ContinuousCorrect CoRN.ftc.IntegrationRules CoRN.ftc.MoreIntegrals CoRN.tactics.CornTac CoRN.model.metric2.LinfDistMonad