diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 3fdbeb17ff..4bd4b04a34 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -4,6 +4,9 @@ ### Added +- in `constructive_ereal.v`: + + lemmas `gt0_fin_numE`, `ltr0_fin_numE` + ### Changed - in `hoelder.v`: diff --git a/theories/charge.v b/theories/charge.v index 1e2e01736e..157892fc32 100644 --- a/theories/charge.v +++ b/theories/charge.v @@ -471,8 +471,7 @@ have := d_ge0 A; rewrite le_eqVlt => /predU1P[<-|d_gt0]. have /ereal_sup_gt/cid2[_ [B/= [mB BDA <- mnuB]]] : m < d_ A. rewrite /m; have [->|dn1oo] := eqVneq (d_ A) +oo. by rewrite min_r ?ltey ?gt0_mulye ?leey. - rewrite -(@fineK _ (d_ A)); last first. - by rewrite ge0_fin_numE// ?(ltW d_gt0)// lt_neqAle dn1oo leey. + rewrite -(@fineK _ (d_ A)); last by rewrite gt0_fin_numE// ltey. rewrite -EFinM -fine_min// lte_fin lt_minl; apply/orP; left. by rewrite ltr_pdivr_mulr// ltr_pmulr ?ltr1n// fine_gt0// d_gt0/= ltey. by exists B; split => //; rewrite (le_trans _ (ltW mnuB)). @@ -649,8 +648,7 @@ have := s_le0 U; rewrite le_eqVlt => /predU1P[->|s_lt0]. have /ereal_inf_lt/cid2[_ [B/= [mB BU] <-] nuBm] : s_ U < m. rewrite /m; have [->|s0oo] := eqVneq (s_ U) -oo. by rewrite max_r ?ltNye// gt0_mulNye// leNye. - rewrite -(@fineK _ (s_ U)); last first. - by rewrite le0_fin_numE// ?(ltW s_lt0)// lt_neqAle leNye eq_sym s0oo. + rewrite -(@fineK _ (s_ U)); last by rewrite lt0_fin_numE// ltNye. rewrite -EFinM -fine_max// lte_fin lt_maxr; apply/orP; left. by rewrite ltr_pdivl_mulr// gtr_nmulr ?ltr1n// fine_lt0// s_lt0/= ltNye andbT. have [C [CB nsC nuCB]] := hahn_decomposition_lemma nu mB. diff --git a/theories/constructive_ereal.v b/theories/constructive_ereal.v index c8a29e13bd..9f099adac0 100644 --- a/theories/constructive_ereal.v +++ b/theories/constructive_ereal.v @@ -1468,9 +1468,15 @@ Proof. by case: x => // x //=; exact: ltNyr. Qed. Lemma ge0_fin_numE x : 0 <= x -> (x \is a fin_num) = (x < +oo). Proof. by move: x => [x| |] => // x0; rewrite fin_numElt ltNyr. Qed. +Lemma gt0_fin_numE x : 0 < x -> (x \is a fin_num) = (x < +oo). +Proof. by move/ltW; exact: ge0_fin_numE. Qed. + Lemma le0_fin_numE x : x <= 0 -> (x \is a fin_num) = (-oo < x). Proof. by move: x => [x| |]//=; rewrite lee_fin => x0; rewrite ltNyr. Qed. +Lemma lt0_fin_numE x : x < 0 -> (x \is a fin_num) = (-oo < x). +Proof. by move/ltW; exact: le0_fin_numE. Qed. + Lemma eqyP x : x = +oo <-> (forall A, (0 < A)%R -> A%:E <= x). Proof. split=> [-> // A A0|Ax]; first by rewrite leey. diff --git a/theories/hoelder.v b/theories/hoelder.v index c1c1193111..5772607ce6 100644 --- a/theories/hoelder.v +++ b/theories/hoelder.v @@ -173,7 +173,7 @@ have foo : \int[mu]_x (`|f x| `^ p)%:E < +oo. move/integrableP: ifp => -[_]. by under eq_integral do rewrite gee0_abs// ?lee_fin ?powR_ge0//. rewrite integralZl//; apply/eqP; rewrite eqe_pdivr_mull ?mule1. -- by rewrite fineK// ge0_fin_numE// ltW. +- by rewrite fineK// gt0_fin_numE. - by rewrite gt_eqF// fine_gt0// foo andbT. Qed. diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v index da42fa74be..308a2a2609 100644 --- a/theories/lebesgue_integral.v +++ b/theories/lebesgue_integral.v @@ -1090,8 +1090,7 @@ apply/eqP; rewrite eq_le; apply/andP; split; last first. by move/cvg_lim => -> //; apply: ereal_sup_ub; exists n. have := leey (\int[mu]_x (f x)). rewrite le_eqVlt => /predU1P[|] mufoo; last first. - have : \int[mu]_x (f x) \is a fin_num. - by rewrite ge0_fin_numE//; exact: integral_ge0. + have : \int[mu]_x (f x) \is a fin_num by rewrite ge0_fin_numE// integral_ge0. rewrite ge0_integralTE// => /ub_ereal_sup_adherent h. apply/lee_addgt0Pr => _/posnumP[e]. have {h} [/= _ [G Gf <-]] := h _ [gt0 of e%:num]. @@ -1275,7 +1274,7 @@ Let fpos_approx_neq0 x : D x -> (0%E < f x < +oo)%E -> \forall n \near \oo, approx n x != 0. Proof. move=> Dx /andP[fx_gt0 fxoo]. -have fxfin : f x \is a fin_num by rewrite ge0_fin_numE// ltW. +have fxfin : f x \is a fin_num by rewrite gt0_fin_numE. rewrite -(fineK fxfin) lte_fin in fx_gt0; near=> n. rewrite /approx paddr_eq0//; last 2 first. by apply: sumr_ge0 => i _; rewrite mulr_ge0. @@ -1421,7 +1420,7 @@ have cvg_af := cvg_approx fi0 Dx fixoo. have is_cvg_af : cvg (approx ^~ x) by apply/cvg_ex; eexists; exact: cvg_af. have {is_cvg_af} := nondecreasing_cvg_le nd_ag is_cvg_af k. rewrite -lee_fin => /le_trans; apply. -rewrite -(@fineK _ (f x)); last by rewrite ge0_fin_numE //; apply: f0. +rewrite -(@fineK _ (f x)); last by rewrite ge0_fin_numE// f0. by move/(cvg_lim (@Rhausdorff R)) : cvg_af => ->. Qed. @@ -1720,7 +1719,7 @@ move=> D [/= mD Deps KDf]; exists (K `\` D); split => //. by apply: measureU2 => //; apply: measurableI => //; apply: measurableC. rewrite [_%:num]splitr EFinD; apply: lee_lt_add => //=; first 2 last. + by rewrite (@le_lt_trans _ _ (mu D)) ?le_measure ?inE//; exact: measurableI. - + rewrite ge0_fin_numE// (@le_lt_trans _ _ (mu A))// le_measure// ?inE//. + + rewrite ge0_fin_numE// (@le_lt_trans _ _ (mu A))// le_measure ?inE//. exact: measurableD. rewrite setDE setC_bigcap setI_bigcupr. apply: (@le_trans _ _(\sum_(k // m /= m0; move: muDoo; rewrite leye_eq => /eqP ->. by rewrite mulry gtr0_sg ?mul1e ?leey// ltr0n. exists `|ceil (M / fine (mu D))|%N => // m /=. - rewrite -(ler_nat R) => MDm. - rewrite -(@fineK _ (mu D)); last by rewrite ge0_fin_numE. + rewrite -(ler_nat R) => MDm; rewrite -(@fineK _ (mu D)) ?ge0_fin_numE//. rewrite -lee_pdivr_mulr; last by rewrite fine_gt0// lt0e muD0 measure_ge0. - rewrite lee_fin; apply: le_trans MDm. + rewrite lee_fin (le_trans _ MDm)//. by rewrite natr_absz (le_trans (ceil_ge _))// ler_int ler_norm. - by move=> n; exact: measurable_cst. - by move=> n x Dx; rewrite lee_fin. @@ -3211,7 +3209,7 @@ have [M M0 muM] : exists2 M, (0 <= M)%R & - by move=> *; rewrite lee_fin. rewrite fineK//; last first. case: (integrableP _ _ _ fint) => _ foo. - by rewrite ge0_fin_numE//; exact: integral_ge0. + by rewrite ge0_fin_numE// integral_ge0. apply: ge0_le_integral => //. - by move=> *; rewrite lee_fin /indic. - exact/EFin_measurable_fun/measurableT_comp. @@ -3303,7 +3301,7 @@ suff: \int[mu]_(x in D) ((g1 \+ g2)^\+ x) + \int[mu]_(x in D) (g1^\- x) + \int[mu]_(x in D) (g1^\+ x) + \int[mu]_(x in D) (g2^\+ x) \is a fin_num. rewrite ge0_fin_numE//. by rewrite lte_add_pinfty//; exact: integral_funepos_lt_pinfty. - by apply: adde_ge0; exact: integral_ge0. + by rewrite adde_ge0// integral_ge0. have g12neg : \int[mu]_(x in D) (g1^\- x) + \int[mu]_(x in D) (g2^\- x) \is a fin_num. rewrite ge0_fin_numE//. @@ -3313,9 +3311,8 @@ suff: \int[mu]_(x in D) ((g1 \+ g2)^\+ x) + \int[mu]_(x in D) (g1^\- x) + - rewrite ge0_fin_numE. apply: lte_add_pinfty; last exact: integral_funeneg_lt_pinfty. apply: lte_add_pinfty; last exact: integral_funeneg_lt_pinfty. - have : mu.-integrable D (g1 \+ g2) by apply: integrableD. - exact: integral_funepos_lt_pinfty. - apply: adde_ge0; last exact: integral_ge0. + exact: integral_funepos_lt_pinfty (integrableD _ _ _). + rewrite adde_ge0//; last exact: integral_ge0. by apply: adde_ge0; exact: integral_ge0. - by rewrite fin_num_adde_defr. rewrite -(addeA (\int[mu]_(x in D) (g1 \+ g2)^\+ x)). @@ -4548,8 +4545,7 @@ have m2Fn_bounded : exists M, forall X, measurable X -> (m2Fn X < M%:E)%E. exists (fine (m2Fn (F n)) + 1) => Y mY. rewrite [in ltRHS]EFinD lte_spadder// fineK; last first. by rewrite ge0_fin_numE ?measure_ge0//= /mrestr/= setIid. - rewrite /= /mrestr/= setIid; apply: le_measure => //; rewrite inE//. - exact: measurableI. + by rewrite /= /mrestr/= setIid le_measure// inE//; exact: measurableI. pose phi' A := m2Fn \o xsection A. pose B' := [set A | measurable A /\ measurable_fun setT (phi' A)]. have subset_B' : measurable `<=` B' by exact: measurable_prod_subset_xsection. @@ -4584,8 +4580,7 @@ have m1Fn_bounded : exists M, forall X, measurable X -> (m1Fn X < M%:E)%E. exists (fine (m1Fn (F n)) + 1) => Y mY. rewrite [in ltRHS]EFinD lte_spadder// fineK; last first. by rewrite ge0_fin_numE ?measure_ge0// /m1Fn/= /mrestr setIid. - rewrite /m1Fn/= /mrestr setIid; apply: le_measure => //; rewrite inE//=. - exact: measurableI. + by rewrite /m1Fn/= /mrestr setIid le_measure// inE//=; exact: measurableI. pose psi' A := m1Fn \o ysection A. pose B' := [set A | measurable A /\ measurable_fun setT (psi' A)]. have subset_B' : measurable `<=` B' by exact: measurable_prod_subset_ysection. diff --git a/theories/measure.v b/theories/measure.v index 49610304fe..8b167b6ba0 100644 --- a/theories/measure.v +++ b/theories/measure.v @@ -2975,7 +2975,7 @@ Let mnormalize1 : mnormalize [set: T] = 1. Proof. rewrite /mnormalize; case: ifPn; first by rewrite probability_setT. rewrite negb_or => /andP[ft0 ftoo]. -have ? : mu setT \is a fin_num by rewrite ge0_fin_numE// lt_neqAle ftoo/= leey. +have ? : mu setT \is a fin_num by rewrite ge0_fin_numE// ltey. by rewrite -{1}(@fineK _ (mu setT))// -EFinM divrr// ?unitfE fine_eq0. Qed. diff --git a/theories/normedtype.v b/theories/normedtype.v index c77eaeba38..f0ebb6e559 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -3795,7 +3795,7 @@ Qed. Lemma edist_pinfty_open : open [set xy : X * X | edist xy = +oo]%E. Proof. rewrite -closedC; have := edist_fin_closed; congr (_ _). -by rewrite eqEsubset; split => z; rewrite /= ?ge0_fin_numE // ltey; move/eqP. +by rewrite eqEsubset; split => z; rewrite /= ?ge0_fin_numE// ltey => /eqP. Qed. Lemma edist_sym (x y : X) : edist (x, y) = edist (y, x). @@ -4034,11 +4034,11 @@ Section topological_urysohn_separator. Context {T : topologicalType} {R : realType}. Definition uniform_separator (A B : set T) := - exists (uT : @Uniform.class_of T^o) (E : set (T * T)), - let UT := Uniform.Pack uT in [/\ + exists (uT : @Uniform.class_of T^o) (E : set (T * T)), + let UT := Uniform.Pack uT in [/\ @entourage UT E, A `*` B `&` E = set0 & (forall x, @nbhs UT UT x `<=` @nbhs T T x)]. - + Local Lemma Urysohn' (A B : set T) : exists (f : T -> R), [/\ continuous f, range f `<=` `[0, 1]