proposition: Lemma filterlim_switch_2 {U : CompleteSpace} F1 (FF1 : ProperFilter F1) F2 (FF2 : ProperFilter F2) (f : T1 -> T2 -> U) g h : filterlim f F1 (locally g) -> (forall x, filterlim (f x) F2 (locally (h x))) -> exists l : U, filterlim h F1 (locally l).
proof: Proof. move => Hfg Hfh. case : (proj1 (filterlim_locally_cauchy h)). move => eps. generalize (proj2 (filterlim_locally_cauchy f)) => Hf. assert (exists y : T2 -> U, filterlim f F1 (locally y)). exists g => P Hp. apply Hfg. case: Hp => d Hp. exists d => y Hy. apply: Hp. by apply Hy. move: H => {} Hfg. move: (Hf Hfg (pos_div_2 eps)) => {Hf Hfg} /= Hf. case: FF2 => HF2 FF2. generalize (fun x => proj1 (filterlim_locally (f x) (h x)) (Hfh x) (pos_div_2 (pos_div_2 eps))) => {} Hfh. case: Hf => P [Hp Hf]. exists P ; split. by []. move => u v Hu Hv. move: (Hfh u) => /= Hu'. move: (Hfh v) => /= Hv'. move: (@filter_and _ F2 FF2 _ _ Hu' Hv') => {Hu' Hv'} Hfh. case: (HF2 _ Hfh) => {Hfh} y Hy. replace (pos eps) with (eps / 2 / 2 + (eps / 2 + eps / 2 / 2)) by field. apply ball_triangle with (f u y). by apply Hy. apply ball_triangle with (f v y). by apply Hf. now apply ball_sym. move => l Hl. by exists l. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub