proposition: Lemma CompactGraph_b_correct1 : forall plX plFEX x s, (inCompact x s) -> inCompact (Couple (x,(Cbind plX f x))) (CompactGraph_b plFEX s).
proof: Proof. intros plX plFEX x s Hs. unfold CompactGraph_b. setoid_replace (Couple (X:=X) (Y:=Y) (x, (Cbind plX f x))) with (Cbind plX graphPoint_b x). auto using CompactImage_b_correct1. intros e1 e2. rewrite Qplus_0_r. split. apply ball_weak_le with (proj1_sig (e1 + (graphPoint_modulus f ((1 # 2) * e2)))%Qpos) ;[|apply regFun_prf]. unfold graphPoint_modulus. destruct (mu f ((1#2)*e2)). simpl. rewrite Q_Qpos_min. assert (Qmin ((1#2)*proj1_sig e2) (proj1_sig q) <= ((1#2)*proj1_sig e2)) by auto with *. apply Qplus_le_r. apply (Qle_trans _ _ _ H). rewrite <- (Qmult_1_l (proj1_sig e2)) at 2. apply Qmult_le_r. apply Qpos_ispos. discriminate. simpl. apply Qplus_le_r. rewrite <- (Qmult_1_l (proj1_sig e2)) at 2. apply Qmult_le_r. apply Qpos_ispos. discriminate. simpl. unfold Cjoin_raw. rewrite <- ball_Cunit. setoid_replace (proj1_sig e1 + proj1_sig e2) with (proj1_sig ((1#2)*e1 + ((1#2)*e1 + (1#2)*e2) + (1#2)*e2)%Qpos) by (simpl; ring). eapply ball_triangle;[|apply ball_approx_r]. eapply ball_triangle. apply (ball_approx_l (approximate (Cmap_fun plX f x) (Qpos2QposInf ((1 # 2)%Qpos * e1))) ((1#2)*e1)). set (e1':=((1 # 2) * e1)%Qpos). set (e2':=((1 # 2) * e2)%Qpos). simpl. apply (mu_sum plX e2' (e1'::nil) f). apply ball_ex_weak_le with (e:= (mu f e1' + graphPoint_modulus f ((1 # 2) * e2))%QposInf). 2: apply regFun_prf_ex. unfold e1'. unfold graphPoint_modulus. replace (fold_right QposInf_plus (mu f e2') (map (mu f) (((1 # 2) * e1)%Qpos :: nil))) with (mu f ((1 # 2) * e1) + mu f e2')%QposInf by reflexivity. destruct (mu f ((1#2)*e1)) as [d0|]; try constructor. unfold e2'. destruct (mu f ((1 # 2) * e2)) as [d|]; try constructor. simpl. rewrite Q_Qpos_min. assert (Qmin (proj1_sig e2') (proj1_sig d) <= proj1_sig d) by auto with *. apply Qplus_le_r. exact H. 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