proposition: Lemma CRmult_uncurry_eq : forall (c:Qpos) (x y : CR), (' (-proj1_sig c)%Q <= x)%CR -> (x <= ' (proj1_sig c)%Q)%CR -> (CRmult_bounded c x y == (Cmap (ProductMS_prelength QPrelengthSpace QPrelengthSpace) (Qmult_uncurry c) (undistrib_Complete (x,y))))%CR.
proof: Proof. intros. transitivity (CRmult_bounded c (CRboundAbs c x) y). apply (ucFun2_wd (CRmult_bounded c) x (CRboundAbs c x)). symmetry. apply (CRboundAbs_Eq c H H0). reflexivity. intros e1 e2. rewrite Qplus_0_r. simpl. unfold Cap_raw; simpl. assert (forall i, eq (QposInf_bind (λ e : Qpos, e) i) i) as bind_id. { intro i. destruct i; reflexivity. } rewrite bind_id. clear bind_id. assert (forall i j k l : Q, Qabs (i*j-k*l) <= Qabs i * Qabs(j-l) + Qabs(i-k)*Qabs l)%Q as multMaj. { intros. setoid_replace (i*j-k*l)%Q with (i*(j-l)+ (i-k)*l)%Q by (unfold equiv, stdlib_rationals.Q_eq; ring). apply (Qle_trans _ _ _ (Qabs_triangle _ _)). rewrite Qabs_Qmult, Qabs_Qmult. apply Qle_refl. } apply AbsSmall_Qabs. apply (Qle_trans _ _ _ (multMaj _ _ _ _)). apply (Qle_trans _ ((1#2)*`e1 + (1#2)*`e2 +((1#2)*`e1 +(1#2)*`e2))). 2: ring_simplify; apply Qle_refl. apply Qplus_le_compat. - apply (Qle_trans _ ( Qabs (approximate y (Qscale_modulus (QboundAbs c (approximate x (Qmult_modulus c ((1 # 2) * e1)))) ((1 # 2) * e1)) - (approximate y (Qmult_modulus c ((1 # 2) * e2)))) * Qabs (QboundAbs c (approximate x (Qmult_modulus c ((1 # 2) * e1)))))). rewrite Qmult_comm. apply Qmult_le_compat_r. apply QboundAbs_contract. apply Qabs_nonneg. unfold Qscale_modulus. simpl (Qmult_modulus c ((1 # 2) * e1)). destruct (QboundAbs c (approximate x (Qmult_modulus c ((1 # 2) ↾ @eq_refl comparison Datatypes.Lt * e1)))) eqn:des. destruct Qnum. + setoid_replace (0#Qden) with (0#1) by reflexivity. rewrite Qmult_0_r. apply (Qpos_nonneg ((1#2)*e1+(1#2)*e2)). + rewrite Qmult_comm, Qabs_pos. 2: discriminate. apply (Qle_trans _ ((Zpos p#Qden) * ((Zpos Qden # p)%Q * ((1 # 2)%Q * `e1) + (1 # 2) * `e2 / `c))). apply Qmult_le_l. reflexivity. pose proof (regFun_prf y ((Zpos Qden # p)%Q ↾ eq_refl * ((1 # 2)%Q ↾ eq_refl * e1))%Qpos ((1 # 2) * e2 * Qpos_inv c)%Qpos) as H3. apply AbsSmall_Qabs in H3. exact H3. rewrite Qmult_plus_distr_r. rewrite Qmult_assoc. setoid_replace ((Zpos p # Qden) * (Zpos Qden # p))%Q with (1#1)%Q by (unfold equiv, stdlib_rationals.Q_eq; unfold Qeq; simpl; rewrite Pos.mul_1_r, Pos.mul_comm; reflexivity). rewrite Qmult_1_l. apply Qplus_le_r. unfold Qdiv. rewrite Qmult_assoc. apply Qle_shift_div_r. apply Qpos_ispos. rewrite Qmult_comm. apply Qmult_le_l. apply (Qpos_ispos ((1#2)*e2)). rewrite <- des. apply Qmax_lub. apply (Qle_trans _ 0). apply (Qopp_le_compat 0). apply Qpos_nonneg. apply Qpos_nonneg. apply Qmin_lb_l. + rewrite Qmult_comm, Qabs_neg. 2: discriminate. setoid_replace (- (Z.neg p # Qden)) with (Zpos p # Qden) by reflexivity. apply (Qle_trans _ ((Zpos p#Qden) * ((Zpos Qden # p)%Q * ((1 # 2)%Q * `e1) + (1 # 2) * `e2 / `c))). apply Qmult_le_l. reflexivity. pose proof (regFun_prf y ((Zpos Qden # p)%Q ↾ eq_refl * ((1 # 2)%Q ↾ eq_refl * e1))%Qpos ((1 # 2) * e2 * Qpos_inv c)%Qpos) as H3. apply AbsSmall_Qabs in H3. exact H3. rewrite Qmult_plus_distr_r. rewrite Qmult_assoc. setoid_replace ((Zpos p # Qden) * (Zpos Qden # p))%Q with (1#1)%Q by (unfold equiv, stdlib_rationals.Q_eq; unfold Qeq; simpl; rewrite Pos.mul_1_r, Pos.mul_comm; reflexivity). rewrite Qmult_1_l. apply Qplus_le_r. unfold Qdiv. rewrite Qmult_assoc. apply Qle_shift_div_r. apply Qpos_ispos. rewrite Qmult_comm. apply Qmult_le_l. apply (Qpos_ispos ((1#2)*e2)). rewrite <- (Qopp_involutive (`c)). setoid_replace (Zpos p # Qden) with (-(Z.neg p # Qden)) by reflexivity. apply Qopp_le_compat. rewrite <- des. apply Qmax_ub_l. - apply (Qle_trans _ (Qabs (approximate x (Qmult_modulus c ((1 # 2) * e1)) - approximate x (Qmult_modulus c ((1 # 2) * e2))) * Qabs (QboundAbs c (approximate y (Qmult_modulus c ((1 # 2) ↾ eq_refl * e2)))))). apply Qmult_le_compat_r. 2: apply Qabs_nonneg. apply QboundAbs_contract. rewrite QboundAbs_abs. apply (Qle_trans _ (`c * Qabs (approximate x (Qmult_modulus c ((1 # 2) * e1)) - approximate x (Qmult_modulus c ((1 # 2) * e2))))). rewrite Qmult_comm. apply Qmult_le_compat_r. 2: apply Qabs_nonneg. apply Qmin_lb_r. apply (Qle_trans _ (`c * ((1#2)*`e1 / `c + (1#2)*`e2 / `c))). apply Qmult_le_l. apply Qpos_ispos. unfold Qmult_modulus. pose proof (regFun_prf x ((1 # 2) * e1 * Qpos_inv c)%Qpos ((1 # 2) * e2 * Qpos_inv c)%Qpos) as H3. apply AbsSmall_Qabs in H3. exact H3. rewrite Qmult_plus_distr_r. apply Qplus_le_compat. unfold Qdiv. rewrite Qmult_assoc. apply Qle_shift_div_r. apply Qpos_ispos. rewrite Qmult_comm. apply Qle_refl. unfold Qdiv. rewrite Qmult_assoc. apply Qle_shift_div_r. apply Qpos_ispos. rewrite Qmult_comm. apply Qle_refl. Qed.
imports: CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.totalorder.QposMinMax CoRN.model.lattice.CRlattice CoRN.model.totalorder.QMinMax Coq.QArith.Qabs CoRN.model.metric2.Qmetric CoRN.metric2.ProductMetric MathClasses.interfaces.canonical_names