proposition: Lemma CRsum_list_prf : forall l, is_RegularFunction Qball (CRsum_list_raw l).
proof: Proof. intros [|a t] e1 e2. apply ball_refl. apply (Qpos_nonneg (e1 + e2)). unfold CRsum_list_raw. simpl. set (p:=P_of_succ_nat (@length (RegularFunction Qball) t)). set (e1':=((1 # p) * e1)%Qpos). set (e2':=((1 # p) * e2)%Qpos). simpl in e1'. fold e1'. simpl in e2'. fold e2'. assert (Qball (proj1_sig e1' + proj1_sig e2') (0 + @approximate Q Qball a e1') (0 + @approximate Q Qball a e2')) as H. { rewrite Qplus_0_l, Qplus_0_l. apply (regFun_prf a). } assert (forall e:Qpos, proj1_sig ((1 # p) * e)%Qpos * inject_Z (Z.of_nat (length t)) + proj1_sig ((1 # p) * e)%Qpos <= proj1_sig e) as X. { intros e. simpl. setoid_replace ((1 # p) * proj1_sig e * (Z.of_nat (length t) # 1) + (1 # p) * proj1_sig e)%Q with ((1#p)*((Z.of_nat (length t) #1) + (1#1))* proj1_sig e)%Q by (unfold canonical_names.equiv, stdlib_rationals.Q_eq; simpl; ring). rewrite <- (Qmult_1_l (proj1_sig e)) at 2. apply Qmult_le_r. apply Qpos_ispos. unfold Qmult, Qplus, Qle, Qnum, Qden. rewrite Z.mul_1_r, Z.mul_1_r, Z.mul_1_r. rewrite Z.mul_1_l, Z.mul_1_l, Pos.mul_1_r. unfold p. rewrite Z.P_of_succ_nat_Zplus. apply Z.le_refl. } generalize (X e1) (X e2). simpl ((1 # p) * e1)%Qpos. simpl ((1 # p) * e2)%Qpos. fold e1' e2'. unfold e1' at 1 3. unfold e2' at 1 3. generalize (Qpos_mult (@exist Q (Qlt {| Qnum := Z0; Qden := xH |}) {| Qnum := Zpos xH; Qden := p |} (@eq_refl comparison Lt)) e1) (Qpos_mult (@exist Q (Qlt {| Qnum := Z0; Qden := xH |}) {| Qnum := Zpos xH; Qden := p |} (@eq_refl comparison Lt)) e2) e1' e2' (0 + @approximate Q Qball a e1') (0 + @approximate Q Qball a e2') H. clear - t. induction t; intros e1'' e2'' e1' e2' x y Hxy H1 H2. - simpl in *. ring_simplify in H1. ring_simplify in H2. apply (@ball_weak_le Q_as_MetricSpace (proj1_sig e1' + proj1_sig e2')); auto. apply Qplus_le_compat; auto. - simpl in *. change (Zpos (P_of_succ_nat (length t))) with (Z_of_nat (1+(length t))) in H1. change (Zpos (P_of_succ_nat (length t))) with (Z_of_nat (1+(length t))) in H2. rewrite -> inj_plus in *. rewrite -> Q.Zplus_Qplus in *. ring_simplify in H1. ring_simplify in H2. apply (IHt e1'' e2'' (e1'' + e1')%Qpos (e2'' + e2')%Qpos); try (autorewrite with QposElim; ring_simplify; assumption). unfold Qball. autorewrite with QposElim. unfold QAbsSmall. setoid_replace (x + approximate a e1'' - (y + approximate a e2''))%Q with ((x - y) + (approximate a e1'' - approximate a e2'')) by (unfold canonical_names.equiv, stdlib_rationals.Q_eq; simpl; ring). simpl. setoid_replace (proj1_sig e1'' + proj1_sig e1' + (proj1_sig e2'' + proj1_sig e2'))%Q with ((proj1_sig e1' + proj1_sig e2') + (proj1_sig e1'' + proj1_sig e2''))%Q by (unfold canonical_names.equiv, stdlib_rationals.Q_eq; simpl; ring). apply QAbsSmall_plus. auto. apply (regFun_prf a). simpl. rewrite Qplus_assoc. assumption. simpl. rewrite Qplus_assoc. assumption. Qed.
imports: CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.totalorder.QposMinMax CoRN.reals.fast.CRArith CoRN.stdlib_omissions.List CoRN.model.metric2.Qmetric