proposition: Lemma filterlim_RInt {U} {V : CompleteNormedModule R_AbsRing} : forall (f : U -> R -> V) (a b : R) F (FF : ProperFilter F) g h, (forall x, is_RInt (f x) a b (h x)) -> (filterlim f F (locally g)) -> exists If, filterlim h F (locally If) /\ is_RInt g a b If.
proof: Proof. intros f a b F FF g h Hfh Hfg. wlog: a b h Hfh / (a <= b) => [Hw | Hab]. case: (Rle_lt_dec a b) => Hab. by apply Hw. destruct (Hw b a (fun x => opp (h x))) as [If [Hfh' Hfg']]. intro x. by apply @is_RInt_swap. by apply Rlt_le. exists (opp If) ; split. apply filterlim_ext with (fun x => opp (opp (h x))). move => x. by apply opp_opp. eapply (filterlim_comp _ _ _ (fun x => opp (h x)) opp). by apply Hfh'. now generalize (filterlim_opp If). by apply @is_RInt_swap. case: Hab => Hab. destruct (fun FF2 HF2 => filterlim_switch_dom F FF (locally_dist (fun ptd : SF_seq.SF_seq => SF_seq.seq_step (SF_seq.SF_lx ptd))) FF2 (fun ptd : SF_seq.SF_seq => SF_seq.pointed_subdiv ptd /\ SF_seq.SF_h ptd = Rmin a b /\ seq.last (SF_seq.SF_h ptd) (SF_seq.SF_lx ptd) = Rmax a b) HF2 (fun (x : U) ptd => scal (sign (b - a)) (Riemann_sum (f x) ptd)) (fun ptd => scal (sign (b - a)) (Riemann_sum g ptd)) h) as [If [Hh Hg]]. by apply locally_dist_filter. intros P [eP HP]. assert (Hn : 0 <= ((b - a) / eP)). apply Rdiv_le_0_compat. apply -> Rminus_le_0. apply Rlt_le, Hab. apply cond_pos. set n := (nfloor _ Hn). exists (SF_seq.SF_seq_f2 (fun x y => x) (SF_seq.unif_part (Rmin a b) (Rmax a b) n)). destruct (Riemann_fine_unif_part (fun x y => x) a b n). intros u v Huv. split. apply Rle_refl. exact Huv. now apply Rlt_le, Hab. rewrite /Rmin /Rmax ; case: Rle_dec (Rlt_le _ _ Hab) => // _ _. split. apply H0. apply HP. apply Rle_lt_trans with (1 := H). apply Rlt_div_l. apply INRp1_pos. unfold n, nfloor. destruct nfloor_ex as [n' Hn']. simpl. rewrite Rmult_comm. apply Rlt_div_l. apply cond_pos. apply Hn'. rewrite /Rmin /Rmax ; case: Rle_dec (Rlt_le _ _ Hab) => // _ _. 2: by apply Hfh. set (M := @norm_factor _ V). intros P [eps HP]. have He: 0 < (eps / (b - a)) / (2 * M). apply Rdiv_lt_0_compat. apply Rdiv_lt_0_compat. by apply eps. by rewrite -Rminus_lt_0. apply Rmult_lt_0_compat. by apply Rlt_0_2. apply norm_factor_gt_0. generalize (Hfg _ (locally_ball g (mkposreal _ He))) => {Hfg Hfh}. unfold filtermap ; apply filter_imp => x Hx. apply HP. case => t [Ht [Ha Hb]] /=. rewrite -> sign_eq_1 by exact: Rlt_Rminus. rewrite 2!scal_one. apply: norm_compat1. generalize (Riemann_sum_minus (f x) g t) => <-. refine (_ (Riemann_sum_norm (fun x0 : R => minus (f x x0) (g x0)) (fun _ => M * ((eps / (b - a)) / (2 * M))) t Ht _)). move => H ; apply Rle_lt_trans with (1 := H). rewrite Riemann_sum_const. rewrite Hb Ha. rewrite /scal /= /mult /=. replace ((b - a) * (M * ((eps / (b - a)) / (2 * M)))) with (eps / 2). rewrite {2}(double_var eps) -{1}(Rplus_0_l (eps / 2)). apply Rplus_lt_compat_r. apply Rdiv_lt_0_compat. by apply eps. by apply Rlt_0_2. field. split. apply Rgt_not_eq. apply Rlt_gt. by rewrite -Rminus_lt_0. apply Rgt_not_eq. apply norm_factor_gt_0. intros t0 Ht0. apply Rlt_le. apply (norm_compat2 _ _ (mkposreal _ He) (Hx t0)). exists If ; split. by apply Hh. by apply Hg. exists zero. rewrite -Hab in Hfh |- * => {b Hab}. split. apply filterlim_ext with (fun _ => zero). intros x. apply filterlim_locally_unique with (2 := Hfh x). apply is_RInt_point. apply filterlim_const. apply is_RInt_point. Qed.
imports: Coq(Reals Psatz) mathcomp(ssreflect ssrbool ssrfun eqtype seq) Markov Rcomplements Rbar Lub Lim_seq SF_seq Continuity Hierarchy