proposition: Lemma mu_sum : forall e0 (es : list Qpos) (f:UniformlyContinuousFunction X Y) a b, ball_ex (fold_right QposInf_plus (mu f e0) (map (mu f) es)) a b -> ball (proj1_sig (fold_right Qpos_plus e0 es)) (f a) (f b).
proof: Proof. intros e0 es f a b Hab. apply ball_closed. intros e' epos. setoid_replace (proj1_sig (fold_right Qpos_plus e0 es + exist _ _ epos)%Qpos) with (proj1_sig (fold_right Qpos_plus e0 (exist _ _ epos::es))) by (simpl; ring). set (ds := map (mu f) es) in *. set (d0 := (mu f e0)) in *. set (d' := (mu f (exist _ _ epos))) in *. assert (H:{ds' | (map Qpos2QposInf ds')=d0::d'::ds}+{In QposInfinity (d0::d'::ds)}). generalize (d0::d'::ds); clear. induction l as [|[d|] ds]. left. exists (@nil Qpos). reflexivity. destruct IHds as [[ds' Hds']|Hds]. left. exists (d::ds'). rewrite <- Hds'. reflexivity. firstorder. firstorder. destruct H as [[ds' Hds']|Hds]. destruct ds' as [|g0 [|g' gs]]; try discriminate Hds'. inversion Hds'. clear Hds'. unfold d0 in *; clear d0. unfold d' in *; clear d'. unfold ds in *; clear ds. replace (fold_right QposInf_plus (mu f e0) (map (mu f) es)) with (Qpos2QposInf (fold_right Qpos_plus g0 gs)) in Hab. simpl in Hab. assert (proj1_sig (fold_right Qpos_plus g0 gs) < Qpos_sum ((g' :: gs)++(g0::nil))) as H. { simpl. apply (Qle_lt_trans _ (Qpos_sum (gs ++ g0::nil))). clear - g0. induction gs. simpl. rewrite Qplus_0_r. apply Qle_refl. simpl. apply Qplus_le_r, IHgs. rewrite -> Qlt_minus_iff. ring_simplify. destruct g'; exact q. } case (trail _ _ _ _ Hab H). clear Hab H. cut (map Qpos2QposInf (g' :: gs) = map (mu f) (exist _ _ epos :: es)). clear H2 H1. generalize (exist _ _ epos::es) (g'::gs) a. clear gs g' es epos e' a. induction l as [|e es]; intros gs a Hes x [Ha Hb] H; destruct gs; try discriminate Hes. simpl in *. apply uc_prf. rewrite <- H0. rewrite <- Hb. rewrite <- Ha. simpl. apply (H 0%nat g0). auto with *. simpl. inversion Hes; clear Hes. eapply ball_triangle. apply uc_prf. rewrite <- H2. rewrite <- Ha. simpl; apply (H 0%nat g0). simpl; auto with *. apply (IHes _ (x 1%nat) H3 (fun i => x (S i))). auto with *. intros. apply (H (S i) z). simpl; auto with *. simpl; congruence. rewrite <- H2. rewrite <- H0. clear - gs. induction gs. reflexivity. simpl. rewrite <- IHgs. reflexivity. assert (H:forall (e:Qpos) es, proj1_sig e < proj1_sig (fold_right Qpos_plus e0 es)%Qpos -> (mu f e)=QposInfinity -> ball (m:=Y) (proj1_sig (fold_right Qpos_plus e0 es)) (f a) (f b)). { intros e esx He Hmu. apply ball_weak_le with (proj1_sig e);[apply Qlt_le_weak; assumption|]. apply uc_prf. rewrite Hmu. constructor. } case (in_inv Hds). intros Hd0. apply H with e0. clear - es. induction es. simpl. rewrite -> Qlt_minus_iff. ring_simplify. exact epos. simpl. apply (Qlt_le_trans _ _ _ IHes). simpl. apply Qplus_le_r. rewrite <- Qplus_0_l, Qplus_assoc. apply Qplus_le_l. rewrite Qplus_0_r. apply Qpos_nonneg. assumption. clear Hds. change (d'::ds) with (map (mu f) (exist _ _ epos::es)). induction (exist _ _ epos::es); intros Hds. elim Hds. simpl in Hds. destruct Hds as [Ha0|Hds]. apply H with a0. simpl. rewrite -> Qlt_minus_iff. ring_simplify. destruct (fold_right Qpos_plus e0 l); exact q. assumption. simpl. eapply ball_weak_le with (proj1_sig (fold_right Qpos_plus e0 l)). simpl. rewrite -> Qle_minus_iff; ring_simplify. auto with *. auto. 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