proposition: Lemma Qmult_uc_uncurry (c:Qpos) : @is_UniformlyContinuousFunction (ProductMS Q_as_MetricSpace Q_as_MetricSpace) Q_as_MetricSpace (fun ab => QboundAbs c (fst ab) * QboundAbs c (snd ab)) (fun e => Qmult_modulus c ((1#2)*e)).
proof: Proof. assert (forall i j k l : Q, Qabs (i*j-k*l) <= Qabs j * Qabs(i-k) + Qabs(j-l)*Qabs k)%Q as multMaj. { intros. setoid_replace (i*j-k*l)%Q with (j*(i-k)+ (j-l)*k)%Q by (unfold equiv, stdlib_rationals.Q_eq; ring). apply (Qle_trans _ _ _ (Qabs_triangle _ _)). rewrite Qabs_Qmult, Qabs_Qmult. apply Qle_refl. } assert (forall i:Q, Qabs (QboundAbs c i) <= ` c) as bound. { intro i. apply Qabs_Qle_condition. split. apply Qmax_ub_l. apply Qmax_lub. apply (Qle_trans _ 0). apply (Qopp_le_compat 0). apply Qpos_nonneg. apply Qpos_nonneg. apply Qmin_lb_l. } simpl. unfold Qmult_modulus. intros e1 [i j] [k l] [H H0]. simpl. simpl in H, H0. apply AbsSmall_Qabs. apply AbsSmall_Qabs in H. apply AbsSmall_Qabs in H0. apply (Qle_trans _ _ _ (multMaj _ _ _ _)). apply (Qle_trans _ (`c * (Qabs (QboundAbs c i - QboundAbs c k)) + `c * (Qabs (QboundAbs c j - QboundAbs c l)))). - apply Qplus_le_compat. apply Qmult_le_compat_r. 2: apply Qabs_nonneg. apply bound. rewrite Qmult_comm. apply Qmult_le_compat_r. 2: apply Qabs_nonneg. apply bound. - apply (Qle_trans _ ((1#2)*`e1+(1#2)*`e1)). apply Qplus_le_compat. apply (Qle_trans _ (`c * Qabs (i-k))). apply Qmult_le_l. apply Qpos_ispos. apply QboundAbs_contract. rewrite Qmult_comm. apply (Qmult_le_r _ _ (/ `c)). apply Qinv_lt_0_compat, Qpos_ispos. rewrite <- Qmult_assoc, Qmult_inv_r, Qmult_1_r. exact H. apply Qpos_nonzero. apply (Qle_trans _ (`c * Qabs (j-l))). apply Qmult_le_l. apply Qpos_ispos. apply QboundAbs_contract. rewrite Qmult_comm. apply (Qmult_le_r _ _ (/ `c)). apply Qinv_lt_0_compat, Qpos_ispos. rewrite <- Qmult_assoc, Qmult_inv_r, Qmult_1_r. exact H0. apply Qpos_nonzero. ring_simplify. apply Qle_refl. 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