perf patch lebesgue_integral.v

theories/convex.v

@@ -226,7 +226,9 @@ have [c1 Ic1 Hc1] : exists2 c1, a < c1 < x & (f x - f a) / (x - a) = 'D_1 f c1.
     have := derivable_within_continuous HDf.
     rewrite continuous_open_subspace//; last exact: interval_open.
     by apply; rewrite inE/= in_itv/= ax.
-  by exists z => //; rewrite fxfa -mulrA divff ?mulr1// subr_eq0 gt_eqF.
+  exists z; first by [].
+  rewrite fxfa -mulrA divff; first exact: mulr1.
+  by rewrite subr_eq0 gt_eqF.
 have c1c2 : c1 < c2.
   by move: Ic2 Ic1 => /andP[+ _] => /[swap] /andP[_] /lt_trans; apply.
 have [d Id h] :
@@ -245,7 +247,9 @@ have [d Id h] :
     + apply: cvg_at_left_filter.
       move: cDf; rewrite continuous_open_subspace//; last exact: interval_open.
       by apply; rewrite inE/= in_itv/= (andP Ic2).2 (lt_trans (andP Ic1).1).
-  by exists z => //; rewrite h -mulrA divff ?mulr1// subr_eq0 gt_eqF.
+  exists z; first by [].
+  rewrite h -mulrA divff; first exact: mulr1.
+  by rewrite subr_eq0 gt_eqF.
 have LfE : L x - f x =
     ((x - a) * (b - x)) / (b - a) * ((f b - f x) / (b - x)) -
     ((b - x) * factor a b x) * ((f x - f a) / (x - a)).

theories/derive.v

@@ -563,14 +563,14 @@ Proof. by move=> df dg; apply/diff_unique; have [] := dadd df dg. Qed.
 Lemma differentiableD (f g : V -> W) x :
   differentiable f x -> differentiable g x -> differentiable (f + g) x.
 Proof.
-by move=> df dg; apply/diff_locallyP; rewrite diffD //; have := dadd df dg.
+by move=> df dg; apply/diff_locallyP; rewrite diffD; have := dadd df dg.
 Qed.
 
 Global Instance is_diffD (f g df dg : V -> W) x :
   is_diff x f df -> is_diff x g dg -> is_diff x (f + g) (df + dg).
 Proof.
 move=> dfx dgx; apply: DiffDef; first exact: differentiableD.
