diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 5ab0033e1..39c539337 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -26,6 +26,9 @@ + module `pi_irrational` + lemma `pi_irrationnal` +- in `numfun.v` + + lemmas `funeposE`, `funenegE`, `funepos_comp`, `funeneg_comp` + ### Changed - in `lebesgue_integrale.v` @@ -34,6 +37,9 @@ - in `derive.v`: + put the notation ``` ^`() ``` and ``` ^`( _ ) ``` in scope `classical_set_scope` +- in `numfun.v` + + lock `funepos`, `funeneg` + ### Renamed ### Generalized diff --git a/theories/esum.v b/theories/esum.v index 57959228b..7549ecad0 100644 --- a/theories/esum.v +++ b/theories/esum.v @@ -600,10 +600,8 @@ Unshelve. all: by end_near. Qed. Lemma summable_eseries_esum (f : nat -> \bar R) (P : pred nat) : summable P f -> \sum_(i Pfoo; rewrite -nneseries_esum; last first. - by move=> n Pn; rewrite /maxe; case: ifPn => //; rewrite -leNgt. -rewrite -nneseries_esum ?[LHS]summable_eseries//. -by move=> n Pn; rewrite /maxe; case: ifPn => //; rewrite leNgt. +move=> Pfoo. +by rewrite -nneseries_esum// -nneseries_esum// [LHS]summable_eseries. Qed. End summable_nat. @@ -620,7 +618,7 @@ Let ge0_esum_posneg D f : (forall x, D x -> 0 <= f x) -> Proof. move=> Sa; rewrite /esum_posneg [X in _ - X](_ : _ = 0) ?sube0; last first. by rewrite esum1// => x Sx; rewrite -[LHS]/(f^\- x) (ge0_funenegE Sa)// inE. -by apply: eq_esum => t St; apply/max_idPl; exact: Sa. +apply: eq_esum => t St; rewrite funeposE; apply/max_idPl; exact: Sa. Qed. Lemma esumB D f g : summable D f -> summable D g -> @@ -630,10 +628,9 @@ Lemma esumB D f g : summable D f -> summable D g -> Proof. move=> Df Dg f0 g0. have /eqP : esum D (f \- g)^\+ + esum_posneg D g = esum D (f \- g)^\- + esum_posneg D f. - rewrite !ge0_esum_posneg// -!esumD//; last 2 first. - by move=> t Dt; rewrite le_max lexx orbT. - by move=> t Dt; rewrite le_max lexx orbT. - apply eq_esum => i Di; have [fg|fg] := leP 0 (f i - g i). + rewrite !ge0_esum_posneg// -!esumD//. + apply eq_esum => i Di; rewrite funeposE funenegE. + have [fg|fg] := leP 0 (f i - g i). rewrite max_r 1?leeNl ?oppe0// add0e subeK//. by rewrite fin_num_abs (summable_pinfty Dg). rewrite add0e max_l; last by rewrite leeNr oppe0 ltW. diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v index 5c9855232..a882d3053 100644 --- a/theories/lebesgue_integral.v +++ b/theories/lebesgue_integral.v @@ -2562,12 +2562,12 @@ Lemma integralN D (f : T -> \bar R) : Proof. have [f_fin _|] := boolP (\int[mu]_(x in D) f^\- x \is a fin_num). rewrite integralE// [in RHS]integralE// fin_num_oppeD ?fin_numN// oppeK addeC. - by rewrite funenegN. + by rewrite funenegN funeposN. rewrite fin_numE negb_and 2!negbK => /orP[nfoo|/eqP nfoo]. exfalso; move/negP : nfoo; apply; rewrite -leeNy_eq; apply/negP. by rewrite -ltNge (lt_le_trans _ (integral_ge0 _ _)). rewrite nfoo adde_defEninfty -leye_eq -ltNge ltey_eq => /orP[f_fin|/eqP pfoo]. - rewrite integralE [in RHS]integralE nfoo [in RHS]addeC/= funenegN. + rewrite integralE [in RHS]integralE funeposN nfoo [in RHS]addeC/= funenegN. by rewrite addye// eqe_oppLR/= (andP (eqbLR (fin_numE _) f_fin)).2. by rewrite integralE// [in RHS]integralE// funeposN funenegN nfoo pfoo. Qed. @@ -3191,9 +3191,9 @@ move=> /integrableP[mf]; apply: le_lt_trans; apply: ge0_le_integral => //. - exact: measurable_funeneg. - exact: measurableT_comp. - move=> x Dx; have [fx0|/ltW fx0] := leP (f x) 0. - rewrite lee0_abs// /funeneg. + rewrite lee0_abs// funenegE. by move: fx0; rewrite -{1}oppe0 -leeNr => /max_idPl ->. - rewrite gee0_abs// /funeneg. + rewrite gee0_abs// funenegE. by move: (fx0); rewrite -{1}oppe0 -leeNl => /max_idPr ->. Qed. @@ -3204,9 +3204,9 @@ move=> /integrableP[mf]; apply: le_lt_trans; apply: ge0_le_integral => //. - exact: measurable_funepos. - exact: measurableT_comp. - move=> x Dx; have [fx0|/ltW fx0] := leP (f x) 0. - rewrite lee0_abs// /funepos. + rewrite lee0_abs// funeposE. by move: (fx0) => /max_idPr ->; rewrite -leeNr oppe0. - by rewrite gee0_abs// /funepos; move: (fx0) => /max_idPl ->. + by rewrite gee0_abs// funeposE; move: (fx0) => /max_idPl ->. Qed. Lemma integrable_neg_fin_num f : @@ -3600,11 +3600,11 @@ suff: \int[mu]_(x in D) ((g1 \+ g2)^\+ x) + \int[mu]_(x in D) (g1^\- x) + have : (g1 \+ g2)^\+ \+ g1^\- \+ g2^\- = (g1 \+ g2)^\- \+ g1^\+ \+ g2^\+. rewrite funeqE => x. apply/eqP; rewrite -2!addeA [in eqbRHS]addeC -sube_eq; last 2 first. - by rewrite /funepos /funeneg -!fine_max. - by rewrite /funepos /funeneg -!fine_max. + by rewrite funeposE !funenegE -!fine_max. + by rewrite !funeposE funenegE -!fine_max. rewrite addeAC eq_sym -sube_eq; last 2 first. - by rewrite /funepos /funeneg -!fine_max. - by rewrite /funepos /funeneg -!fine_max. + by rewrite !funeposE -!fine_max. + by rewrite funeposE !funenegE -!fine_max. apply/eqP. rewrite -[LHS]/((g1^\+ \+ g2^\+ \- (g1^\- \+ g2^\-)) x) -funeD_posD. by rewrite -[RHS]/((_ \- _) x) -funeD_Dpos. @@ -3619,7 +3619,7 @@ rewrite (ge0_integralD mu mD); last 4 first. - by []. - exact/measurable_funepos/emeasurable_funD. - by []. - - exact/measurable_funepos/measurableT_comp. + - exact/measurable_funeneg. move=> ->. rewrite (ge0_integralD mu mD); last 4 first. - by move=> x _; exact: adde_ge0. @@ -4123,11 +4123,11 @@ Local Open Scope ereal_scope. Lemma integral_pushforward : \int[pushforward mu mphi]_y f y = \int[mu]_x (f \o phi) x. Proof. -transitivity (\int[mu]_y ((f^\+ \o phi) \- (f^\- \o phi)) y); last first. - by apply: eq_integral => x _; rewrite [in RHS](funeposneg (f \o phi)). -rewrite integralB//; [|exact: integrable_funepos|exact: integrable_funeneg]. +rewrite integralE. +under [X in X - _]eq_integral do rewrite funepos_comp. +under [X in _ - X]eq_integral do rewrite funeneg_comp. rewrite -[X in _ = X - _]ge0_integral_pushforward//; last first. - exact: measurable_funepos. + exact/measurable_funepos. rewrite -[X in _ = _ - X]ge0_integral_pushforward//; last first. exact: measurable_funeneg. rewrite -integralB//=; last first. @@ -4335,16 +4335,15 @@ transitivity ((\sum_(i //. + apply: measurable_funeneg. by case/integrableP : fi. rewrite [X in X - _]nneseries_esum; last by move=> n _; exact: integral_ge0. rewrite [X in _ - X]nneseries_esum; last by move=> n _; exact: integral_ge0. rewrite set_true -esumB//=; last 4 first. - apply: integrable_summable => //; apply: integrable_funepos => //. exact: bigcup_measurable. - - apply: integrable_summable => //; apply: integrable_funepos => //. + - apply: integrable_summable => //; apply: integrable_funeneg => //. exact: bigcup_measurable. - - exact: integrableN. - by move=> n _; exact: integral_ge0. - by move=> n _; exact: integral_ge0. rewrite summable_eseries; last first. @@ -5816,7 +5815,12 @@ Let F := fubini_F m2 f. Let Fplus x := \int[m2]_y f^\+ (x, y). Let Fminus x := \int[m2]_y f^\- (x, y). -Let FE : F = Fplus \- Fminus. Proof. apply/funext=> x; exact: integralE. Qed. +Let FE : F = Fplus \- Fminus. +Proof. +apply/funext=> x; rewrite [LHS]integralE. +under eq_integral do rewrite funepos_comp/=. +by under [X in _ - X = _]eq_integral do rewrite funeneg_comp/=. +Qed. Let measurable_Fplus : measurable_fun setT Fplus. Proof. @@ -5841,11 +5845,11 @@ apply: le_lt_trans (fubini1a.1 imf); apply: ge0_le_integral => //. - exact: measurableT_comp. - by move=> x _; exact: integral_ge0. - move=> x _; apply: le_trans. - apply: le_abse_integral => //; apply: measurable_funepos => //. - exact: measurableT_comp. + apply: le_abse_integral => //; apply: measurableT_comp => //. + exact: measurable_funepos. apply: ge0_le_integral => //. - apply: measurableT_comp => //. - by apply: measurable_funepos => //; exact: measurableT_comp. + by apply: measurableT_comp => //; exact: measurable_funepos. - by apply: measurableT_comp => //; exact/measurableT_comp. - by move=> y _; rewrite gee0_abs// -/((abse \o f) (x, y)) fune_abse leeDl. Qed. @@ -5857,11 +5861,11 @@ apply: le_lt_trans (fubini1a.1 imf); apply: ge0_le_integral => //. - exact: measurableT_comp. - by move=> *; exact: integral_ge0. - move=> x _; apply: le_trans. - apply: le_abse_integral => //; apply: measurable_funeneg => //. - exact: measurableT_comp. + apply: le_abse_integral => //; apply: measurableT_comp => //. + exact: measurable_funeneg. apply: ge0_le_integral => //. - + apply: measurableT_comp => //; apply: measurable_funeneg => //. - exact: measurableT_comp. + + apply: measurableT_comp => //; apply: measurableT_comp => //. + exact: measurable_funeneg. + by apply: measurableT_comp => //; exact: measurableT_comp. + by move=> y _; rewrite gee0_abs// -/((abse \o f) (x, y)) fune_abse leeDr. Qed. @@ -5874,7 +5878,12 @@ Let G := fubini_G m1 f. Let Gplus y := \int[m1]_x f^\+ (x, y). Let Gminus y := \int[m1]_x f^\- (x, y). -Let GE : G = Gplus \- Gminus. Proof. apply/funext=> x; exact: integralE. Qed. +Let GE : G = Gplus \- Gminus. +Proof. +apply/funext=> x; rewrite [LHS]integralE. +under eq_integral do rewrite funepos_comp/=. +by under [X in _ - X = _]eq_integral do rewrite funeneg_comp/=. +Qed. Let measurable_Gplus : measurable_fun setT Gplus. Proof. @@ -5896,11 +5905,11 @@ apply: le_lt_trans (fubini1b.1 imf); apply: ge0_le_integral => //. - exact: measurableT_comp. - by move=> *; exact: integral_ge0. - move=> y _; apply: le_trans. - apply: le_abse_integral => //; apply: measurable_funepos => //. - exact: measurableT_comp. + apply: le_abse_integral => //; apply: measurableT_comp => //. + exact: measurable_funepos. apply: ge0_le_integral => //. - apply: measurableT_comp => //. - by apply: measurable_funepos => //; exact: measurableT_comp. + by apply: measurableT_comp => //; exact: measurable_funepos. - by apply: measurableT_comp => //; exact: measurableT_comp. - by move=> x _; rewrite gee0_abs// -/((abse \o f) (x, y)) fune_abse leeDl. Qed. @@ -5912,11 +5921,11 @@ apply: le_lt_trans (fubini1b.1 imf); apply: ge0_le_integral => //. - exact: measurableT_comp. - by move=> *; exact: integral_ge0. - move=> y _; apply: le_trans. - apply: le_abse_integral => //; apply: measurable_funeneg => //. - exact: measurableT_comp. + apply: le_abse_integral => //; apply: measurableT_comp => //. + exact: measurable_funeneg. apply: ge0_le_integral => //. + apply: measurableT_comp => //. - by apply: measurable_funeneg => //; exact: measurableT_comp. + by apply: measurableT_comp => //; exact: measurable_funeneg. + by apply: measurableT_comp => //; exact: measurableT_comp. + by move=> x _; rewrite gee0_abs// -/((abse \o f) (x, y)) fune_abse leeDr. Qed. diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v index e249063c6..2a1e1993c 100644 --- a/theories/lebesgue_measure.v +++ b/theories/lebesgue_measure.v @@ -1516,11 +1516,14 @@ Qed. Lemma measurable_funepos D (f : T -> \bar R) : measurable_fun D f -> measurable_fun D f^\+. -Proof. by move=> mf; exact: measurable_maxe. Qed. +Proof. by move=> mf; rewrite unlock; exact: measurable_maxe. Qed. Lemma measurable_funeneg D (f : T -> \bar R) : measurable_fun D f -> measurable_fun D f^\-. -Proof. by move=> mf; apply: measurable_maxe => //; exact: measurableT_comp. Qed. +Proof. +move=> mf; rewrite unlock; apply: measurable_maxe => //. +exact: measurableT_comp. +Qed. Lemma measurable_mine D (f g : T -> \bar R) : measurable_fun D f -> measurable_fun D g -> diff --git a/theories/measure.v b/theories/measure.v index b16befccb..527b029ea 100644 --- a/theories/measure.v +++ b/theories/measure.v @@ -4105,7 +4105,9 @@ Proof. by apply: filterS => x /[apply] /= ->. Qed. Lemma ae_eq_funeposneg f g : ae_eq f g <-> ae_eq f^\+ g^\+ /\ ae_eq f^\- g^\-. Proof. split=> [fg|[]]. - by rewrite /funepos /funeneg; split; apply: filterS fg => x /[apply] ->. + split; apply: filterS fg => x /[apply]. + by rewrite !funeposE => ->. + by rewrite !funenegE => ->. apply: filterS2 => x + + Dx => /(_ Dx) fg /(_ Dx) gf. by rewrite (funeposneg f) (funeposneg g) fg gf. Qed. diff --git a/theories/numfun.v b/theories/numfun.v index 92f31a9c9..4a81ae2aa 100644 --- a/theories/numfun.v +++ b/theories/numfun.v @@ -127,69 +127,85 @@ Proof. by apply/funext=> x; rewrite /patch/=; case: ifP; rewrite ?mule0. Qed. End erestrict_lemmas. -Section funposneg. -Local Open Scope ereal_scope. - +HB.lock Definition funepos T (R : realDomainType) (f : T -> \bar R) := fun x => maxe (f x) 0. +HB.lock Definition funeneg T (R : realDomainType) (f : T -> \bar R) := - fun x => maxe (- f x) 0. - -End funposneg. + fun x => maxe (oppe (f x)) 0. Notation "f ^\+" := (funepos f) : ereal_scope. Notation "f ^\-" := (funeneg f) : ereal_scope. Section funposneg_lemmas. Local Open Scope ereal_scope. -Variables (T : Type) (R : realDomainType) (D : set T). -Implicit Types (f g : T -> \bar R) (r : R). +Variables (T U : Type) (R : realDomainType) (D : set T). +Implicit Types (f g : T -> \bar R) (h : U -> T) (r : R). + +Lemma funeposE f x : f^\+ x = maxe (f x) 0. +Proof. by rewrite unlock. Qed. + +Lemma funenegE f x : f^\- x = maxe (- f x) 0. +Proof. by rewrite unlock. Qed. Lemma funepos_ge0 f x : 0 <= f^\+ x. -Proof. by rewrite /funepos /= le_max lexx orbT. Qed. +Proof. by rewrite funeposE le_max lexx orbT. Qed. Lemma funeneg_ge0 f x : 0 <= f^\- x. -Proof. by rewrite /funeneg le_max lexx orbT. Qed. +Proof. by rewrite funenegE le_max lexx orbT. Qed. -Lemma funeposN f : (\- f)^\+ = f^\-. Proof. exact/funext. Qed. +Lemma funeposN f : (\- f)^\+ = f^\-. +Proof. by apply/funext => x; rewrite funeposE funenegE. Qed. Lemma funenegN f : (\- f)^\- = f^\+. -Proof. by apply/funext => x; rewrite /funeneg oppeK. Qed. +Proof. by apply/funext => x; rewrite funeposE funenegE oppeK. Qed. + +Lemma funepos_comp f h : (f \o h)^\+ = f^\+ \o h. +Proof. by rewrite !unlock. Qed. + +Lemma funeneg_comp f h : (f \o h)^\- = f^\- \o h. +Proof. by rewrite !unlock. Qed. Lemma funepos_restrict f : (f \_ D)^\+ = (f^\+) \_ D. Proof. -by apply/funext => x; rewrite /patch/_^\+; case: ifP; rewrite //= maxxx. +by apply/funext => x; rewrite /patch !funeposE; case: ifP; rewrite //= maxxx. Qed. Lemma funeneg_restrict f : (f \_ D)^\- = (f^\-) \_ D. Proof. -by apply/funext => x; rewrite /patch/_^\-; case: ifP; rewrite //= oppr0 maxxx. +apply/funext => x; rewrite /patch !funenegE. +by case: ifP; rewrite //= oppr0 maxxx. Qed. Lemma ge0_funeposE f : (forall x, D x -> 0 <= f x) -> {in D, f^\+ =1 f}. -Proof. by move=> f0 x; rewrite inE => Dx; apply/max_idPl/f0. Qed. +Proof. by move=> f0 x; rewrite inE funeposE => Dx; apply/max_idPl/f0. Qed. Lemma ge0_funenegE f : (forall x, D x -> 0 <= f x) -> {in D, f^\- =1 cst 0}. Proof. -by move=> f0 x; rewrite inE => Dx; apply/max_idPr; rewrite leeNl oppe0 f0. +move=> f0 x; rewrite inE funenegE => Dx; apply/max_idPr. +by rewrite leeNl oppe0 f0. Qed. Lemma le0_funeposE f : (forall x, D x -> f x <= 0) -> {in D, f^\+ =1 cst 0}. -Proof. by move=> f0 x; rewrite inE => Dx; exact/max_idPr/f0. Qed. +Proof. by move=> f0 x; rewrite inE funeposE => Dx; exact/max_idPr/f0. Qed. Lemma le0_funenegE f : (forall x, D x -> f x <= 0) -> {in D, f^\- =1 \- f}. Proof. -by move=> f0 x; rewrite inE => Dx; apply/max_idPl; rewrite leeNr oppe0 f0. +move=> f0 x; rewrite inE funenegE => Dx; apply/max_idPl. +by rewrite leeNr oppe0 f0. Qed. Lemma ge0_funeposM r f : (0 <= r)%R -> (fun x => r%:E * f x)^\+ = (fun x => r%:E * (f^\+ x)). -Proof. by move=> ?; rewrite funeqE => x; rewrite /funepos maxe_pMr// mule0. Qed. +Proof. +move=> ?; rewrite funeqE => x. +by rewrite !funeposE maxe_pMr// mule0. +Qed. Lemma ge0_funenegM r f : (0 <= r)%R -> (fun x => r%:E * f x)^\- = (fun x => r%:E * (f^\- x)). Proof. -by move=> r0; rewrite funeqE => x; rewrite /funeneg -muleN maxe_pMr// mule0. +by move=> r0; rewrite funeqE => x; rewrite !funenegE -muleN maxe_pMr// mule0. Qed. Lemma le0_funeposM r f : (r <= 0)%R -> @@ -209,36 +225,36 @@ Qed. Lemma fune_abse f : abse \o f = f^\+ \+ f^\-. Proof. rewrite funeqE => x /=; have [fx0|/ltW fx0] := leP (f x) 0. -- rewrite lee0_abs// /funepos /funeneg. +- rewrite lee0_abs// funeposE funenegE. move/max_idPr : (fx0) => ->; rewrite add0e. by move: fx0; rewrite -{1}oppe0 leeNr => /max_idPl ->. -- rewrite gee0_abs// /funepos /funeneg; move/max_idPl : (fx0) => ->. +- rewrite gee0_abs// funeposE funenegE; move/max_idPl : (fx0) => ->. by move: fx0; rewrite -{1}oppe0 leeNl => /max_idPr ->; rewrite adde0. Qed. Lemma funeposneg f : f = (fun x => f^\+ x - f^\- x). Proof. -rewrite funeqE => x; rewrite /funepos /funeneg; have [|/ltW] := leP (f x) 0. +rewrite funeqE => x; rewrite funeposE funenegE; have [|/ltW] := leP (f x) 0. by rewrite -{1}oppe0 -leeNr => /max_idPl ->; rewrite oppeK add0e. by rewrite -{1}oppe0 -leeNl => /max_idPr ->; rewrite sube0. Qed. Lemma add_def_funeposneg f x : (f^\+ x +? - f^\- x). Proof. -by rewrite /funeneg /funepos; case: (f x) => [r| |]; +by rewrite funenegE funeposE; case: (f x) => [r| |]; [rewrite -fine_max/=|rewrite /maxe /= ltNyr|rewrite /maxe /= ltNyr]. Qed. Lemma funeD_Dpos f g : f \+ g = (f \+ g)^\+ \- (f \+ g)^\-. Proof. -apply/funext => x; rewrite /funepos /funeneg; have [|/ltW] := leP 0 (f x + g x). +apply/funext => x; rewrite funeposE funenegE; have [|/ltW] := leP 0 (f x + g x). - by rewrite -{1}oppe0 -leeNl => /max_idPr ->; rewrite sube0. - by rewrite -{1}oppe0 -leeNr => /max_idPl ->; rewrite oppeK add0e. Qed. Lemma funeD_posD f g : f \+ g = (f^\+ \+ g^\+) \- (f^\- \+ g^\-). Proof. -apply/funext => x; rewrite /funepos /funeneg. +apply/funext => x; rewrite !funeposE !funenegE. have [|fx0] := leP 0 (f x); last rewrite add0e. - rewrite -{1}oppe0 leeNl => /max_idPr ->; have [|/ltW] := leP 0 (g x). by rewrite -{1}oppe0 leeNl => /max_idPr ->; rewrite adde0 sube0. @@ -255,7 +271,7 @@ Qed. Lemma funepos_le f g : {in D, forall x, f x <= g x} -> {in D, forall x, f^\+ x <= g^\+ x}. Proof. -move=> fg x Dx; rewrite /funepos /maxe; case: ifPn => fx; case: ifPn => gx //. +move=> fg x Dx; rewrite !funeposE /maxe; case: ifPn => fx; case: ifPn => gx //. - by rewrite leNgt. - by move: fx; rewrite -leNgt => /(lt_le_trans gx); rewrite ltNge fg. - exact: fg. @@ -264,7 +280,7 @@ Qed. Lemma funeneg_le f g : {in D, forall x, f x <= g x} -> {in D, forall x, g^\- x <= f^\- x}. Proof. -move=> fg x Dx; rewrite /funeneg /maxe; case: ifPn => gx; case: ifPn => fx //. +move=> fg x Dx; rewrite !funenegE /maxe; case: ifPn => gx; case: ifPn => fx //. - by rewrite leNgt. - by move: gx; rewrite -leNgt => /(lt_le_trans fx); rewrite lteN2 ltNge fg. - by rewrite leeN2; exact: fg.