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

change inequality in ereal_{d,}nbhs and {p,n}infty_{d,}nbhs #487

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

change inequality in ereal_{d,}nbhs and {p,n}infty_{d,}nbhs #487

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
8 changes: 8 additions & 0 deletions CHANGELOG_UNRELEASED.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -31,6 +31,14 @@
+ lemmas `cvgr_expR`, `cvgn_expR`

### Changed


- in `ereal.v`:
+ definitions `ereal_dnbhs` and `ereal_nbhs` changed to use large inequality instead
of strict inequality
- in `normedtype.v`:
+ definitions `pinfty_dnbhs` and `ninfty_nbhs` changed to use large inequality instead
of strict inequality

- The file `topology.v` has been split into several files in the directory
`topology_theory`. Unless stated otherwise, definitions, lemmas, etc.
Expand Down
4 changes: 2 additions & 2 deletions theories/derive.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1409,8 +1409,8 @@ have imf_sup : has_sup imf.
split; first by exists (f a); apply/imageP; rewrite /= in_itv /= lexx.
have [M [Mreal imfltM]] : bounded_set (f @` `[a, b]).
by apply/compact_bounded/continuous_compact => //; exact: segment_compact.
exists (M + 1) => y /imfltM yleM.
by rewrite (le_trans _ (yleM _ _)) ?ler_norm ?ltrDl.
exists (M + 1); apply/ubP => y /imfltM/= yleM.
by rewrite (le_trans _ (yleM _ _)) ?lerDl ?ler_norm.
have [|imf_ltsup] := pselect (exists2 c, c \in `[a, b]%R & f c = sup imf).
move=> [c cab fceqsup]; exists c => // t tab; rewrite fceqsup.
by apply/sup_upper_bound => //; exact/imageP.
Expand Down
232 changes: 114 additions & 118 deletions theories/ereal.v
View file
Open in desktop

Large diffs are not rendered by default.

2 changes: 1 addition & 1 deletion theories/exp.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -69,7 +69,7 @@ apply: series_le_cvg Kzxn _ _ => [//=| /= n|].
rewrite !normrM normr_id mulrAC mulfK // normr_eq0 expf_eq0 andbC.
by case: ltrgt0P zLx; rewrite //= normr_lt0.
do! (apply: ler_pM || apply: mulr_ge0 || rewrite invr_ge0) => //.
by apply Kf => //; rewrite (lt_le_trans _ (ler_norm _))// ltrDl.
by apply Kf => //; rewrite (le_trans _ (ler_norm _))// lerDl.
have F : `|z / x| < 1.
by rewrite normrM normfV ltr_pdivrMr ?mul1r // (le_lt_trans _ zLx).
rewrite (_ : (fun _ => _) = geometric `|K + 1| `|z / x|); last first.
Expand Down
22 changes: 12 additions & 10 deletions theories/landau.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -481,8 +481,8 @@ split=> [[k k0 fOg] | [k [kreal fOg]]].
exists k; rewrite realE (ltW k0) /=; split=> // l ltkl; move: fOg.
by apply: filter_app; near=> x => /le_trans; apply; rewrite ler_wpM2r // ltW.
exists (Num.max 1 `|k + 1|) => //.
apply: fOg; rewrite (@lt_le_trans _ _ `|k + 1|) //.
by rewrite (@lt_le_trans _ _ (k + 1)) ?ltrDl // real_ler_norm ?realD.
apply: fOg; rewrite (@le_trans _ _ `|k + 1|) //.
by rewrite (@le_trans _ _ (k + 1)) ?lerDl// real_ler_norm ?realD.
by rewrite comparable_le_max ?real_comparable// lexx orbT.
Unshelve. end_near. Qed.

Expand Down Expand Up @@ -680,9 +680,11 @@ Notation "[o_ x e 'of' f ]" := (mklittleo gen_tag x f e).
(*Printing*)
Notation "[o '_' x e 'of' f ]" := (the_littleo _ _ (PhantomF x) f e).

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; split => // k kgt0; apply: littleoP. Qed.
Lemma eqoO (F : filter_on T) (f : T -> V) (e : T -> W) : [o_F e of f] =O_F e.
Proof.
apply/eqOP; exists 1; split => // k kge1; apply: littleoP.
by rewrite (lt_le_trans _ kge1).
Qed.
Hint Resolve eqoO : core.

(* NB: duplicate from Section Domination *)
Expand Down Expand Up @@ -1117,10 +1119,10 @@ rewrite -linearB opprD addrC addrNK linearN normrN; near: y.
suff flip : \forall k \near +oo, forall x, `|f x| <= k * `|x|.
near +oo => k; near=> y.
rewrite (le_lt_trans (near flip k _ _)) // -ltr_pdivlMl; last first.
by near: k; exists 0.
by near: k; exact: nbhs_pinfty_gt.
near: y; apply/nbhs_normP.
eexists; last by move=> ?; rewrite /= sub0r normrN; apply.
by rewrite /= mulr_gt0 // invr_gt0; near: k; exists 0.
by rewrite /= mulr_gt0 // invr_gt0; near: k; exact: nbhs_pinfty_gt.
have /nbhs_normP [_/posnumP[d]] := Of1.
rewrite /cst [X in _ * X]normr1 mulr1 => fk; near=> k => y.
case: (ler0P `|y|) => [|y0].
Expand All @@ -1132,7 +1134,7 @@ rewrite -(ler_pM2l [gt0 of k0%:num]) mulr1 mulrA -[_ / _]ger0_norm //.
rewrite -normm_s.
rewrite -linearZ fk //= /= distrC subr0 normrZ ger0_norm //.
rewrite invfM mulrA mulfVK ?lt0r_neq0 // ltr_pdivrMr //.
by rewrite -ltr_pdivrMl//.
by rewrite -ltr_pdivrMl.
Unshelve. all: by end_near. Qed.

End Linear3.
Expand Down Expand Up @@ -1338,7 +1340,7 @@ rewrite (@le_trans _ _ ((k2%:num * k1%:num)^-1 * `|(W1 * W2) x|)) //.
rewrite invrM ?unitfE ?gtr_eqF // -mulrA ler_pdivlMl //.
rewrite ler_pdivlMl // (mulrA k1%:num) mulrCA (@normrM _ (W1 x)).
by rewrite ler_pM ?mulr_ge0 //; near: x.
by rewrite ler_wpM2r // ltW //.
by rewrite ler_wpM2r // ltW.
Unshelve. all: by end_near. Qed.

End big_omega_in_R.
Expand Down Expand Up @@ -1500,7 +1502,7 @@ rewrite [`|_|]normrM (@le_trans _ _ ((k2%:num * k1%:num)^-1 * `|(T1 * T2) x|)) /
rewrite invrM ?unitfE ?gtr_eqF // -mulrA ler_pdivlMl //.
rewrite ler_pdivlMl // (mulrA k1%:num) mulrCA (@normrM _ (T1 x)) ler_pM //;
by [rewrite mulr_ge0 //|near: x].
by rewrite ler_wpM2r // ltW //.
by rewrite ler_wpM2r // ltW.
Unshelve. all: by end_near. Qed.

End big_theta_in_R.
12 changes: 6 additions & 6 deletions theories/lebesgue_integral.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -445,7 +445,7 @@ Lemma simple_bounded (f : {sfun T >-> R}) : bounded_fun f.
Proof.
have /finite_seqP[r fr] := fimfunP f.
exists (fine (\big[maxe/-oo%E]_(i <- r) `|i|%:E)).
split; rewrite ?num_real// => x mx z _; apply/ltW/(le_lt_trans _ mx).
split; rewrite ?num_real// => x mx z _; apply/(le_trans _ mx).
have ? : f z \in r by have := imageT f z; rewrite fr.
rewrite -[leLHS]/(fine `|f z|%:E) fine_le//.
have := @bigmaxe_fin_num _ (map normr r) `|f z|.
Expand Down Expand Up @@ -3115,7 +3115,7 @@ apply/le_lt_trans/ge0_le_integral => //.
- apply/emeasurable_funM => //; apply/measurableT_comp => //.
exact: measurable_int gi.
- move=> x Dx; rewrite lee_wpmul2r//= lee_fin Mh//=.
by rewrite (lt_le_trans _ (ler_norm _))// ltrDl.
by rewrite (le_trans _ (ler_norm _))// lerDl.
Qed.

Lemma integrableMl f (h : T -> R) :
Expand Down Expand Up @@ -4969,7 +4969,7 @@ Proof.
move=> Afin mfA bdA; apply/integrableP; split; first exact/EFin_measurable_fun.
have [M [_ mrt]] := bdA; apply: le_lt_trans.
apply: (integral_le_bound (`|M| + 1)%:E) => //; first exact: measurableT_comp.
by apply: aeW => z Az; rewrite lee_fin mrt// ltr_pwDr// ler_norm.
by apply: aeW => z Az; rewrite lee_fin mrt// ler_wpDr// ler_norm.
by rewrite lte_mul_pinfty.
Qed.

Expand Down Expand Up @@ -5063,7 +5063,7 @@ Lemma compact_finite_measure (A : set R^o) : compact A -> mu A < +oo.
Proof.
move=> /[dup]/compact_measurable => mA /compact_bounded[N [_ N1x]].
have AN1 : (A `<=` `[- (`|N| + 1), `|N| + 1])%R.
by move=> z Az; rewrite set_itvcc /= -ler_norml N1x// ltr_pwDr// ler_norm.
by move=> z Az; rewrite set_itvcc /= -ler_norml N1x// ler_wpDr// ler_norm.
rewrite (le_lt_trans (le_measure _ _ _ AN1)) ?inE//=.
by rewrite lebesgue_measure_itv/= lte_fin gtrN// EFinD ltry.
Qed.
Expand Down Expand Up @@ -5121,7 +5121,7 @@ have mg : measurable_fun E g by exact: measurable_funTS.
have [M Mpos Mbd] : (exists2 M, 0 < M & forall x, `|g x| <= M)%R.
have [M [_ /= bdM]] := simple_bounded g.
exists (`|M| + 1)%R; first exact: ltr_pwDr.
by move=> x; rewrite bdM// ltr_pwDr// ler_norm.
by move=> x; rewrite bdM// ler_wpDr// ler_norm.
have [] // := @measurable_almost_continuous _ _ mE _ g (eps%:num / 2 / (M *+ 2)).
by rewrite divr_gt0// mulrn_wgt0.
move=> A [cptA AE /= muAE ctsAF].
Expand All @@ -5135,7 +5135,7 @@ move=> h [gh ctsh hbdM]; have mh : measurable_fun E h.
have intg : mu.-integrable E (EFin \o h).
apply: measurable_bounded_integrable => //.
exists M; split; rewrite ?num_real // => x Mx y _ /=.
by rewrite (le_trans _ (ltW Mx)).
by rewrite (le_trans _ Mx).
exists h; split => //; rewrite [eps%:num]splitr; apply: le_lt_trans.
pose fgh x := `|(f x - g x)%:E| + `|(g x - h x)%:E|.
apply: (@ge0_le_integral _ _ _ mu _ mE _ fgh) => //.
Expand Down
Loading