-by rewrite diffD // !diff_val.
+by rewrite diffD; first (congr (_ + _); apply: diff_val).
 Qed.
 
 Lemma differentiable_sum n (f : 'I_n -> V -> W) (x : V) :
@@ -606,7 +606,9 @@ Proof. by move=> dfx dgx; apply: is_diff_eq. Qed.
 Lemma diffB (f g : V -> W) x :
   differentiable f x -> differentiable g x ->
   'd (f - g) x = 'd f x \- 'd g x :> (V -> W).
-Proof. by move=> /differentiableP df /differentiableP dg; rewrite diff_val. Qed.
+Proof.
+by move=> /differentiableP df /differentiableP dg; rewrite [LHS]diff_val.
+Qed.
 
 Lemma differentiableB (f g : V -> W) x :
   differentiable f x -> differentiable g x -> differentiable (f \- g) x.
@@ -920,7 +922,9 @@ Qed.
 Lemma diffM (f g : V -> R) x :
   differentiable f x -> differentiable g x ->
   'd (f * g) x = f x \*: 'd g x + g x \*: 'd f x :> (V -> R).
-Proof. by move=> /differentiableP df /differentiableP dg; rewrite diff_val. Qed.
+Proof.
+by move=> /differentiableP df /differentiableP dg; rewrite [LHS]diff_val.
+Qed.
 
 Lemma differentiableM (f g : V -> R) x :
   differentiable f x -> differentiable g x -> differentiable (f * g) x.
@@ -1279,7 +1283,7 @@ evar (fg : R -> R); rewrite [X in X @ _](_ : _ = fg) /=; last first.
   rewrite scalerDr scalerA mulrC -scalerA.
   by rewrite [_ *: (g x *: _)]scalerA mulrC -scalerA /fg.
 apply: cvgD; last exact: cvgZr df.
-apply: cvg_comp2 (@mul_continuous _ (_, _)) => /=; last exact: dg.
+apply: cvg_comp2 (@scale_continuous _ _ (_, _)) => /=; last exact: dg.
 suff : {for 0, continuous (fun h : R => f(h *: v + x))}.
   by move=> /continuous_withinNx; rewrite scale0r add0r.
 exact/differentiable_continuous/derivable1_diffP/(derivable1P _ _ _).1.

theories/lebesgue_integral.v

@@ -3586,14 +3586,13 @@ suff: \int[mu]_(x in D) ((g1 \+ g2)^\+ x) + \int[mu]_(x in D) (g1^\- x) +
         apply: lte_add_pinfty; last exact: integral_funeneg_lt_pinfty.
         apply: lte_add_pinfty; last exact: integral_funeneg_lt_pinfty.
         exact: integral_funepos_lt_pinfty (integrableD _ _ _).
-      rewrite adde_ge0//; last exact: integral_ge0.
-      by rewrite adde_ge0// integral_ge0.
-    - by rewrite fin_num_adde_defr.
-  rewrite -(addeA (\int[mu]_(x in D) (g1 \+ g2)^\+ x)).
-  rewrite (addeC (\int[mu]_(x in D) (g1 \+ g2)^\+ x)) -[eqbLHS]addeA.
-  rewrite (addeC (\int[mu]_(x in D) g1^\- x + \int[mu]_(x in D) g2^\- x)).
-  rewrite eq_sym -(sube_eq g12pos) ?fin_num_adde_defl// => /eqP <-.
-  rewrite fin_num_oppeD; last first.
+      apply: adde_ge0; last exact: integral_ge0.
+      by apply: adde_ge0; apply: integral_ge0.
+    - exact/fin_num_adde_defr/g12pos.
+  rewrite -[X in X - _ == _]addeA [X in X - _ == _]addeC -[eqbLHS]addeA.
+  rewrite [eqbLHS]addeC eq_sym.
+  rewrite -(sube_eq g12pos) ?fin_num_adde_defl// => /eqP g12E.
+  rewrite -{}[LHS]g12E fin_num_oppeD; last first.
     rewrite ge0_fin_numE; first exact: integral_funeneg_lt_pinfty if2.
     exact: integral_ge0.
   by rewrite addeACA (integralE _ _ g1) (integralE _ _ g2).
@@ -3619,8 +3618,8 @@ rewrite (ge0_integralD mu mD); last 4 first.
   - by [].
   - exact/measurable_funepos/emeasurable_funD.
   - by [].
-  - exact/measurable_funeneg.
-move=> ->.
+  - exact/measurable_funepos/measurableT_comp.
+move=> g12E; rewrite {}[LHS]g12E.
 rewrite (ge0_integralD mu mD); last 4 first.
   - by move=> x _; exact: adde_ge0.
   - apply: emeasurable_funD; last exact: measurable_funepos.
@@ -5294,6 +5293,7 @@ have mfn : mu.-integrable E (fun z => `|f^\- z - (n_ n z)%:E|).
   apply/integrable_abse/integrableB => //; first exact: integrable_funeneg.
   exact: intn.
 rewrite -[x in (_ <= `|x|)%R]fineD // -integralD //.
+move: finfn finfp => _ _.
 rewrite !ger0_norm ?fine_ge0 ?integral_ge0 ?fine_le//.
 - by apply: integral_fune_fin_num => //; exact/integrable_abse/mfpn.
 - by apply: integral_fune_fin_num => //; exact: integrableD.
@@ -5397,8 +5397,9 @@ exists h; split => //; rewrite [eps%:num]splitr; apply: le_lt_trans.
   - apply: (measurable_funS mE) => //; do 2 apply: measurableT_comp => //.
     exact: measurable_funB.
   - by move=> z _; rewrite adde_ge0.
