proposition: Lemma Cauchy_IR_mult_as_CRmult_bounded : forall x y:Cauchy_IR, forall (z:Qpos) (N:nat), (forall i:nat, (N<=i) -> AbsSmall (proj1_sig z) (CS_seq _ y i)) -> (ucFun2 (CRmult_bounded z) (Cauchy_IRasCR x) (Cauchy_IRasCR y) == Cauchy_IRasCR (x[*]y))%CR.
proof: Proof. intros [x Hx] y z N Hz. destruct y as [y Hy]. apply regFunEq_equiv, regFunEq_e. intros e. simpl. destruct CS_seq_mult as [n3 Hn3]. unfold Cap_raw. simpl in *. destruct Hx as [n1 Hn1]. apply Qscale_modulus_elim. intros Hxn1. pose (n:=(Nat.max n3 (Nat.max n1 N))). rewrite -> Hxn1. assert (Qeq (0 * Qmax (- proj1_sig z) (Qmin (proj1_sig z) (Cauchy_IRasCR_raw (Build_CauchySeq Q_as_COrdField y Hy)(QposInf_bind (fun e0 : Qpos => e0) QposInfinity))))%Q (0 * y n)%Q). ring. rewrite -> H. clear H. change (@ball Q_as_MetricSpace (proj1_sig e+proj1_sig e) (0 * y n) (x n3 * y n3))%Q. apply ball_triangle with (x n*y n)%Q;[|eapply Hn3; unfold n; auto with *]. apply ball_sym. simpl. setoid_replace (0 * y n)%Q with (x n1 * y n)%Q. 2: rewrite Hxn1; reflexivity. unfold Qball. unfold QAbsSmall. setoid_replace (x n * y n - x n1 * y n)%Q with ((x n - x n1)*y n)%Q. 2: ring. apply AbsSmall_trans with ((1#2)*proj1_sig e)%Q. apply half_3. apply Qpos_ispos. stepl (((1#2)*proj1_sig e/ proj1_sig z)* proj1_sig z)%Q; [| simpl;field;apply Qpos_nonzero]. apply mult_AbsSmall;[apply Hn1|apply Hz]; unfold n; apply Nat.le_trans with (Nat.max n1 N); auto with *. intros w Hw. simpl. destruct (Hy (proj1_sig w) (Qpos_ispos w)) as [n2 Hn2]. pose (n:=(Nat.max (Nat.max n1 n2) (Nat.max n3 N))). assert (n1 <= n);[unfold n; apply Nat.le_trans with (Nat.max n1 n2); auto with *|]. assert (n2 <= n);[unfold n; apply Nat.le_trans with (Nat.max n1 n2); auto with *|]. assert (n3 <= n);[unfold n; apply Nat.le_trans with (Nat.max n3 N); auto with *|]. assert (N <= n);[unfold n; apply Nat.le_trans with (Nat.max n3 N); auto with *|]. change (Qball (proj1_sig e+proj1_sig e)) with (@ball Q_as_MetricSpace (proj1_sig e + proj1_sig e)). apply ball_triangle with (x n * y n)%Q;[|eapply Hn3; assumption]. clear Hn3. assert (QposEq e ((1#2)*e + (1#2)*e)) by (unfold QposEq; simpl; ring). apply (ball_wd _ H3 _ _ (reflexivity _) _ _ (reflexivity _)). clear H3. apply ball_triangle with (x n1 * y n)%Q; apply ball_sym; simpl; unfold Qball. unfold QAbsSmall. setoid_replace (x n1 * y n - x n1 * Qmax (- proj1_sig z) (Qmin (proj1_sig z) (y n2)))%Q with (x n1*(y n - Qmax (- proj1_sig z) (Qmin (proj1_sig z) (y n2))))%Q. 2: ring. simpl. stepl (((1#2)*proj1_sig e/proj1_sig w)*proj1_sig w)%Q; [| simpl;field;apply Qpos_nonzero]. apply mult_AbsSmall;[apply Hw|]. destruct (Hz n H2) as [X0 X1]. destruct (Hn2 _ H0) as [X2 X3]. unfold cg_minus in *. simpl in *. change (Qmax (- proj1_sig z) (Qmin (proj1_sig z) (y n2)))%Q with (QboundAbs z (y n2))%Q. assert (A0:(- proj1_sig w<=0)%Q). rewrite -> Qle_minus_iff. ring_simplify. apply Qpos_nonneg. rewrite -> Qle_minus_iff in *. clear - A0 X0 X1 X2 X3 Hn2 H0. ring_simplify in A0. ring_simplify in X0. ring_simplify in X1. ring_simplify in X2. ring_simplify in X3. apply QboundAbs_elim; intros I; try solve [apply Hn2;assumption]; rewrite -> Qle_minus_iff in I. apply AbsSmall_minus. unfold cg_minus;simpl. apply leEq_imp_AbsSmall. apply X1. rewrite -> Qle_minus_iff. stepr ((y n + (-1 # 1) * y n2 + proj1_sig w)+(y n2 + - proj1_sig z))%Q; [| simpl; ring]. eapply plus_resp_nonneg; assumption. eapply leEq_imp_AbsSmall; simpl; ring_simplify. apply X0. rewrite -> Qle_minus_iff. stepr ((proj1_sig w + (-1 # 1) * y n + y n2)+(- proj1_sig z + - y n2))%Q; [| simpl; ring]. eapply plus_resp_nonneg; assumption. unfold QAbsSmall. setoid_replace (x n * y n - x n1 * y n)%Q with ((x n - x n1)*y n)%Q. 2: ring. autorewrite with QposElim. stepl (((1#2)*proj1_sig e/proj1_sig z)*proj1_sig z)%Q; [| simpl; field; apply Qpos_nonzero]. apply mult_AbsSmall;[apply Hn1;assumption|apply Hz;assumption]. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.totalorder.QposMinMax CoRN.model.reals.Cauchy_IR CoRN.tactics.CornTac Coq(Lia) CoRN.model.metric2.Qmetric CoRN.model.totalorder.QMinMax Coq.QArith.Qabs CoRN.reals.fast.CRFieldOps