proposition: Lemma filterlim_Rbar_mult : forall x y z, is_Rbar_mult x y z -> filterlim (fun z => fst z * snd z) (filter_prod (Rbar_locally x) (Rbar_locally y)) (Rbar_locally z).
proof: Proof. intros x y z. wlog: x y z / (Rbar_le 0 x). intros Hw. case: (Rbar_le_lt_dec 0 x) => Hx Hp. by apply Hw. apply (filterlim_ext (fun z => - (- fst z * snd z))). intros t. ring. rewrite -(Rbar_opp_involutive z). eapply filterlim_comp. 2: apply filterlim_Rbar_opp. assert (Hw' : filterlim (fun z => fst z * snd z) (filter_prod (Rbar_locally (Rbar_opp x)) (Rbar_locally y)) (Rbar_locally (Rbar_opp z))). apply Hw. replace (Finite 0) with (Rbar_opp 0) by apply (f_equal Finite), Ropp_0. apply Rbar_opp_le. by apply Rbar_lt_le. by apply is_Rbar_mult_opp_l. clear Hw. intros P HP. specialize (Hw' P HP). destruct Hw' as [Q R H1 H2 H3]. exists (fun x => Q (- x)) R. now apply filterlim_Rbar_opp. exact H2. intros u v HQ HR. exact (H3 _ _ HQ HR). wlog: x y z / (Rbar_le 0 y). intros Hw. case: (Rbar_le_lt_dec 0 y) => Hy Hx Hp. by apply Hw. apply (filterlim_ext (fun z => - (fst z * -snd z))). intros t. ring. rewrite -(Rbar_opp_involutive z). eapply filterlim_comp. 2: apply filterlim_Rbar_opp. assert (Hw' : filterlim (fun z => fst z * snd z) (filter_prod (Rbar_locally x) (Rbar_locally (Rbar_opp y))) (Rbar_locally (Rbar_opp z))). apply Hw. replace (Finite 0) with (Rbar_opp 0) by apply (f_equal Finite), Ropp_0. apply Rbar_opp_le. by apply Rbar_lt_le. by []. by apply is_Rbar_mult_opp_r. clear Hw. intros P HP. specialize (Hw' P HP). destruct Hw' as [Q R H1 H2 H3]. exists Q (fun x => R (- x)). exact H1. now apply filterlim_Rbar_opp. intros u v HQ HR. exact (H3 _ _ HQ HR). wlog: x y z / (Rbar_le x y). intros Hw. case: (Rbar_le_lt_dec x y) => Hl Hx Hy Hp. by apply Hw. assert (Hw' : filterlim (fun z => fst z * snd z) (filter_prod (Rbar_locally y) (Rbar_locally x)) (Rbar_locally z)). apply Hw ; try assumption. by apply Rbar_lt_le. by apply is_Rbar_mult_sym. intros P HP. specialize (Hw' P HP). destruct Hw' as [Q R H1 H2 H3]. exists R Q ; try assumption. intros u v HR HQ. simpl. rewrite Rmult_comm. exact (H3 _ _ HQ HR). case: x => [x| | ] ; case: y => [y| | ] ; case: z => [z| | ] Hl Hy Hx Hp ; try (by case: Hl) || (by case: Hx) || (by case: Hy). case: Hp => <-. intros P [eps HP]. assert (He: 0 < eps / (x + y + 1)). apply Rdiv_lt_0_compat. apply cond_pos. apply Rplus_le_lt_0_compat. now apply Rplus_le_le_0_compat. apply Rlt_0_1. set (d := mkposreal _ (Rmin_stable_in_posreal (mkposreal _ Rlt_0_1) (mkposreal _ He))). exists (fun u => Rabs (u - x) < d) (fun v => Rabs (v - y) < d). now exists d. now exists d. simpl. intros u v Hu Hv. apply HP. rewrite /ball /= /AbsRing_ball /abs /minus /plus /opp /=. replace (u * v + - (x * y)) with (x * (v - y) + y * (u - x) + (u - x) * (v - y)) by ring. replace (pos eps) with (x * (eps / (x + y + 1)) + y * (eps / (x + y + 1)) + 1 * (eps / (x + y + 1))). apply Rle_lt_trans with (1 := Rabs_triang _ _). apply Rplus_le_lt_compat. apply Rle_trans with (1 := Rabs_triang _ _). apply Rplus_le_compat. rewrite Rabs_mult Rabs_pos_eq //. apply Rmult_le_compat_l with (1 := Hx). apply Rlt_le. apply Rlt_le_trans with (1 := Hv). apply Rmin_r. rewrite Rabs_mult Rabs_pos_eq //. apply Rmult_le_compat_l with (1 := Hy). apply Rlt_le. apply Rlt_le_trans with (1 := Hu). apply Rmin_r. rewrite Rabs_mult. apply Rmult_le_0_lt_compat ; try apply Rabs_pos. apply Rlt_le_trans with (1 := Hu). apply Rmin_l. apply Rlt_le_trans with (1 := Hv). apply Rmin_r. field. apply Rgt_not_eq. apply Rplus_le_lt_0_compat. now apply Rplus_le_le_0_compat. apply Rlt_0_1. move: Hp ; unfold is_Rbar_mult, Rbar_mult'. case: Rle_dec => // Hx'. case: Rle_lt_or_eq_dec => {Hl Hx Hy Hx'} // Hx. move: Hp ; unfold is_Rbar_mult, Rbar_mult'. case: Rle_dec => // Hx'. case: Rle_lt_or_eq_dec => {Hl Hx Hy Hx'} // Hx _. intros P [N HN]. exists (fun u => Rabs (u - x) < x / 2) (fun v => Rmax 0 (N / (x / 2)) < v). now exists (pos_div_2 (mkposreal _ Hx)). now exists (Rmax 0 (N / (x / 2))). intros u v Hu Hv. simpl. apply HN. apply Rle_lt_trans with ((x - x / 2) * Rmax 0 (N / (x / 2))). apply Rmax_case_strong => H. rewrite Rmult_0_r ; apply Rnot_lt_le ; contradict H ; apply Rlt_not_le. repeat apply Rdiv_lt_0_compat => //. by apply Rlt_R0_R2. apply Req_le ; field. by apply Rgt_not_eq. apply Rmult_le_0_lt_compat. lra. apply Rmax_l. now apply Rabs_lt_between'. exact Hv. move: Hp ; unfold is_Rbar_mult, Rbar_mult'. case: Rle_dec => // Hx'. case: Rle_lt_or_eq_dec => {Hl Hx Hy Hx'} // Hx. clear. intros P [N HN]. exists (fun u => 1 < u) (fun v => Rabs N < v). now exists 1. now exists (Rabs N). intros u v Hu Hv. simpl. apply HN. apply Rle_lt_trans with (1 := Rle_abs _). rewrite -(Rmult_1_l (Rabs N)). apply Rmult_le_0_lt_compat. by apply Rle_0_1. by apply Rabs_pos. exact Hu. exact Hv. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lub Markov Hierarchy