proposition: Lemma CRmult_le_0_compat_bounded : forall (a b : CR) (c : Qpos), CRnonNeg b -> CRnonNeg a -> (forall e:Qpos, -`c <= approximate a e) -> (forall e:Qpos, approximate a e <= `c) -> (forall e:Qpos, -`c <= approximate b e) -> (forall e:Qpos, approximate b e <= `c) -> (0 <= CRmult_bounded c a b)%CR.
proof: Proof. intros a b c H0 H alower aupper blower bupper. rewrite CRmult_uncurry_eq. intro e. simpl. unfold Cap_raw;simpl. rewrite Qplus_0_r. unfold Qmult_modulus. destruct (Qlt_le_dec (`c*`c) (`e)). apply (Qle_trans _ (-(`c*`c))). apply Qopp_le_compat, Qlt_le_weak, q. apply QboundAbs_mult. specialize (H ((1 # 2) * ((1 # 2) * e) * Qpos_inv c)%Qpos). specialize (H0 ((1 # 2) * ((1 # 2) * e) * Qpos_inv c)%Qpos). apply Qle_minus_iff in H. rewrite Qopp_involutive in H. apply Qle_minus_iff in H0. rewrite Qopp_involutive in H0. apply (Qmult_le_0_compat _ _ H) in H0. clear H. rewrite Qmult_plus_distr_r in H0. rewrite Qmult_plus_distr_l, Qmult_plus_distr_l in H0. assert (forall i j k l:Q, 0 <= i + j + (k + l) -> -(j+k+l) <= i). { intros. apply (Qplus_le_r _ _ (j+k+l)). ring_simplify. rewrite <- Qplus_assoc, (Qplus_comm i) in H. rewrite Qplus_assoc in H. exact H. } apply H in H0. clear H. simpl in H0. assert (forall i j : Q, i<=j -> Qmax i j == j)%Q as elim_max. { intros. apply (Qle_max_r i j), H. } assert (forall i j : Q, j<=i -> Qmin i j == j)%Q as elim_min. { intros. apply (Qle_min_r i j), H. } rewrite elim_min, elim_min, elim_max, elim_max. refine (Qle_trans _ _ _ _ H0). apply Qopp_le_compat. apply (Qle_trans _ ((1#3)*`e + (1#3)*`e + (1#3)*`e)). 2: ring_simplify; apply Qle_refl. apply Qplus_le_compat. apply Qplus_le_compat. - apply (Qle_trans _ _ _ (Qle_Qabs _)). rewrite Qabs_Qmult. rewrite Qmult_comm. apply (Qle_trans _ (`c * Qabs ((1 # 2) * ((1 # 2) * ` e) * / ` c))). apply Qmult_le_compat_r. 2: apply Qabs_nonneg. pose proof (QboundAbs_abs c (approximate b ((1 # 2) * ((1 # 2) * e) * Qpos_inv c)%Qpos)) as H. simpl in H. rewrite elim_min, elim_max in H. rewrite H. clear H. apply Qmin_lb_r. apply blower. apply bupper. rewrite Qmult_comm, Qabs_pos, <- Qmult_assoc. rewrite (Qmult_comm (/`c)), Qmult_inv_r, Qmult_1_r. 2: apply Qpos_nonzero. rewrite Qmult_assoc. apply Qmult_le_r. apply Qpos_ispos. discriminate. apply Qmult_le_0_compat. apply Qmult_le_0_compat. discriminate. apply Qmult_le_0_compat. discriminate. apply Qpos_nonneg. apply Qlt_le_weak, Qinv_lt_0_compat, Qpos_ispos. - apply (Qle_trans _ _ _ (Qle_Qabs _)). rewrite Qabs_Qmult. apply (Qle_trans _ (`c * Qabs ((1 # 2) * ((1 # 2) * ` e) * / ` c))). apply Qmult_le_compat_r. 2: apply Qabs_nonneg. pose proof (QboundAbs_abs c (approximate a ((1 # 2) * ((1 # 2) * e) * Qpos_inv c)%Qpos)). simpl in H. rewrite elim_min, elim_max in H. rewrite H. clear H. apply Qmin_lb_r. apply alower. apply aupper. rewrite Qmult_comm, Qabs_pos, <- Qmult_assoc. rewrite (Qmult_comm (/`c)), Qmult_inv_r, Qmult_1_r. 2: apply Qpos_nonzero. rewrite Qmult_assoc. apply Qmult_le_r. apply Qpos_ispos. discriminate. apply Qmult_le_0_compat. apply Qmult_le_0_compat. discriminate. apply Qmult_le_0_compat. discriminate. apply Qpos_nonneg. apply Qlt_le_weak, Qinv_lt_0_compat, Qpos_ispos. - apply (Qle_trans _ ((1#16)*(`e*/`c*/`c)*`e)). ring_simplify. apply Qle_refl. apply Qmult_le_r. apply Qpos_ispos. apply (Qle_trans _ ((1#16)*(1#1))). 2: discriminate. apply Qmult_le_l. reflexivity. apply Qle_shift_div_r. apply Qpos_ispos. apply Qle_shift_div_r. apply Qpos_ispos. rewrite Qmult_1_l. exact q. - apply blower. - apply alower. - apply bupper. - apply aupper. - intro e. simpl. unfold Cap_raw. simpl. apply (Qle_trans _ 0). apply (Qopp_le_compat 0), Qpos_nonneg. rewrite <- Qle_minus_iff. apply alower. - intro e. simpl. unfold Cap_raw. simpl. apply (Qle_trans _ 0). apply (Qopp_le_compat 0), Qpos_nonneg. rewrite <- Qle_minus_iff. apply aupper. Qed.
imports: CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.totalorder.QMinMax CoRN.model.totalorder.QposMinMax Coq.setoid_ring.Ring_theory Coq.Setoids.Setoid Coq.QArith.QArith Coq.QArith.Qabs Coq.QArith.Qround CoRN.metric2.Complete CoRN.metric2.ProductMetric CoRN.reals.fast.CRFieldOps CoRN.model.metric2.Qmetric CoRN.logic.Stability Coq.Logic.ConstructiveEpsilon CoRN.util.Qdlog MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders