proposition: Lemma filterlim_switch_1 {U : UniformSpace} F1 (FF1 : ProperFilter F1) F2 (FF2 : Filter F2) (f : T1 -> T2 -> U) g h (l : U) : filterlim f F1 (locally g) -> (forall x, filterlim (f x) F2 (locally (h x))) -> filterlim h F1 (locally l) -> filterlim g F2 (locally l).
proof: Proof. intros Hfg Hfh Hhl P. case: FF1 => HF1 FF1. apply filterlim_locally. move => eps. have FF := (filter_prod_filter _ _ F1 F2 FF1 FF2). assert (filter_prod F1 F2 (fun x => ball (g (snd x)) (eps / 2 / 2) (f (fst x) (snd x)))). apply Filter_prod with (fun x : T1 => ball g (eps / 2 / 2) (f x)) (fun _ => True). move: (proj1 (@filterlim_locally _ _ F1 FF1 f g) Hfg (pos_div_2 (pos_div_2 eps))) => {Hfg} /= Hfg. by []. by apply FF2. simpl ; intros. apply H. move: H => {} Hfg. assert (filter_prod F1 F2 (fun x : T1 * T2 => ball l (eps / 2) (h (fst x)))). apply Filter_prod with (fun x : T1 => ball l (eps / 2) (h x)) (fun _ => True). move: (proj1 (@filterlim_locally _ _ F1 FF1 h l) Hhl (pos_div_2 eps)) => {Hhl} /= Hhl. by []. by apply FF2. by []. move: H => {} Hhl. case: (@filter_and _ _ FF _ _ Hhl Hfg) => {Hhl Hfg} /= ; intros. move: (fun x => proj1 (@filterlim_locally _ _ F2 FF2 (f x) (h x)) (Hfh x) (pos_div_2 (pos_div_2 eps))) => {Hfh} /= Hfh. case: (HF1 Q f0) => x Hx. move: (@filter_and _ _ FF2 _ _ (Hfh x) g0) => {Hfh}. apply filter_imp => y Hy. rewrite (double_var eps). apply ball_triangle with (h x). apply (p x y). by []. by apply Hy. rewrite (double_var (eps / 2)). apply ball_triangle with (f x y). by apply Hy. apply ball_sym, p. by []. by apply Hy. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub