From c211b5eb15c8e7810151cbf0ba463a33e950c86e Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Wed, 19 Jul 2023 23:52:47 +0900 Subject: [PATCH 1/4] minor generalizations, renaming --- CHANGELOG_UNRELEASED.md | 8 ++++++ theories/lebesgue_integral.v | 2 +- theories/lebesgue_measure.v | 4 +-- theories/sequences.v | 53 +++++++++++++++++++++++++----------- 4 files changed, 48 insertions(+), 19 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 455a55a98..d2c3f93d8 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -79,6 +79,8 @@ - in `constructive_ereal.v`: + lemmas `lte_pmulr`, `lte_pmull`, `lte_nmulr`, `lte_nmull` + lemmas `lte0n`, `lee0n`, `lte1n`, `lee1n` +- in `sequences.v`: + + lemma `eseries_cond` ### Changed @@ -91,6 +93,9 @@ - in `exp.v`: + lemmas `power_posD` (now `powRD`), `power_posB` (now `powRB`) +- in `sequences.v`: + + lemma `nneseriesrM` generalized and renamed to `nneseriesZl` + ### Renamed - in `boolp.v`: @@ -177,6 +182,9 @@ (from measure to content) + lemma `subset_measure0` (from `realType` to `realFieldType`) +- in `sequences.v`: + + lemmas `eq_eseriesr`, `lee_nneseries` + ### Deprecated ### Removed diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v index 3d201b891..57a48de42 100644 --- a/theories/lebesgue_integral.v +++ b/theories/lebesgue_integral.v @@ -2673,7 +2673,7 @@ rewrite ge0_integral_fsum//; last 2 first. transitivity (\sum_(i \in range f) (\sum_(n r _. - rewrite integralZl_indic_nnsfun// integral_measure_series_indic// nneseriesrM//. + rewrite integralZl_indic_nnsfun// integral_measure_series_indic// nneseriesZl//. by move=> n _; apply: integral_ge0 => t _; rewrite lee_fin. rewrite fsbig_finite//= -nneseries_sum; last first. move=> r j _. diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v index dd0b3aed1..08a223d7a 100644 --- a/theories/lebesgue_measure.v +++ b/theories/lebesgue_measure.v @@ -2076,9 +2076,9 @@ apply/uniform_restrict_cvg => /= U /=; rewrite ?uniform_nbhsT. case/nbhs_ex => del /filterS; apply. have [N _ /(_ N)/(_ (leqnn _)) Ndel] := near_infty_natSinv_lt del. exists (badn N) => // r badNr x. -rewrite /patch; case xAB: (x \in A`\`_) => //; apply: (lt_trans _ Ndel). +rewrite /patch; case xAB: (x \in A `\` _) => //; apply: (lt_trans _ Ndel). move/set_mem: xAB; rewrite setDE; case => Ax; rewrite setC_bigcup => /(_ N I). -rewrite /E setC_bigcup => /(_ (r)) /=; rewrite /h => /(_ badNr) /not_andP [] //. +rewrite /E setC_bigcup => /(_ r) /=; rewrite /h => /(_ badNr) /not_andP [] //. by move/negP; rewrite real_ltNge // distrC. Qed. diff --git a/theories/sequences.v b/theories/sequences.v index f1b6a29b1..7591a38c1 100644 --- a/theories/sequences.v +++ b/theories/sequences.v @@ -1571,9 +1571,26 @@ Lemma ereal_nondecreasing_series (R : realDomainType) (u_ : (\bar R)^nat) nondecreasing_seq (fun n => \sum_(0 <= i < n | P i) u_ i). Proof. by move=> u_ge0 n m nm; rewrite lee_sum_nneg_natr// => k _ /u_ge0. Qed. -Lemma eq_eseriesr (R : realFieldType) (f g : (\bar R)^nat) (P : pred nat) : +Lemma eseries_cond {R : numFieldType} (f : nat -> \bar R) P N : + \sum_(N <= i n /=; have [Nn|nN] := leqP N n; last first. + rewrite [in LHS]/index_iota (@size0nil _ (iota _ _)) ?big_nil; last first. + by apply/eqP; rewrite size_iota subn_eq0 ltnW. + rewrite /index_iota subn0 big_seq_cond big1// => /= k. + rewrite mem_iota add0n leq0n/= => /andP[+ _]. + by move/ltn_trans/(_ nN); rewrite ltnNge => /negbTE ->. +rewrite {2}/index_iota subn0 -[in RHS](@subnKC N n)// iotaD big_cat/= add0n. +rewrite [X in _ = X + _]big_seq_cond [X in _ = X + _]big1 ?adde0 /=; last first. + move=> i; rewrite mem_iota add0n leq0n/= => /andP[+ _]. + by rewrite ltnNge => /negbTE ->. +rewrite add0e [LHS]big_seq_cond [RHS]big_seq_cond; apply: eq_bigr => /= k. +by rewrite mem_iota subnKC// => /andP[/andP[-> _]]. +Qed. + +Lemma eq_eseriesr (R : numFieldType) (f g : (\bar R)^nat) (P : pred nat) {N} : (forall i, P i -> f i = g i) -> - \sum_(i efg; congr (lim _); apply/funext => n; exact: eq_bigr. Qed. Lemma eq_eseriesl (R : realFieldType) (P Q : pred nat) (f : (\bar R)^nat) : @@ -1658,7 +1675,9 @@ Proof. by move=> u_le0; apply: is_cvg_ereal_npos_natsum_cond => n /u_le0. Qed. Lemma is_cvg_nneseries_cond P N : (forall n, P n -> 0 <= u_ n) -> cvg (fun n => \sum_(N <= i < n | P i) u_ i). -Proof. by move=> u_ge0; apply: is_cvg_ereal_nneg_natsum_cond => n _ /u_ge0. Qed. +Proof. +by move=> u_ge0; apply: is_cvg_ereal_nneg_natsum_cond => n _; exact: u_ge0. +Qed. Lemma is_cvg_npeseries_cond P N : (forall n, P n -> u_ n <= 0) -> cvg (fun n => \sum_(N <= i < n | P i) u_ i). @@ -1688,6 +1707,7 @@ Qed. End cvg_eseries. Arguments is_cvg_nneseries {R}. +Arguments nneseries_ge0 {R u_ P} N. Lemma nnseries_is_cvg {R : realType} (u : nat -> R) : (forall i, 0 <= u i)%R -> \sum_(k cvg (series u). @@ -1703,9 +1723,9 @@ rewrite /ubound/= => _ [n _ <-]; rewrite -lee_fin fineK//; last first. by rewrite -sumEFin; apply: nneseries_lim_ge => i _; rewrite lee_fin. Qed. -Lemma nneseriesrM (R : realType) (f : nat -> \bar R) (P : pred nat) x : +Lemma nneseriesZl (R : realType) (f : nat -> \bar R) (P : pred nat) x N : (forall i, P i -> 0 <= f i) -> - (\sum_(i f0; rewrite -limeMl//; last exact: is_cvg_nneseries. by congr (lim _); apply/funext => /= n; rewrite ge0_sume_distrr. @@ -1755,15 +1775,16 @@ move=> u_ge0 Pk ukoo; apply: (eseries_pinfty _ Pk ukoo) => // n Pn. by rewrite gt_eqF// (lt_le_trans _ (u_ge0 _ Pn)). Qed. -Lemma lee_nneseries (R : realType) (u v : (\bar R)^nat) (P : pred nat) : - (forall i, P i -> 0 <= u i) -> (forall n, P n -> u n <= v n) -> - \sum_(i 0 <= u i) -> + (forall n, P n -> u n <= v n) -> + \sum_(N <= i u0 Puv; apply: lee_lim. -- by apply: is_cvg_ereal_nneg_natsum_cond => n _ /u0. +- by apply: is_cvg_ereal_nneg_natsum_cond => n ? /u0; exact. - apply: is_cvg_ereal_nneg_natsum_cond => n _ Pn. by rewrite (le_trans _ (Puv _ Pn))// u0. -- by near=> n; exact: lee_sum. +- by near=> n; apply: lee_sum => k; exact: Puv. Unshelve. all: by end_near. Qed. Lemma lee_npeseries (R : realType) (u v : (\bar R)^nat) (P : pred nat) : @@ -1951,10 +1972,10 @@ rewrite big_nat_recr// -IHn/= -nneseriesD//; last by move=> i; rewrite sume_ge0. by congr (lim _); apply/funext => m; apply: eq_bigr => i _; rewrite big_nat_recr. Qed. -Lemma nneseries_sum I (r : seq I) (P : {pred I}) - [R : realType] [f : I -> nat -> \bar R] : - (forall i j, P i -> 0 <= f i j) -> - \sum_(j nat -> \bar R] : (forall i j, P i -> 0 <= f i j) -> + \sum_(j f_ge0; case Dr : r => [|i r']; rewrite -?{}[_ :: _]Dr. by rewrite big_nil eseries0// => i; rewrite big_nil. @@ -2635,8 +2656,8 @@ have [q_gt0 | | q0] := ltrgt0P q%:num. - near=> n => /=; apply: (le_lt_trans (@ctrfq (_, _) _)) => //=. + split; last exact: funS. by apply: closed_cvg contraction_cvg => //; apply: nearW => ?; exact: funS. - + rewrite -ltr_pdivl_mull //; near: n; move/cvgrPdist_lt: contraction_cvg; apply. - by rewrite mulr_gt0 // invr_gt0. + + rewrite -ltr_pdivl_mull //; near: n; move/cvgrPdist_lt: contraction_cvg. + by apply; rewrite mulr_gt0 // invr_gt0. - by rewrite ltNge//; exact: contraNP. - apply: nearW => /= n; apply: (le_lt_trans (@ctrfq (_, _) _)). + split; last exact: funS. From 6b09cee9daf99863a871830f4f74d578331894f2 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Wed, 19 Jul 2023 17:21:51 +0200 Subject: [PATCH 2/4] decomposing eseries_cond into bits --- theories/sequences.v | 25 ++++++++++--------------- 1 file changed, 10 insertions(+), 15 deletions(-) diff --git a/theories/sequences.v b/theories/sequences.v index 7591a38c1..6f0842f0a 100644 --- a/theories/sequences.v +++ b/theories/sequences.v @@ -1572,21 +1572,16 @@ Lemma ereal_nondecreasing_series (R : realDomainType) (u_ : (\bar R)^nat) Proof. by move=> u_ge0 n m nm; rewrite lee_sum_nneg_natr// => k _ /u_ge0. Qed. Lemma eseries_cond {R : numFieldType} (f : nat -> \bar R) P N : - \sum_(N <= i n /=; have [Nn|nN] := leqP N n; last first. - rewrite [in LHS]/index_iota (@size0nil _ (iota _ _)) ?big_nil; last first. - by apply/eqP; rewrite size_iota subn_eq0 ltnW. - rewrite /index_iota subn0 big_seq_cond big1// => /= k. - rewrite mem_iota add0n leq0n/= => /andP[+ _]. - by move/ltn_trans/(_ nN); rewrite ltnNge => /negbTE ->. -rewrite {2}/index_iota subn0 -[in RHS](@subnKC N n)// iotaD big_cat/= add0n. -rewrite [X in _ = X + _]big_seq_cond [X in _ = X + _]big1 ?adde0 /=; last first. - move=> i; rewrite mem_iota add0n leq0n/= => /andP[+ _]. - by rewrite ltnNge => /negbTE ->. -rewrite add0e [LHS]big_seq_cond [RHS]big_seq_cond; apply: eq_bigr => /= k. -by rewrite mem_iota subnKC// => /andP[/andP[-> _]]. -Qed. + \sum_(N <= i n /=; apply: big_nat_widenl. Qed. + +Lemma eseries_mkcondl {R : numFieldType} (f : nat -> \bar R) P Q : + \sum_(i n; rewrite big_mkcondl. Qed. + +Lemma eseries_mkcondr {R : numFieldType} (f : nat -> \bar R) P Q : + \sum_(i n; rewrite big_mkcondr. Qed. Lemma eq_eseriesr (R : numFieldType) (f g : (\bar R)^nat) (P : pred nat) {N} : (forall i, P i -> f i = g i) -> From ae266942bb773b03724c45bf2e020d6cc5e57bb5 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 20 Jul 2023 18:28:46 +0900 Subject: [PATCH 3/4] changelog --- CHANGELOG_UNRELEASED.md | 1 + 1 file changed, 1 insertion(+) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index d2c3f93d8..4671f5b16 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -81,6 +81,7 @@ + lemmas `lte0n`, `lee0n`, `lte1n`, `lee1n` - in `sequences.v`: + lemma `eseries_cond` + + lemmas `eseries_mkcondl`, `eseries_mkcondr` ### Changed From f469b5a98f5bc4b0911363a1c528615173371b92 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Sat, 29 Jul 2023 07:34:22 +0900 Subject: [PATCH 4/4] fix CI --- theories/normedtype.v | 12 ++++++------ theories/probability.v | 6 +++--- theories/reals.v | 2 +- 3 files changed, 10 insertions(+), 10 deletions(-) diff --git a/theories/normedtype.v b/theories/normedtype.v index 55a5cb339..4970e3caf 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -3714,8 +3714,8 @@ rewrite -[edist (x, y)]fineK//; apply: cvg_EFin. by have := edist_fin_open efin; apply: filter_app; near=> w. move=> U /=; rewrite nbhs_simpl/= -nbhs_ballE. move=> [] _/posnumP[r] distrU; rewrite nbhs_simpl /=. -have r2p : 0 < r%:num / 4 by rewrite divr_gt0// ltr0n. -exists (ball x (r%:num / 4), ball y (r%:num / 4)). +have r2p : 0 < r%:num / 4%:R by rewrite divr_gt0// ltr0n. +exists (ball x (r%:num / 4%:R), ball y (r%:num / 4%:R)). by split => //=; rewrite nbhs_ballE; exact: (@nbhsx_ballx _ _ _ (@PosNum _ _ r2p)). case => a b /= [/ball_sym xar yar]; apply: distrU => /=. @@ -3724,11 +3724,11 @@ have abxy : (edist (a, b) <= edist (a, x) + edist (x, y) + edist (y, b))%E. have abfin : edist (a, b) \is a fin_num. rewrite ge0_fin_numE// (le_lt_trans abxy)//. by apply: lte_add_pinfty; [apply: lte_add_pinfty|]; - rewrite -ge0_fin_numE //; apply/edist_finP; exists (r%:num / 4). + rewrite -ge0_fin_numE //; apply/edist_finP; exists (r%:num / 4%:R). have xyabfin : `|edist (x, y) - edist (a, b)|%E \is a fin_num. by rewrite abse_fin_num fin_numB abfin efin. -have daxr : edist (a, x) \is a fin_num by apply/edist_finP; exists (r%:num / 4). -have dybr : edist (y, b) \is a fin_num by apply/edist_finP; exists (r%:num / 4). +have daxr : edist (a, x) \is a fin_num by apply/edist_finP; exists (r%:num / 4%:R). +have dybr : edist (y, b) \is a fin_num by apply/edist_finP; exists (r%:num / 4%:R). rewrite -fineB// -fine_abse ?fin_numB ?abfin ?efin//. rewrite (@le_lt_trans _ _ (fine (edist (a, x) + edist (y, b))))//. rewrite fine_le// ?fin_numD ?daxr ?dybr//. @@ -3739,7 +3739,7 @@ rewrite (@le_lt_trans _ _ (fine (edist (a, x) + edist (y, b))))//. rewrite lte0_abs ?subre_lt0// oppeB ?fin_num_adde_defr// addeC. by rewrite lee_subl_addr// addeAC. rewrite fineD // [_%:num]splitr. -have r42 : r%:num / 4 < r%:num / 2. +have r42 : r%:num / 4%:R < r%:num / 2. by rewrite ltr_pmul2l// ltf_pinv ?posrE ?ltr0n// ltr_nat. by apply: ltr_add; rewrite (le_lt_trans _ r42)// -lee_fin fineK // edist_fin. Unshelve. end_near. Qed. diff --git a/theories/probability.v b/theories/probability.v index 25ea47399..38947401c 100644 --- a/theories/probability.v +++ b/theories/probability.v @@ -488,8 +488,8 @@ rewrite -sqrteM ?variance_ge0//. rewrite lee_sqrE ?sqrte_ge0// sqr_sqrte ?mule_ge0 ?variance_ge0//. rewrite -(fineK (variance_fin_num X1 X2)) -(fineK (variance_fin_num Y1 Y2)). rewrite -(fineK (covariance_fin_num X1 Y1 XY1)). -rewrite -EFin_expe -EFinM lee_fin -(@ler_pmul2l _ 4) ?ltr0n// [leRHS]mulrA. -rewrite [in leLHS](_ : 4 = 2 * 2)%R -natrM// natrM mulrACA -expr2 -subr_le0. +rewrite -EFin_expe -EFinM lee_fin -(@ler_pmul2l _ 4%:R) ?ltr0n// [leRHS]mulrA. +rewrite [in leLHS](natrM _ 2 2) mulrACA -expr2 -subr_le0. apply: deg_le2_ge0 => r; rewrite -lee_fin !EFinD. rewrite EFinM fineK ?variance_fin_num// muleC -varianceZ//. rewrite -mulrA EFinM mulrC EFinM ?fineK ?covariance_fin_num// -covarianceZl//. @@ -630,7 +630,7 @@ pose u0 := (fine 'V_P[X] / lambda)%R. have u0ge0 : (0 <= u0)%R. by apply: divr_ge0 (ltW lambda_gt0); rewrite -lee_fin finVK variance_ge0. apply: le_trans (le _ u0ge0) _; rewrite lee_fin le_eqVlt; apply/orP; left. -rewrite eqr_div; [|apply: lt0r_neq0..]; last 2 first. +rewrite GRing.eqr_div; [|apply: lt0r_neq0..]; last 2 first. - by rewrite exprz_gt0 -1?[ltLHS]addr0 ?ltr_le_add. - by rewrite ltr_paddl ?fine_ge0 ?variance_ge0 ?exprz_gt0. apply/eqP; have -> : fine 'V_P[X] = (u0 * lambda)%R. diff --git a/theories/reals.v b/theories/reals.v index 62bd83734..b401650ba 100644 --- a/theories/reals.v +++ b/theories/reals.v @@ -460,7 +460,7 @@ apply: le_anti; apply/andP; split. by move=> ? [p Ap [q Bq] <-]; apply: ler_add; exact: sup_ub. rewrite real_leNgt ?num_real// -subr_gt0; apply/negP. set eps := (_ + _ - _) => epos. -have e2pos : 0 < eps / 2 by rewrite divr_gt0// ltr0n. +have e2pos : 0 < eps / 2%:R by rewrite divr_gt0// ltr0n. have [r Ar supBr] := sup_adherent e2pos supA. have [s Bs supAs] := sup_adherent e2pos supB. have := ltr_add supBr supAs.