Lock funepos and funeneg

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

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 <oo | P i) f i = esum P f^\+ - esum P f^\-.
 Proof.
-move=> 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.

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 <oo) \int[mu]_(x in F i) g^\+ x) -
   rewrite ge0_integral_bigcup//; last first.
     by apply: measurable_funepos; case/integrableP : fi.
   rewrite ge0_integral_bigcup//.
-    apply: measurable_funepos; apply: measurableT_comp => //.
+    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.

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

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.