proposition: Lemma Integrate01_correct : forall F (H01:[0][<=]([1]:IR)) (HF:Continuous_I H01 F) (f:Q_as_MetricSpace --> CR), (forall (o:Q) H, (0 <= o <= 1) -> (f o == IRasCR (F (inj_Q IR o) H)))%CR -> (IRasCR (integral [0] [1] H01 F HF)==Integrate01 f)%CR.
proof: Proof. intros F H01' HF' f Hf. assert (H01:(inj_Q IR 0)[<=](inj_Q IR 1)). { apply inj_Q_leEq. discriminate. } assert (HF:Continuous_I H01 F). { apply (included_imp_contin _ _ H01'). apply included_compact. apply (compact_wd _ _ H01' [0]). apply compact_inc_lft. apply eq_symmetric; apply (inj_Q_nring IR 0). apply (compact_wd _ _ H01' [1]). apply compact_inc_rht. rstepl (nring 1:IR). apply eq_symmetric; apply (inj_Q_nring IR 1). assumption. } transitivity (IRasCR (integral _ _ H01 F HF)). apply IRasCR_wd. apply integral_wd'. apply eq_symmetric; apply (inj_Q_nring IR 0). rstepl (nring 1:IR). apply eq_symmetric; apply (inj_Q_nring IR 1). clear H01' HF'. apply ball_eq. intros e epos. setoid_replace e with (proj1_sig ((1#2)*exist _ _ epos + (1#2)*exist _ _ epos)%Qpos) by (simpl; ring). generalize ((1#2)*exist _ _ epos)%Qpos. clear epos e. intros e. eapply ball_triangle; [|apply (@ball_approx_l Q_as_MetricSpace)]. change (Cunit (approximate (Integrate01 f) e)) with ('(approximate (Integrate01 f) e))%CR. setoid_replace ('(approximate (Integrate01 f) e))%CR with ('((1-0)*(approximate (Integrate01 f) e))%Q)%CR. Focus 2. change (' approximate (Integrate01 f) e == ' ((1 - 0) * approximate (Integrate01 f) e)%Q)%CR. ring. rewrite <- CRAbsSmall_ball. stepl ('((1-0)*proj1_sig e)%Q)%CR; [| apply inject_Q_CR_wd; change ((1 - 0) * proj1_sig e == proj1_sig e)%Q; ring]. set (z:=(integral (inj_Q IR 0) (inj_Q IR 1) H01 F HF)). simpl. unfold Cjoin_raw. simpl. unfold distribComplete_raw. unfold id01_raw. assert (X:=stepSampleDistanceToId (id01_raw_help (mu f ((1 # 2) * e)))). revert X. remember (stepSample (id01_raw_help (mu f ((1 # 2) * e)))) as s. simpl in Heqs. rewrite <- Heqs. clear Heqs. intros Hs. assert (X:QposInf_le (Qpos2QposInf (SupDistanceToLinear s (pos_one Q_as_COrdField))) (mu f ((1 # 2) * e))). destruct (mu f ((1#2) *e)); try constructor. unfold QposEq in Hs. simpl. rewrite -> Hs. apply id01_raw_help_le. clear Hs. rename X into Hs. revert s Hs. generalize (pos_one Q_as_COrdField). intros c s Hs. simpl in c, Hs. revert c s Hs. unfold z. clear z. revert H01 HF. revert Hf. apply Integrate01_correct_generalize. 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