Library agm.filter_Rlt
From mathcomp Require Import ssreflect.
Require Import Reals Coquelicot.Coquelicot Fourier.
Lemma ball_Rabs x y e : ball x e y <-> Rabs (y - x) < e.
Proof. intros; tauto. Qed.
Definition filter_Rlt F1 F2 :=
exists m, filter_prod F1 F2 (fun p => fst p < m < snd p).
Lemma filter_Rlt_witness m (F1 F2 : (R -> Prop) -> Prop) :
F1 (Rgt m) -> F2 (Rlt m) -> filter_Rlt F1 F2.
Proof.
exists m; split with (Rgt m) (Rlt m); simpl; auto with real.
Qed.
Lemma filter_Rlt_m_infty_p_infty :
filter_Rlt (Rbar_locally m_infty) (Rbar_locally p_infty).
Proof.
apply (filter_Rlt_witness 0); exists 0; tauto.
Qed.
Lemma filter_Rlt_m_infty_at_left b :
filter_Rlt (Rbar_locally m_infty) (at_left b).
Proof.
apply (filter_Rlt_witness (b - 1)).
now exists (b - 1); intros x cmpx; apply Rlt_gt.
exists pos_half; intros x yb _.
enough (b - x < 1) by fourier.
apply Rle_lt_trans with (abs (minus b x)).
now apply Rle_abs.
apply ball_sym in yb; apply AbsRing_norm_compat2 in yb.
apply Rlt_trans with (1 := yb).
rewrite Rmult_1_l; simpl.
fourier.
Qed.
Lemma filter_Rlt_at_right_p_infty b :
filter_Rlt (at_right b) (Rbar_locally p_infty).
Proof.
apply (filter_Rlt_witness (b + 1)).
exists pos_half; intros y yb _.
enough (y - b < 1) by fourier.
apply Rle_lt_trans with (abs (minus y b)).
now apply Rle_abs.
apply AbsRing_norm_compat2 in yb.
apply Rlt_trans with (1 := yb).
rewrite Rmult_1_l; simpl.
fourier.
now exists (b + 1); intros x cmpx.
Qed.
Lemma filter_Rlt_at_point_p_infty b :
filter_Rlt (at_point b) (Rbar_locally p_infty).
Proof.
apply (filter_Rlt_witness (b + 1)).
now unfold at_point; fourier.
now exists (b + 1); tauto.
Qed.
Lemma filter_Rlt_m_infty_at_point b :
filter_Rlt (Rbar_locally m_infty) (at_point b).
Proof.
apply (filter_Rlt_witness (b - 1)).
now exists (b - 1); tauto.
now unfold at_point; fourier.
Qed.
Local Lemma compare_half_sum a b (altb : a < b) : a < (a + b) / 2 < b.
Proof.
assert ((a + b) / 2 * 2 = a + b) by field.
split; apply Rmult_lt_reg_r with 2; fourier.
Qed.
Lemma filter_Rlt_at_point a b : a < b ->
filter_Rlt (at_point a) (at_point b).
Proof.
intros altb; apply filter_Rlt_witness with ((a + b) / 2).
unfold at_point.
now destruct (compare_half_sum _ _ altb); tauto.
unfold at_point.
now destruct (compare_half_sum _ _ altb); tauto.
Qed.
Lemma Rplus_minus_cancel1 : forall a b, a + b - a = b.
Proof. intros; ring. Qed.
Lemma filter_Rlt_locally a b : a < b ->
filter_Rlt (Rbar_locally a) (Rbar_locally b).
Proof.
intros ab.
assert (bmap: 0 < (b - a)/2).
apply Rmult_lt_reg_r with 2;[fourier | ].
unfold Rdiv; rewrite -> Rmult_0_l, Rmult_assoc.
rewrite -> Rinv_l, Rmult_1_r;[ | apply Rgt_not_eq]; fourier.
apply (filter_Rlt_witness ((a + b)/2)).
exists (mkposreal _ bmap); intros y ya.
enough (yma : y * 2 - a * 2 < b - a).
apply Rmult_lt_reg_r with 2;[fourier | ].
unfold Rdiv; rewrite -> Rmult_assoc, Rinv_l;[ | apply Rgt_not_eq; fourier].
rewrite -> Rmult_1_r; fourier.
rewrite <- Rmult_minus_distr_r; apply Rmult_lt_reg_r with (/2).
apply Rinv_0_lt_compat; fourier.
rewrite -> Rmult_assoc, Rinv_r, Rmult_1_r;[|apply Rgt_not_eq; fourier].
apply Rle_lt_trans with (abs (minus y a)).
now apply Rle_abs.
apply AbsRing_norm_compat2 in ya; apply Rlt_le_trans with (1 := ya).
now rewrite -> Rmult_1_l; simpl; auto with real.
exists (mkposreal _ bmap); intros y yb.
enough (yma : b * 2 - y * 2 < b - a).
apply Rmult_lt_reg_r with 2;[fourier | ].
unfold Rdiv; rewrite -> Rmult_assoc, Rinv_l;[ | apply Rgt_not_eq; fourier].
rewrite -> Rmult_1_r; fourier.
rewrite <- Rmult_minus_distr_r; apply Rmult_lt_reg_r with (/2).
apply Rinv_0_lt_compat; fourier.
rewrite -> Rmult_assoc, Rinv_r, Rmult_1_r;[|apply Rgt_not_eq; fourier].
apply Rle_lt_trans with (abs (minus b y)).
now apply Rle_abs.
apply ball_sym in yb; apply AbsRing_norm_compat2 in yb.
apply Rlt_le_trans with (1 := yb).
now rewrite -> Rmult_1_l; simpl; auto with real.
Qed.
Lemma filter_Rlt_left_right a b : a <= b ->
filter_Rlt (at_left a) (at_right b).
intros ab; apply (filter_Rlt_witness a).
now exists pos_half; intros y _; apply Rgt_lt.
now exists pos_half; intros y _ yb ; apply Rle_lt_trans with b.
Qed.
Lemma filter_Rlt_trans a F G {FF : Filter F} {GG : Filter G} :
filter_Rlt F (at_point a) ->
filter_Rlt (at_point a) G -> filter_Rlt F G.
Proof.
intros [m1 Pm1] [m2 Pm2].
apply filter_Rlt_witness with a.
destruct Pm1 as [P Q FP atQ cnd1].
assert (qa : Q a) by now apply atQ; intros; apply ball_center.
apply (filter_imp P); auto.
intros x px.
assert (t := cnd1 x a px qa); simpl in t; destruct t; fourier.
destruct Pm2 as [P Q atP GQ cnd2].
assert (pa : P a) by now apply atP; intros; apply ball_center.
apply (filter_imp Q); auto.
intros x qx.
assert (t := cnd2 a x pa qx); simpl in t; destruct t; fourier.
Qed.
Lemma filter_Rlt_right_left a b : a < b ->
filter_Rlt (at_right a) (at_left b).
Proof.
intros ab.
assert (bmap: 0 < (b - a)/2).
apply Rmult_lt_reg_r with 2;[fourier | ].
unfold Rdiv; rewrite -> Rmult_0_l, Rmult_assoc.
rewrite -> Rinv_l, Rmult_1_r;[ | apply Rgt_not_eq]; fourier.
apply (filter_Rlt_witness ((a + b)/2)).
exists (mkposreal _ bmap); intros y ya cmp.
enough (yma : y * 2 - a * 2 < b - a).
apply Rmult_lt_reg_r with 2;[fourier | ].
unfold Rdiv; rewrite -> Rmult_assoc, Rinv_l;[ | apply Rgt_not_eq; fourier].
rewrite -> Rmult_1_r; fourier.
rewrite <- Rmult_minus_distr_r; apply Rmult_lt_reg_r with (/2).
apply Rinv_0_lt_compat; fourier.
rewrite -> Rmult_assoc, Rinv_r, Rmult_1_r;[|apply Rgt_not_eq; fourier].
apply Rle_lt_trans with (abs (minus y a)).
now apply Rle_abs.
apply AbsRing_norm_compat2 in ya; apply Rlt_le_trans with (1 := ya).
now rewrite -> Rmult_1_l; simpl; auto with real.
exists (mkposreal _ bmap); intros y yb cmp.
enough (yma : b * 2 - y * 2 < b - a).
apply Rmult_lt_reg_r with 2;[fourier | ].
unfold Rdiv; rewrite -> Rmult_assoc, Rinv_l;[ | apply Rgt_not_eq; fourier].
rewrite -> Rmult_1_r; fourier.
rewrite <- Rmult_minus_distr_r; apply Rmult_lt_reg_r with (/2).
apply Rinv_0_lt_compat; fourier.
rewrite -> Rmult_assoc, Rinv_r, Rmult_1_r;[|apply Rgt_not_eq; fourier].
apply Rle_lt_trans with (abs (minus b y)).
now apply Rle_abs.
apply ball_sym in yb; apply AbsRing_norm_compat2 in yb.
apply Rlt_le_trans with (1 := yb).
now rewrite -> Rmult_1_l; simpl; auto with real.
Qed.
Local Ltac chain_comparisons :=
match goal with
| h : ?a <= _ |- ?a < _ => apply Rle_lt_trans with (1 := h)
| h : _ <= ?a |- _ < ?a => apply Rlt_le_trans with (2 := h)
| h : ?a < _ |- ?a < _ => apply Rlt_trans with (1 := h)
| h : _ < ?a |- _ < ?a => apply Rlt_trans with (2 := h)
end.
Lemma ex_RInt_gen_bound (g : R -> R) (f : R -> R) F G
{PF : ProperFilter F} {PG : ProperFilter G} :
filter_Rlt F G ->
ex_RInt_gen g F G ->
filter_prod F G
(fun p => (forall x, fst p < x < snd p -> 0 <= f x <= g x) /\
ex_RInt f (fst p) (snd p)) ->
ex_RInt_gen f F G.
Proof.
intros [m mmid] [gl intg] cmp.
assert (F (Rgt m)).
destruct mmid as [pf pg fpf gpg cmp'].
apply (filter_imp pf); destruct (filter_ex pg) as [y py]; auto.
intros x px; destruct (cmp' x y px py) as [it _]; exact it.
assert (G (Rlt m)).
destruct mmid as [pf pg fpf gpg cmp'].
apply (filter_imp pg); destruct (filter_ex (F := F) pf) as [x px]; auto.
intros y py; destruct (cmp' x y px py) as [_ it]; exact it.
exists (lim (filtermap (fun p => RInt f (fst p) (snd p)) (filter_prod F G))).
destruct cmp as [Q1 R1 fq1 gr1 cmp]; simpl in cmp.
assert (cc : cauchy (filtermap (fun p => RInt f (fst p) (snd p))
(filter_prod F G))).
intros eps.
destruct (intg _ (locally_ball gl (pos_div_2 eps))) as [Qg Rg FQg GRg main].
assert (fq : F (fun x => Q1 x /\ Qg x /\ m > x))
by now repeat apply filter_and.
assert (gr : G (fun x => R1 x /\ Rg x /\ m < x))
by now repeat apply filter_and.
destruct (filter_ex _ fq) as [x qx], (filter_ex _ gr) as [y ry].
exists (RInt f x y).
exists (fun x => Q1 x /\ Qg x /\ m > x)
(fun y => R1 y /\ Rg y /\ m < y);
try now repeat apply filter_and.
intros u v Qu Rv.
assert (wlog_cc : forall a b c d,
Q1 a /\ Qg a ->
Q1 b /\ Qg b ->
R1 c /\ Rg c ->
R1 d /\ Rg d ->
a <= b -> c <=d -> b < m -> m < c ->
(ball (RInt f a d) eps (RInt f b c) /\
ball (RInt f a c) eps (RInt f b d))).
clear x y qx ry u v Qu Rv; intros a b c d Qa Qb Rc Rd ab cd bm mc.
assert (ex_RInt f a c /\ ex_RInt f b c /\ ex_RInt f b d).
now repeat apply conj; apply cmp.
move main after mc.
destruct (main a c) as [gac [acP acQ]]; try tauto; simpl in acP.
assert (ex_RInt g a c) by (eapply ex_intro; eauto).
destruct (main b c) as [gbc [bcP bcQ]]; try tauto; simpl in bcP.
assert (ex_RInt g b c) by (eapply ex_intro; eauto).
destruct (main b d) as [gbd [bdP bdQ]]; try tauto; simpl in bdP.
assert (ex_RInt g b d) by (eapply ex_intro; eauto).
assert (ex_RInt f a b).
now apply ex_RInt_Chasles with c;[ | apply ex_RInt_swap].
assert (ex_RInt f c d).
now apply ex_RInt_Chasles with b;[apply ex_RInt_swap | ].
assert (ex_RInt g a b).
now apply ex_RInt_Chasles with c;[ | apply ex_RInt_swap];
eapply ex_intro; eauto.
assert (ex_RInt g c d).
now apply ex_RInt_Chasles with b;[apply ex_RInt_swap | ];
eapply ex_intro; eauto.
assert (bc : b < c) by (apply Rlt_trans with m; tauto).
split.
apply ball_sym, Rle_lt_trans with (Rabs (RInt g a d - RInt g b c)).
rewrite <- (RInt_Chasles f a b d), <- (RInt_Chasles f b c d),
<- (RInt_Chasles g a b d), <- (RInt_Chasles g b c d),
!(Rplus_comm (RInt _ a b)), !Rplus_assoc, !Rplus_minus_cancel1;
try tauto.
unfold abs; simpl; rewrite -> !Rabs_right;
try (apply Rle_ge, Rplus_le_le_0_compat; apply RInt_ge_0; auto);
try (intros x [x1 x2]; enough (0 <= f x <= g x)
by (solve[tauto | apply Rle_trans with (f x); tauto]);
apply (cmp a d); try tauto; split;
solve[repeat (auto; chain_comparisons)]).
apply Rplus_le_compat; apply RInt_le; try tauto;
try (intros x [x1 x2]; enough (0 <= f x <= g x)
by (solve[tauto | apply Rle_trans with (f x); tauto]);
apply (cmp a d); try tauto; split;
solve[repeat (auto; chain_comparisons)]).
change (ball (RInt g b c) eps (RInt g a d)).
replace (pos eps) with (pos_div_2 eps + pos_div_2 eps) by (simpl; field).
apply ball_triangle with gl.
now rewrite -> (is_RInt_unique _ _ _ _ bcP); apply ball_sym.
destruct (main a d) as [gad [adP adQ]]; try tauto; simpl in adP.
now rewrite -> (is_RInt_unique _ _ _ _ adP).
change (Rabs (RInt f b d + - RInt f a c) < eps).
rewrite <- (RInt_Chasles f b c d), <- (RInt_Chasles f a b c),
Ropp_plus_distr, !Rplus_assoc, (Rplus_comm (RInt f b c)), !Rplus_assoc,
Rplus_opp_l, Rplus_0_r; try tauto.
apply Rle_lt_trans with (1 := Rabs_triang _ _);
rewrite -> Rabs_Ropp, !Rabs_right;
try (apply Rle_ge, RInt_ge_0; try tauto);
try (intros x [x1 x2]; enough (0 <= f x <= g x)
by (solve[tauto | apply Rle_trans with (f x); tauto]);
apply (cmp a d); try tauto; split;
solve[repeat (auto; chain_comparisons)]).
replace (pos eps) with (pos_div_2 eps + pos_div_2 eps)
by (simpl; field).
assert (dc : RInt f c d <= RInt g c d /\ RInt f a b <= RInt g a b).
split; apply RInt_le; try tauto;
try (intros x [x1 x2]; enough (0 <= f x <= g x)
by (solve[tauto | apply Rle_trans with (f x); tauto]);
apply (cmp a d); try tauto; split;
solve[repeat (auto; chain_comparisons)]).
apply Rle_lt_trans with (1 := Rplus_le_compat _ _ _ _ (proj1 dc)(proj2 dc)).
apply Rle_lt_trans with (1 := Rle_abs _).
replace (RInt _ _ _ + _) with
((RInt g a d - gl) - (RInt g b c - gl)) by
(rewrite <- (RInt_Chasles g a b d), <- (RInt_Chasles g b c d);
try tauto; set (zoo := plus); change zoo with Rplus; ring).
apply Rle_lt_trans with (1 := Rabs_triang _ _), Rplus_lt_compat.
destruct (main a d) as [gad [adP adQ]]; try tauto; simpl in adP.
now rewrite -> (is_RInt_unique _ _ _ _ adP).
now rewrite -> Rabs_Ropp; rewrite -> (is_RInt_unique _ _ _ _ bcP).
destruct (Rlt_dec x u), (Rlt_dec v y);
[apply (wlog_cc x u v y) | apply (wlog_cc x u y v) |
apply ball_sym, (wlog_cc u x v y) | apply ball_sym, (wlog_cc u x y v)];
try split;
try solve[tauto | apply Rlt_le; tauto |
apply Rge_le; tauto | apply Rle_ge; tauto|
apply Rnot_lt_le; tauto].
intros P [eps Peps].
move cc after Peps.
unfold filtermapi.
assert (tmp := complete_cauchy _ _ cc eps).
destruct tmp as [Q2 R2 Q2P R2P PP2].
exists (fun x => Q2 x /\ Q1 x) (fun x => R2 x /\ R1 x);
try (apply filter_and; auto).
intros x y [Q2x Q1x] [R2x R1x].
destruct (cmp x y Q1x R1x) as [cmp' [fxy intxy]].
exists fxy; split;[assumption | apply Peps].
rewrite <- (is_RInt_unique _ _ _ _ intxy); apply PP2; auto.
Qed.
Lemma is_RInt_gen_Rle (g : R -> R) gl (f : R -> R) fl F G
{PF : ProperFilter F} {PG : ProperFilter G} :
filter_Rlt F G ->
is_RInt_gen g F G gl ->
is_RInt_gen f F G fl ->
filter_prod F G
(fun p => (forall x, fst p < x < snd p -> f x <= g x)) ->
fl <= gl.
Proof.
intros [m mmid] intg intf cmp.
apply (filterlim_le (F := filter_prod F G) (fun p => RInt f (fst p) (snd p))
(fun p => RInt g (fst p) (snd p)) fl gl).
specialize (intf _ (locally_ball fl (mkposreal _ Rlt_0_1))).
specialize (intg _ (locally_ball gl (mkposreal _ Rlt_0_1))).
unfold filtermapi in intg, intf.
apply: filter_imp (filter_and _ _ (filter_and _ _ intg intf)
(filter_and _ _ mmid cmp)).
intros [a b]; simpl; intros [[[Ig [Hg1 Hg2]] [If [Hf1 Hf2]]] [cmp']].
apply RInt_le;
[apply Rle_trans with m;apply Rlt_le | exists If| exists Ig| ]; tauto.
intros P HP; specialize (intf P HP); unfold filtermapi, filtermap in intf |- *.
apply: filter_imp intf.
intros [a b]; simpl; intros [y [inty Py]].
now rewrite -> (is_RInt_unique _ _ _ _ inty).
intros P HP; specialize (intg P HP); unfold filtermapi, filtermap in intg |- *.
apply: filter_imp intg.
intros [a b]; simpl; intros [y [inty Py]].
now rewrite -> (is_RInt_unique _ _ _ _ inty).
Qed.
Lemma is_RInt_gen_at_point_at_right (f : R -> R) (a : R) F {FF : ProperFilter F}
v : locally a (continuous f) -> is_RInt_gen f (at_point a) F v ->
filter_Rlt (at_point a) F -> is_RInt_gen f (at_right a) F v.
Proof.
intros [delta1 pd1] intf [m [P Q FP FQ cmp]]; simpl in cmp.
destruct (pd1 a (ball_center a delta1)
(ball (f a) (mkposreal _ Rlt_0_1)) (locally_ball _ _)) as
[delta2 Pd2].
assert (pa : P a) by (apply FP; intros; apply ball_center).
assert (intf2 := intf).
intros P2 PP2; specialize (intf P2 PP2); destruct PP2 as [eps P2eps].
set (M := Rabs (f a) + 1).
assert (M0 : 0 < eps / M).
apply Rmult_lt_0_compat;[apply cond_pos | apply Rinv_0_lt_compat].
now assert (0 <= Rabs (f a)) by apply Rabs_pos; unfold M; fourier.
assert (close : forall y, y <> a -> ball a delta2 y -> Rabs (f y) < M).
intros y ay b_y; unfold M.
replace (f y) with (f a + (f y - f a)) by ring.
apply Rle_lt_trans with (1 := Rabs_triang _ _).
now apply Rplus_lt_compat_l, Pd2; auto.
assert (exrint_close : forall a', ball a delta1 a' -> ex_RInt f a a').
intros a' baa'.
apply (ex_RInt_continuous f); intros z pz; apply pd1.
destruct (Rle_dec a a') as [aa' | a'a].
rewrite -> Rmin_left, Rmax_right in pz; auto.
change (Rabs (z - a) < delta1).
rewrite -> Rabs_right; cycle 1.
destruct pz; fourier.
destruct pz; apply Rle_lt_trans with (a' - a); try fourier.
rewrite <- (Rabs_right (a' - a)); try fourier.
tauto.
change (Rabs (z - a) < delta1).
destruct (Rle_dec a z) as [az | za].
apply Rnot_le_lt in a'a.
rewrite -> Rmin_right, Rmax_left in pz; try (destruct pz; fourier).
assert (za' : z = a).
now apply Rle_antisym; (destruct pz; fourier).
now rewrite -> za', Rminus_eq_0, Rabs_R0; case delta1; tauto.
apply Rnot_le_lt in a'a; apply Rnot_le_lt in za.
rewrite -> Rmin_right, Rmax_left in pz; try fourier.
rewrite -> Rabs_left;[ | fourier].
apply Rle_lt_trans with (a - a'); try (intuition fourier).
rewrite <- (Rabs_right (a - a')); try (intuition fourier).
now change (ball a' delta1 a); apply ball_sym; tauto.
assert (pre_ep2 : 0 < eps / 2 * /M).
repeat apply Rmult_lt_0_compat; try fourier;[destruct eps; tauto | ].
now apply Rinv_0_lt_compat; unfold M; assert (t := Rabs_pos (f a)); fourier.
set (ep2 := mkposreal _ pre_ep2).
assert (at_right a (fun x => ball a delta1 x /\ ball a ep2 x /\
ball a delta2 x /\ a < x /\ x < m)).
repeat apply filter_and; try (now apply filter_le_within, locally_ball).
now exists ep2; intros; tauto.
destruct (filter_ex _ FQ) as [y' Py'].
assert (ma0 : 0 < m - a).
now destruct (cmp a y'); auto; fourier.
exists (mkposreal _ ma0); simpl; intros y.
intros bay ay; change (Rabs (y - a) < m - a) in bay.
now rewrite -> Rabs_right in bay; fourier.
specialize (intf2 _ (locally_ball v (pos_div_2 eps))).
destruct intf2 as [Pl Ql FPl FQl closerint].
assert (pla : Pl a) by (apply FPl; intros; apply ball_center).
assert (F (fun y => Q y /\ Ql y)) by (apply filter_and; auto).
exists (fun x => ball a delta1 x /\ ball a ep2 x /\
ball a delta2 x /\ a < x /\ x < m)
(fun y => Q y /\ Ql y); auto.
intros x y bx Ry; exists (RInt f x y).
destruct (closerint a y) as [fay [close_fay]]; try tauto.
split.
simpl. apply (RInt_correct f x y).
apply (ex_RInt_Chasles_2 f a);[ | exists fay; tauto].
split; apply Rlt_le;
[| apply Rlt_trans with m; assert (t := cmp a y pa (proj1 Ry))]; tauto.
apply P2eps.
assert (Rabs (RInt f a x) < pos_div_2 eps).
apply Rle_lt_trans with ((x - a) * M).
apply abs_RInt_le_const;[apply Rlt_le; tauto | | ].
now apply exrint_close; tauto.
intros t atx.
replace (f t) with (f a + (f t - f a)) by ring.
apply Rle_trans with (1 := Rabs_triang _ _).
apply Rplus_le_compat;[apply Rle_refl | ].
apply Rlt_le, (Pd2 t).
change (Rabs (t - a) < delta2); rewrite -> Rabs_right;[ | intuition fourier].
apply Rle_lt_trans with (x - a);[intuition fourier | ].
now rewrite <- (Rabs_right (x - a));[tauto | intuition fourier].
replace (pos (pos_div_2 eps)) with (ep2 * M).
rewrite <- (Rabs_right (x - a));[|intuition fourier].
apply Rmult_lt_compat_r;[unfold M | tauto].
now assert (t := Rabs_pos (f a)); fourier.
simpl; field; unfold M; apply Rgt_not_eq; assert (t := Rabs_pos (f a)).
now fourier.
replace (pos eps) with (pos_div_2 eps + pos_div_2 eps) by (simpl; field).
apply ball_triangle with (RInt f a y); cycle 1.
change (Rabs (RInt f x y - RInt f a y) < pos_div_2 eps).
replace (RInt f a y) with (RInt f a x + RInt f x y); cycle 1.
apply (RInt_Chasles f).
now apply exrint_close; tauto.
apply (ex_RInt_Chasles_2 f a).
split;[apply Rlt_le; tauto | apply Rlt_le, Rlt_trans with m; try tauto].
now destruct (cmp a y); tauto.
now exists fay.
match goal with |- Rabs ?v < _ => replace v with (-RInt f a x) by ring end.
now rewrite -> Rabs_Ropp.
now rewrite -> (is_RInt_unique f a y fay).
Qed.
Lemma is_RInt_gen_at_point_at_left (f : R -> R) (a : R) F {FF : ProperFilter F}
v : locally a (continuous f) -> is_RInt_gen f F (at_point a) v ->
filter_Rlt F (at_point a) -> is_RInt_gen f F (at_left a) v.
Proof.
intros [delta1 pd1] intf [m [P Q FP FQ cmp]]; simpl in cmp.
destruct (pd1 a (ball_center a delta1)
(ball (f a) (mkposreal _ Rlt_0_1)) (locally_ball _ _)) as
[delta2 Pd2].
assert (qa : Q a) by (apply FQ; intros; apply ball_center).
assert (intf2 := intf).
intros P2 PP2; specialize (intf P2 PP2); destruct PP2 as [eps P2eps].
set (M := Rabs (f a) + 1).
assert (M0 : 0 < eps / M).
apply Rmult_lt_0_compat;[apply cond_pos | apply Rinv_0_lt_compat].
now assert (0 <= Rabs (f a)) by apply Rabs_pos; unfold M; fourier.
assert (close : forall y, y <> a -> ball a delta2 y -> Rabs (f y) < M).
intros y ay b_y; unfold M.
replace (f y) with (f a + (f y - f a)) by ring.
apply Rle_lt_trans with (1 := Rabs_triang _ _).
now apply Rplus_lt_compat_l, Pd2; auto.
assert (exrint_close : forall a', ball a delta1 a' -> ex_RInt f a' a).
intros a' baa'.
apply (ex_RInt_continuous f); intros z pz; apply pd1.
destruct (Rle_dec a a') as [aa' | a'a].
rewrite -> Rmin_right, Rmax_left in pz; auto.
change (Rabs (z - a) < delta1).
rewrite -> Rabs_right; cycle 1.
destruct pz; fourier.
destruct pz; apply Rle_lt_trans with (a' - a); try fourier.
rewrite <- (Rabs_right (a' - a)); try fourier.
tauto.
change (Rabs (z - a) < delta1).
destruct (Rle_dec a z) as [az | za].
apply Rnot_le_lt in a'a.
rewrite -> Rmin_left, Rmax_right in pz; try (destruct pz; fourier).
assert (za' : z = a).
now apply Rle_antisym; (destruct pz; fourier).
now rewrite -> za', Rminus_eq_0, Rabs_R0; case delta1; tauto.
apply Rnot_le_lt in a'a; apply Rnot_le_lt in za.
rewrite -> Rmin_left, Rmax_right in pz; try fourier.
rewrite -> Rabs_left;[ | fourier].
apply Rle_lt_trans with (a - a'); try (intuition fourier).
rewrite <- (Rabs_right (a - a')); try (intuition fourier).
now change (ball a' delta1 a); apply ball_sym; tauto.
assert (pre_ep2 : 0 < eps / 2 * /M).
repeat apply Rmult_lt_0_compat; try fourier;[destruct eps; tauto | ].
now apply Rinv_0_lt_compat; unfold M; assert (t := Rabs_pos (f a)); fourier.
set (ep2 := mkposreal _ pre_ep2).
assert (at_left a (fun x => ball a delta1 x /\ ball a ep2 x /\
ball a delta2 x /\ m < x /\ x < a)).
repeat apply filter_and; try (now apply filter_le_within, locally_ball).
destruct (filter_ex _ FP) as [y' Py'].
assert (ma0 : 0 < a - m).
now destruct (cmp y' a); auto; fourier.
exists (mkposreal _ ma0); simpl; intros y.
now rewrite ball_Rabs; intros bay ay; rewrite Rabs_left in bay; fourier.
now exists ep2; intros; tauto.
specialize (intf2 _ (locally_ball v (pos_div_2 eps))).
destruct intf2 as [Pl Ql FPl FQl closerint].
assert (pla : Ql a) by (apply FQl; intros; apply ball_center).
assert (F (fun y => P y /\ Pl y)) by (apply filter_and; auto).
exists (fun y => P y /\ Pl y)
(fun x => ball a delta1 x /\ ball a ep2 x /\
ball a delta2 x /\ m < x /\ x < a); auto.
intros x y bx Ry; exists (RInt f x y).
destruct (closerint x a) as [fxa [close_fxa]]; try tauto.
split.
simpl. apply (RInt_correct f x y).
apply (ex_RInt_Chasles_1 f _ _ a);[ | exists fxa; tauto].
split; apply Rlt_le;
[apply Rlt_trans with m; assert (t := cmp x a (proj1 bx) qa) |]; tauto.
apply P2eps.
assert (Rabs (RInt f y a) < pos_div_2 eps).
apply Rle_lt_trans with ((a - y) * M).
apply abs_RInt_le_const;[apply Rlt_le; tauto | | ].
now apply exrint_close; tauto.
intros t yta.
replace (f t) with (f a + (f t - f a)) by ring.
apply Rle_trans with (1 := Rabs_triang _ _).
apply Rplus_le_compat;[apply Rle_refl | ].
apply Rlt_le, (Pd2 t).
change (Rabs (t - a) < delta2); rewrite -> Rabs_left1;[ |intuition fourier].
apply Rle_lt_trans with (a - y);[intuition fourier | ].
rewrite <- (Rabs_right (a - y));[ | intuition fourier].
now rewrite <- Rabs_Ropp, Ropp_minus_distr; tauto.
replace (pos (pos_div_2 eps)) with (ep2 * M).
rewrite <- (Rabs_right (a - y));[|intuition fourier].
apply Rmult_lt_compat_r;[unfold M |].
now assert (t := Rabs_pos (f a)); fourier.
now rewrite <- Rabs_Ropp, Ropp_minus_distr; tauto.
simpl; field; unfold M; apply Rgt_not_eq; assert (t := Rabs_pos (f a)).
now fourier.
replace (pos eps) with (pos_div_2 eps + pos_div_2 eps) by (simpl; field).
apply ball_triangle with (RInt f x a); cycle 1.
change (Rabs (RInt f x y - RInt f x a) < pos_div_2 eps).
replace (RInt f x a) with (RInt f x y + RInt f y a); cycle 1.
apply (RInt_Chasles f).
apply (ex_RInt_Chasles_1 f _ _ a).
split;[ apply Rlt_le, Rlt_trans with m; try tauto| apply Rlt_le; tauto].
now destruct (cmp x a); tauto.
now exists fxa.
now apply exrint_close; tauto.
match goal with |- Rabs ?v < _ => replace v with (-RInt f y a) by ring end.
now rewrite -> Rabs_Ropp.
now rewrite -> (is_RInt_unique f x a fxa).
Qed.
Lemma ex_RInt_gen_cut (a : R) (F G: (R -> Prop) -> Prop)
{FF : ProperFilter F} {FG : ProperFilter G} (f : R -> R) :
filter_Rlt F (at_point a) -> filter_Rlt (at_point a) G ->
ex_RInt_gen f F G -> ex_RInt_gen f (at_point a) G.
Proof.
intros lFa laG [vfg Pvfg].
assert (lFG := filter_Rlt_trans _ _ _ lFa laG).
set (v := R_complete_lim (filtermap (fun x => RInt f a x) G)).
exists v; intros P PP2.
destruct laG as [m [S1 S2 p1 p2 laG]]; cbn in laG.
destruct lFa as [m' [S5 S6 p5 p6 lFa]]; cbn in lFa.
assert (S6 a) by apply p6.
assert (S1 a) by apply p1.
assert (t': forall eps : posreal, exists x,
filtermap (fun x => RInt f a x) G (ball x eps)).
intros eps.
specialize (Pvfg (ball vfg (pos_div_2 eps)) (locally_ball _ _)).
destruct Pvfg as [S7 S8 p7 p8 vfg'].
destruct (filter_ex (F := G)
(fun y => S8 y /\ S2 y)) as [y Py].
repeat apply filter_and; tauto.
exists (RInt f a y); destruct (filter_ex (F := F)
(fun x => S7 x /\ S5 x)) as [x Px].
repeat apply filter_and; tauto.
unfold filtermap; apply (filter_imp (fun y => S8 y /\ S2 y)).
intros z PZ; change (Rabs (RInt f a z - RInt f a y) < eps).
replace (RInt f a z - RInt f a y) with
((RInt f x a + RInt f a z) - (RInt f x a + RInt f a y)) by ring.
destruct (vfg' x y) as [xy pxy]; try tauto.
destruct (vfg' x z) as [xz pxz]; try tauto.
assert (ex_RInt f x y) by (exists xy; tauto).
assert (ex_RInt f x z) by (exists xz; tauto).
assert (x < a) by (destruct (lFa x a); intuition fourier || tauto).
assert (a < y) by (destruct (laG a y); intuition fourier || tauto).
assert (a < z) by (destruct (laG a z); intuition fourier || tauto).
assert (ex_RInt f x a).
apply (ex_RInt_Chasles_1 f x a y);[intuition fourier | assumption].
rewrite -> !(RInt_Chasles f); auto;
try (apply (ex_RInt_Chasles_2 f x); auto; intuition fourier); cycle 1.
change (ball (RInt f x y) eps (RInt f x z)).
replace (pos eps) with (pos_div_2 eps + pos_div_2 eps) by (simpl; field).
replace (RInt f x y) with xy by (symmetry; apply is_RInt_unique; tauto).
replace (RInt f x z) with xz by (symmetry; apply is_RInt_unique; tauto).
now apply (ball_triangle _ vfg); [apply ball_sym | ]; tauto.
now repeat apply filter_and; tauto.
destruct PP2 as [eps Peps].
assert (t := (R_complete
(filtermap (fun x => RInt f a x) G) _
t' eps)).
unfold filtermap, filtermapi in t |- *.
assert (atpa : at_point a (eq a)) by reflexivity.
enough (H1 : exists S4, G S4 /\ forall x, S4 x -> is_RInt f a x (RInt f a x)).
destruct H1 as [S4 [gs4 Ps4]].
apply (Filter_prod (at_point a) G _ (eq a)
(fun x => ball
(R_complete_lim
(fun P : R -> Prop => G (fun x0 => P (RInt f a x0)))) eps
(RInt f a x) /\ S4 x) atpa (filter_and _ _ t gs4)).
intros x y <- dist.
now exists (RInt f a y);split;[apply Ps4; tauto| apply Peps; tauto].
destruct (Pvfg (ball vfg (mkposreal _ Rlt_0_1))) as [S3 S4 fs3 gs4 Ps4].
now apply locally_ball.
assert (F (Rgt a)).
apply (filter_imp S5); [intros x s5x | auto].
assert (s6a : S6 a) by apply p6.
destruct (lFa x a s5x s6a); fourier.
destruct (filter_ex (F := F) (fun x => a > x /\ S3 x)) as [w Pw];
[apply filter_and; auto | ].
exists (fun x => S4 x /\ a < x); split;[ | intros x px; apply (RInt_correct f)].
apply filter_and;[assumption | apply (filter_imp S2);[intros x s2x | easy]].
assert (s1a : S1 a) by apply p1.
destruct (laG a x s1a s2x); fourier.
apply ex_RInt_Chasles_2 with w;[split; apply Rlt_le; tauto | ].
destruct (Ps4 w x) as [wx [Pwx closewx]]; try tauto; exists wx; tauto.
Qed.
Require Import Reals Coquelicot.Coquelicot Fourier.
Lemma ball_Rabs x y e : ball x e y <-> Rabs (y - x) < e.
Proof. intros; tauto. Qed.
Definition filter_Rlt F1 F2 :=
exists m, filter_prod F1 F2 (fun p => fst p < m < snd p).
Lemma filter_Rlt_witness m (F1 F2 : (R -> Prop) -> Prop) :
F1 (Rgt m) -> F2 (Rlt m) -> filter_Rlt F1 F2.
Proof.
exists m; split with (Rgt m) (Rlt m); simpl; auto with real.
Qed.
Lemma filter_Rlt_m_infty_p_infty :
filter_Rlt (Rbar_locally m_infty) (Rbar_locally p_infty).
Proof.
apply (filter_Rlt_witness 0); exists 0; tauto.
Qed.
Lemma filter_Rlt_m_infty_at_left b :
filter_Rlt (Rbar_locally m_infty) (at_left b).
Proof.
apply (filter_Rlt_witness (b - 1)).
now exists (b - 1); intros x cmpx; apply Rlt_gt.
exists pos_half; intros x yb _.
enough (b - x < 1) by fourier.
apply Rle_lt_trans with (abs (minus b x)).
now apply Rle_abs.
apply ball_sym in yb; apply AbsRing_norm_compat2 in yb.
apply Rlt_trans with (1 := yb).
rewrite Rmult_1_l; simpl.
fourier.
Qed.
Lemma filter_Rlt_at_right_p_infty b :
filter_Rlt (at_right b) (Rbar_locally p_infty).
Proof.
apply (filter_Rlt_witness (b + 1)).
exists pos_half; intros y yb _.
enough (y - b < 1) by fourier.
apply Rle_lt_trans with (abs (minus y b)).
now apply Rle_abs.
apply AbsRing_norm_compat2 in yb.
apply Rlt_trans with (1 := yb).
rewrite Rmult_1_l; simpl.
fourier.
now exists (b + 1); intros x cmpx.
Qed.
Lemma filter_Rlt_at_point_p_infty b :
filter_Rlt (at_point b) (Rbar_locally p_infty).
Proof.
apply (filter_Rlt_witness (b + 1)).
now unfold at_point; fourier.
now exists (b + 1); tauto.
Qed.
Lemma filter_Rlt_m_infty_at_point b :
filter_Rlt (Rbar_locally m_infty) (at_point b).
Proof.
apply (filter_Rlt_witness (b - 1)).
now exists (b - 1); tauto.
now unfold at_point; fourier.
Qed.
Local Lemma compare_half_sum a b (altb : a < b) : a < (a + b) / 2 < b.
Proof.
assert ((a + b) / 2 * 2 = a + b) by field.
split; apply Rmult_lt_reg_r with 2; fourier.
Qed.
Lemma filter_Rlt_at_point a b : a < b ->
filter_Rlt (at_point a) (at_point b).
Proof.
intros altb; apply filter_Rlt_witness with ((a + b) / 2).
unfold at_point.
now destruct (compare_half_sum _ _ altb); tauto.
unfold at_point.
now destruct (compare_half_sum _ _ altb); tauto.
Qed.
Lemma Rplus_minus_cancel1 : forall a b, a + b - a = b.
Proof. intros; ring. Qed.
Lemma filter_Rlt_locally a b : a < b ->
filter_Rlt (Rbar_locally a) (Rbar_locally b).
Proof.
intros ab.
assert (bmap: 0 < (b - a)/2).
apply Rmult_lt_reg_r with 2;[fourier | ].
unfold Rdiv; rewrite -> Rmult_0_l, Rmult_assoc.
rewrite -> Rinv_l, Rmult_1_r;[ | apply Rgt_not_eq]; fourier.
apply (filter_Rlt_witness ((a + b)/2)).
exists (mkposreal _ bmap); intros y ya.
enough (yma : y * 2 - a * 2 < b - a).
apply Rmult_lt_reg_r with 2;[fourier | ].
unfold Rdiv; rewrite -> Rmult_assoc, Rinv_l;[ | apply Rgt_not_eq; fourier].
rewrite -> Rmult_1_r; fourier.
rewrite <- Rmult_minus_distr_r; apply Rmult_lt_reg_r with (/2).
apply Rinv_0_lt_compat; fourier.
rewrite -> Rmult_assoc, Rinv_r, Rmult_1_r;[|apply Rgt_not_eq; fourier].
apply Rle_lt_trans with (abs (minus y a)).
now apply Rle_abs.
apply AbsRing_norm_compat2 in ya; apply Rlt_le_trans with (1 := ya).
now rewrite -> Rmult_1_l; simpl; auto with real.
exists (mkposreal _ bmap); intros y yb.
enough (yma : b * 2 - y * 2 < b - a).
apply Rmult_lt_reg_r with 2;[fourier | ].
unfold Rdiv; rewrite -> Rmult_assoc, Rinv_l;[ | apply Rgt_not_eq; fourier].
rewrite -> Rmult_1_r; fourier.
rewrite <- Rmult_minus_distr_r; apply Rmult_lt_reg_r with (/2).
apply Rinv_0_lt_compat; fourier.
rewrite -> Rmult_assoc, Rinv_r, Rmult_1_r;[|apply Rgt_not_eq; fourier].
apply Rle_lt_trans with (abs (minus b y)).
now apply Rle_abs.
apply ball_sym in yb; apply AbsRing_norm_compat2 in yb.
apply Rlt_le_trans with (1 := yb).
now rewrite -> Rmult_1_l; simpl; auto with real.
Qed.
Lemma filter_Rlt_left_right a b : a <= b ->
filter_Rlt (at_left a) (at_right b).
intros ab; apply (filter_Rlt_witness a).
now exists pos_half; intros y _; apply Rgt_lt.
now exists pos_half; intros y _ yb ; apply Rle_lt_trans with b.
Qed.
Lemma filter_Rlt_trans a F G {FF : Filter F} {GG : Filter G} :
filter_Rlt F (at_point a) ->
filter_Rlt (at_point a) G -> filter_Rlt F G.
Proof.
intros [m1 Pm1] [m2 Pm2].
apply filter_Rlt_witness with a.
destruct Pm1 as [P Q FP atQ cnd1].
assert (qa : Q a) by now apply atQ; intros; apply ball_center.
apply (filter_imp P); auto.
intros x px.
assert (t := cnd1 x a px qa); simpl in t; destruct t; fourier.
destruct Pm2 as [P Q atP GQ cnd2].
assert (pa : P a) by now apply atP; intros; apply ball_center.
apply (filter_imp Q); auto.
intros x qx.
assert (t := cnd2 a x pa qx); simpl in t; destruct t; fourier.
Qed.
Lemma filter_Rlt_right_left a b : a < b ->
filter_Rlt (at_right a) (at_left b).
Proof.
intros ab.
assert (bmap: 0 < (b - a)/2).
apply Rmult_lt_reg_r with 2;[fourier | ].
unfold Rdiv; rewrite -> Rmult_0_l, Rmult_assoc.
rewrite -> Rinv_l, Rmult_1_r;[ | apply Rgt_not_eq]; fourier.
apply (filter_Rlt_witness ((a + b)/2)).
exists (mkposreal _ bmap); intros y ya cmp.
enough (yma : y * 2 - a * 2 < b - a).
apply Rmult_lt_reg_r with 2;[fourier | ].
unfold Rdiv; rewrite -> Rmult_assoc, Rinv_l;[ | apply Rgt_not_eq; fourier].
rewrite -> Rmult_1_r; fourier.
rewrite <- Rmult_minus_distr_r; apply Rmult_lt_reg_r with (/2).
apply Rinv_0_lt_compat; fourier.
rewrite -> Rmult_assoc, Rinv_r, Rmult_1_r;[|apply Rgt_not_eq; fourier].
apply Rle_lt_trans with (abs (minus y a)).
now apply Rle_abs.
apply AbsRing_norm_compat2 in ya; apply Rlt_le_trans with (1 := ya).
now rewrite -> Rmult_1_l; simpl; auto with real.
exists (mkposreal _ bmap); intros y yb cmp.
enough (yma : b * 2 - y * 2 < b - a).
apply Rmult_lt_reg_r with 2;[fourier | ].
unfold Rdiv; rewrite -> Rmult_assoc, Rinv_l;[ | apply Rgt_not_eq; fourier].
rewrite -> Rmult_1_r; fourier.
rewrite <- Rmult_minus_distr_r; apply Rmult_lt_reg_r with (/2).
apply Rinv_0_lt_compat; fourier.
rewrite -> Rmult_assoc, Rinv_r, Rmult_1_r;[|apply Rgt_not_eq; fourier].
apply Rle_lt_trans with (abs (minus b y)).
now apply Rle_abs.
apply ball_sym in yb; apply AbsRing_norm_compat2 in yb.
apply Rlt_le_trans with (1 := yb).
now rewrite -> Rmult_1_l; simpl; auto with real.
Qed.
Local Ltac chain_comparisons :=
match goal with
| h : ?a <= _ |- ?a < _ => apply Rle_lt_trans with (1 := h)
| h : _ <= ?a |- _ < ?a => apply Rlt_le_trans with (2 := h)
| h : ?a < _ |- ?a < _ => apply Rlt_trans with (1 := h)
| h : _ < ?a |- _ < ?a => apply Rlt_trans with (2 := h)
end.
Lemma ex_RInt_gen_bound (g : R -> R) (f : R -> R) F G
{PF : ProperFilter F} {PG : ProperFilter G} :
filter_Rlt F G ->
ex_RInt_gen g F G ->
filter_prod F G
(fun p => (forall x, fst p < x < snd p -> 0 <= f x <= g x) /\
ex_RInt f (fst p) (snd p)) ->
ex_RInt_gen f F G.
Proof.
intros [m mmid] [gl intg] cmp.
assert (F (Rgt m)).
destruct mmid as [pf pg fpf gpg cmp'].
apply (filter_imp pf); destruct (filter_ex pg) as [y py]; auto.
intros x px; destruct (cmp' x y px py) as [it _]; exact it.
assert (G (Rlt m)).
destruct mmid as [pf pg fpf gpg cmp'].
apply (filter_imp pg); destruct (filter_ex (F := F) pf) as [x px]; auto.
intros y py; destruct (cmp' x y px py) as [_ it]; exact it.
exists (lim (filtermap (fun p => RInt f (fst p) (snd p)) (filter_prod F G))).
destruct cmp as [Q1 R1 fq1 gr1 cmp]; simpl in cmp.
assert (cc : cauchy (filtermap (fun p => RInt f (fst p) (snd p))
(filter_prod F G))).
intros eps.
destruct (intg _ (locally_ball gl (pos_div_2 eps))) as [Qg Rg FQg GRg main].
assert (fq : F (fun x => Q1 x /\ Qg x /\ m > x))
by now repeat apply filter_and.
assert (gr : G (fun x => R1 x /\ Rg x /\ m < x))
by now repeat apply filter_and.
destruct (filter_ex _ fq) as [x qx], (filter_ex _ gr) as [y ry].
exists (RInt f x y).
exists (fun x => Q1 x /\ Qg x /\ m > x)
(fun y => R1 y /\ Rg y /\ m < y);
try now repeat apply filter_and.
intros u v Qu Rv.
assert (wlog_cc : forall a b c d,
Q1 a /\ Qg a ->
Q1 b /\ Qg b ->
R1 c /\ Rg c ->
R1 d /\ Rg d ->
a <= b -> c <=d -> b < m -> m < c ->
(ball (RInt f a d) eps (RInt f b c) /\
ball (RInt f a c) eps (RInt f b d))).
clear x y qx ry u v Qu Rv; intros a b c d Qa Qb Rc Rd ab cd bm mc.
assert (ex_RInt f a c /\ ex_RInt f b c /\ ex_RInt f b d).
now repeat apply conj; apply cmp.
move main after mc.
destruct (main a c) as [gac [acP acQ]]; try tauto; simpl in acP.
assert (ex_RInt g a c) by (eapply ex_intro; eauto).
destruct (main b c) as [gbc [bcP bcQ]]; try tauto; simpl in bcP.
assert (ex_RInt g b c) by (eapply ex_intro; eauto).
destruct (main b d) as [gbd [bdP bdQ]]; try tauto; simpl in bdP.
assert (ex_RInt g b d) by (eapply ex_intro; eauto).
assert (ex_RInt f a b).
now apply ex_RInt_Chasles with c;[ | apply ex_RInt_swap].
assert (ex_RInt f c d).
now apply ex_RInt_Chasles with b;[apply ex_RInt_swap | ].
assert (ex_RInt g a b).
now apply ex_RInt_Chasles with c;[ | apply ex_RInt_swap];
eapply ex_intro; eauto.
assert (ex_RInt g c d).
now apply ex_RInt_Chasles with b;[apply ex_RInt_swap | ];
eapply ex_intro; eauto.
assert (bc : b < c) by (apply Rlt_trans with m; tauto).
split.
apply ball_sym, Rle_lt_trans with (Rabs (RInt g a d - RInt g b c)).
rewrite <- (RInt_Chasles f a b d), <- (RInt_Chasles f b c d),
<- (RInt_Chasles g a b d), <- (RInt_Chasles g b c d),
!(Rplus_comm (RInt _ a b)), !Rplus_assoc, !Rplus_minus_cancel1;
try tauto.
unfold abs; simpl; rewrite -> !Rabs_right;
try (apply Rle_ge, Rplus_le_le_0_compat; apply RInt_ge_0; auto);
try (intros x [x1 x2]; enough (0 <= f x <= g x)
by (solve[tauto | apply Rle_trans with (f x); tauto]);
apply (cmp a d); try tauto; split;
solve[repeat (auto; chain_comparisons)]).
apply Rplus_le_compat; apply RInt_le; try tauto;
try (intros x [x1 x2]; enough (0 <= f x <= g x)
by (solve[tauto | apply Rle_trans with (f x); tauto]);
apply (cmp a d); try tauto; split;
solve[repeat (auto; chain_comparisons)]).
change (ball (RInt g b c) eps (RInt g a d)).
replace (pos eps) with (pos_div_2 eps + pos_div_2 eps) by (simpl; field).
apply ball_triangle with gl.
now rewrite -> (is_RInt_unique _ _ _ _ bcP); apply ball_sym.
destruct (main a d) as [gad [adP adQ]]; try tauto; simpl in adP.
now rewrite -> (is_RInt_unique _ _ _ _ adP).
change (Rabs (RInt f b d + - RInt f a c) < eps).
rewrite <- (RInt_Chasles f b c d), <- (RInt_Chasles f a b c),
Ropp_plus_distr, !Rplus_assoc, (Rplus_comm (RInt f b c)), !Rplus_assoc,
Rplus_opp_l, Rplus_0_r; try tauto.
apply Rle_lt_trans with (1 := Rabs_triang _ _);
rewrite -> Rabs_Ropp, !Rabs_right;
try (apply Rle_ge, RInt_ge_0; try tauto);
try (intros x [x1 x2]; enough (0 <= f x <= g x)
by (solve[tauto | apply Rle_trans with (f x); tauto]);
apply (cmp a d); try tauto; split;
solve[repeat (auto; chain_comparisons)]).
replace (pos eps) with (pos_div_2 eps + pos_div_2 eps)
by (simpl; field).
assert (dc : RInt f c d <= RInt g c d /\ RInt f a b <= RInt g a b).
split; apply RInt_le; try tauto;
try (intros x [x1 x2]; enough (0 <= f x <= g x)
by (solve[tauto | apply Rle_trans with (f x); tauto]);
apply (cmp a d); try tauto; split;
solve[repeat (auto; chain_comparisons)]).
apply Rle_lt_trans with (1 := Rplus_le_compat _ _ _ _ (proj1 dc)(proj2 dc)).
apply Rle_lt_trans with (1 := Rle_abs _).
replace (RInt _ _ _ + _) with
((RInt g a d - gl) - (RInt g b c - gl)) by
(rewrite <- (RInt_Chasles g a b d), <- (RInt_Chasles g b c d);
try tauto; set (zoo := plus); change zoo with Rplus; ring).
apply Rle_lt_trans with (1 := Rabs_triang _ _), Rplus_lt_compat.
destruct (main a d) as [gad [adP adQ]]; try tauto; simpl in adP.
now rewrite -> (is_RInt_unique _ _ _ _ adP).
now rewrite -> Rabs_Ropp; rewrite -> (is_RInt_unique _ _ _ _ bcP).
destruct (Rlt_dec x u), (Rlt_dec v y);
[apply (wlog_cc x u v y) | apply (wlog_cc x u y v) |
apply ball_sym, (wlog_cc u x v y) | apply ball_sym, (wlog_cc u x y v)];
try split;
try solve[tauto | apply Rlt_le; tauto |
apply Rge_le; tauto | apply Rle_ge; tauto|
apply Rnot_lt_le; tauto].
intros P [eps Peps].
move cc after Peps.
unfold filtermapi.
assert (tmp := complete_cauchy _ _ cc eps).
destruct tmp as [Q2 R2 Q2P R2P PP2].
exists (fun x => Q2 x /\ Q1 x) (fun x => R2 x /\ R1 x);
try (apply filter_and; auto).
intros x y [Q2x Q1x] [R2x R1x].
destruct (cmp x y Q1x R1x) as [cmp' [fxy intxy]].
exists fxy; split;[assumption | apply Peps].
rewrite <- (is_RInt_unique _ _ _ _ intxy); apply PP2; auto.
Qed.
Lemma is_RInt_gen_Rle (g : R -> R) gl (f : R -> R) fl F G
{PF : ProperFilter F} {PG : ProperFilter G} :
filter_Rlt F G ->
is_RInt_gen g F G gl ->
is_RInt_gen f F G fl ->
filter_prod F G
(fun p => (forall x, fst p < x < snd p -> f x <= g x)) ->
fl <= gl.
Proof.
intros [m mmid] intg intf cmp.
apply (filterlim_le (F := filter_prod F G) (fun p => RInt f (fst p) (snd p))
(fun p => RInt g (fst p) (snd p)) fl gl).
specialize (intf _ (locally_ball fl (mkposreal _ Rlt_0_1))).
specialize (intg _ (locally_ball gl (mkposreal _ Rlt_0_1))).
unfold filtermapi in intg, intf.
apply: filter_imp (filter_and _ _ (filter_and _ _ intg intf)
(filter_and _ _ mmid cmp)).
intros [a b]; simpl; intros [[[Ig [Hg1 Hg2]] [If [Hf1 Hf2]]] [cmp']].
apply RInt_le;
[apply Rle_trans with m;apply Rlt_le | exists If| exists Ig| ]; tauto.
intros P HP; specialize (intf P HP); unfold filtermapi, filtermap in intf |- *.
apply: filter_imp intf.
intros [a b]; simpl; intros [y [inty Py]].
now rewrite -> (is_RInt_unique _ _ _ _ inty).
intros P HP; specialize (intg P HP); unfold filtermapi, filtermap in intg |- *.
apply: filter_imp intg.
intros [a b]; simpl; intros [y [inty Py]].
now rewrite -> (is_RInt_unique _ _ _ _ inty).
Qed.
Lemma is_RInt_gen_at_point_at_right (f : R -> R) (a : R) F {FF : ProperFilter F}
v : locally a (continuous f) -> is_RInt_gen f (at_point a) F v ->
filter_Rlt (at_point a) F -> is_RInt_gen f (at_right a) F v.
Proof.
intros [delta1 pd1] intf [m [P Q FP FQ cmp]]; simpl in cmp.
destruct (pd1 a (ball_center a delta1)
(ball (f a) (mkposreal _ Rlt_0_1)) (locally_ball _ _)) as
[delta2 Pd2].
assert (pa : P a) by (apply FP; intros; apply ball_center).
assert (intf2 := intf).
intros P2 PP2; specialize (intf P2 PP2); destruct PP2 as [eps P2eps].
set (M := Rabs (f a) + 1).
assert (M0 : 0 < eps / M).
apply Rmult_lt_0_compat;[apply cond_pos | apply Rinv_0_lt_compat].
now assert (0 <= Rabs (f a)) by apply Rabs_pos; unfold M; fourier.
assert (close : forall y, y <> a -> ball a delta2 y -> Rabs (f y) < M).
intros y ay b_y; unfold M.
replace (f y) with (f a + (f y - f a)) by ring.
apply Rle_lt_trans with (1 := Rabs_triang _ _).
now apply Rplus_lt_compat_l, Pd2; auto.
assert (exrint_close : forall a', ball a delta1 a' -> ex_RInt f a a').
intros a' baa'.
apply (ex_RInt_continuous f); intros z pz; apply pd1.
destruct (Rle_dec a a') as [aa' | a'a].
rewrite -> Rmin_left, Rmax_right in pz; auto.
change (Rabs (z - a) < delta1).
rewrite -> Rabs_right; cycle 1.
destruct pz; fourier.
destruct pz; apply Rle_lt_trans with (a' - a); try fourier.
rewrite <- (Rabs_right (a' - a)); try fourier.
tauto.
change (Rabs (z - a) < delta1).
destruct (Rle_dec a z) as [az | za].
apply Rnot_le_lt in a'a.
rewrite -> Rmin_right, Rmax_left in pz; try (destruct pz; fourier).
assert (za' : z = a).
now apply Rle_antisym; (destruct pz; fourier).
now rewrite -> za', Rminus_eq_0, Rabs_R0; case delta1; tauto.
apply Rnot_le_lt in a'a; apply Rnot_le_lt in za.
rewrite -> Rmin_right, Rmax_left in pz; try fourier.
rewrite -> Rabs_left;[ | fourier].
apply Rle_lt_trans with (a - a'); try (intuition fourier).
rewrite <- (Rabs_right (a - a')); try (intuition fourier).
now change (ball a' delta1 a); apply ball_sym; tauto.
assert (pre_ep2 : 0 < eps / 2 * /M).
repeat apply Rmult_lt_0_compat; try fourier;[destruct eps; tauto | ].
now apply Rinv_0_lt_compat; unfold M; assert (t := Rabs_pos (f a)); fourier.
set (ep2 := mkposreal _ pre_ep2).
assert (at_right a (fun x => ball a delta1 x /\ ball a ep2 x /\
ball a delta2 x /\ a < x /\ x < m)).
repeat apply filter_and; try (now apply filter_le_within, locally_ball).
now exists ep2; intros; tauto.
destruct (filter_ex _ FQ) as [y' Py'].
assert (ma0 : 0 < m - a).
now destruct (cmp a y'); auto; fourier.
exists (mkposreal _ ma0); simpl; intros y.
intros bay ay; change (Rabs (y - a) < m - a) in bay.
now rewrite -> Rabs_right in bay; fourier.
specialize (intf2 _ (locally_ball v (pos_div_2 eps))).
destruct intf2 as [Pl Ql FPl FQl closerint].
assert (pla : Pl a) by (apply FPl; intros; apply ball_center).
assert (F (fun y => Q y /\ Ql y)) by (apply filter_and; auto).
exists (fun x => ball a delta1 x /\ ball a ep2 x /\
ball a delta2 x /\ a < x /\ x < m)
(fun y => Q y /\ Ql y); auto.
intros x y bx Ry; exists (RInt f x y).
destruct (closerint a y) as [fay [close_fay]]; try tauto.
split.
simpl. apply (RInt_correct f x y).
apply (ex_RInt_Chasles_2 f a);[ | exists fay; tauto].
split; apply Rlt_le;
[| apply Rlt_trans with m; assert (t := cmp a y pa (proj1 Ry))]; tauto.
apply P2eps.
assert (Rabs (RInt f a x) < pos_div_2 eps).
apply Rle_lt_trans with ((x - a) * M).
apply abs_RInt_le_const;[apply Rlt_le; tauto | | ].
now apply exrint_close; tauto.
intros t atx.
replace (f t) with (f a + (f t - f a)) by ring.
apply Rle_trans with (1 := Rabs_triang _ _).
apply Rplus_le_compat;[apply Rle_refl | ].
apply Rlt_le, (Pd2 t).
change (Rabs (t - a) < delta2); rewrite -> Rabs_right;[ | intuition fourier].
apply Rle_lt_trans with (x - a);[intuition fourier | ].
now rewrite <- (Rabs_right (x - a));[tauto | intuition fourier].
replace (pos (pos_div_2 eps)) with (ep2 * M).
rewrite <- (Rabs_right (x - a));[|intuition fourier].
apply Rmult_lt_compat_r;[unfold M | tauto].
now assert (t := Rabs_pos (f a)); fourier.
simpl; field; unfold M; apply Rgt_not_eq; assert (t := Rabs_pos (f a)).
now fourier.
replace (pos eps) with (pos_div_2 eps + pos_div_2 eps) by (simpl; field).
apply ball_triangle with (RInt f a y); cycle 1.
change (Rabs (RInt f x y - RInt f a y) < pos_div_2 eps).
replace (RInt f a y) with (RInt f a x + RInt f x y); cycle 1.
apply (RInt_Chasles f).
now apply exrint_close; tauto.
apply (ex_RInt_Chasles_2 f a).
split;[apply Rlt_le; tauto | apply Rlt_le, Rlt_trans with m; try tauto].
now destruct (cmp a y); tauto.
now exists fay.
match goal with |- Rabs ?v < _ => replace v with (-RInt f a x) by ring end.
now rewrite -> Rabs_Ropp.
now rewrite -> (is_RInt_unique f a y fay).
Qed.
Lemma is_RInt_gen_at_point_at_left (f : R -> R) (a : R) F {FF : ProperFilter F}
v : locally a (continuous f) -> is_RInt_gen f F (at_point a) v ->
filter_Rlt F (at_point a) -> is_RInt_gen f F (at_left a) v.
Proof.
intros [delta1 pd1] intf [m [P Q FP FQ cmp]]; simpl in cmp.
destruct (pd1 a (ball_center a delta1)
(ball (f a) (mkposreal _ Rlt_0_1)) (locally_ball _ _)) as
[delta2 Pd2].
assert (qa : Q a) by (apply FQ; intros; apply ball_center).
assert (intf2 := intf).
intros P2 PP2; specialize (intf P2 PP2); destruct PP2 as [eps P2eps].
set (M := Rabs (f a) + 1).
assert (M0 : 0 < eps / M).
apply Rmult_lt_0_compat;[apply cond_pos | apply Rinv_0_lt_compat].
now assert (0 <= Rabs (f a)) by apply Rabs_pos; unfold M; fourier.
assert (close : forall y, y <> a -> ball a delta2 y -> Rabs (f y) < M).
intros y ay b_y; unfold M.
replace (f y) with (f a + (f y - f a)) by ring.
apply Rle_lt_trans with (1 := Rabs_triang _ _).
now apply Rplus_lt_compat_l, Pd2; auto.
assert (exrint_close : forall a', ball a delta1 a' -> ex_RInt f a' a).
intros a' baa'.
apply (ex_RInt_continuous f); intros z pz; apply pd1.
destruct (Rle_dec a a') as [aa' | a'a].
rewrite -> Rmin_right, Rmax_left in pz; auto.
change (Rabs (z - a) < delta1).
rewrite -> Rabs_right; cycle 1.
destruct pz; fourier.
destruct pz; apply Rle_lt_trans with (a' - a); try fourier.
rewrite <- (Rabs_right (a' - a)); try fourier.
tauto.
change (Rabs (z - a) < delta1).
destruct (Rle_dec a z) as [az | za].
apply Rnot_le_lt in a'a.
rewrite -> Rmin_left, Rmax_right in pz; try (destruct pz; fourier).
assert (za' : z = a).
now apply Rle_antisym; (destruct pz; fourier).
now rewrite -> za', Rminus_eq_0, Rabs_R0; case delta1; tauto.
apply Rnot_le_lt in a'a; apply Rnot_le_lt in za.
rewrite -> Rmin_left, Rmax_right in pz; try fourier.
rewrite -> Rabs_left;[ | fourier].
apply Rle_lt_trans with (a - a'); try (intuition fourier).
rewrite <- (Rabs_right (a - a')); try (intuition fourier).
now change (ball a' delta1 a); apply ball_sym; tauto.
assert (pre_ep2 : 0 < eps / 2 * /M).
repeat apply Rmult_lt_0_compat; try fourier;[destruct eps; tauto | ].
now apply Rinv_0_lt_compat; unfold M; assert (t := Rabs_pos (f a)); fourier.
set (ep2 := mkposreal _ pre_ep2).
assert (at_left a (fun x => ball a delta1 x /\ ball a ep2 x /\
ball a delta2 x /\ m < x /\ x < a)).
repeat apply filter_and; try (now apply filter_le_within, locally_ball).
destruct (filter_ex _ FP) as [y' Py'].
assert (ma0 : 0 < a - m).
now destruct (cmp y' a); auto; fourier.
exists (mkposreal _ ma0); simpl; intros y.
now rewrite ball_Rabs; intros bay ay; rewrite Rabs_left in bay; fourier.
now exists ep2; intros; tauto.
specialize (intf2 _ (locally_ball v (pos_div_2 eps))).
destruct intf2 as [Pl Ql FPl FQl closerint].
assert (pla : Ql a) by (apply FQl; intros; apply ball_center).
assert (F (fun y => P y /\ Pl y)) by (apply filter_and; auto).
exists (fun y => P y /\ Pl y)
(fun x => ball a delta1 x /\ ball a ep2 x /\
ball a delta2 x /\ m < x /\ x < a); auto.
intros x y bx Ry; exists (RInt f x y).
destruct (closerint x a) as [fxa [close_fxa]]; try tauto.
split.
simpl. apply (RInt_correct f x y).
apply (ex_RInt_Chasles_1 f _ _ a);[ | exists fxa; tauto].
split; apply Rlt_le;
[apply Rlt_trans with m; assert (t := cmp x a (proj1 bx) qa) |]; tauto.
apply P2eps.
assert (Rabs (RInt f y a) < pos_div_2 eps).
apply Rle_lt_trans with ((a - y) * M).
apply abs_RInt_le_const;[apply Rlt_le; tauto | | ].
now apply exrint_close; tauto.
intros t yta.
replace (f t) with (f a + (f t - f a)) by ring.
apply Rle_trans with (1 := Rabs_triang _ _).
apply Rplus_le_compat;[apply Rle_refl | ].
apply Rlt_le, (Pd2 t).
change (Rabs (t - a) < delta2); rewrite -> Rabs_left1;[ |intuition fourier].
apply Rle_lt_trans with (a - y);[intuition fourier | ].
rewrite <- (Rabs_right (a - y));[ | intuition fourier].
now rewrite <- Rabs_Ropp, Ropp_minus_distr; tauto.
replace (pos (pos_div_2 eps)) with (ep2 * M).
rewrite <- (Rabs_right (a - y));[|intuition fourier].
apply Rmult_lt_compat_r;[unfold M |].
now assert (t := Rabs_pos (f a)); fourier.
now rewrite <- Rabs_Ropp, Ropp_minus_distr; tauto.
simpl; field; unfold M; apply Rgt_not_eq; assert (t := Rabs_pos (f a)).
now fourier.
replace (pos eps) with (pos_div_2 eps + pos_div_2 eps) by (simpl; field).
apply ball_triangle with (RInt f x a); cycle 1.
change (Rabs (RInt f x y - RInt f x a) < pos_div_2 eps).
replace (RInt f x a) with (RInt f x y + RInt f y a); cycle 1.
apply (RInt_Chasles f).
apply (ex_RInt_Chasles_1 f _ _ a).
split;[ apply Rlt_le, Rlt_trans with m; try tauto| apply Rlt_le; tauto].
now destruct (cmp x a); tauto.
now exists fxa.
now apply exrint_close; tauto.
match goal with |- Rabs ?v < _ => replace v with (-RInt f y a) by ring end.
now rewrite -> Rabs_Ropp.
now rewrite -> (is_RInt_unique f x a fxa).
Qed.
Lemma ex_RInt_gen_cut (a : R) (F G: (R -> Prop) -> Prop)
{FF : ProperFilter F} {FG : ProperFilter G} (f : R -> R) :
filter_Rlt F (at_point a) -> filter_Rlt (at_point a) G ->
ex_RInt_gen f F G -> ex_RInt_gen f (at_point a) G.
Proof.
intros lFa laG [vfg Pvfg].
assert (lFG := filter_Rlt_trans _ _ _ lFa laG).
set (v := R_complete_lim (filtermap (fun x => RInt f a x) G)).
exists v; intros P PP2.
destruct laG as [m [S1 S2 p1 p2 laG]]; cbn in laG.
destruct lFa as [m' [S5 S6 p5 p6 lFa]]; cbn in lFa.
assert (S6 a) by apply p6.
assert (S1 a) by apply p1.
assert (t': forall eps : posreal, exists x,
filtermap (fun x => RInt f a x) G (ball x eps)).
intros eps.
specialize (Pvfg (ball vfg (pos_div_2 eps)) (locally_ball _ _)).
destruct Pvfg as [S7 S8 p7 p8 vfg'].
destruct (filter_ex (F := G)
(fun y => S8 y /\ S2 y)) as [y Py].
repeat apply filter_and; tauto.
exists (RInt f a y); destruct (filter_ex (F := F)
(fun x => S7 x /\ S5 x)) as [x Px].
repeat apply filter_and; tauto.
unfold filtermap; apply (filter_imp (fun y => S8 y /\ S2 y)).
intros z PZ; change (Rabs (RInt f a z - RInt f a y) < eps).
replace (RInt f a z - RInt f a y) with
((RInt f x a + RInt f a z) - (RInt f x a + RInt f a y)) by ring.
destruct (vfg' x y) as [xy pxy]; try tauto.
destruct (vfg' x z) as [xz pxz]; try tauto.
assert (ex_RInt f x y) by (exists xy; tauto).
assert (ex_RInt f x z) by (exists xz; tauto).
assert (x < a) by (destruct (lFa x a); intuition fourier || tauto).
assert (a < y) by (destruct (laG a y); intuition fourier || tauto).
assert (a < z) by (destruct (laG a z); intuition fourier || tauto).
assert (ex_RInt f x a).
apply (ex_RInt_Chasles_1 f x a y);[intuition fourier | assumption].
rewrite -> !(RInt_Chasles f); auto;
try (apply (ex_RInt_Chasles_2 f x); auto; intuition fourier); cycle 1.
change (ball (RInt f x y) eps (RInt f x z)).
replace (pos eps) with (pos_div_2 eps + pos_div_2 eps) by (simpl; field).
replace (RInt f x y) with xy by (symmetry; apply is_RInt_unique; tauto).
replace (RInt f x z) with xz by (symmetry; apply is_RInt_unique; tauto).
now apply (ball_triangle _ vfg); [apply ball_sym | ]; tauto.
now repeat apply filter_and; tauto.
destruct PP2 as [eps Peps].
assert (t := (R_complete
(filtermap (fun x => RInt f a x) G) _
t' eps)).
unfold filtermap, filtermapi in t |- *.
assert (atpa : at_point a (eq a)) by reflexivity.
enough (H1 : exists S4, G S4 /\ forall x, S4 x -> is_RInt f a x (RInt f a x)).
destruct H1 as [S4 [gs4 Ps4]].
apply (Filter_prod (at_point a) G _ (eq a)
(fun x => ball
(R_complete_lim
(fun P : R -> Prop => G (fun x0 => P (RInt f a x0)))) eps
(RInt f a x) /\ S4 x) atpa (filter_and _ _ t gs4)).
intros x y <- dist.
now exists (RInt f a y);split;[apply Ps4; tauto| apply Peps; tauto].
destruct (Pvfg (ball vfg (mkposreal _ Rlt_0_1))) as [S3 S4 fs3 gs4 Ps4].
now apply locally_ball.
assert (F (Rgt a)).
apply (filter_imp S5); [intros x s5x | auto].
assert (s6a : S6 a) by apply p6.
destruct (lFa x a s5x s6a); fourier.
destruct (filter_ex (F := F) (fun x => a > x /\ S3 x)) as [w Pw];
[apply filter_and; auto | ].
exists (fun x => S4 x /\ a < x); split;[ | intros x px; apply (RInt_correct f)].
apply filter_and;[assumption | apply (filter_imp S2);[intros x s2x | easy]].
assert (s1a : S1 a) by apply p1.
destruct (laG a x s1a s2x); fourier.
apply ex_RInt_Chasles_2 with w;[split; apply Rlt_le; tauto | ].
destruct (Ps4 w x) as [wx [Pwx closewx]]; try tauto; exists wx; tauto.
Qed.