proposition: Lemma Qinv_pos_uc_prf (c:Qpos) : @is_UniformlyContinuousFunction Q_as_MetricSpace Q_as_MetricSpace (fun a:Q => /(Qmax (proj1_sig c) a) ) (Qinv_modulus c).
proof: Proof. intros e a0 a1 Ha. simpl in *. unfold Qball in *. assert (forall (a:Qpos) (b:Q), 0 < Qmax (`a) b) as max_pos. { intros. apply (Qlt_le_trans _ (`a)). destruct a; exact q. apply Qmax_ub_l. } assert ( 0 < Qmax (` c) a0 * Qmax (` c) a1). { apply (Qle_lt_trans _ (Qmax (`c) a0 * 0)). rewrite Qmult_0_r. apply Qle_refl. apply Qmult_lt_l. apply max_pos. apply max_pos. } apply AbsSmall_Qabs. setoid_replace (/ Qmax (` c) a0 - / Qmax (` c) a1) with ((Qmax (` c) a1 - Qmax (` c) a0) / (Qmax (` c) a0 * Qmax (` c) a1)). 2: unfold equiv, stdlib_rationals.Q_eq; field. unfold Qdiv. rewrite Qabs_Qmult. rewrite (Qabs_pos (/ ( Qmax (` c) a0 * Qmax (` c) a1))). 2: apply Qlt_le_weak, Qinv_lt_0_compat, H. apply Qle_shift_div_r. exact H. apply (Qle_trans _ _ _ (Qmax_contract _ _ _)). apply AbsSmall_Qabs in Ha. rewrite Qabs_Qminus. apply (Qle_trans _ _ _ Ha). rewrite (Qmult_comm (`e)). apply Qmult_le_r. apply Qpos_ispos. apply (Qle_trans _ (`c * Qmax (`c) a1)). apply Qmult_le_l. apply Qpos_ispos. apply Qmax_ub_l. apply Qmult_le_r. apply max_pos. apply Qmax_ub_l. split; intro abs. specialize (max_pos c a1). rewrite abs in max_pos. exact (Qlt_irrefl 0 max_pos). specialize (max_pos c a0). rewrite abs in max_pos. exact (Qlt_irrefl 0 max_pos). 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