proposition: Lemma filterlim_scal (k : K) (x : V) : filterlim (fun z => scal (fst z) (snd z)) (filter_prod (locally k) (locally x)) (locally (scal k x)).
proof: Proof. apply filterlim_locally => /= eps. eapply filter_imp. move => /= u Hu. rewrite (double_var eps). apply ball_triangle with (scal (fst u) x). apply norm_compat1. rewrite -scal_minus_distr_r. eapply Rle_lt_trans. apply norm_scal. eapply Rle_lt_trans. apply Rmult_le_compat_l. by apply abs_ge_0. apply Rlt_le, Rlt_plus_1. apply <- Rlt_div_r. 2: apply Rle_lt_0_plus_1, norm_ge_0. by eapply (proj1 Hu). apply norm_compat1. rewrite -scal_minus_distr_l. eapply Rle_lt_trans. apply norm_scal. eapply Rle_lt_trans. apply Rmult_le_compat_r. by apply norm_ge_0. replace (fst u) with (plus k (minus (fst u) k)). eapply Rle_trans. apply abs_triangle. apply Rplus_le_compat_l. apply Rlt_le. instantiate (1 := 1). eapply (proj1 (proj2 Hu)). by rewrite plus_comm -plus_assoc plus_opp_l plus_zero_r. rewrite Rmult_comm. apply <- Rlt_div_r. 2: apply Rle_lt_0_plus_1, abs_ge_0. by apply (proj2 (proj2 Hu)). repeat apply filter_and. assert (Hd : 0 < eps / 2 / (norm x + 1)). apply Rdiv_lt_0_compat. by apply is_pos_div_2. apply Rle_lt_0_plus_1, norm_ge_0. eexists. apply (locally_ball_norm (V := AbsRing_NormedModule K) _ (mkposreal _ Hd)). apply filter_true. by []. eexists. apply (locally_ball_norm (V := AbsRing_NormedModule K) _ (mkposreal _ Rlt_0_1)). apply filter_true. by []. assert (Hd : 0 < eps / 2 / (abs k + 1)). apply Rdiv_lt_0_compat. by apply is_pos_div_2. apply Rle_lt_0_plus_1, abs_ge_0. eexists. apply filter_true. apply (locally_ball_norm _ (mkposreal _ Hd)). by []. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub