proposition: Lemma CRmult_bounded_weaken : forall (c1 c2:Qpos) x y, ((' (-proj1_sig c1)%Q <= y) -> (y <= ' proj1_sig c1) -> (proj1_sig c1 <= proj1_sig c2)%Q -> CRmult_bounded c1 x y == CRmult_bounded c2 x y)%CR.
proof: Proof. intros c1 c2 x y Hc1a Hc1b Hc2. assert (Hy:=CRboundAbs_Eq _ Hc1a Hc1b). set (y':= (CRboundAbs c1 y)) in *. transitivity (ucFun2 (CRmult_bounded c2) x y'); [|rewrite -> Hy;reflexivity]. assert (H:forall x:Qpos, proj1_sig (x*c1*Qpos_inv c2)%Qpos <= proj1_sig x). { intros a. simpl. rewrite <- (Qmult_1_r (`a)), <- Qmult_assoc, <- Qmult_assoc. apply Qmult_le_l. destruct a; exact q. rewrite Qmult_1_l. apply Qle_shift_div_r. destruct c2; exact q. rewrite Qmult_1_l. exact Hc2. } change (ucFun2 (CRmult_bounded c1) x y == ucFun2 (CRmult_bounded c2) x y')%CR. rewrite <- (QreduceApprox_Eq x). set (x''':=(QreduceApprox x)). set (x':=faster x''' (fun x => (x * c1 * Qpos_inv c2)%Qpos) H). transitivity (ucFun2 (CRmult_bounded c1) x' y). unfold x'. rewrite -> fasterIsEq. reflexivity. apply regFunEq_equiv, regFunEq_e; intros e. intros. simpl. do 3 (unfold Cap_raw; simpl). assert (X:=fun c => QboundAbs_absorb _ _ c Hc2). unfold QboundAbs in X. simpl in X. rewrite -> X. clear X. assert (eq (Qpos_red ((1 # 2) * e * Qpos_inv c1 * c1 * Qpos_inv c2)) (Qpos_red ((1 # 2) * e * Qpos_inv c2))). { apply Qpos_red_eq. unfold QposEq. simpl. field. split. intro abs. destruct c2. simpl in abs. apply (Qlt_not_le _ _ q). rewrite abs. apply Qle_refl. intro abs. destruct c1. simpl in abs. apply (Qlt_not_le _ _ q). rewrite abs. apply Qle_refl. } simpl. simpl in H0. rewrite H0. do 2 rewrite QposInf_bind_id. apply Qball_Reflexive. apply (Qpos_nonneg (e+e)). 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