-  - apply: measurableT_comp => //; apply: measurable_funD => //;
-      apply: (measurable_funS mE) => //; (apply: measurableT_comp => //);
+  - apply: measurableT_comp => //; apply: measurable_funD;
+      apply: (measurable_funS mE (@subset_refl _ E));
+      (apply: measurableT_comp => //);
       exact: measurable_funB.
   - move=> x _; rewrite -(subrK (g x) (f x)) -(addrA (_ + _)%R) lee_fin.
     by rewrite ler_normD.
@@ -5573,15 +5574,16 @@ transitivity (\sum_(k \in range f)
   rewrite indic_fubini_tonelli1// -ge0_integralZl//; last by rewrite lee_fin.
   - exact: indic_measurable_fun_fubini_tonelli_F.
   - by move=> /= x _; exact: indic_fubini_tonelli_F_ge0.
-rewrite -ge0_integral_fsum //; last 2 first.
+rewrite -ge0_integral_fsum; last by [].
+  - apply: eq_integral => x _; rewrite sfun_fubini_tonelli_FE.
+    by under eq_fsbigr do rewrite indic_fubini_tonelli_FE//.
+  - by [].
   - by move=> r; apply/measurable_funeM/indic_measurable_fun_fubini_tonelli_F.
-  - move=> r x _; rewrite /fubini_F.
-    have [r0|r0] := leP 0%R r.
-      by rewrite mule_ge0//; exact: indic_fubini_tonelli_F_ge0.
-    rewrite integral0_eq ?mule0// => y _.
-    by rewrite preimage_nnfun0//= indicE in_set0.
-apply: eq_integral => x _; rewrite sfun_fubini_tonelli_FE.
-by under eq_fsbigr do rewrite indic_fubini_tonelli_FE//.
+move=> r x _; rewrite /fubini_F.
+have [r0|r0] := leP 0%R r.
+  by rewrite mule_ge0//; exact: indic_fubini_tonelli_F_ge0.
+rewrite integral0_eq ?mule0// => y _.
+by rewrite preimage_nnfun0//= indicE in_set0.
 Qed.
 
 Lemma sfun_fubini_tonelli2 : \int[m1 \x^ m2]_z (f z)%:E = \int[m2]_y G y.
@@ -5600,15 +5602,16 @@ transitivity (\sum_(k \in range f)
   rewrite indic_fubini_tonelli2// -ge0_integralZl//; last by rewrite lee_fin.
   - exact: indic_measurable_fun_fubini_tonelli_G.
   - by move=> /= x _; exact: indic_fubini_tonelli_G_ge0.
-rewrite -ge0_integral_fsum //; last 2 first.
+rewrite -ge0_integral_fsum; last by [].
+  - apply: eq_integral => x _; rewrite sfun_fubini_tonelli_GE.
+    by under eq_fsbigr do rewrite indic_fubini_tonelli_GE//.
+  - by [].
   - by move=> r; apply/measurable_funeM/indic_measurable_fun_fubini_tonelli_G.
-  - move=> r y _; rewrite /fubini_G.
-    have [r0|r0] := leP 0%R r.
-      by rewrite mule_ge0//; exact: indic_fubini_tonelli_G_ge0.
-    rewrite integral0_eq ?mule0// => x _.
-    by rewrite preimage_nnfun0//= indicE in_set0.
-apply: eq_integral => x _; rewrite sfun_fubini_tonelli_GE.
-by under eq_fsbigr do rewrite indic_fubini_tonelli_GE//.
+move=> r y _; rewrite /fubini_G.
+have [r0|r0] := leP 0%R r.
+  by rewrite mule_ge0//; exact: indic_fubini_tonelli_G_ge0.
+rewrite integral0_eq ?mule0// => x _.
+by rewrite preimage_nnfun0//= indicE in_set0.
 Qed.
 
 Lemma sfun_fubini_tonelli :
@@ -5841,9 +5844,12 @@ Qed.
 Let integrable_Fplus : m1.-integrable setT Fplus.
 Proof.
 apply/integrableP; split=> //.
-apply: le_lt_trans (fubini1a.1 imf); apply: ge0_le_integral => //.
-- exact: measurableT_comp.
+apply: le_lt_trans (fubini1a.1 imf); apply: ge0_le_integral.
+- by [].
+- by [].
+- by apply: measurableT_comp; last apply: measurable_Fplus.
 - by move=> x _; exact: integral_ge0.
+- exact: measurable_fun1.
 - move=> x _; apply: le_trans.
     apply: le_abse_integral => //; apply: measurableT_comp => //.
     exact: measurable_funepos.
@@ -5901,9 +5907,12 @@ Proof. by rewrite GE; exact: emeasurable_funB. Qed.
 Let integrable_Gplus : m2.-integrable setT Gplus.
 Proof.
 apply/integrableP; split=> //.
-apply: le_lt_trans (fubini1b.1 imf); apply: ge0_le_integral => //.
-- exact: measurableT_comp.
+apply: le_lt_trans (fubini1b.1 imf). apply: ge0_le_integral.
+- by [].
+- by [].
+- by apply: measurableT_comp; last apply: measurable_Gplus.
 - by move=> *; exact: integral_ge0.
+- exact: measurable_fun2.
 - move=> y _; apply: le_trans.
     apply: le_abse_integral => //; apply: measurableT_comp => //.
     exact: measurable_funepos.
@@ -5917,9 +5926,12 @@ Qed.
 Let integrable_Gminus : m2.-integrable setT Gminus.
 Proof.
 apply/integrableP; split=> //.
-apply: le_lt_trans (fubini1b.1 imf); apply: ge0_le_integral => //.
+apply: le_lt_trans (fubini1b.1 imf); apply: ge0_le_integral.
+- by [].
+- by [].
 - exact: measurableT_comp.
 - by move=> *; exact: integral_ge0.
+- exact: measurable_fun2.
 - move=> y _; apply: le_trans.
     apply: le_abse_integral => //; apply: measurableT_comp => //.
     exact: measurable_funeneg.
@@ -6351,12 +6363,13 @@ have ? : k <= \int[mu]_(z in ball y (r + d)) `|(f z)%:E|.
   by apply: measurable_funTS; do 2 apply: measurableT_comp => //.
 have afxrdi : a%:E < (fine (mu (ball x (r + d))))^-1%:E *
     \int[mu]_(z in ball y (r + d)) `|(f z)%:E|.
-  by rewrite (lt_le_trans axrdk)// lee_wpmul2l// lee_fin invr_ge0// fine_ge0.
+  apply/(lt_le_trans axrdk)/lee_wpmul2l => //.
+  by rewrite lee_fin invr_ge0 fine_ge0.
 have /lt_le_trans : a%:E < iavg f (ball y (r + d)).
   apply: (lt_le_trans afxrdi); rewrite /iavg.
   do 2 (rewrite lebesgue_measure_ball; last by rewrite addr_ge0// ltW).
-  rewrite lee_wpmul2l// lee_fin invr_ge0// fine_ge0//= lee_fin pmulrn_rge0//.
-  by rewrite addr_gt0.
+  rewrite lee_wpmul2l ?lexx// lee_fin invr_ge0// fine_ge0//= lee_fin.
+  by rewrite pmulrn_rge0// addr_gt0.
 apply; apply: ereal_sup_ubound => /=.
 by exists (r + d)%R => //; rewrite in_itv/= andbT addr_gt0.
 Unshelve. all: by end_near. Qed.

theories/measure.v

@@ -4890,20 +4890,20 @@ apply: (@le_trans _ _ (limn BA + limn BNA)); [apply: leeD|].
     apply: (@le_trans _ _ (mu_ext mu (\bigcup_k (B k `\` A)))).
       by apply: le_mu_ext; rewrite -setI_bigcupl; exact: setISS.
     exact: outer_measure_sigma_subadditive.
-have ? : cvg (BNA @ \oo) by exact: is_cvg_nneseries.
-have ? : cvg (BA @ \oo) by exact: is_cvg_nneseries.
-have ? : cvg (eseries (Rmu \o B) @ \oo) by exact: is_cvg_nneseries.
+have cBNA : cvg (BNA @ \oo) by exact: is_cvg_nneseries.
+have cBA : cvg (BA @ \oo) by exact: is_cvg_nneseries.
+have cB : cvg (eseries (Rmu \o B) @ \oo) by exact: is_cvg_nneseries.
 have [def|] := boolP (lim (BA @ \oo) +? lim (BNA @ \oo)); last first.
   rewrite /adde_def negb_and !negbK=> /orP[/andP[BAoo BNAoo]|/andP[BAoo BNAoo]].
   - suff -> : limn (eseries (Rmu \o B)) = +oo by rewrite leey.
-    apply/eqP; rewrite -leye_eq -(eqP BAoo); apply/lee_lim => //.
+    apply/eqP; rewrite -leye_eq -(eqP BAoo); apply/(lee_lim cBA cB).
     near=> n; apply: lee_sum => m _; apply: le_measure; rewrite /mkset; by
       [rewrite inE; exact: measurableI | rewrite inE | apply: subIset; left].
   - suff -> : limn (eseries (Rmu \o B)) = +oo by rewrite leey.
-    apply/eqP; rewrite -leye_eq -(eqP BNAoo); apply/lee_lim => //.
+    apply/eqP; rewrite -leye_eq -(eqP BNAoo); apply/(lee_lim cBNA cB).
     by near=> n; apply: lee_sum => m _; rewrite -setDE; apply: le_measure;
        rewrite /mkset ?inE//; apply: measurableD.
-rewrite -limeD // (_ : (fun _ => _) =
+rewrite -(limeD cBA cBNA) // (_ : (fun _ => _) =
     eseries (fun k => Rmu (B k `&` A) + Rmu (B k `&` ~` A))); last first.
   by rewrite funeqE => n; rewrite -big_split /=; exact: eq_bigr.
 apply/lee_lim => //.

theories/probability.v

@@ -594,8 +594,9 @@ have h (Y : {RV P >-> R}) :
     - by move=> r _; exact: sqr_ge0.
     - move=> x y; rewrite !nnegrE => x0 y0.
       by rewrite ler_sqr.
-  apply: expectation_le => //.
+  apply: expectation_le.
     - by apply: measurableT_comp => //; exact: measurableT_comp.
+  - by [].
   - by move=> x /=; exact: sqr_ge0.
   - by move=> x /=; exact: sqr_ge0.
   - by apply/aeW => t /=; rewrite real_normK// num_real.

theories/realfun.v

@@ -2454,7 +2454,7 @@ case=> ? [l + <- <-]; rewrite -/(total_variation x b f).
 move: l => [|i j].
   by move=> /itv_partition_nil /eqP; rewrite lt_eqF.
 move=> [/= /andP[xi ij /eqP ijb]] tv_eps.
-apply: filter_app (nbhs_right_ge _).
+apply: (filter_app _ _ (nbhs_right_ge _)).
 apply: filter_app (nbhs_right_lt xi).
 have e20 : 0 < eps%:num / 2 by [].
 move/cvgrPdist_lt/(_ (eps%:num/2) e20) : ctsf; apply: filter_app.
@@ -2552,7 +2552,7 @@ have /near_eq_cvg/cvg_trans : {near (- x)^'+,
     (fun t => fine (TV (- b) (- a) (f \o -%R)) - fine (TV (- b) t (f \o -%R))) =1
     (fine \o (TV a)^~ f) \o -%R}.
   apply: filter_app (nbhs_right_lt xa).
-  apply: filter_app (nbhs_right_ge _).
+  apply: (filter_app _ _ (nbhs_right_ge _)).
   near=> t => xt ta; have ? : -b <= t by exact: (le_trans bx).
   have ? : t <= -a by exact: ltW.
   apply/eqP; rewrite eq_sym -subr_eq opprK addrC.

theories/trigo.v

@@ -482,7 +482,7 @@ rewrite -seriesN lt_sum_lim_series //.
 move=> d.
 rewrite /cos_coeff' 2!exprzD_nat (exprSz _ d.*2) -[in (-1) ^ d.*2](muln2 d).
 rewrite -(exprnP _ (d * 2)) (exprM (-1)) sqrr_sign 2!mulr1 -exprSzr.
-rewrite (_ : 4 = 2 * 2)%N // -(exprnP _ (2 * 2)) (exprM (-1)) sqrr_sign.
+rewrite -[4%Z]/(_ (2 * 2))%N -(exprnP _ (2 * 2)) (exprM (-1)) sqrr_sign.
 rewrite mul1r [(-1) ^ 3](_ : _ = -1) ?mulN1r ?mulNr ?opprK; last first.
   by rewrite -exprnP 2!exprS expr1 mulrN1 opprK mulr1.
 rewrite subr_gt0.