Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

replacing strict inequality by a large one in locally_Rbar #122

Draft
wants to merge 1 commit into
base: master
Choose a base branch
from
Draft

replacing strict inequality by a large one in locally_Rbar #122

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 3 additions & 3 deletions derive.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -162,7 +162,7 @@ move=> /diff_locallyP [dfc]; rewrite -addrA.
rewrite (littleo_bigO_eqo (cst (1 : R^o))); last first.
apply/eqOP; near=> k; rewrite /cst [`|[1 : R^o]|]absr1 mulr1.
near=> y; rewrite ltrW //; near: y; apply/locally_normP.
by exists k; [near: k; exists 0|move=> ? /=; rewrite sub0r normmN].
by exists k => // ? /=; rewrite sub0r normmN.
rewrite addfo; first by move=> /eqolim; rewrite flim_shift add0r.
by apply/eqolim0P; apply: (flim_trans (dfc 0)); rewrite linear0.
Grab Existential Variables. all: end_near. Qed.
Expand Down Expand Up @@ -1297,7 +1297,7 @@ have imf_sup : has_sup imf.
apply/compact_bounded/continuous_compact; last exact: segment_compact.
by move=> ?; rewrite inE => /asboolP /fcont.
exists (M + 1); apply/ubP => y; rewrite !inE => /asboolP /imfltM yltM.
apply/ltrW; apply: ler_lt_trans (yltM _ _); last by rewrite ltr_addl.
apply/ltrW; apply: ler_lt_trans (yltM _ _); last by rewrite ler_addl.
by rewrite [ `|[_]| ]absRE ler_norm.
case: (pselect (exists2 c, c \in `[a, b] & f c = sup imf)) => [|imf_ltsup].
move=> [c cab fceqsup]; exists c => // t tab.
Expand All @@ -1324,7 +1324,7 @@ rewrite ltr_subl_addr - ltr_subl_addl.
suff : sup imf - f t > k^-1 by move=> /ltrW; rewrite lerNgt => /negbTE ->.
rewrite -[X in _ < X]invrK ltr_pinv.
rewrite -div1r; apply: ler_lt_trans (ler_norm _) _; rewrite -absRE.
by apply: imVfltM; [rewrite ltr_maxr ltr_addl ltr01|apply: imageP].
by apply: imVfltM; [rewrite ler_maxr ler_addl ler01|apply: imageP].
by rewrite inE kgt0 unitfE lt0r_neq0.
have invsupft_gt0 : 0 < (sup imf - f t)^-1.
by rewrite invr_gt0 subr_gt0 imf_ltsup.
Expand Down
84 changes: 51 additions & 33 deletions hierarchy.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1198,14 +1198,14 @@ Notation "'-oo'" := m_infty : real_scope.
Definition Rbar_locally' (a : Rbar) (P : R -> Prop) :=
match a with
| Finite a => locally' a P
| +oo => exists M : R, forall x, M < x -> P x
| -oo => exists M : R, forall x, x < M -> P x
| +oo => exists M : R, forall x, M <= x -> P x
| -oo => exists M : R, forall x, x <= M -> P x
end.
Definition Rbar_locally (a : Rbar) (P : R -> Prop) :=
match a with
| Finite a => locally a P
| +oo => exists M : R, forall x, M < x -> P x
| -oo => exists M : R, forall x, x < M -> P x
| +oo => exists M : R, forall x, M <= x -> P x
| -oo => exists M : R, forall x, x <= M -> P x
end.

Canonical Rbar_eqType := EqType Rbar gen_eqMixin.
Expand All @@ -1226,19 +1226,18 @@ Global Instance Rbar_locally'_filter : forall x, ProperFilter (Rbar_locally' x).
Proof.
case=> [x||]; first exact: Rlocally'_proper.
apply Build_ProperFilter.
by move=> P [M gtMP]; exists (M + 1); apply: gtMP; rewrite ltr_addl.
split=> /= [|P Q [MP gtMP] [MQ gtMQ] |P Q sPQ [M gtMP]]; first by exists 0.
by exists (maxr MP MQ) => ?; rewrite ltr_maxl => /andP [/gtMP ? /gtMQ].
by exists M => ? /gtMP /sPQ.
by move=> P [M geMP]; exists M; apply: geMP.
split=> /= [|P Q [MP geMP] [MQ geMQ] |P Q sPQ [M geMP]]; first by exists 0.
by exists (maxr MP MQ) => ?; rewrite ler_maxl => /andP [/geMP ? /geMQ].
by exists M => ? /geMP /sPQ.
apply Build_ProperFilter.
by move=> P [M ltMP]; exists (M - 1); apply: ltMP; rewrite gtr_addl oppr_lt0.
split=> /= [|P Q [MP ltMP] [MQ ltMQ] |P Q sPQ [M ltMP]]; first by exists 0.
by exists (minr MP MQ) => ?; rewrite ltr_minr => /andP [/ltMP ? /ltMQ].
by exists M => ? /ltMP /sPQ.
by move=> P [M leMP]; exists M; apply: leMP.
split=> /= [|P Q [MP leMP] [MQ leMQ] |P Q sPQ [M leMP]]; first by exists 0.
by exists (minr MP MQ) => ?; rewrite ler_minr => /andP [/leMP ? /leMQ].
by exists M => ? /leMP /sPQ.
Qed.
Typeclasses Opaque Rbar_locally'.


Global Instance Rbar_locally_filter : forall x, ProperFilter (Rbar_locally x).
Proof.
case=> [x||].
Expand All @@ -1251,18 +1250,38 @@ Typeclasses Opaque Rbar_locally.
Lemma near_pinfty_div2 (A : set R) :
(\forall k \near +oo, A k) -> (\forall k \near +oo, A (k / 2)).
Proof.
by move=> [M AM]; exists (M * 2) => x; rewrite -ltr_pdivl_mulr //; apply: AM.
by move=> [M AM]; exists (M * 2) => x; rewrite -ler_pdivl_mulr //; apply: AM.
Qed.

Lemma locally_pinfty_ge c : \forall x \near +oo, c <= x.
Proof. by exists c. Qed.

Lemma locally_pinfty_gt c : \forall x \near +oo, c < x.
Proof. by exists (c + 1) => ? /ltr_le_trans; apply; rewrite ltr_addl. Qed.

Hint Extern 0 (is_true (_ <= _)) =>
match goal with _ : ?x \is_near (locally +oo) |- is_true (_ <= ?x) =>
now (near: x; apply: locally_pinfty_ge) end : core.

Hint Extern 0 (is_true (_ < _)) =>
match goal with _ : ?x \is_near (locally +oo) |- is_true (_ < ?x) =>
now (near: x; apply: locally_pinfty_gt) end : core.

Lemma locally_minfty_le c : \forall x \near -oo, x <= c.
Proof. by exists c. Qed.

Lemma locally_pinfty_ge c : \forall x \near +oo, c <= x.
Proof. by exists c; apply: ltrW. Qed.
Lemma locally_minfty_lt c : \forall x \near -oo, x < c.
Proof.
by exists (c - 1) => ? /ler_lt_trans; apply; rewrite ltr_subl_addl ltr_addr.
Qed.

Hint Extern 0 (is_true (0 < _)) => match goal with
H : ?x \is_near (locally +oo) |- _ =>
solve[near: x; exists 0 => _/posnumP[x] //] end : core.
Hint Extern 0 (is_true (_ <= _)) =>
match goal with _ : ?x \is_near (locally +oo) |- is_true (?x <= _) =>
now (near: x; apply: locally_minfty_le) end : core.

Hint Extern 0 (is_true (_ < _)) =>
match goal with _ : ?x \is_near (locally +oo) |- is_true (?x < _) =>
now (near: x; apply: locally_minfty_lt) end : core.

(** ** Modules with a norm *)

Expand Down Expand Up @@ -1616,12 +1635,11 @@ Proof. by move=> /flim_normP. Qed.
Lemma flim_bounded {F : set (set V)} {FF : Filter F} (y : V) :
F --> y -> \forall M \near +oo, \forall y' \near F, `|[y']|%real < M.
Proof.
move=> /flim_norm Fy; exists `|[y]| => M.
rewrite -subr_gt0 => subM_gt0; have := Fy _ subM_gt0.
apply: filterS => y' yy'; rewrite -(@ltr_add2r _ (- `|[y]|)).
rewrite (ler_lt_trans _ yy') //.
by rewrite (ler_trans _ (ler_distm_dist _ _)) // absRE distrC ler_norm.
Qed.
move=> /flim_norm Fy; near=> M; have MP : M - `|[y]| > 0 by rewrite subr_gt0.
near=> y'; rewrite -(@ltr_add2r _ (- `|[y]|)) (@ler_lt_trans _ `|[y - y']|)//.
by rewrite (ler_trans (ler_norm _)) // distrC ler_distm_dist.
by apply: (near (Fy _ _) y').
Grab Existential Variables. all: end_near. Qed.

Lemma flimi_map_lim {F} {FF : ProperFilter F} (f : T -> V -> Prop) (l : V) :
F (fun x : T => is_prop (f x)) ->
Expand Down Expand Up @@ -1819,7 +1837,8 @@ rewrite (@distm_lt_split _ _ (k *: z)) // -?(scalerBr, scalerBl) normmZ.
by apply: flim_norm; rewrite // mulr_gt0 // ?invr_gt0 ltr_paddl.
have zM: `|[z]| < M by near: z; near: M; apply: flim_bounded; apply: flim_refl.
rewrite (ler_lt_trans (ler_pmul _ _ (lerr _) (_ : _ <= M))) // ?ltrW//.
by rewrite -ltr_pdivl_mulr //; near: l; apply: (flim_norm (_ : K^o)).
rewrite -ltr_pdivl_mulr //; near: l.
by apply: (flim_norm (_ : K^o)) => //; rewrite divr_gt0.
Grab Existential Variables. all: end_near. Qed.

Arguments scale_continuous _ _ : clear implicits.
Expand Down Expand Up @@ -2640,7 +2659,7 @@ have /Aco [] := covA.
by rewrite -{1}(subrK p q) ler_normm_add.
move=> D _ DcovA.
exists (bigmaxr 0 [seq n%:~R | n <- enum_fset D]).
move=> x ltmaxx p /DcovA [n Dn /ltr_trans]; apply; apply: ler_lt_trans ltmaxx.
move=> x ltmaxx p /DcovA [n Dn /ltr_le_trans]; apply; apply: ler_trans ltmaxx.
have ltin : (index n (enum_fset D) < size (enum_fset D))%N by rewrite index_mem.
rewrite -(nth_index 0 Dn) -(nth_map _ 0) //; apply: bigmaxr_ler.
by rewrite size_map.
Expand Down Expand Up @@ -2713,7 +2732,7 @@ have Mnco : compact
by move=> _; apply: segment_compact.
apply: subclosed_compact Acl Mnco _ => v /normAltM normvltM i.
suff /ltrW : `|[v ord0 i : R^o]| < M + 1 by rewrite [ `|[_]| ]absRE ler_norml.
apply: ler_lt_trans (normvltM _ _); last by rewrite ltr_addl.
apply: ler_lt_trans (normvltM _ _); last by rewrite ler_addl.
have vinseq : `|v ord0 i| \in [seq `|v ij.1 ij.2| | ij : 'I_1 * 'I_n.+1].
by apply/mapP; exists (ord0, i) => //=; rewrite mem_enum.
rewrite -[X in X <= _](nth_index 0 vinseq); apply: bigmaxr_ler.
Expand Down Expand Up @@ -2741,16 +2760,15 @@ Qed.
Lemma open_Rbar_lt' x y : Rbar_lt x y -> Rbar_locally x (fun u => Rbar_lt u y).
Proof.
case: x => [x|//|] xy; first exact: open_Rbar_lt.
case: y => [y||//] /= in xy *.
exists y => /= x ? //.
case: y => [y||//] in xy *; first exact: locally_minfty_lt.
by exists 0.
Qed.

Lemma open_Rbar_gt' x y : Rbar_lt y x -> Rbar_locally x (fun u => Rbar_lt y u).
Proof.
case: x => [x||] //=; do ?[exact: open_Rbar_gt];
case: y => [y||] //=; do ?by exists 0.
by exists y => x yx //=.
by move=> _; exact: locally_pinfty_gt.
Qed.

Lemma Rbar_locally'_le x : Rbar_locally' x --> Rbar_locally x.
Expand Down Expand Up @@ -2778,13 +2796,13 @@ move=> P; rewrite /Rbar_loc_seq.
case: x => /= [x [_/posnumP[delta] Hp] |[delta Hp] |[delta Hp]]; last 2 first.
have /ZnatP [N Nfloor] : ifloor (maxr delta 0) \is a Znat.
by rewrite Znat_def ifloor_ge0 ler_maxr lerr orbC.
exists N.+1 => // n ltNn; apply: Hp.
exists N.+1 => // n ltNn; apply: Hp; apply: ltrW.
have /ler_lt_trans : delta <= maxr delta 0 by rewrite ler_maxr lerr.
apply; apply: ltr_le_trans (floorS_gtr _) _; rewrite floorE Nfloor.
by rewrite -(@natrD [ringType of R] N 1) INRE ler_nat addn1.
have /ZnatP [N Nfloor] : ifloor (maxr (- delta) 0) \is a Znat.
by rewrite Znat_def ifloor_ge0 ler_maxr lerr orbC.
exists N.+1 => // n ltNn; apply: Hp; rewrite ltr_oppl.
exists N.+1 => // n ltNn; apply: Hp; rewrite ler_oppl; apply: ltrW.
have /ler_lt_trans : - delta <= maxr (- delta) 0 by rewrite ler_maxr lerr.
apply; apply: ltr_le_trans (floorS_gtr _) _; rewrite floorE Nfloor.
by rewrite -(@natrD [ringType of R] N 1) INRE ler_nat addn1.
Expand Down
13 changes: 7 additions & 6 deletions landau.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -568,8 +568,8 @@ Proof.
split=> [[k _ fOg] | [k fOg]].
exists k => l ltkl; move: fOg; apply: filter_app; near=> x.
by move/ler_trans; apply; rewrite ler_wpmul2r // ltrW.
exists (maxr 1 (k + 1)); first by rewrite ltr_maxr ltr01.
by apply: fOg; rewrite ltr_maxr orbC ltr_addl ltr01.
exists (maxr 1 k); first by rewrite ltr_maxr ltr01.
by apply: fOg; rewrite ler_maxr orbC lerr.
Unshelve. end_near. Qed.

Structure bigO_type (F : set (set T)) (g : T -> W) := BigO {
Expand Down Expand Up @@ -758,7 +758,8 @@ Proof. by have := @eqaddOE F f g h e; rewrite !funeqE. Qed.

Lemma eqoO (F : filter_on T) (f : T -> V) (e : T -> W) :
[o_F e of f] =O_F e.
Proof. by apply/eqOP; exists 0 => k kgt0; apply: littleoP. Qed.
Proof. by apply/eqOP; near=> M; apply: littleoP.
Grab Existential Variables. all: end_near. Qed.
Hint Resolve eqoO.

Lemma littleo_eqO (F : filter_on T) (e : T -> W) (f : {o_F e}) :
Expand Down Expand Up @@ -1063,8 +1064,7 @@ Proof.
rewrite [RHS]bigOE//; have [ O1 k1 Oh1] := bigO; have [ O2 k2 Oh2] := bigO.
near=> k; move: Oh1 Oh2; apply: filter_app2; near=> x => leOh1 leOh2.
rewrite [`|[_]|]absrM (ler_trans (ler_pmul _ _ leOh1 leOh2)) //.
rewrite mulrACA [`|[_]| in X in _ <= X]normrM ler_wpmul2r // ?mulr_ge0 //.
by near: k; apply: locally_pinfty_ge.
by rewrite mulrACA [`|[_]| in X in _ <= X]normrM ler_wpmul2r // ?mulr_ge0.
Unshelve. end_near. Grab Existential Variables. end_near. Qed.

End rule_of_products_in_R.
Expand Down Expand Up @@ -1135,7 +1135,8 @@ suff flip : \forall k \near +oo, forall x, `|[f x]| <= k * `|[x]|.
near +oo => k; near=> y.
rewrite (ler_lt_trans (near flip k _ _)) // -ltr_pdivl_mull //.
near: y; apply/locally_normP.
by eexists; last by move=> ?; rewrite /= sub0r normmN; apply.
eexists; last by move=> ?; rewrite /= sub0r normmN; apply.
by rewrite mulr_gt0// ?invr_gt0.
have /locally_normP [_/posnumP[d]] := Of1.
rewrite /cst [X in _ * X]absr1 mulr1 => fk; near=> k => y.
case: (ler0P `|[y]|) => [|y0].
Expand Down