proposition: Lemma CompactGraph_b_correct3 : forall plX plFEX p s, inCompact p (CompactGraph_b plFEX s) -> msp_eq (Cbind plX f (Cfst p)) (Csnd p).
proof: Proof. intros plX plFEX p s H. apply ball_eq. intros e1 epos. apply regFunBall_e. intros e2. set (e':=((1#6)*exist _ _ epos)%Qpos). setoid_replace (proj1_sig e2 + e1 + proj1_sig e2) with (proj1_sig ((e2 + e') + ((e' + e') + (e' + e')) + (e2 + e'))%Qpos) by (unfold e'; simpl; ring). set (d' := graphPoint_modulus f ((1#2)*e')). assert (Hd'1 : proj1_sig d' <= proj1_sig e'). unfold d', graphPoint_modulus. destruct (mu f ((1#2)*e')); autorewrite with QposElim. apply Qle_trans with ((1#2)*proj1_sig e'); auto with *. rewrite <- (Qmult_1_l (proj1_sig e')) at 2. apply Qmult_le_r. apply Qpos_ispos. discriminate. rewrite <- (Qmult_1_l (proj1_sig e')). apply Qmult_le_r. apply Qpos_ispos. discriminate. assert (Hd'2 : QposInf_le (d') (mu f ((1#2)*e'))). unfold d', graphPoint_modulus. destruct (mu f ((1#2)*e')). apply Qpos_min_lb_r. constructor. assert (H':= H ((1#2)*d')%Qpos d'). apply ball_triangle with (approximate (Csnd p) (Qpos2QposInf ((1#2)%Qpos*d'))). simpl (approximate (Cbind plX f (Cfst (X:=X) (Y:=Y) p)) e2). apply ball_triangle with (approximate (f (Cfst_raw p (Qpos2QposInf (1#2)*d'))) (Qpos2QposInf (1#2)*d'))%Qpos. unfold Cjoin_raw. simpl. apply ball_weak_le with (proj1_sig ((1#2)*e2 + ((1#2)*e2 + (1#2)*e') + (1#2)*d')%Qpos). simpl. clear - Hd'1. rewrite -> Qle_minus_iff in *. setoid_replace (proj1_sig e2 + (1 # 6) * e1 + - ((1 # 2) * proj1_sig e2 + ((1 # 2) * proj1_sig e2 + (1 # 2) * ((1 # 6) * e1)) + (1 # 2) * proj1_sig d')) with ((1 # 2) * (proj1_sig e' + - proj1_sig d')) by (simpl; ring). apply Qmult_le_0_compat. discriminate. exact Hd'1. cut (ball ((1 # 2) * proj1_sig e2 + (1 # 2) * proj1_sig e') (f (Cfst_raw p (mu f ((1 # 2) * e2)))) (f (Cfst_raw p ((1 # 2) * d')%Qpos))). intros L. apply L. apply (mu_sum plX ((1#2)*e') (((1#2)*e2)::nil) f)%Qpos. apply ball_ex_weak_le with (QposInf_plus (mu f ((1#2)*e2)) (Qpos2QposInf (1#2)*d'))%Qpos. simpl. destruct (@mu X (Complete Y) f (Qpos_mult (@exist Q (Qlt {| Qnum := Z0; Qden := xH |}) {| Qnum := Z.pos xH; Qden := xO xH |} (@eq_refl comparison Lt)) e2)) ; try constructor. simpl in Hd'2. destruct (@mu X (Complete Y) f (Qpos_mult (@exist Q (Qlt {| Qnum := Z0; Qden := xH |}) {| Qnum := Z.pos xH; Qden := xO xH |} (@eq_refl comparison Lt)) e')) ; try constructor. clear - Hd'2. simpl in *. apply Qplus_le_r. refine (Qle_trans _ _ _ _ Hd'2). rewrite <- (Qmult_1_l (proj1_sig d')) at 2. apply Qmult_le_r. apply Qpos_ispos. discriminate. unfold Cfst_raw. assert (Z:=regFun_prf_ex p (mu f ((1#2)*e2)) (Qpos2QposInf (1#2)%Qpos*d')). destruct (mu f ((1#2)*e2)); try constructor. destruct Z; auto. assert (L:existsC X (fun x => ball (proj1_sig (((1#2)*d') + d')%Qpos) (approximate p (Qpos2QposInf (1#2)%Qpos*d')) (Couple_raw ((Cunit x), (f x)) (Qpos2QposInf ((1#2)*d')%Qpos)))). clear -H'. simpl in H'. unfold Cjoin_raw in H'. simpl in H'. unfold FinEnum_map_modulus, graphPoint_modulus in H'. remember (match mu f ((1 # 2) * d') with | Qpos2QposInf d => Qpos_min ((1 # 2) * d') d | QposInfinity => ((1 # 2) * d')%Qpos end) as mm. simpl in Heqmm. rewrite <- Heqmm in H'. induction (@approximate _ (FinEnum_ball X) s mm). exfalso; exact (FinSubset_ball_nil H'). apply FinSubset_ball_orC in H'. destruct H' as [G | H | H] using orC_ind. intro abs; contradict G; intro G; contradiction. apply existsWeaken. exists a. apply H. auto. clear - L Hd'1 Hd'2 plX. destruct L as [G | a [Hl Hr]] using existsC_ind. apply (msp_stable (msp _)), G. apply ball_triangle with (approximate (f a) (Qpos2QposInf ((1#2)%Qpos*d'))). apply ball_weak_le with (proj1_sig ((1#2)*d' + ((1#2)*e' + (1#2)*e') + (1#2)*d')%Qpos). clear - Hd'1. simpl. rewrite -> Qle_minus_iff in *. setoid_replace ( (1 # 6) * e1 + (1 # 6) * e1 + - ((1 # 2) * proj1_sig d' + ((1 # 2) * ((1 # 6) * e1) + (1 # 2) * ((1 # 6) * e1)) + (1 # 2) * proj1_sig d')) with (proj1_sig e' + - proj1_sig d') by (simpl; ring). exact Hd'1. simpl. rewrite <- ball_Cunit. eapply ball_triangle;[|apply (ball_approx_r _ ((1#2)*d')%Qpos)]. eapply ball_triangle;[apply (ball_approx_l _ ((1#2)*d'))|]. apply (mu_sum plX ((1#2)*e') (((1#2)*e')::nil) f)%Qpos. simpl. unfold graphPoint_modulus in d'. apply ball_ex_weak_le with (d' + d')%Qpos. clear - Hd'2. simpl in Hd'2. destruct (@mu X (Complete Y) f (Qpos_mult (@exist Q (Qlt {| Qnum := Z0; Qden := xH |}) {| Qnum := Z.pos xH; Qden := xO xH |} (@eq_refl comparison Lt)) e')) ; try constructor. simpl in *. apply Qplus_le_compat; exact Hd'2. simpl. eapply ball_weak_le;[|apply Hl]. simpl. apply Qplus_le_l. rewrite <- (Qmult_1_l (proj1_sig d')) at 2. apply Qmult_le_r. apply Qpos_ispos. discriminate. apply ball_sym. eapply ball_weak_le;[|apply Hr]. apply Qplus_le_compat. 2: exact Hd'1. refine (Qle_trans _ _ _ _ Hd'1). rewrite <- (Qmult_1_l (proj1_sig d')). apply Qmult_le_r. apply Qpos_ispos. discriminate. eapply ball_weak_le;[|apply (regFun_prf (Csnd p) ((1#2)*d')%Qpos)]. rewrite Qplus_comm. apply Qplus_le_r. refine (Qle_trans _ _ _ _ Hd'1). rewrite <- (Qmult_1_l (proj1_sig d')). apply Qmult_le_r. apply Qpos_ispos. discriminate. Qed.
imports: CoRN.metric2.UniformContinuity CoRN.metric2.Compact CoRN.metric2.Prelength CoRN.metric2.CompleteProduct CoRN.model.totalorder.QposMinMax CoRN.model.totalorder.QMinMax CoRN.logic.Classic