proposition: Lemma CompactGraph_correct3 : forall plX plFEX p s, inCompact p (CompactGraph plFEX s) -> msp_eq (Cmap 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 e'). assert (Hd'1 : proj1_sig d' <= proj1_sig e'). unfold d', graphPoint_modulus. destruct (mu f e'); auto with *. apply Qpos_min_lb_l. assert (Hd'2 : QposInf_le d' (mu f e')). unfold d', graphPoint_modulus. destruct (mu f e'). apply Qpos_min_lb_r. constructor. assert (H':= H d' d'). apply ball_triangle with (approximate (Csnd p) d'). apply ball_triangle with (f (Cfst_raw p d')). apply (mu_sum plX e' (e2::nil) f). simpl. apply ball_ex_weak_le with (mu f e2 + d')%QposInf. destruct (mu f e2); try constructor. destruct (mu f e'); try constructor. clear - Hd'2. simpl in *. apply Qplus_le_r. exact Hd'2. unfold Cfst_raw. simpl. assert (Z:=regFun_prf_ex p (mu f e2) d'). destruct (mu f e2); try constructor. destruct Z; auto. assert (L:existsC X (fun x => ball (proj1_sig d' + proj1_sig d') (approximate p d') (x, (f x)))). clear -H'. simpl in H'. unfold FinEnum_map_modulus, graphPoint_modulus in H'. induction (@approximate _ (FinEnum_ball X) s (Qpos2QposInf match @mu X Y f d' return Qpos with | Qpos2QposInf d => Qpos_min d' d | QposInfinity => d' end)). 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 (f a). simpl. apply (mu_sum plX e' (e'::nil) f). simpl. unfold graphPoint_modulus in d'. apply ball_ex_weak_le with (d' + d')%Qpos. clear - Hd'2. destruct (mu f e'); try constructor. simpl in *. apply Qplus_le_compat; exact Hd'2. apply Hl. apply ball_sym. eapply ball_weak_le;[|apply Hr]. simpl. clear - Hd'1. apply Qplus_le_compat; exact Hd'1. eapply ball_weak_le;[|apply regFun_prf]. simpl. rewrite Qplus_comm. apply Qplus_le_r. exact Hd'1. 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