From d22e2dc28a51715c97d9735c2b58b4fbab0fec61 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 1 Jul 2025 14:15:59 +0900 Subject: [PATCH] fixes #1463 --- CHANGELOG_UNRELEASED.md | 16 ++++ theories/derive.v | 12 +-- theories/exp.v | 2 +- theories/gauss_integral.v | 4 +- theories/normedtype_theory/normed_module.v | 104 +++++++++++++-------- theories/pi_irrational.v | 2 +- theories/sequences.v | 12 +-- 7 files changed, 99 insertions(+), 53 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index b5f05e6a97..4092f4f4a8 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -241,6 +241,22 @@ - in `lebesgue_integral_fubiniv.`: + `fubini1` -> `integral12_prod_meas1` + `fubini2` -> `integral21_prod_meas1` +- in `normed_module.v`: + + `cvgZl` -> `cvgZr_tmp` + + `is_cvgZl` -> `is_cvgZr_tmp` + + `cvgZr` -> `cvgZl_tmp` + + `is_cvgZr` -> `is_cvgZl_tmp` + + `is_cvgZrE` -> `is_cvgZlE` + + `cvgMl` -> `cvgMr_tmp` + + `cvgMr` -> `cvgMl_tmp` + + `is_cvgMr` -> `is_cvgMl_tmp` + + `is_cvgMrE` -> `is_cvgMlE_tmp` + + `is_cvgMl` -> `is_cvgMr_tmp` + + `is_cvgMlE` -> `is_cvgMrE_tmp` + + `limZl` -> `limZr_tmp` + + `limZr` -> `limZl_tmp` + + `continuousZr` -> `continuousZl_tmp` + + `continuousZl` -> `continuousZr_tmp` ### Generalized diff --git a/theories/derive.v b/theories/derive.v index 419c54179a..4669920fdd 100644 --- a/theories/derive.v +++ b/theories/derive.v @@ -322,7 +322,7 @@ apply: cvg_lim => //. pose g1 : R -> W := fun h => (h^-1 * h) *: 'd f a v. pose g2 : R -> W := fun h : R => h^-1 *: k (h *: v ). rewrite (_ : g = g1 + g2) ?funeqE // -(addr0 (_ _ v)); apply: cvgD. - rewrite -(scale1r (_ _ v)); apply: cvgZl => /= X [e e0]. + rewrite -(scale1r (_ _ v)); apply: cvgZr_tmp => /= X [e e0]. rewrite /ball_ /= => eX. apply/nbhs_ballP. by exists e => //= x _ x0; apply eX; rewrite mulVr // ?unitfE //= subrr normr0. @@ -434,7 +434,7 @@ Fact dscale (f : V -> W) k x : differentiable f x -> continuous (k \*: 'd f x) /\ (k *: f) \o shift x = cst ((k *: f) x) + k \*: 'd f x +o_ 0 id. Proof. -move=> df; split; first by move=> ?; apply: continuousZr. +move=> df; split; first by move=> ?; apply: continuousZl_tmp. apply/eqaddoE; rewrite funeqE => y /=. by rewrite -[(k *: f) _]/(_ *: _) diff_locallyx // !scalerDr scaleox. Qed. @@ -447,7 +447,7 @@ Fact dscalel (k : V -> R) (f : W) x : cst (k x *: f) + (fun z => 'd k x z *: f) +o_ 0 id. Proof. move=> df; split. - move=> ?; exact/continuousZl/diff_continuous. + move=> ?; exact/continuousZr_tmp/diff_continuous. apply/eqaddoE; rewrite funeqE => y /=. by rewrite diff_locallyx //= !scalerDl scaleolx. Qed. @@ -945,7 +945,7 @@ move=> xn0; suff: continuous (fun h : R => - (1 / x) ^+ 2 *: h) /\ rewrite !mul1r !GRing.exprVn. rewrite (_ : (fun x => x^-1) = (fun x => 1 / x ))//. by rewrite funeqE => y; rewrite mul1r. -split; first by move=> ?; apply: continuousZr. +split; first by move=> ?; exact: continuousZl_tmp. apply/eqaddoP => _ /posnumP[e]; near=> h. rewrite -[(_ + _ : R -> R) h]/(_ + _) -[(- _ : R -> R) h]/(- _) /=. rewrite opprD scaleNr opprK /cst /=. @@ -1222,7 +1222,7 @@ Proof. move=> df; evar (h : R -> W); rewrite [X in X @ _](_ : _ = h) /=; last first. rewrite funeqE => r. by rewrite scalerBr !scalerA mulrC -!scalerA -!scalerBr /h. -exact: cvgZr. +exact: cvgZl_tmp. Qed. Lemma deriveZ f (k : R) (x v : V) : derivable f x v -> @@ -1285,7 +1285,7 @@ evar (fg : R -> R); rewrite [X in X @ _](_ : _ = fg) /=; last first. by rewrite !scalerBr -addrA ![g x *: _]mulrC addKr. rewrite scalerDr scalerA mulrC -scalerA. by rewrite [_ *: (g x *: _)]scalerA mulrC -scalerA /fg. -apply: cvgD; last exact: cvgZr df. +apply: cvgD; last exact: cvgZl_tmp df. 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. diff --git a/theories/exp.v b/theories/exp.v index d4e0311dfd..ba7fec0374 100644 --- a/theories/exp.v +++ b/theories/exp.v @@ -223,7 +223,7 @@ suff Cc : limn (h^-1 *: (series (shx h - sx))) @[h --> 0^'] --> limn (series s). move=> t; rewrite /ball /= sub0r normrN => H tNZ. rewrite (lt_le_trans H)// ler_pdivrMr // mulr2n mulrDr mulr1. by rewrite ler_wpDr // subr_ge0 ltW. - rewrite limZr; last exact/is_cvg_seriesB/Csx. + rewrite limZl_tmp; last exact/is_cvg_seriesB/Csx. by rewrite lim_seriesB; last exact: Csx. apply: cvg_zero => /=. suff Cc : limn diff --git a/theories/gauss_integral.v b/theories/gauss_integral.v index 44a3e99a8c..e3caf20ad7 100644 --- a/theories/gauss_integral.v +++ b/theories/gauss_integral.v @@ -110,7 +110,7 @@ Let continuous_NsqrM x : continuous (fun r : R => - (r * x) ^+ 2). Proof. move=> z; apply: cvgN => /=. apply: (cvg_comp (fun z => z * x) (fun z => z ^+ 2)). - by apply: cvgMl; exact: cvg_id. + by apply: cvgMr_tmp; exact: cvg_id. exact: exprn_continuous. Qed. @@ -127,7 +127,7 @@ Proof. rewrite /u /= => y; rewrite /continuous_at. apply: cvgM; last exact: continuous_oneDsqrV. apply: continuous_comp => /=; last exact: continuous_expR. -by apply: cvgMr; exact: continuous_oneDsqr. +by apply: cvgMl_tmp; exact: continuous_oneDsqr. Qed. Definition integral01_u x := \int[mu]_(t in `[0, 1]) u x t. diff --git a/theories/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v index 7270947475..3ec114f2fd 100644 --- a/theories/normedtype_theory/normed_module.v +++ b/theories/normedtype_theory/normed_module.v @@ -496,25 +496,35 @@ Lemma is_cvgZ s f : cvg (s @ F) -> cvg (f @ F) -> cvg ((fun x => s x *: f x) @ F). Proof. by have := cvgP _ (cvgZ _ _); apply. Qed. -Lemma cvgZl s k a : s @ F --> k -> s x *: a @[x --> F] --> k *: a. +Lemma cvgZr_tmp s k a : s @ F --> k -> s x *: a @[x --> F] --> k *: a. Proof. by move=> ?; apply: cvgZ => //; exact: cvg_cst. Qed. -Lemma is_cvgZl s a : cvg (s @ F) -> cvg ((fun x => s x *: a) @ F). -Proof. by have := cvgP _ (cvgZl _); apply. Qed. +Lemma is_cvgZr_tmp s a : cvg (s @ F) -> cvg ((fun x => s x *: a) @ F). +Proof. by have := cvgP _ (cvgZr_tmp _); apply. Qed. -Lemma cvgZr k f a : f @ F --> a -> k \*: f @ F --> k *: a. -Proof. apply: cvgZ => //; exact: cvg_cst. Qed. +Lemma cvgZl_tmp k f a : f @ F --> a -> k \*: f @ F --> k *: a. +Proof. by apply: cvgZ => //; exact: cvg_cst. Qed. -Lemma is_cvgZr k f : cvg (f @ F) -> cvg (k *: f @ F). -Proof. by have := cvgP _ (cvgZr _); apply. Qed. +Lemma is_cvgZl_tmp k f : cvg (f @ F) -> cvg (k *: f @ F). +Proof. by have := cvgP _ (cvgZl_tmp _); apply. Qed. -Lemma is_cvgZrE k f : k != 0 -> cvg (k *: f @ F) = cvg (f @ F). +Lemma is_cvgZlE k f : k != 0 -> cvg (k *: f @ F) = cvg (f @ F). Proof. -move=> k_neq0; rewrite propeqE; split => [/(@cvgZr k^-1)|/(@cvgZr k)/cvgP//]. +move=> k_neq0; rewrite propeqE; split => [/(@cvgZl_tmp k^-1)|/(@cvgZl_tmp k)/cvgP//]. by under [_ \*: _]funext => x /= do rewrite scalerK//; apply: cvgP. Qed. End cvg_composition_normed. +#[deprecated(since="mathcomp-analysis 1.12.0", note="renamed to `cvgZr_tmp`")] +Notation cvgZl := cvgZr_tmp (only parsing). +#[deprecated(since="mathcomp-analysis 1.12.0", note="renamed to `is_cvgZr_tmp`")] +Notation is_cvgZl := is_cvgZr_tmp (only parsing). +#[deprecated(since="mathcomp-analysis 1.12.0", note="renamed to `cvgZl_tmp`")] +Notation cvgZr := cvgZl_tmp (only parsing). +#[deprecated(since="mathcomp-analysis 1.12.0", note="renamed to `is_cvgZl_tmp`")] +Notation is_cvgZr := is_cvgZl_tmp (only parsing). +#[deprecated(since="mathcomp-analysis 1.12.0", note="renamed to `is_cvgZlE`")] +Notation is_cvgZrE := is_cvgZlE (only parsing). Section cvg_composition_field. Context {K : numFieldType} {T : Type}. @@ -538,34 +548,46 @@ Proof. by move=> /cvgV cvf /cvf /cvgP. Qed. Lemma cvgM f g a b : f @ F --> a -> g @ F --> b -> (f \* g) @ F --> a * b. Proof. exact: cvgZ. Qed. -Lemma cvgMl f a b : f @ F --> a -> (f x * b) @[x --> F] --> a * b. -Proof. exact: cvgZl. Qed. +Lemma cvgMr_tmp f a b : f @ F --> a -> f x * b @[x --> F] --> a * b. +Proof. exact: cvgZr_tmp. Qed. -Lemma cvgMr g a b : g @ F --> b -> (a * g x) @[x --> F] --> a * b. -Proof. exact: cvgZr. Qed. +Lemma cvgMl_tmp g a b : g @ F --> b -> a * g x @[x --> F] --> a * b. +Proof. exact: cvgZl_tmp. Qed. Lemma is_cvgM f g : cvg (f @ F) -> cvg (g @ F) -> cvg (f \* g @ F). Proof. exact: is_cvgZ. Qed. -Lemma is_cvgMr g a (f := fun=> a) : cvg (g @ F) -> cvg (f \* g @ F). -Proof. exact: is_cvgZr. Qed. +Lemma is_cvgMl_tmp g a (f := fun=> a) : cvg (g @ F) -> cvg (f \* g @ F). +Proof. exact: is_cvgZl_tmp. Qed. -Lemma is_cvgMrE g a (f := fun=> a) : a != 0 -> cvg (f \* g @ F) = cvg (g @ F). -Proof. exact: is_cvgZrE. Qed. +Lemma is_cvgMlE_tmp g a (f := fun=> a) : a != 0 -> cvg (f \* g @ F) = cvg (g @ F). +Proof. exact: is_cvgZlE. Qed. -Lemma is_cvgMl f a (g := fun=> a) : cvg (f @ F) -> cvg (f \* g @ F). +Lemma is_cvgMr_tmp f a (g := fun=> a) : cvg (f @ F) -> cvg (f \* g @ F). Proof. move=> f_cvg; have -> : f \* g = g \* f by apply/funeqP=> x; rewrite /= mulrC. -exact: is_cvgMr. +exact: is_cvgMl_tmp. Qed. -Lemma is_cvgMlE f a (g := fun=> a) : a != 0 -> cvg (f \* g @ F) = cvg (f @ F). +Lemma is_cvgMrE_tmp f a (g := fun=> a) : a != 0 -> cvg (f \* g @ F) = cvg (f @ F). Proof. move=> a_neq0; have -> : f \* g = g \* f by apply/funeqP=> x; rewrite /= mulrC. -exact: is_cvgMrE. +exact: is_cvgMlE_tmp. Qed. End cvg_composition_field. +#[deprecated(since="mathcomp-analysis 1.12.0", note="renamed to `cvgMr_tmp`")] +Notation cvgMl := cvgMr_tmp (only parsing). +#[deprecated(since="mathcomp-analysis 1.12.0", note="renamed to `cvgMl_tmp`")] +Notation cvgMr := cvgMl_tmp (only parsing). +#[deprecated(since="mathcomp-analysis 1.12.0", note="renamed to `is_cvgMl_tmp`")] +Notation is_cvgMr := is_cvgMl_tmp (only parsing). +#[deprecated(since="mathcomp-analysis 1.12.0", note="renamed to `is_cvgMr_tmp`")] +Notation is_cvgMl := is_cvgMr_tmp (only parsing). +#[deprecated(since="mathcomp-analysis 1.12.0", note="renamed to `is_cvgMrE_tmp`")] +Notation is_cvgMlE := is_cvgMrE_tmp (only parsing). +#[deprecated(since="mathcomp-analysis 1.12.0", note="renamed to `is_cvgMlE_tmp`")] +Notation is_cvgMrE := is_cvgMlE_tmp (only parsing). Section limit_composition_normed. Context {K : numFieldType} {V : normedModType K} {T : Type}. @@ -573,17 +595,21 @@ Context (F : set_system T) {FF : ProperFilter F}. Implicit Types (f g : T -> V) (s : T -> K) (k : K) (x : T) (a : V). Lemma limZ s f : cvg (s @ F) -> cvg (f @ F) -> - lim ((fun x => s x *: f x) @ F) = lim (s @ F) *: lim (f @ F). -Proof. by move=> ? ?; apply: cvg_lim => //; apply: cvgZ. Qed. + lim ((fun x => s x *: f x) @ F) = lim (s @ F) *: lim (f @ F). +Proof. by move=> ? ?; apply: cvg_lim => //; exact: cvgZ. Qed. -Lemma limZl s a : cvg (s @ F) -> - lim ((fun x => s x *: a) @ F) = lim (s @ F) *: a. -Proof. by move=> ?; apply: cvg_lim => //; apply: cvgZl. Qed. +Lemma limZr_tmp s a : cvg (s @ F) -> + lim ((fun x => s x *: a) @ F) = lim (s @ F) *: a. +Proof. by move=> ?; apply: cvg_lim => //; exact: cvgZr_tmp. Qed. -Lemma limZr k f : cvg (f @ F) -> lim (k *: f @ F) = k *: lim (f @ F). -Proof. by move=> ?; apply: cvg_lim => //; apply: cvgZr. Qed. +Lemma limZl_tmp k f : cvg (f @ F) -> lim (k *: f @ F) = k *: lim (f @ F). +Proof. by move=> ?; apply: cvg_lim => //; exact: cvgZl_tmp. Qed. End limit_composition_normed. +#[deprecated(since="mathcomp-analysis 1.12.0", note="renamed to `limZr_tmp`")] +Notation limZl := limZr_tmp (only parsing). +#[deprecated(since="mathcomp-analysis 1.12.0", note="renamed to `limZl_tmp`")] +Notation limZr := limZl_tmp (only parsing). Section limit_composition_field. Context {K : numFieldType} {T : Type}. @@ -591,8 +617,8 @@ Context (F : set_system T) {FF : ProperFilter F}. Implicit Types (f g : T -> K). Lemma limM f g : cvg (f @ F) -> cvg (g @ F) -> - lim (f \* g @ F) = lim (f @ F) * lim (g @ F). -Proof. by move=> ? ?; apply: cvg_lim => //; apply: cvgM. Qed. + lim (f \* g @ F) = lim (f @ F) * lim (g @ F). +Proof. by move=> ? ?; apply: cvg_lim => //; exact: cvgM. Qed. End limit_composition_field. @@ -603,13 +629,13 @@ Implicit Types (f g : T -> K) (a b : K). Lemma limV f : lim (f @ F) != 0 -> lim (f\^-1 @ F) = (lim (f @ F))^-1. Proof. -by move=> ?; apply: cvg_lim => //; apply: cvgV => //; apply: cvgNpoint. +by move=> ?; apply: cvg_lim => //; apply: cvgV => //; exact: cvgNpoint. Qed. Lemma is_cvgVE f : lim (f @ F) != 0 -> cvg (f\^-1 @ F) = cvg (f @ F). Proof. move=> ?; apply/propeqP; split=> /is_cvgV; last exact. -by rewrite inv_funK; apply; rewrite limV ?invr_eq0//. +by rewrite inv_funK; apply; rewrite limV ?invr_eq0. Qed. End cvg_composition_field_proper. @@ -655,24 +681,28 @@ Lemma continuousZ s f x : {for x, continuous (fun x => s x *: f x)}. Proof. by move=> ? ?; apply: cvgZ. Qed. -Lemma continuousZr f k x : +Lemma continuousZl_tmp f k x : {for x, continuous f} -> {for x, continuous (k \*: f)}. -Proof. by move=> ?; apply: cvgZr. Qed. +Proof. by move=> ?; exact: cvgZl_tmp. Qed. -Lemma continuousZl s a x : +Lemma continuousZr_tmp s a x : {for x, continuous s} -> {for x, continuous (fun z => s z *: a)}. -Proof. by move=> ?; apply: cvgZl. Qed. +Proof. by move=> ?; exact: cvgZr_tmp. Qed. Lemma continuousM s t x : {for x, continuous s} -> {for x, continuous t} -> {for x, continuous (s \* t)}. -Proof. by move=> f_cont g_cont; apply: cvgM. Qed. +Proof. by move=> f_cont g_cont; exact: cvgM. Qed. Lemma continuousV s x : s x != 0 -> {for x, continuous s} -> {for x, continuous (fun x => (s x)^-1%R)}. Proof. by move=> ?; apply: cvgV. Qed. End local_continuity. +#[deprecated(since="mathcomp-analysis 1.12.0", note="renamed to `continuousZl_tmp`")] +Notation continuousZr := continuousZl_tmp (only parsing). +#[deprecated(since="mathcomp-analysis 1.12.0", note="renamed to `continuousZr_tmp`")] +Notation continuousZl := continuousZr_tmp (only parsing). Section cvg_fin. Context {R : numFieldType}. diff --git a/theories/pi_irrational.v b/theories/pi_irrational.v index 70724c64bb..fd08173283 100644 --- a/theories/pi_irrational.v +++ b/theories/pi_irrational.v @@ -395,7 +395,7 @@ near: n. have : pi * (pi * a) ^+ n / n`!%:R @[n --> \oo] --> 0. rewrite -[X in _ --> X](mulr0 pi). under eq_fun do rewrite -mulrA. - by apply: cvgMr; exact: exp_fact. + by apply: cvgMl_tmp; exact: exp_fact. move/cvgrPdist_lt => /(_ e e0). apply: filterS => n. rewrite sub0r normrN ger0_norm; last first. diff --git a/theories/sequences.v b/theories/sequences.v index d4bfe00040..efd5c573de 100644 --- a/theories/sequences.v +++ b/theories/sequences.v @@ -554,11 +554,11 @@ Lemma lim_seriesN f : cvg (series f @ \oo) -> Proof. by move=> cf; rewrite seriesN limN. Qed. Lemma is_cvg_seriesZ f k : cvgn (series f) -> cvgn (series (k *: f)). -Proof. by move=> cf; rewrite seriesZ; exact: is_cvgZr. Qed. +Proof. by move=> cf; rewrite seriesZ; exact: is_cvgZl_tmp. Qed. Lemma lim_seriesZ f k : cvgn (series f) -> limn (series (k *: f)) = k *: limn (series f). -Proof. by move=> cf; rewrite seriesZ limZr. Qed. +Proof. by move=> cf; rewrite seriesZ limZl_tmp. Qed. Lemma is_cvg_seriesD f g : cvgn (series f) -> cvgn (series g) -> cvgn (series (f + g)). @@ -930,7 +930,7 @@ Proof. move=> Nz_lt1; apply/norm_cvg0P; pose t := (1 - `|z|). apply: (@squeeze_cvgr _ _ _ _ (cst 0) (t^-1 *: @harmonic R)); last 2 first. - exact: cvg_cst. -- by rewrite -(scaler0 _ t^-1); exact: (cvgZr cvg_harmonic). +- by rewrite -(scaler0 _ t^-1); exact: (cvgZl_tmp cvg_harmonic). near=> n; rewrite normr_ge0 normrX/= ler_pdivlMl ?subr_gt0//. rewrite -(@ler_pM2l _ n.+1%:R)// mulfV// [t * _]mulrC mulr_natl. have -> : 1 = (`|z| + t) ^+ n.+1 by rewrite addrC addrNK expr1n. @@ -956,7 +956,7 @@ Lemma cvg_geometric_series (R : archiFieldType) (a z : R) : `|z| < 1 -> Proof. move=> Nz_lt1; rewrite geometric_seriesE ?lt_eqF 1?ltr_normlW//. have -> : a / (1 - z) = (a * (1 - 0)) / (1 - z) by rewrite subr0 mulr1. -by apply: cvgMl; apply: cvgMr; apply: cvgB; [apply: cvg_cst|apply: cvg_expr]. +by apply: cvgMr_tmp; apply: cvgMl_tmp; apply: cvgB; [apply: cvg_cst|apply: cvg_expr]. Qed. Lemma cvg_geometric_series_half (R : archiFieldType) (r : R) n : @@ -1117,7 +1117,7 @@ Let S0 N n := (N ^ N)%:R * \sum_(N.+1 <= i < n) (x / N%:R) ^+ i. Let is_cvg_S0 N : x < N%:R -> cvgn (S0 N). Proof. -move=> xN; apply: is_cvgZr; rewrite is_cvg_series_restrict exprn_geometric. +move=> xN; apply: is_cvgZl_tmp; rewrite is_cvg_series_restrict exprn_geometric. apply/is_cvg_geometric_series; rewrite normrM normfV. by rewrite ltr_pdivrMr ?mul1r !ger0_norm // 1?ltW // (lt_trans x0). Qed. @@ -2809,7 +2809,7 @@ rewrite eqOP; split => [|Bf]. by near: M. Unshelve. all: by end_near. Qed. -(* TODO: to be changed once PR#1107 is integrated, and the following put in evt.v *) +(* TODO: to be changed once PR#1107 is integrated, and the following put in tvs.v *) (* Definition bounded_top (K: realType) (E : normedModType K) (B : set E) := forall (U : set E), nbhs 0 U ->