proposition: Lemma Cap_fun_correct : forall X Y plX (f:Complete (X --> Y)) x, msp_eq (Cap_fun plX f x) (Cap_slow_fun f x).
proof: Proof. intros X Y plX f x e1 e2. pose (exist (Qlt 0) (1#2) eq_refl) as half. simpl. unfold Cap_raw, Cap_slow_raw. set (e1':=(half * e1)%Qpos). set (e2':=(half * e2)%Qpos). rewrite Qplus_0_r. change (ball (proj1_sig e1 + proj1_sig e2) (approximate (Cmap plX (approximate f (half * e1)%Qpos) x) e1') (approximate (Cmap_slow (approximate f (half * e2)%Qpos) x) e2')). setoid_replace (proj1_sig e1 + proj1_sig e2) with (proj1_sig (e1' + ((half * e1)%Qpos + (half * e2)%Qpos) + e2'))%Qpos by (unfold e1', e2'; simpl; ring). generalize x e1' e2'. assert (ball (proj1_sig (half * e1 + half * e2)%Qpos) (Cmap plX (approximate f (half * e1)%Qpos)) (Cmap_slow (approximate f (half * e2)%Qpos))). { assert (QposEq (half * e1 + half * e2) (half * e1 + half * e2)) by reflexivity. apply (ball_wd _ H _ _ (Cmap_correct _ _) _ _ (reflexivity _)). set (f1:=(approximate f (half * e1)%Qpos)). set (f2:=(approximate f (half * e2)%Qpos)). apply Cmap_strong_slow_prf. apply (@regFun_prf _ (@ball (X-->Y))). } apply H. Qed.
imports: CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.metric2.Complete CoRN.model.totalorder.QMinMax CoRN.model.totalorder.QposMinMax CoRN.stdlib_omissions.List CoRN.stdlib_omissions.Q