proposition: Lemma filterlim_le : forall {T F} {FF : ProperFilter' F} (f g : T -> R) (lf lg : Rbar), F (fun x => f x <= g x) -> filterlim f F (Rbar_locally lf) -> filterlim g F (Rbar_locally lg) -> Rbar_le lf lg.
proof: Proof. intros T F FF f g lf lg H Hf Hg. apply Rbar_not_lt_le. intros Hl. apply filter_not_empty. destruct lf as [lf| |] ; destruct lg as [lg| |] ; try easy. - assert (Hl' : 0 < (lf - lg) / 2). apply Rdiv_lt_0_compat. now apply -> Rminus_lt_0. apply Rlt_R0_R2. assert (Hlf : locally lf (fun y => (lf + lg) / 2 < y)). apply open_gt. replace ((lf + lg) / 2) with (lf - (lf - lg) / 2) by field. apply Rabs_lt_between'. by rewrite /Rminus Rplus_opp_r Rabs_R0. assert (Hlg : locally lg (fun y => y < (lf + lg) / 2)). apply open_lt. replace ((lf + lg) / 2) with (lg + (lf - lg) / 2) by field. apply Rabs_lt_between'. by rewrite /Rminus Rplus_opp_r Rabs_R0. specialize (Hf _ Hlf). specialize (Hg _ Hlg). unfold filtermap in Hf, Hg. generalize (filter_and _ _ (filter_and _ _ Hf Hg) H). apply filter_imp. intros x [[H1 H2] H3]. apply Rle_not_lt with (1 := H3). now apply Rlt_trans with ((lf + lg) / 2). - assert (Hlf : locally lf (fun y => lf - 1 < y)). apply open_gt. apply Rabs_lt_between'. rewrite /Rminus Rplus_opp_r Rabs_R0. apply Rlt_0_1. assert (Hlg : Rbar_locally m_infty (fun y => Rbar_lt y (lf - 1))). now apply open_Rbar_lt'. specialize (Hf _ Hlf). specialize (Hg _ Hlg). unfold filtermap in Hf, Hg. generalize (filter_and _ _ (filter_and _ _ Hf Hg) H). apply filter_imp. intros x [[H1 H2] H3]. apply Rle_not_lt with (1 := H3). now apply Rlt_trans with (lf - 1). - assert (Hlf : Rbar_locally p_infty (fun y => Rbar_lt (lg + 1) y)). now apply open_Rbar_gt'. assert (Hlg : locally lg (fun y => y < lg + 1)). apply open_lt. apply Rabs_lt_between'. rewrite /Rminus Rplus_opp_r Rabs_R0. apply Rlt_0_1. specialize (Hf _ Hlf). specialize (Hg _ Hlg). unfold filtermap in Hf, Hg. generalize (filter_and _ _ (filter_and _ _ Hf Hg) H). apply filter_imp. intros x [[H1 H2] H3]. apply Rle_not_lt with (1 := H3). now apply Rlt_trans with (lg + 1). - assert (Hlf : Rbar_locally p_infty (fun y => Rbar_lt 0 y)). now apply open_Rbar_gt'. assert (Hlg : Rbar_locally m_infty (fun y => Rbar_lt y 0)). now apply open_Rbar_lt'. specialize (Hf _ Hlf). specialize (Hg _ Hlg). unfold filtermap in Hf, Hg. generalize (filter_and _ _ (filter_and _ _ Hf Hg) H). apply filter_imp. intros x [[H1 H2] H3]. apply Rle_not_lt with (1 := H3). now apply Rlt_trans with 0. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lub Markov Hierarchy