Skip to content

Commit

Permalink
change inequality in ereal_{d,}nbhs
Browse files Browse the repository at this point in the history
- from strict to large
- also in {p,n}infty_{d,}nbhs

closed #122
  • Loading branch information
affeldt-aist committed Aug 13, 2024
1 parent 99c3a83 commit b719baa
Show file tree
Hide file tree
Showing 11 changed files with 232 additions and 196 deletions.
8 changes: 8 additions & 0 deletions CHANGELOG_UNRELEASED.md
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,14 @@
### Added

### 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

### Renamed

Expand Down
4 changes: 2 additions & 2 deletions theories/derive.v
Original file line number Diff line number Diff line change
Expand Up @@ -1337,8 +1337,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
236 changes: 116 additions & 120 deletions theories/ereal.v

Large diffs are not rendered by default.

2 changes: 1 addition & 1 deletion theories/exp.v
Original file line number Diff line number Diff line change
Expand Up @@ -70,7 +70,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
Original file line number Diff line number Diff line change
Expand Up @@ -480,8 +480,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 @@ -679,9 +679,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 @@ -1116,10 +1118,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 @@ -1131,7 +1133,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 @@ -1337,7 +1339,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 @@ -1499,7 +1501,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
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 @@ -3116,7 +3116,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 @@ -4958,7 +4958,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 @@ -5052,7 +5052,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 @@ -5110,7 +5110,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 @@ -5124,7 +5124,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

0 comments on commit b719baa

Please sign in to comment.