diff --git a/theories/convex.v b/theories/convex.v index dde76d9a1..fbd28dd43 100644 --- a/theories/convex.v +++ b/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)). diff --git a/theories/derive.v b/theories/derive.v index f1c1fd31d..9cd9384f8 100644 --- a/theories/derive.v +++ b/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. diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v index a882d3053..187ee9f08 100644 --- a/theories/lebesgue_integral.v +++ b/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). @@ -3620,7 +3619,7 @@ rewrite (ge0_integralD mu mD); last 4 first. - exact/measurable_funepos/emeasurable_funD. - by []. - exact/measurable_funeneg. -move=> ->. +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. diff --git a/theories/measure.v b/theories/measure.v index 527b029ea..96e695153 100644 --- a/theories/measure.v +++ b/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 => //. diff --git a/theories/probability.v b/theories/probability.v index 11f4d758c..1ff17ee46 100644 --- a/theories/probability.v +++ b/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. diff --git a/theories/realfun.v b/theories/realfun.v index a9764f421..235f87458 100644 --- a/theories/realfun.v +++ b/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. diff --git a/theories/trigo.v b/theories/trigo.v index 5da3ff7ce..18735a73a 100644 --- a/theories/trigo.v +++ b/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.