proposition: Lemma CRmult_inv_r_bounded : forall (x : CR) (q b : Qpos), (' ` q <= x)%CR -> (`q < `b)%Q -> (/ `q <= `b)%Q -> (forall e:Qpos, approximate x e <= `b)%Q -> (forall e:Qpos, - `b <= approximate x e)%Q -> CRmult_bounded b x (CRinv_pos q x) == 1.
proof: Proof. intros x q b pos qltb invqleb xbelow xabove. rewrite CRmult_uncurry_eq. intros e1 e2. simpl. apply AbsSmall_Qabs. assert (forall a c : Q, 0 < c -> Qabs (a*/c-(1#1)) == Qabs (/c) * Qabs (a-c))%Q as absShift. { intros. rewrite <- (Qmult_inv_r c). setoid_replace (a * / c - c * / c)%Q with ((a-c)*/c)%Q by (unfold equiv, stdlib_rationals.Q_eq; ring). rewrite Qabs_Qmult. apply Qmult_comm. intro abs. rewrite abs in H. exact (Qlt_irrefl 0 H). } 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. } assert (QboundAbs b (/ Qmax (` q) (approximate x (Qinv_modulus q ((1 # 2) ↾ eq_refl * e1 * Qpos_inv b)))) == / Qmax (` q) (approximate x (Qinv_modulus q ((1 # 2) ↾ eq_refl * e1 * Qpos_inv b))))%Q. { simpl. rewrite elim_max. apply Qle_min_r. apply (Qle_trans _ (/`q)). 2: exact invqleb. apply Qle_shift_inv_l. apply Qpos_ispos. rewrite Qmult_comm. apply Qle_shift_div_r. apply (Qlt_le_trans _ (`q)). apply Qpos_ispos. apply Qmax_ub_l. rewrite Qmult_1_l. apply Qmax_ub_l. apply (Qle_trans _ 0). apply (Qopp_le_compat 0), Qpos_nonneg. apply Qmin_glb. apply Qpos_nonneg. apply Qlt_le_weak, Qinv_lt_0_compat. apply (Qlt_le_trans _ (`q)). apply Qpos_ispos. apply Qmax_ub_l. } simpl in H. rewrite H, absShift. clear absShift H. rewrite Qabs_pos. rewrite Qmult_comm. apply Qle_shift_div_r. apply (Qlt_le_trans _ (`q)). apply Qpos_ispos. apply Qmax_ub_l. apply (Qle_trans _ ((1#2)*`e1 * `q + (1#2)*`e1 * `q)). assert (((1 # 2) * ` e1 * / ` b + ` q * ` q * ((1 # 2) * ` e1 * / ` b) <= (1 # 2) * ` e1 * ` q + (1 # 2) * ` e1 * ` q))%Q as dist_ok. { apply Qplus_le_compat. - apply Qmult_le_l. apply (Qpos_ispos ((1#2)*e1)). apply Qle_shift_inv_r. apply Qpos_ispos. rewrite <- (Qmult_inv_r (`q)). apply Qmult_le_l. apply Qpos_ispos. exact invqleb. apply Qpos_nonzero. - rewrite <- Qmult_assoc, (Qmult_comm (`q)). apply Qmult_le_r. apply Qpos_ispos. rewrite Qmult_assoc. apply (Qle_shift_div_r _ (`b)). apply Qpos_ispos. rewrite Qmult_comm. apply Qmult_le_l. apply (Qpos_ispos ((1#2)*e1)). apply Qlt_le_weak, qltb. } apply (Qmax_case (`q)). - unfold Qinv_modulus. intros. unfold Qmult_modulus. assert (QboundAbs b (` q) == `q)%Q as H1. { simpl. transitivity (Qmin (`b) (`q)). apply Qle_max_r. apply (Qle_trans _ 0). apply (Qopp_le_compat 0), Qpos_nonneg. apply Qmin_glb. apply Qpos_nonneg. apply Qpos_nonneg. apply Qle_min_r. apply Qlt_le_weak, qltb. } rewrite <- H1 at 1. clear H1. apply (Qle_trans _ (Qabs (approximate x ((1 # 2)%Q ↾ eq_refl * e1 * Qpos_inv b)%Qpos - (` q)))). apply QboundAbs_contract. apply (Qle_trans _ ((`q * `q * ((1 # 2) * `e1 * / `b)) + (1 # 2) * `e1 * / `b )). apply (CRbound_distance_from_below x (`q) (q * q * ((1 # 2)%Q ↾ eq_refl * e1 * Qpos_inv b))%Qpos ((1 # 2) * e1 * Qpos_inv b)%Qpos). 2: exact pos. exact H. rewrite Qplus_comm. exact dist_ok. - unfold Qinv_modulus. intros. unfold Qmult_modulus. rewrite elim_min. rewrite elim_max. pose proof (regFun_prf x ((1 # 2)%Q ↾ eq_refl * e1 * Qpos_inv b)%Qpos (q * q * ((1 # 2)%Q ↾ eq_refl * e1 * Qpos_inv b))%Qpos) as H1. apply AbsSmall_Qabs in H1. apply (Qle_trans _ _ _ H1). clear H1. exact dist_ok. apply xabove. apply xbelow. - rewrite <- Qmult_plus_distr_l. rewrite <- Qmult_plus_distr_l. setoid_replace ((1 # 2) + (1 # 2))%Q with (1#1)%Q by reflexivity. rewrite Qmult_1_l. apply (Qle_trans _ ((`e1+`e2)*`q)). rewrite <- Qplus_0_r, Qmult_plus_distr_l. apply Qplus_le_r. apply (Qpos_nonneg (e2*q)). rewrite Qplus_0_r. apply Qmult_le_l. apply (Qpos_ispos (e1+e2)). apply Qmax_ub_l. - apply Qlt_le_weak, Qinv_lt_0_compat. apply (Qlt_le_trans _ (`q)). apply Qpos_ispos. apply Qmax_ub_l. - apply (Qlt_le_trans _ (`q)). apply Qpos_ispos. apply Qmax_ub_l. - intro e. simpl. unfold Cap_raw. simpl. apply (Qle_trans _ 0). apply (Qopp_le_compat 0), Qpos_nonneg. rewrite <- Qle_minus_iff. apply xabove. - intro e. simpl. unfold Cap_raw. simpl. apply (Qle_trans _ 0). apply (Qopp_le_compat 0), Qpos_nonneg. rewrite <- Qle_minus_iff. apply xbelow. 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