proposition: Lemma CRmult_assoc_bounded (x y z : CR) : let b := ((CR_b (1#1) x + (1#1)) * (CR_b (1#1) y + (1#1)) * (CR_b (1#1) z + (1#1)))%Qpos in (CRmult_bounded b (CRmult_bounded b x y) z == CRmult_bounded b x (CRmult_bounded b y z))%CR.
proof: Proof. intros. assert (' (- ` b)%Q <= x)%CR as xlower. { apply (@CRle_trans _ (' (-proj1_sig (CR_b (1#1) x))%Q)). 2: apply (CR_b_lowerBound _ _). apply CRle_Qle. apply Qopp_le_compat. apply (Qle_trans _ ((` (CR_b (1#1)%Qpos x) + (1#1)))). rewrite <- Qplus_0_r at 1. apply Qplus_le_r. discriminate. apply CRmult_assoc_xfactor_le. } assert (x <= ' (` b)%Q)%CR as xupper. { apply (@CRle_trans _ (' (proj1_sig (CR_b (1#1) x))%Q)). apply CR_b_upperBound. apply CRle_Qle. apply (Qle_trans _ ((` (CR_b (1#1)%Qpos x) + (1#1)))). rewrite <- Qplus_0_r at 1. apply Qplus_le_r. discriminate. apply CRmult_assoc_xfactor_le. } assert (' (- ` b)%Q <= y)%CR as ylower. { apply (@CRle_trans _ (' (-proj1_sig (CR_b (1#1) y))%Q)). 2: apply (CR_b_lowerBound _ _). apply CRle_Qle. apply Qopp_le_compat. apply (Qle_trans _ ((` (CR_b (1#1)%Qpos y) + (1#1)))). rewrite <- Qplus_0_r at 1. apply Qplus_le_r. discriminate. apply CRmult_assoc_yfactor_le. } assert (y <= ' (` b)%Q)%CR as yupper. { apply (@CRle_trans _ (' (proj1_sig (CR_b (1#1) y))%Q)). apply CR_b_upperBound. apply CRle_Qle. apply (Qle_trans _ ((` (CR_b (1#1)%Qpos y) + (1#1)))). rewrite <- Qplus_0_r at 1. apply Qplus_le_r. discriminate. apply CRmult_assoc_yfactor_le. } assert (` (CR_b (1 ↾ eq_refl) x + 1 ↾ eq_refl)%Qpos * ` (CR_b (1 ↾ eq_refl) y + 1 ↾ eq_refl)%Qpos <= ` b) as xyfactor_le. { rewrite <- Qmult_1_l. unfold b. simpl. rewrite (Qmult_comm ((Qabs (approximate x (Qpos2QposInf (1 ↾ eq_refl))) + 1 + 1) * (Qabs (approximate y (Qpos2QposInf (1 ↾ eq_refl))) + 1 + 1))). apply Qmult_le_compat_r. apply (Qle_trans _ (0+2)). discriminate. rewrite <- Qplus_assoc. apply Qplus_le_l, Qabs_nonneg. apply Qmult_le_0_compat. apply (Qle_trans _ (0+2)). discriminate. rewrite <- Qplus_assoc. apply Qplus_le_l, Qabs_nonneg. apply (Qle_trans _ (0+2)). discriminate. rewrite <- Qplus_assoc. apply Qplus_le_l, Qabs_nonneg. } rewrite CRmult_uncurry_eq_3r. rewrite CRmult_uncurry_eq_3. 2: exact xlower. 2: exact xupper. 4: exact xlower. 4: exact xupper. 4: exact ylower. 4: exact yupper. apply Cmap_wd_loc with (e:=(1#4)%Qpos). intros [[i j] k]. intros H. specialize (H (1#4)%Qpos (1#4)%Qpos). destruct H,H. simpl in H1. simpl in H0. apply Qball_0. apply (@Qmult_uncurry_assoc i j k b). - clear H0 H1. simpl in H. apply AbsSmall_Qabs in H. apply (Qle_trans _ (proj1_sig (CR_b (1#1) x + (1#1))%Qpos)). setoid_replace ((1#4)+(1#4)+(1#4)) with (3#4) in H by reflexivity. apply quarter_approx_le_abs_1, H. clear H. apply CRmult_assoc_xfactor_le. - clear H H0. apply (Qle_trans _ (proj1_sig (CR_b (1#1) y + (1#1))%Qpos)). apply AbsSmall_Qabs in H1. setoid_replace ((1#4)+(1#4)+(1#4)) with (3#4) in H1 by reflexivity. apply quarter_approx_le_abs_1, H1. apply CRmult_assoc_yfactor_le. - clear H H1. apply (Qle_trans _ (proj1_sig (CR_b (1#1) z + (1#1))%Qpos)). apply AbsSmall_Qabs in H0. setoid_replace ((1#4)+(1#4)+(1#4)) with (3#4) in H0 by reflexivity. apply quarter_approx_le_abs_1, H0. apply CRmult_assoc_zfactor_le. - apply (Qle_trans _ (proj1_sig (CR_b (1#1) y + (1#1))%Qpos * proj1_sig (CR_b (1#1) z + (1#1))%Qpos)). rewrite Qabs_Qmult. apply (Qle_trans _ (proj1_sig (CR_b (1#1) y + (1#1))%Qpos * Qabs k)). apply Qmult_le_compat_r. apply AbsSmall_Qabs in H1. setoid_replace ((1#4)+(1#4)+(1#4)) with (3#4) in H1 by reflexivity. apply quarter_approx_le_abs_1, H1. apply Qabs_nonneg. apply Qmult_le_l. apply Qpos_ispos. apply AbsSmall_Qabs in H0. setoid_replace ((1#4)+(1#4)+(1#4)) with (3#4) in H0 by reflexivity. apply quarter_approx_le_abs_1, H0. rewrite <- Qmult_1_l, Qmult_assoc. apply Qmult_le_compat_r. 2: apply Qpos_nonneg. apply Qmult_le_compat_r. 2: apply Qpos_nonneg. simpl. rewrite <- Qplus_assoc. apply (Qle_trans _ (0+2)). discriminate. apply Qplus_le_l, Qabs_nonneg. - apply (Qle_trans _ (proj1_sig (CR_b (1#1) x + (1#1))%Qpos * proj1_sig (CR_b (1#1) y + (1#1))%Qpos)). rewrite Qabs_Qmult. apply (Qle_trans _ (proj1_sig (CR_b (1#1) x + (1#1))%Qpos * Qabs j)). apply Qmult_le_compat_r. simpl in H. apply AbsSmall_Qabs in H. setoid_replace ((1#4)+(1#4)+(1#4)) with (3#4) in H by reflexivity. apply quarter_approx_le_abs_1, H. apply Qabs_nonneg. apply Qmult_le_l. apply Qpos_ispos. apply AbsSmall_Qabs in H1. setoid_replace ((1#4)+(1#4)+(1#4)) with (3#4) in H1 by reflexivity. apply quarter_approx_le_abs_1, H1. exact xyfactor_le. - rewrite (@CRmult_bounded_mult b). 2: exact ylower. 2: exact yupper. apply (@CRle_trans _ ('(-proj1_sig ((CR_b (1#1) x) * CR_b (1#1) y)%Qpos)%Q)). 2: apply CR_b_lowerBound_2. apply CRle_Qle, Qopp_le_compat. apply (Qle_trans _ (proj1_sig (CR_b (1#1) x + (1#1))%Qpos * proj1_sig ((CR_b (1#1) y) + (1#1))%Qpos)). apply (Qpos_mult_le_compat (CR_b (1#1) x) (CR_b (1#1) y)). rewrite <- Qplus_0_r at 1. apply Qplus_le_r. discriminate. rewrite <- Qplus_0_r at 1. apply Qplus_le_r. discriminate. exact xyfactor_le. - rewrite (@CRmult_bounded_mult b). 2: exact ylower. 2: exact yupper. apply (@CRle_trans _ ('(proj1_sig ((CR_b (1#1) x) * CR_b (1#1) y)%Qpos)%Q)). apply CR_b_upperBound_2. apply CRle_Qle. apply (Qle_trans _ (proj1_sig (CR_b (1#1) x + (1#1))%Qpos * proj1_sig ((CR_b (1#1) y) + (1#1))%Qpos)). apply (Qpos_mult_le_compat (CR_b (1#1) x) (CR_b (1#1) y)). rewrite <- Qplus_0_r at 1. apply Qplus_le_r. discriminate. rewrite <- Qplus_0_r at 1. apply Qplus_le_r. discriminate. exact xyfactor_le. 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